Making use of a definition inside a proof

Using Coq
1

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

2

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.

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. However, such usage is more advanced and you should learn the basics first before worrying about well-definedness.

1 Like
3

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

4

@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.

Definition Foo : ABC.
Proof.
  ...
Defined.

But certainly this usage goes beyond the basics.

6

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