代码之家 › 专栏 › 技术社区 › Siddharth Bhat

关于类型类实例的推理在一个定理中得到了应用?

coq-tactic coq

Siddharth Bhat · 技术社区 · 7 年前

Class Action (Actor: Type) (Acted: Type) :=
  {
    act : Actor -> Acted -> Acted;
    someProof: forall (a: Actor), a = a;
  }.

Instance natListAction: Action nat (list nat) :=
  {
    act (n: nat) (l: list nat) := cons n l;
  }.
Proof.
    auto.
Qed.


Lemma natListAction_is_cons: forall (n: nat) (l: list nat),
    act n l = cons n l.
Proof.
  intros.
  unfold act.
  (** I cannot unfold it, since I have someProof.
   If I remove this, this unfold works **)
  unfold natListAction.
Abort.

我真正想要的是:因为我知道 act 解析为 natListAction ,我知道 act = cons .因此,引理应该经过。

如果我没有 someProof 在我的 Action 上课,然后我可以 unfold natListAction 一切都会好起来的。但现在,我不能这样做。

但是,我如何说服COQ ACT=施工 在这种情况下?

1 回复 | 直到 7 年前

Siddharth Bhat 7 年前

我在另一条so线索上找到了答案: Coq: unfolding typeclass instances

Proof 带A的节 Qed Defined

为了完整起见,以下是最终证明:

Class Action (Actor: Type) (Acted: Type) :=
  {
    act : Actor -> Acted -> Acted;
    someProof: forall (a: Actor), a = a;
  }.

Instance natListAction: Action nat (list nat) :=
  {
    act (n: nat) (l: list nat) := cons n l;
  }.
Proof.
  auto.
  (** vvv Notice the change! this is now "Defined" vvv **)
Defined.


Lemma natListAction_is_cons: forall (n: nat) (l: list nat),
    act n l = cons n l.
Proof.
  intros.
  unfold act.
  unfold natListAction.
  reflexivity.
Qed.

推荐文章

Mei Zhang · 定义“依赖类型”模函子

7 年前

Jason Hu · 参见Ltac中的Hintbase

7 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

7 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

7 年前

user9335697 · 实例化参数以评估函数定义

7 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

7 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

7 年前

jmite · Coq:在校样脚本编写期间查看校样术语

7 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

7 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

7 年前