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

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.

What I actually want is this: because I know that act resolves to natListAction, I know that act = cons. Hence, the lemma should go through.

If I do not have the someProof in my Action class, then I can unfold natListAction and stuff works. But now, I am unable to do so.

However, how do I convince coq that act = cons in this case?

Answer 1

I found the answer on another SO thread: Coq: unfolding typeclass instances.

Ending the Proof section with a Qed makes it opaque. Instead, end the proof with a Defined and it will go through.

For the sake of completeness, here is the final proof:

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.