The Coq mailing list

[Pierre Cast�ran <pierre.casteran AT labri.fr>]

Hi,

 test1 is proved using the inversion tactic, which uses the fact that
the only way to prove n <= 0 is given by le's first constructor.


Lemma test1 : forall n:nat, n<=0 -> n=0.
 intros n H; inversion H.
 trivial.
Qed.

For test2, have a look at Coq's standard library : module Arith / Minus
section "Relation"  with Plus.

By the way, your statement of test2 seems to be erroneous: assume
"m <= n" isnstead of "n <= m".

Pierre

Quoting Wan Hai 
<wan.whyhigh AT gmail.com>:

> Deal all,
>
> Now I'm using Coq to prove something list as follows:
> 1) Lemma test1 : forall n:nat, n<=0 -> n=0
> 1) Lemma test2 : forall n m:nat, n<=m -> n-m+m=n
> these are right of course, but I don't know how to prove. I used the
> omega tactic. This tactic did solve these problems. But when I used
> Print test1 or Print test2 to see what happens, I really find the
> proof steps are difficult to follow.
> Could any one tell me some easy way to do this?
> Thanks a lot!
>
> --
> Hai Wan
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club



Pierre Castéran