The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Hello,

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.

The key to this proof is that it relies more on algebraic computation 
than on the
notion of even numbers: if n^2=2p^2, and n <> 0, then 0 < 2p-n < n and 
(2p-n)^2=(n-p)^2.
Thus, we can build an infinite decreasing sequence of numbers that share 
the property of n.

To improve the conciseness of the proof, the "assert ... by ...", 
"replace ... by ..." play a significant
role, as does the new "ring [Heq]" tactic, which performs ring 
simplification modulo a collection
of monomial rewritings.

The proof could be made much shorter with the concise proof language of 
ssreflect, as proposed
by Georges Gonthier.  I also believe that the conciseness goes along 
with readability in this
case: the succession of asserts corresponds to important steps in the 
proof that can be used to
read the proof; in some sense one almost does not need to understand 
what the other proofs do.

A reasoning step that still takes a lot of space is the step that goes from
  n and p such that n^2=2p^2 and n<>0,
to
  n' and a p' such that n^2=2p^2 and  0 < n, 0 <= p

This is "without loss of generality step", and we still have to figure 
out how to do these efficiently.

Two other places where readability is not satisfactory are the 
preparation to the induction step,
and  the proofs by absurdity, for instance, p < n, because n <= p would 
lead to a contradiction.
To make these steps readable, I had to add comments.

Yves

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

Lemma tech_square : forall x, x^2 = x*x.
intros; ring.
Qed.

Lemma Zabs_cases : forall x, Zabs x = x \/ Zabs x = -x .
intros; case (Zabs_dec x); intros; omega.
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).
case (Zabs_cases n); case (Zabs_cases p); assert (Hpn := Zabs_pos n);
assert (Hpp := Zabs_pos p); intros Heqp Heqn; unfold n', p';
  split; omega || ring [Heqp Heqn Heq].
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]].
assert (Hmain_eq: (2*p-n)^2 = 2*(n -p)^2) by ring [Heq].
assert (Hns: 0 < n^2) by (rewrite tech_square; apply Zmult_lt_0_compat; 
auto).
assert (Hps: 0 < p^2) by omega.
assert (Hpn : p < n).
 case (Zle_or_lt n p); auto; intros Habsurd. (* Habsurd: n <= p *)
 assert (2*p^2 <= p^2).
   rewrite <- Heq; repeat rewrite tech_square;
   apply Zmult_le_compat; auto with zarith.
 omega. (* finishes the proof by contradiction. *)
assert (Hn2p: n < 2*p).
 elim (Zle_or_lt (2*p) n); auto; intros Habsurd'. (* Habsurd': 2p <= n *)
 assert (2*n^2 <= n^2).
   replace (2*n^2) with ((2*p)^2) by ring [Heq].
   repeat rewrite tech_square; apply Zmult_le_compat; auto with zarith.
 omega. (* finishes the proof by contradiction. *)
apply (IHn (2*p-n)); unfold Zwf; try omega.
exists (n-p); omega. (* uses Hpn and Hmain_eq *)
Qed.