*** file: /net/cs/htdocs/users/goguen/kumo/sqrt2/sqrt2.duck
*****************************************
style: beijing
*****************************************
spec: /net/cs/htdocs/users/goguen/kumo/sqrt2/sqrt2.bob
*****************************************
dir: /net/cs/htdocs/groups/tatami/kumo/exs/sqrt2
*****************************************
proof: <<NatOddEven>>
goal: (forall M : Nat)(exists N : Nat)
(M = 2 * N or M = 2 * N + 1) .
by: induction on M with scheme {0, s};
<<NatOddEven.1>>
exq-let N = 0 ;
<<NatOddEven.2>>
all-uq-elim;
imp-elim >> {A1};
skolem A1 >> {A2};
case-anal A2 >> {A3 A4};
*** case 1
to-rule A3;
exq-let N = n1 ;
*** case 2
<<NatOddEven.2.1.1.1.2>>
to-rule A4;
exq-let N = n1 + 1 ;
[]
************************************************************
proof: <<Div2Time2>>
goal: (forall M : Nat) div2(2 * M) = M .
by: induction on M with scheme {0, s};
[]
************************************************************
proof: <<Mod2Double>>
goal: (forall M : Nat) mod2(2 * M) = 0 .
by: induction on M with scheme {0, s};
[]
************************************************************
proof: <<Mod2DoublePlus1>>
goal: (forall M : Nat) mod2(2 * M + 1) = 1 .
by: induction on M with scheme {0, s};
[]
***********************************************************
proof: <<SumSubtr>>
goal: (forall N M : Nat) ((M + N) - N) = M .
by: induction on N with scheme {0, s};
[]
**********************************************************
proof: <<NzNatGtZero>>
goal: (forall K : NzNat) K > 0 .
by: induction on K with scheme {1, s};
[]
**********************************************************
proof: <<SumNzNatGt>>
goal: (forall M : Nat)(forall K : NzNat) M + K > M .
by: induction on M with scheme {0, s};
lemma NzNatGtZero;
[]
***********************************************************
proof: <<Lemma1>>
goal: (forall M N : Nat)
(2 * M * M = N * N implies (exists K : Nat) N = 2 * K) .
by: all-uq-elim;
imp-elim >> { A1 };
lemma NatOddEven >> { Lemma };
instance Lemma with n >> { A2 };
skolem A2 >> { A3 };
case-anal A3 >> { A4 A5 };
*** case 1
to-rule A4;
exq-let K = n1;
red;
*** case 2
eq-apply A5 A1 >> { A6 };
lemma Mod2Double;
lemma Mod2DoublePlus1;
op-apply mod2 A6 >> { A7 };
red A7;
[]
***********************************************************
proof: <<Lemma2>>
goal: (forall M N : Nat) (2 * M = 2 * N implies M = N) .
by: all-uq-elim;
imp-elim >> {A};
lemma Div2Time2;
op-apply div2 A >> {B};
to-rule B;
red;
[]
***********************************************************
induction-scheme: GCD
sort NzNat .
assertion P : NzNat NzNat .
base P(1,1) .
induction
ops m n : -> NzNat .
assume P(m, n) .
prove P(m + n, n) .
induction
ops m n : -> NzNat .
assume P(m, n) .
prove P(m, m + n) .
[]
***********************************************************
proof: <<Lemma3>>
goal: (forall M N : NzNat) (gcd(2 * M , 2 * N) > 1) .
by: lemma SumSubtr ;
induction on <M, N> with scheme GCD ;
[]
***********************************************************
proof: <<SqrtRoot>>
goal: not (exists M N : NzNat) (2 * M * M = N * N and gcd(M, N) = 1) .
by: neg-elim;
skolem;
de-conj >> {A1 A2} ;
lemma Lemma1 >> {Lemma1} ;
modus Lemma1 A1 ;
skolem >> {A3} ;
eq-apply A3 A1;
backward >> {A4} ;
lemma Lemma2 >> {Lemma2} ;
modus Lemma2 A4 >> {A5} ;
modus Lemma1 A5;
skolem >> {A6} ;
eq-apply A3 A2 >> {A7} ;
eq-apply A6 A7 >> {A8} ;
lemma Lemma3 >> {Lemma3} ;
instance Lemma3 with n4 n3 >> {A9} ;
eq-apply A8 A9 >> {A10} ;
[]
***********************************************************
display: <<NatOddEven>>
title: "A Natural Number Must be Odd or Even"
<<NatOddEven>>
[]
***********************************************************
display: <<Div2Time2>>
title: "Div2 is an inverse operation of double operation"
<<Div2Time2>>
[]
************************************************************
display: <<Mod2Double>>
title: "A Lemma About Mod2"
<<Mod2Double>>
[]
************************************************************
display: <<Mod2DoublePlus1>>
title: "A Lemma About Mod2"
<<Mod2DoublePlus1>>
[]
************************************************************
display: <<SumSubtr>>
title: "A Relation between Sum and Subtract"
<<SumSubtr>>
[]
***********************************************************
display: <<NzNatGtZero>>
title: "NzNat is Greater than Zero"
<<NzNatGtZero>>
[]
***********************************************************
display: <<SumNzNatGt>>
title: "Increasing by Adding Positive Number"
<<SumNzNatGt>>
[]
***********************************************************
display: <<Lemma1>>
title: "A Lemma About Double Operation"
<<Lemma1>>
[]
***********************************************************
display: <<Lemma2>>
title: "A Lemma About Double Operation"
<<Lemma2>>
[]
***********************************************************
display: <<Lemma3>>
title: "A Lemma About GCD"
<<Lemma3>>
[]
***********************************************************
display: <<SqrtRoot>>
title: "The Square Root of 2 is Irrational"
<<SqrtRoot>>
intro: "We want to prove the square root of 2 is irrational. "+
"<p/>By the definition of rational number, we will show that "+
"there are no numbers <math>N</math> and <math>M</math> "+
" such that <math>2 * M * M = N * N</math> and "+
" <math>gcd(M, N) = 1</math> ."
[]
|
