From 1e3adb3b850d4cf863463e1231fcecf36020e106 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 16 Apr 2004 09:41:45 +0000 Subject: New files. --- coq/root2.v | 135 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 135 insertions(+) create mode 100644 coq/root2.v (limited to 'coq') diff --git a/coq/root2.v b/coq/root2.v new file mode 100644 index 00000000..ecba1a7f --- /dev/null +++ b/coq/root2.v @@ -0,0 +1,135 @@ +(****************************************************************************** + * * + * 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. -- cgit v1.2.3