The Coq mailing list

["�����" <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