(****************************************************************************** * * * Proof that sqrt 2 is irrational * * * * Laurent.Thery@sophia.inria.fr * * February 2002 * * (Revised April 2004 for coq 8.0) * ******************************************************************************) Require Import ArithRing. Require Import Wf_nat. Require Import Peano_dec. Require Import Div2. Require Import Even. (****************************************************************************** * * * Properties of div2 and double (these theorems should be in Div2.v) * * * ******************************************************************************) Theorem double_div2: forall (n : nat), div2 (double n) = n. simple induction n; auto with arith. intros n0 H. rewrite double_S; pattern n0 at 2; rewrite <- H; simpl; auto. Qed. Theorem double_inv: forall (n m : nat), double n = double m -> n = m. intros n m H; rewrite <- (double_div2 n); rewrite <- (double_div2 m); rewrite H; auto. Qed. Theorem double_mult_l: forall (n m : nat), double (n * m) = double n * m. unfold double; auto with arith. Qed. Theorem double_mult_r: forall (n m : nat), double (n * m) = n * double m. unfold double; intros; ring. Qed. (****************************************************************************** * * * If the power to the 2 of a number is even, then this number is even * * * ******************************************************************************) Theorem even_is_even_times_even: forall (n : nat), even (n * n) -> even n. intros n H; (try case (even_or_odd n)); auto. intros; apply even_mult_inv_r with (1 := H); auto. Qed. (****************************************************************************** * * * Useful fact 4*(n/2)*(n/2) = n*n if n is even * * * ******************************************************************************) Theorem main_thm_aux: forall (n : nat), even n -> double (double (div2 n * div2 n)) = n * n. intros; rewrite double_mult_l; rewrite double_mult_r; (repeat rewrite <- even_double); auto. Qed. (****************************************************************************** * Main theorem * * We do the proof of the theorem by well founded induction: * * Suppose that we have n*n = 2*p*p * * if n=0 then p = O * * if n<>0 then * * - n is even (n=2n') and p is even (p=2p') * * - we have n'*n'=2*p'*p' and n' < n * * - by the induction hypothesis we have p'=O * * - so p=O * ******************************************************************************) Theorem main_thm: forall (n p : nat), n * n = double (p * p) -> p = 0. intros n; pattern n; apply lt_wf_ind; clear n. intros n H p H0. case (eq_nat_dec n 0); intros H1. generalize H0; rewrite H1; case p; auto; intros; discriminate. assert (H2: even n). apply even_is_even_times_even. apply double_even; rewrite H0; rewrite double_div2; auto. assert (H3: even p). apply even_is_even_times_even. rewrite <- (double_inv (double (div2 n * div2 n)) (p * p)). apply double_even; rewrite double_div2; auto. rewrite main_thm_aux; auto. assert (H4: div2 p = 0). apply (H (div2 n)). apply lt_div2; apply neq_O_lt; auto. apply double_inv; apply double_inv; (repeat rewrite main_thm_aux); auto. rewrite (even_double p); auto; rewrite H4; auto. Qed. (****************************************************************************** * * * Coercions from nat and Z to R * * * ******************************************************************************) Require Import Reals. Require Import Field. Coercion INR : nat >-> R. Coercion IZR : Z >-> R. (****************************************************************************** * * * Definition of irrational * * * ******************************************************************************) Definition irrational (x : R) : Prop := forall (p : Z) (q : nat), q <> 0 -> x <> (p / q)%R. (****************************************************************************** * * * Final theorem * * * ******************************************************************************) Theorem irrational_sqrt_2: irrational (sqrt 2%nat). intros p q H H0; case H. apply (main_thm (Zabs_nat p)). replace (Div2.double (q * q)) with (2 * (q * q)); [idtac | unfold Div2.double; ring]. case (eq_nat_dec (Zabs_nat p * Zabs_nat p) (2 * (q * q))); auto; intros H1. case (not_nm_INR _ _ H1); (repeat rewrite mult_INR). rewrite <- (sqrt_def (INR 2)); auto with real. rewrite H0; auto with real. assert (q <> 0%R :> R); auto with real. field; auto with real; case p; simpl; intros; ring. Qed.