helphomeduck scriptspecificationfirst proof page


Duck Proof Script
The Square Root of 2 is Irrational


*** 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> ."
[]