(* \sqrt 2 is irrationnal, (c) 2006 Pierre Corbineau *)
Set Firstorder Depth 1.
Require Import ArithRing Wf_nat Peano_dec Div2 Even Lt.
Lemma double_div2: forall n, div2 (double n) = n.
proof.
assume n:nat.
per induction on n.
suppose it is 0.
suffices (0=0) to show thesis.
thus thesis.
suppose it is (S m) and Hrec:thesis for m.
have (div2 (double (S m))= div2 (S (S (double m)))).
~= (S (div2 (double m))).
thus ~= (S m) by Hrec.
end induction.
end proof.
Show Script.
Qed.
Lemma double_inv : forall n m, double n = double m -> n = m .
proof.
let n, m be such that H:(double n = double m).
have (n = div2 (double n)) by double_div2,H.
~= (div2 (double m)) by H.
thus ~= m by double_div2.
end proof.
Qed.
Lemma double_mult_l : forall n m, (double (n * m)=n * double m).
proof.
assume n:nat and m:nat.
have (double (n * m) = n*m + n * m).
~= (n * (m+m)) by * using ring.
thus ~= (n * double m).
end proof.
Qed.
Lemma double_mult_r : forall n m, (double (n * m)=double n * m).
proof.
assume n:nat and m:nat.
have (double (n * m) = n*m + n * m).
~= ((n + n) * m) by * using ring.
thus ~= (double n * m).
end proof.
Qed.
Lemma even_is_even_times_even: forall n, even (n*n) -> even n.
proof.
let n be such that H:(even (n*n)).
per cases of (even n \/ odd n) by even_or_odd.
suppose (odd n).
hence thesis by H,even_mult_inv_r.
end cases.
end proof.
Qed.
Lemma main_thm_aux: forall n,even n ->
double (double (div2 n *div2 n))=n*n.
proof.
given n such that H:(even n).
*** have (double (double (div2 n * div2 n))
= double (div2 n) * double (div2 n))
by double_mult_l,double_mult_r.
thus ~= (n*n) by H,even_double.
end proof.
Qed.
Require Omega.
Lemma even_double_n: (forall m, even (double m)).
proof.
assume m:nat.
per induction on m.
suppose it is 0.
thus thesis.
suppose it is (S mm) and thesis for mm.
then H:(even (S (S (mm+mm)))).
have (S (S (mm + mm)) = S mm + S mm) using omega.
hence (even (S mm +S mm)) by H.
end induction.
end proof.
Qed.
Theorem main_theorem: forall n p, n*n=double (p*p) -> p=0.
proof.
assume n0:nat.
define P n as (forall p, n*n=double (p*p) -> p=0).
claim rec_step: (forall n, (forall m,m P m) -> P n).
let n be such that H:(forall m : nat, m < n -> P m) and p:nat .
per cases of ({n=0}+{n<>0}) by eq_nat_dec.
suppose H1:(n=0).
per cases on p.
suppose it is (S p').
assume (n * n = double (S p' * S p')).
=~ 0 by H1,mult_n_O.
~= (S ( p' + p' * S p' + S p'* S p'))
by plus_n_Sm.
hence thesis .
suppose it is 0.
thus thesis.
end cases.
suppose H1:(n<>0).
assume H0:(n*n=double (p*p)).
have (even (double (p*p))) by even_double_n .
then (even (n*n)) by H0.
then H2:(even n) by even_is_even_times_even.
then (double (double (div2 n *div2 n))=n*n)
by main_thm_aux.
~= (double (p*p)) by H0.
then H':(double (div2 n *div2 n)= p*p) by double_inv.
have (even (double (div2 n *div2 n))) by even_double_n.
then (even (p*p)) by even_double_n,H'.
then H3:(even p) by even_is_even_times_even.
have (double(double (div2 n * div2 n)) = n*n)
by H2,main_thm_aux.
~= (double (p*p)) by H0.
~= (double(double (double (div2 p * div2 p))))
by H3,main_thm_aux.
then H'':(div2 n * div2 n = double (div2 p * div2 p))
by double_inv.
then (div2 n < n) by lt_div2,neq_O_lt,H1.
then H4:(div2 p=0) by (H (div2 n)),H''.
then (double (div2 p) = double 0).
=~ p by even_double,H3.
thus ~= 0.
end cases.
end claim.
hence thesis by (lt_wf_ind n0 P).
end proof.
Qed.
Require Import Reals Field.
(*Coercion INR: nat >->R.
Coercion IZR: Z >->R.*)
Open Scope R_scope.
Lemma square_abs_square:
forall p,(INR (Zabs_nat p) * INR (Zabs_nat p)) = (IZR p * IZR p).
proof.
assume p:Z.
per cases on p.
suppose it is (0%Z).
thus thesis.
suppose it is (Zpos z).
thus thesis.
suppose it is (Zneg z).
have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (Zneg z))) =
(IZR (Zpos z) * IZR (Zpos z))).
~= ((- IZR (Zpos z)) * (- IZR (Zpos z))).
thus ~= (IZR (Zneg z) * IZR (Zneg z)).
end cases.
end proof.
Qed.
Definition irrational (x:R):Prop :=
forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q).
Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)).
proof.
let p:Z,q:nat be such that H:(q<>0%nat)
and H0:(sqrt (INR 2%nat)=(IZR p/INR q)).
have H_in_R:(INR q<>0:>R) by H.
have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field.
have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def.
have (INR (Zabs_nat p * Zabs_nat p)
= (INR (Zabs_nat p) * INR (Zabs_nat p)))
by mult_INR.
~= (IZR p* IZR p) by square_abs_square.
~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *)
~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring.
~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0.
~= (INR (2%nat * (q*q))) by sqrt2,mult_INR.
then (Zabs_nat p * Zabs_nat p = 2* (q * q))%nat.
~= ((q*q)+(q*q))%nat.
~= (Div2.double (q*q)).
then (q=0%nat) by main_theorem.
hence thesis by H.
end proof.
Qed.