The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

 You are right, at the beginning it was a typo (in the english
and the chinese version of our book).

If you replace the hypothesis "8 < n+6" by "8 <= n+6", the proof
as it is explained in the book works fine.

Now, if we keep the original statement, the proof remains correct
because "8 <= n+6" is implied by "8 < n+6".

There is another proof of the original statement, using your
argument and the principle of explosion a.k.a. "ex falso quodlibet"
(elimination of False).


Require Import Omega.
Lemma cond_rewrite_example :forall n:nat, 8<n+6 -> 3+n < 6 -> n*n=n+n.
Proof.
intros n H H0.
assert (H1:False).
omega.
destruct H1.
Qed.


We are sorry for this typo, we will correct immediately and
signal it in the errata of the book site.


Pierre




Quoting 许庆国 
<qgxu AT mail.shu.edu.cn>:

> Hello coq-club:
>   Now, I am reading the book "Interactive theorem proving and  
> program development: Coq'Art : ...".
>  I have some question about the proving "le_lt_S_eq"  in section 5.3.4.
>
> Lemma cond_rewrite_example : forall n:nat,   8 < n+6 ->  3+n < 6 ->  
> n*n = n+n.
>
>     From the above,  n  is a natural number that is both greater  
> than 2  and little than 3, i.e., 2<3<n.
> But such a natural number does not exist.
>
> why the  following srcipts  can succeed.
>
> Proof.
>  intros n  H H0.
>  rewrite <- (le_lt_S_eq 2 n).
>  simpl; auto.
>  apply  plus_le_reg_l with (p := 6).
>  rewrite plus_comm in H. simpl. auto with arith.
>  apply   plus_lt_reg_l with (p:= 3); auto with arith.
> Qed.
>
> That is to say, the theorem "plus_le_reg_l" can apllied be  
> simplified the "<=" to "<"
>
> Is there some problem?
>
> thank you
>
> 2010-09-03
>
>
>
>  Best Kinds!
>   Q.g. XU