# Making use of a definition inside a proof

**URL:** <https://discourse.rocq-prover.org/t/making-use-of-a-definition-inside-a-proof/2315>\
**Category:** Using Rocq\
**Created:** [June 4, 2024, 9:42am UTC](https://discourse.rocq-prover.org/t/making-use-of-a-definition-inside-a-proof/2315 "2024-06-04T09:42:21Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Lilipop](https://avatars.discourse-cdn.com/v4/letter/l/8491ac/32.png) [@Lilipop](https://discourse.rocq-prover.org/u/Lilipop)\
**Post date:** [June 4, 2024, 9:42am UTC](https://discourse.rocq-prover.org/t/making-use-of-a-definition-inside-a-proof/2315/1 "2024-06-04T09:42:21Z")

</div>

Hi all,

I have the following example, not working:  
Definition NatProp := forall (a b : nat), a \> b → (a + 1) \> (b + 1).  
Lemma Test : forall (a b : nat), a \> b → (a + 1) \> (b + 1).  
Proof. intros. apply NatProp. (\* stuck \*)

However, this works:  
Axiom NatProp : forall (a b : nat), a \> b → (a + 1) \> (b + 1).  
Lemma Test : forall (a b : nat), a \> b → (a + 1) \> (b + 1).  
Proof. intros. apply NatProp. Qed.

This works too:  
Lemma NatProp : forall (a b : nat), a \> b → (a + 1) \> (b + 1).  
Proof. intros. lia. Qed.  
Lemma Test : forall (a b : nat), a \> b → (a + 1) \> (b + 1).  
Proof. intros. apply NatProp. exact H. Qed.

I’m still not really understanding how to kind of apply a definition in a proof, and did not find much when searching for this.

PS:because I am working with a system with multiple properties that I want to add as definitions to be used all along my proofs.

Thanks !  
Lili

---

<div class="post-metadata">

**Author:** ![davidjao](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/davidjao/32/866_2.png) [@davidjao](https://discourse.rocq-prover.org/u/davidjao)\
**Post date:** [June 4, 2024, 9:49am UTC](https://discourse.rocq-prover.org/t/making-use-of-a-definition-inside-a-proof/2315/2 "2024-06-04T09:49:49Z")

</div>

A definition is just a rename operation. If you want to use the definition of NatProp in a lemma, here’s how to do it.

```auto
From Coq Require Import Utf8.

Definition NatProp := forall (a b : nat), a > b → (a + 1) > (b + 1).

Lemma Test : NatProp.
Proof.
  unfold NatProp.
  intros.
Admitted.

```

An axiom is quite different. An axiom means “assume the following statement is true, without proof.”

In summary:

- `Axiom Foo : ABC.` “Assume the statement `ABC` is true, without proof.”
- `Theorem Foo : ABC.` “The statement `ABC` is true. I will give a proof of `ABC` below.”
- `Definition Foo := ABC.` “The word `Foo` is another name for `ABC`.”

What is sometimes confusing is that definitions can have proofs. Such a situation arises when you are defining something and you need to prove that the object you are defining is [well-defined](https://en.wikipedia.org/wiki/Well-defined_expression). However, such usage is more advanced and you should learn the basics first before worrying about well-definedness.

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [June 4, 2024, 9:58am UTC](https://discourse.rocq-prover.org/t/making-use-of-a-definition-inside-a-proof/2315/3 "2024-06-04T09:58:42Z")

</div>

@davidjao please fix the typo: you put “:” intead of “:=” in Definition.

---

<div class="post-metadata">

**Author:** ![davidjao](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/davidjao/32/866_2.png) [@davidjao](https://discourse.rocq-prover.org/u/davidjao)\
**Post date:** [June 4, 2024, 10:17am UTC](https://discourse.rocq-prover.org/t/making-use-of-a-definition-inside-a-proof/2315/4 "2024-06-04T10:17:50Z")

</div>

@Matafou Thanks for the correction! It should be noted that the `:` notation is valid in the second case I mentioned, where a definition is followed by a proof.

```auto
Definition Foo : ABC.
Proof.
  ...
Defined.

```

But certainly this usage goes beyond the basics.

---

<div class="post-metadata">

**Author:** ![zepalmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zepalmer/32/923_2.png) [@zepalmer](https://discourse.rocq-prover.org/u/zepalmer)\
**Post date:** [June 5, 2024, 5:34pm UTC](https://discourse.rocq-prover.org/t/making-use-of-a-definition-inside-a-proof/2315/6 "2024-06-05T17:34:22Z")

</div>

@davidjao As a novice who is lurking and learning, I appreciate the clarification. 😃