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 +++++++++++++++++++++ hol98/root2.sml | 83 +++++++++++++ lego/root2.l | 368 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 586 insertions(+) create mode 100644 coq/root2.v create mode 100644 hol98/root2.sml create mode 100644 lego/root2.l 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. diff --git a/hol98/root2.sml b/hol98/root2.sml new file mode 100644 index 00000000..0644fc3e --- /dev/null +++ b/hol98/root2.sml @@ -0,0 +1,83 @@ +(* Example proof by Konrad Slind. See http://www.cs.kun.nl/~freek/comparison/ + Taken from HOL4 distribution hol98/examples/root2.sml *) + +(*---------------------------------------------------------------------------*) +(* Challenge from Freek Wiedijk: the square root of two is not rational. *) +(* I've adapted a proof in HOL Light by John Harrison. *) +(*---------------------------------------------------------------------------*) + +load "transcTheory"; open arithmeticTheory BasicProvers; + +(*---------------------------------------------------------------------------*) +(* Need a predicate on reals that picks out the rational ones *) +(*---------------------------------------------------------------------------*) + +val Rational_def = Define `Rational r = ?p q. ~(q=0) /\ (abs(r) = &p / &q)`; + +(*---------------------------------------------------------------------------*) +(* Trivial lemmas *) +(*---------------------------------------------------------------------------*) + +val EXP_2 = Q.prove(`!n:num. n**2 = n*n`, + REWRITE_TAC [TWO,ONE,EXP] THEN RW_TAC arith_ss []); + +val EXP2_LEM = Q.prove(`!x y:num. ((2*x)**2 = 2*(y**2)) = (2*(x**2) = y**2)`, + REWRITE_TAC [TWO,EXP_2] + THEN PROVE_TAC [MULT_MONO_EQ,MULT_ASSOC,MULT_SYM]); + +(*---------------------------------------------------------------------------*) +(* Lemma: squares are not doublings of squares, except trivially. *) +(*---------------------------------------------------------------------------*) + +val lemma = Q.prove +(`!m n. (m**2 = 2 * n**2) ==> (m=0) /\ (n=0)`, + completeInduct_on `m` THEN NTAC 2 STRIP_TAC THEN + `?k. m = 2*k` by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT,EVEN_EXISTS] + THEN VAR_EQ_TAC THEN + `?p. n = 2*p` by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT, + EVEN_EXISTS,EXP2_LEM] + THEN VAR_EQ_TAC THEN + `k**2 = 2*(p**2)` by PROVE_TAC [EXP2_LEM] THEN + `(k=0) \/ k < 2*k` by numLib.ARITH_TAC + THENL [FULL_SIMP_TAC arith_ss [EXP_2], + PROVE_TAC [MULT_EQ_0, DECIDE (Term `~(2 = 0n)`)]]); + +(*---------------------------------------------------------------------------*) +(* The proof moves the problem from R to N, then uses lemma *) +(*---------------------------------------------------------------------------*) + +local open realTheory transcTheory +in +val SQRT_2_IRRATIONAL = Q.prove +(`~Rational (sqrt 2r)`, + RW_TAC std_ss [Rational_def,abs,SQRT_POS_LE,REAL_POS] + THEN Cases_on `q = 0` THEN ASM_REWRITE_TAC [] + THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `\x. x pow 2`) + THEN RW_TAC arith_ss [SQRT_POW_2, REAL_POS, REAL_POW_DIV, + REAL_EQ_RDIV_EQ,REAL_LT, REAL_POW_LT] + THEN REWRITE_TAC [REAL_OF_NUM_POW, REAL_MUL, REAL_INJ] + THEN PROVE_TAC [lemma]) +end; + +(*---------------------------------------------------------------------------*) +(* The following is a bit more declarative *) +(*---------------------------------------------------------------------------*) + +infix THEN1; +fun ie q tac = Q_TAC SUFF_TAC q THEN1 tac; + +local open realTheory transcTheory +in +val SQRT_2_IRRATIONAL = Q.prove +(`~Rational (sqrt 2r)`, + ie `!p q. ~(q=0) ==> ~(sqrt 2 = & p / & q)` + (RW_TAC std_ss [Rational_def,abs,SQRT_POS_LE,REAL_POS] + THEN PROVE_TAC[]) THEN RW_TAC std_ss [] THEN + ie `~(sqrt 2 = & p / & q)` (PROVE_TAC []) THEN + ie `~(2 * q**2 = p**2)` + (DISCH_TAC THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `\x. x pow 2`) + THEN RW_TAC arith_ss [SQRT_POW_2,REAL_POS, + REAL_POW_DIV,REAL_EQ_RDIV_EQ,REAL_LT, REAL_POW_LT] + THEN ASM_REWRITE_TAC [REAL_OF_NUM_POW, REAL_MUL,REAL_INJ]) + THEN PROVE_TAC [lemma]) +end; diff --git a/lego/root2.l b/lego/root2.l new file mode 100644 index 00000000..5712b129 --- /dev/null +++ b/lego/root2.l @@ -0,0 +1,368 @@ +(************************************************************************ + Conor McBride's proof that 2 has no rational root. + + This proof is accepted by LEGO version 1.3.1 with its standard library. +*************************************************************************) + +Make lib_nat; (* loading basic logic, nat, plus, times etc *) + +(* note, plus and times are defined by recursion on their first arg *) + + +(************************************************************************ + Alternative eliminators for nat + + LEGO's induction tactic figures out which induction principle to use + by looking at the type of the variable on which we're doing induction. + Consequently, we can persuade the tactic to use an alternative induction + principle if we alias the type. + + Nat_elim is just the case analysis principle for natural numbers---the + same as the induction principle except that there's no inductive hypothesis + in the step case. It's intended to be used in combination with... + + ...NAT_elim, which performs no case analysis but says you can have an + inductive hypothesis for any smaller value, where y is smaller than + suc (plus x y). This is `well-founded induction' for the < relation, + but expressed more concretely. + + The effect is very similar to that of `Case' and `Fix' in Coq. +************************************************************************) + +[Nat = nat]; +[NAT = Nat]; + +(* case analysis: just a weakening of induction *) + +Goal Nat_elim : {Phi:nat->Type} + {phiz:Phi zero} + {phis:{n:Nat}Phi (suc n)} + {n:Nat}Phi n; +intros ___; + Expand Nat; Induction n; + Immed; + intros; Immed; +Save; + +(* suc-plus guarded induction: the usual proof *) + +Goal NAT_elim : + {Phi:nat->Type} + {phi:{n:Nat} + {ih:{x,y|Nat}(Eq n (suc (plus x y)))->Phi y} + Phi n} + {n:NAT}Phi n; +intros Phi phi n'; +(* claim that we can build the hypothesis collector for each n *) +Claim {n:nat}{x,y|Nat}(Eq n (suc (plus x y)))->Phi y; +(* use phi on the claimed collector *) +Refine phi n' (?+1 n'); +(* now build the collector by one-step induction *) + Induction n; + Qnify; (* nothing to collect for zero *) + intros n nhyp; + Induction x; (* case analysis on the slack *) + Qnify; + Refine phi; (* if the bound is tight, use phi to *) + Immed; (* generate the new member of the collection *) + Qnify; + Refine nhyp; (* otherwise, we've already collected it *) + Immed; +Save; + + +(*************************************************************************** + Equational laws governing plus and times: + some of these are doubtless in the library, but it takes longer to + remember their names than to prove them again. +****************************************************************************) + +Goal plusZero : {x:nat}Eq (plus x zero) x; +Induction x; + Refine Eq_refl; + intros; + Refine Eq_resp suc; + Immed; +Save; + +Goal plusSuc : {x,y:nat}Eq (plus x (suc y)) (suc (plus x y)); +Induction x; + intros; Refine Eq_refl; + intros; + Refine Eq_resp suc; + Immed; +Save; + +Goal plusAssoc : {x,y,z:nat}Eq (plus (plus x y) z) (plus x (plus y z)); +Induction x; + intros; Refine Eq_refl; + intros; + Refine Eq_resp suc; + Immed; +Save; + +Goal plusComm : {x,y:nat}Eq (plus x y) (plus y x); +Induction y; + Refine plusZero; + intros y yh x; + Refine Eq_trans (plusSuc x y); + Refine Eq_resp suc; + Immed; +Save; + +Goal plusCommA : {x,y,z:nat}Eq (plus x (plus y z)) (plus y (plus x z)); +intros; + Refine Eq_trans ? (plusAssoc ???); + Refine Eq_trans (Eq_sym (plusAssoc ???)); + Refine Eq_resp ([w:nat]plus w z); + Refine plusComm; +Save; + +Goal timesZero : {x:nat}Eq (times x zero) zero; +Induction x; + Refine Eq_refl; + intros; + Immed; +Save; + +Goal timesSuc : {x,y:nat}Eq (times x (suc y)) (plus x (times x y)); +Induction x; + intros; Refine Eq_refl; + intros x xh y; + Equiv Eq (suc (plus y (times x (suc y)))) ?; + Equiv Eq ? (suc (plus x (plus y (times x y)))); + Refine Eq_resp; + Qrepl xh y; + Refine plusCommA; +Save; + +Goal timesComm : {x,y:nat}Eq (times x y) (times y x); +Induction y; + Refine timesZero; + intros y yh x; + Refine Eq_trans (timesSuc ??); + Refine Eq_resp (plus x); + Immed; +Save; + +Goal timesDistL : {x,y,z:nat}Eq (times (plus x y) z) + (plus (times x z) (times y z)); +Induction x; + intros; Refine Eq_refl; + intros x xh y z; + Refine Eq_trans (Eq_resp (plus z) (xh y z)); + Refine Eq_sym (plusAssoc ???); +Save; + +Goal timesAssoc : {x,y,z:nat}Eq (times (times x y) z) (times x (times y z)); +Induction x; + intros; Refine Eq_refl; + intros x xh y z; + Refine Eq_trans (timesDistL ???); + Refine Eq_resp (plus (times y z)); + Immed; +Save; + +(********************************************************************** + Inversion principles for equations governing plus and times: + these aren't in the library, at least not in this form. +***********************************************************************) + +[Phi|Type]; (* Inversion principles are polymorphic in any goal *) + +Goal plusCancelL : {y,z|nat}{phi:{q':Eq y z}Phi}{x|nat} + {q:Eq (plus x y) (plus x z)}Phi; +intros ___; +Induction x; + intros; + Refine phi q; + intros x xh; Qnify; + Refine xh; + Immed; +Save; + +Goal timesToZero : {a,b|Nat} + {phiL:(Eq a zero)->Phi} + {phiR:(Eq b zero)->Phi} + {tz:Eq (times a b) zero} + Phi; +Induction a; + intros; Refine phiL (Eq_refl ?); + intros a; + Induction b; + intros; Refine phiR (Eq_refl ?); + Qnify; +Save; + +Goal timesToNonZero : {x,y|nat} + {phi:{x',y'|nat}(Eq x (suc x'))->(Eq y (suc y'))->Phi} + {z|nat}{q:Eq (times x y) (suc z)}Phi; +Induction x; + Qnify; + intros x xh; + Induction y; + intros __; Qrepl timesZero (suc x); Qnify; + intros; + [EQR=Eq_refl]; Refine phi Then Immed; +Save; + +(* I actually want plusDivisionL, but plusDivisionR is easier to prove, + because here we do induction where times does computation. *) +Goal plusDivisionR : {b|nat}{a,x,c|Nat} + {phi:{c'|nat}(Eq (times c' (suc x)) c)-> + (Eq a (plus b c'))->Phi} + {q:Eq (times a (suc x)) (plus (times b (suc x)) c)} + Phi; +Induction b; + intros _____; Refine phi; + Immed; + Refine Eq_refl; + intros b bh; + Induction a; + Qnify; + intros a x c phi; + Qrepl plusAssoc (suc x) (times b (suc x)) c; + Refine plusCancelL; + Refine bh; + intros c q1 q2; Refine phi q1; + Refine Eq_resp ? q2; +Save; + +(* A bit of timesComm gives us the one we really need. *) +Goal plusDivisionL : {b|nat}{a,x,c|Nat} + {phi:{c'|nat}(Eq (times (suc x) c') c)-> + (Eq a (plus b c'))->Phi} + {q:Eq (times (suc x) a) (plus (times (suc x) b) c)} + Phi; +intros _____; + Qrepl timesComm (suc x) a; Qrepl timesComm (suc x) b; + Refine plusDivisionR; + intros c'; Qrepl timesComm c' (suc x); + Immed; +Save; + +Discharge Phi; + + +(************************************************************************** + Definition of primality: + + This choice of definition makes primality easy to exploit + (especially as it's presented as an inversion principle), but hard to + establish. +***************************************************************************) + +[Prime = [p:nat] + {a|NAT}{b,x|Nat}{Phi|Prop} + {q:Eq (times p x) (times a b)} + {phiL:{a':nat} + (Eq a (times p a'))->(Eq x (times a' b))->Phi} + {phiR:{b':nat} + (Eq b (times p b'))->(Eq x (times a b'))->Phi} + Phi +]; + + +(************************************************************************** + Proof that 2 is Prime. Nontrivial because of the above definition. + Manageable because 1 is the only number between 0 and 2. +***************************************************************************) + +Goal doublePlusGood : {x,y:nat}Eq (times (suc (suc x)) y) + (plus (times two y) (times x y)); +intros __; + Refine Eq_trans ? (Eq_sym (plusAssoc ???)); + Refine Eq_resp (plus y); + Refine Eq_trans ? (Eq_sym (plusAssoc ???)); + Refine Eq_refl; +Save; + +Goal twoPrime : Prime two; +Expand Prime; + Induction a; + Induction n; + intros useless b x _; + Refine timesToZero Then Expand Nat Then Qnify; + (* Qnify needs to know it's a nat *) + intros; Refine phiL; + Refine +1 (Eq_sym (timesZero ?)); + Refine Eq_refl; + Induction n; + intros useless b x _; + Qrepl plusZero b; + intros; Refine phiR; + Refine +1 Eq_sym q; + Refine Eq_sym (plusZero x); + intros n nhyp b x _; + Qrepl doublePlusGood n b; + Refine plusDivisionL; + intros c q1 q2; Qrepl q2; intros __; + Refine nhyp|one (Eq_refl ?) q1; + intros a' q3 q4; Refine phiL (suc a'); + Refine Eq_resp suc; + Refine Eq_trans ? (Eq_sym (plusSuc ??)); + Refine Eq_resp ? q3; + Refine Eq_resp (plus b) q4; + intros b' q3 q4; Refine phiR b'; + Immed; + Qrepl q3; Qrepl q4; + Refine Eq_sym (doublePlusGood ??); +Save; + + +(************************************************************************** + Now the proof that primes (>=2) have no rational root. It's the + classic `minimal counterexample' proof unwound as an induction: we + apply the inductive hypothesis to the smaller counterexample we + construct. +***************************************************************************) + +[pm2:nat] +[p=suc (suc pm2)] (* p is at least 2 *) +[Pp:Prime p]; + +Goal noRatRoot : {b|NAT}{a|Nat}{q:Eq (times p (times a a)) (times b b)} + and (Eq a zero) (Eq b zero); +Induction b; + Induction n; (* if b is zero, so is a, and the result holds *) + intros useless; + intros a; + Refine timesToZero; + Expand Nat; Qnify; + Refine timesToZero; Refine ?+1; + intros; Refine pair; Immed; Refine Eq_refl; + intros b hyp a q; (* otherwise, build a smaller counterexample *) + Refine Pp q; (* use primality once *) + Refine cut ?+1; (* standard technique for exploiting symmetry *) + intros H a' aq1 aq2; Refine H; + Immed; + Refine Eq_trans aq2; + Refine timesComm; + intros c bq; Qrepl bq; Qrepl timesAssoc p c c; + Refine timesToNonZero ? (Eq_sym bq); (* need c to be nonzero *) + intros p' c' dull cq; Qrepl cq; intros q2; + Refine Pp (Eq_sym q2); (* use primality twice *) + Refine cut ?+1; (* symmetry again *) + intros H a' aq1 aq2; Refine H; + Immed; + Refine Eq_trans aq2; + Refine timesComm; + intros d aq; Qrepl aq; Qrepl timesAssoc p d d; + intros q3; + Refine hyp ? (Eq_sym q3); (* now use ind hyp *) + Next +2; Expand NAT Nat; Qnify; (* trivial solution *) + Next +1; (* show induction was properly guarded *) + Refine Eq_trans bq; Expand p; Qrepl cq; + Refine plusComm; +Save; + +Discharge pm2; + +(********************************************************************** + Putting it all together +***********************************************************************) + +[noRatRootTwo = noRatRoot zero twoPrime + : {b|nat}{a|nat}(Eq (times two (times a a)) (times b b))-> + (Eq a zero /\ Eq b zero)]; + -- cgit v1.2.3