What is the syntax to give an explicit proof object (lambda term) to a lemma in Coq?

Using Coq
1

I figure out that one can print them (the lambda terms) with Show proof. in the middle of a proof (proof mode) and Print lemma_name but I wasn’t able to actually give one. I won;t print all different attempts I did but here are a few of the identity function/P->P implication I did:

thm_identity' := fun (P : Type) (X : P) => X
	 : forall P : Type, P -> P.

Lemma thm_identity2 : forall (P:Type), P -> P :=
fun (P : Type) (X : P) => X.

Lemma thm_identity2 : forall (P:Type), P -> P :=
  fun x => x.

but it won’t accept them even though I used the printed lambda term of my theorem…any help?

rest of my script:

Definition my_id1 {A:Type} (a:A) := a.

Compute my_id1 2.
Compute my_id1 3.

Print my_id1.

Definition my_id1' (A:Type) (a:A) := a.

Compute my_id1' nat 2.

Lemma thm_identity : forall (P:Type), P -> P.
Proof.
    intros.
    Show Proof.
    assumption.
    Show Proof.
Qed.

Print thm_identity.

thm_identity' := fun (P : Type) (X : P) => X
	 : forall P : Type, P -> P.

Lemma thm_identity2 : forall (P:Type), P -> P :=
fun (P : Type) (X : P) => X.

Lemma thm_identity2 : forall (P:Type), P -> P :=
  fun x => x.
2

The syntax is.

Definition name : type := term.

So, it works if you replace Lemma by Definition.

Definition thm_identity2 : forall (P:Type), P -> P :=
fun (P : Type) (X : P) => X.
1 Like
3

I thought a theorem was a type for the lambda term and the lambda term the proof (object). So why can’t I do:

Lemma thm_identity2' : forall (P:Type), P -> P :=
fun (P : Type) (X : P) => X.

or something like that and give the lambda term?

4

I guess the way to do is as follows:

Lemma thm_identity2' : forall (P:Type), P -> P. 
Proof.
  exact (fun (P : Type) (X : P) => X).
Qed.

Thanks!

I guess Coq really wants to go into proof mode (my guess it otherwise doesn’t know when to apply the type checker).

5

Yes, a theorem is the type of a lambda term
It just happens that for the keywords Lemma, Theorem, the lambda-term is constructed using the proof mode.
For Definition, the parser accepts both ways.
You can write either
Definition term : type. Proof. ... Qed.
or
Definition term : type := term.
Eventually, Lemma, Theorem, Definition are the same and Print won’t make a difference.

2 Likes
6

they are conceptually the same but the fact doesn’t let me use them the same way means there is some difference…I wish they just acted the same way to avoid this problem all together - though I assume it’s not super important for real development.

Thanks! I appreciate your help!