The Coq mailing list

[fr�d�ric BESSON <fbesson AT irisa.fr>]

Hello Yves,

You give me the opportunity to advertise for my micromega tactic[*].

> Once in a while, I like to revisit the proof that the square root  
> of 2 is non rational; the conciseness
> of this proof makes it possible to measure the evolution of the  
> proof system.  Currently, with
> Coq V8.1, I reach a proof of 40 lines, but admittedly, the  
> statement I use is less "general"
> than the statement found in the "Seventeen theorem" book.

Using  this tactic, your proof shrinks to about 20 lines.
The "reasoning step that still takes a lot of space"  in your proof  
is automatically discharged.

[*] micromega is a Coq reflexive tactic able to cope with (certain)  
non-linear goals over Z.
It is available from http://www.irisa.fr/lande/fbesson/fbesson.html.
Comments (including bug reports) are welcome!

=====
Require Import ZArith ZArithRing Omega Zwf.
Require Import Micromegatac.
Open Scope Z_scope.


Lemma Zabs_square : forall x,  (Zabs  x)^2 = x^2.
Proof.
  intros ; case (Zabs_dec x) ; intros ; micromega.
Qed.

Theorem sqrt2_not_rational :  ~exists n, exists p, n ^2 = 2* p^2 /\ n  
<> 0.
Proof.
intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p).
assert (Heq' : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)).
unfold n', p';
  assert (Hpn := Zabs_pos n) ; assert (Hpp:= Zabs_pos p) ;
    assert (Hn2 :=Zabs_square n) ; assert (Hp2:=Zabs_square p);
      micromega.
assert (Hex : exists m, 0 <= m /\ n'^2=2*m^2) by (exists p'; intuition).
assert (Hpos : 0 < n') by intuition.
generalize Hpos Hex.
elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
intros n IHn Hn [p [Hp Heq]].
apply (IHn (2*p-n)) ;unfold Zwf.
zrelax ; micromega.
zrelax ; micromega.
exists (n-p) ; zrelax ; micromega.
Qed.

--
Frédéric Besson