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

**URL:** <https://discourse.rocq-prover.org/t/what-is-the-syntax-to-give-an-explicit-proof-object-lambda-term-to-a-lemma-in-coq/1354>\
**Category:** Using Rocq\
**Created:** [June 18, 2021, 4:25pm UTC](https://discourse.rocq-prover.org/t/what-is-the-syntax-to-give-an-explicit-proof-object-lambda-term-to-a-lemma-in-coq/1354 "2021-06-18T16:25:40Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [June 18, 2021, 4:25pm UTC](https://discourse.rocq-prover.org/t/what-is-the-syntax-to-give-an-explicit-proof-object-lambda-term-to-a-lemma-in-coq/1354/1 "2021-06-18T16:25:40Z")

</div>

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:

```auto
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:

```auto
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.

```

---

<div class="post-metadata">

**Author:** ![fajb](https://avatars.discourse-cdn.com/v4/letter/f/54ee81/32.png) [@fajb](https://discourse.rocq-prover.org/u/fajb)\
**Post date:** [June 18, 2021, 6:14pm UTC](https://discourse.rocq-prover.org/t/what-is-the-syntax-to-give-an-explicit-proof-object-lambda-term-to-a-lemma-in-coq/1354/2 "2021-06-18T18:14:45Z")

</div>

The syntax is.

```auto
Definition name : type := term.

```

So, it works if you replace Lemma by Definition.

```auto
Definition thm_identity2 : forall (P:Type), P -> P :=
fun (P : Type) (X : P) => X.

```

---

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [June 18, 2021, 6:35pm UTC](https://discourse.rocq-prover.org/t/what-is-the-syntax-to-give-an-explicit-proof-object-lambda-term-to-a-lemma-in-coq/1354/3 "2021-06-18T18:35:15Z")

</div>

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

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

```

or something like that and give the lambda term?

---

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [June 18, 2021, 6:36pm UTC](https://discourse.rocq-prover.org/t/what-is-the-syntax-to-give-an-explicit-proof-object-lambda-term-to-a-lemma-in-coq/1354/4 "2021-06-18T18:36:35Z")

</div>

I guess the way to do is as follows:

```auto
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).

---

<div class="post-metadata">

**Author:** ![fajb](https://avatars.discourse-cdn.com/v4/letter/f/54ee81/32.png) [@fajb](https://discourse.rocq-prover.org/u/fajb)\
**Post date:** [June 18, 2021, 7:01pm UTC](https://discourse.rocq-prover.org/t/what-is-the-syntax-to-give-an-explicit-proof-object-lambda-term-to-a-lemma-in-coq/1354/5 "2021-06-18T19:01:46Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [June 18, 2021, 7:09pm UTC](https://discourse.rocq-prover.org/t/what-is-the-syntax-to-give-an-explicit-proof-object-lambda-term-to-a-lemma-in-coq/1354/6 "2021-06-18T19:09:56Z")

</div>

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!