aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coq/root2.v135
-rw-r--r--hol98/root2.sml83
-rw-r--r--lego/root2.l368
3 files changed, 586 insertions, 0 deletions
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)];
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:00:06 +0000