diff options
Diffstat (limited to 'test-suite/success/decl_mode.v')
| -rw-r--r-- | test-suite/success/decl_mode.v | 182 |
1 files changed, 182 insertions, 0 deletions
diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v new file mode 100644 index 00000000..fede31a8 --- /dev/null +++ b/test-suite/success/decl_mode.v @@ -0,0 +1,182 @@ +(* \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<n-> 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. |