coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] help, how to prove this? forall n:nat, n<=0 -> n=0

From: "Yevgeniy Makarov" <emakarov AT gmail.com>
To: "Coq Club" <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] help, how to prove this? forall n:nat, n<=0 -> n=0
Date: Wed, 31 Oct 2007 14:57:36 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=Ugvvm06XYBsJhL61fgxzvEmLexZBooSKsJA/IaRBH2X/qK6bKaH/X62pVNT1NaHYOT3XTmsrr2h7uAXcgWHVs6m6sSrLlCAm87vFV3MWa3E3Pxscd9KNDPclKAV5BuIGZmz80/0fq+2yMjqdhy1UuCv9hiucYqoCkMmrqQwgo38=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

test1 could also be proved using the theorem le_n_O_eq from the
standard library (Coq.Arith.Le).

Lemma test1 : forall n : nat, n <= 0 -> n = 0.
Proof.
intros n H. symmetry. apply le_n_O_eq; assumption.
Qed.

You can find the theorem name using the command

SearchPattern (0 = _).

once you import Arith library. Finally, it can be proved using the
omega tactic, but first you need to introduce the universally
quantified variable:

Proof.
intro. omega.
Qed.

Omega can also solve the second goal. Otherwise, use the theorem
le_plus_minus.

Evgeny

[Coq-Club] help, how to prove this? forall n:nat, n<=0 -> n=0, Wan Hai
- Re: [Coq-Club] help, how to prove this? forall n:nat, n<=0 -> n=0, Pierre Cast�ran
- Re: [Coq-Club] help, how to prove this? forall n:nat, n<=0 -> n=0, Yevgeniy Makarov