关于在定理中选取的类型类实例的推理？

Question

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。因此，引理应该通过。

如果我的 Action class 中没有 someProof，那么我可以 unfold natListAction 并且一切正常。但是现在，我做不到了。

但是，在这种情况下，我如何说服 coq act = cons？

Answer 1

我在另一个 SO 线程上找到了答案：Coq: unfolding typeclass instances。

以 Qed 结束 Proof 部分使其不透明。相反，以 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.

关于在定理中选取的类型类实例的推理？

reasoning about typeclass instance that has been picked up in a theorem?

coq

coq-tactic