miz3/Samples/irrat2.ml

   1 needs "Library/transc.ml";;
   2 needs "Examples/sos.ml";;
   3
   4 prioritize_real();;
   5
   6 horizon := 1;;
   7
   8 let rational = new_definition
   9  `rational(r) = ?p q. ~(q = 0) /\ abs(r) = &p/ &q`;;
  10
  11 (* ======== Mizar-style version ============================================ *)
  12
  13 let NSQRT_2_1 = thm `;
  14   !p q. p*p = 2*q*q ==> q = 0
  15   proof
  16     exec MATCH_MP_TAC num_WF;
  17     let p be num;
  18     assume !p'. p' < p ==> !q. p'*p' = 2*q*q ==> q = 0 [1];
  19     let q be num;
  20     assume p*p = 2*q*q [2];
  21     EVEN (p*p) by EVEN_DOUBLE;
  22     EVEN p by EVEN_MULT;
  23     consider p' such that
  24       p = 2*p' [3] by EVEN_EXISTS;
  25     q*q = 2*p'*p' [4] by 2,NUM_RING;
  26     EVEN (q*q) by EVEN_DOUBLE;
  27     EVEN q by EVEN_MULT;
  28     consider q' such that
  29       q = 2*q' [5] by EVEN_EXISTS;
  30     p'*p' = 2*q'*q' [6] by 4,NUM_RING;
  31     assume ~(q = 0) [7];
  32     ~(p = 0) by 2,NUM_RING;
  33     p > 0 by ARITH_TAC;
  34     p' < p by 3,ARITH_TAC;
  35     q' = 0 by 1,6;
  36   qed by 5,7,MULT_EQ_0`;;
  37
  38 let SQRT_2_IRRATIONAL_1 = thm `;
  39   ~rational(sqrt(&2))
  40   proof
  41     assume rational(sqrt(&2));
  42     set x = abs(sqrt(&2));
  43     consider p q such that
  44       ~(q = 0) /\ x = &p/ &q [7] by rational;
  45     ~(&q = &0) by REAL_INJ;
  46     x* &q = &p [8] by 7,REAL_DIV_RMUL;
  47     &0 <= &2 by REAL_ARITH_TAC;
  48     sqrt(&2) pow 2 = &2 by SQRT_POW2;
  49     x pow 2 = &2 by REAL_ARITH_TAC;
  50     &p* &p = &2* &q* &q by 8,REAL_RING;
  51     p*p = 2*q*q by 8,REAL_INJ,REAL_OF_NUM_MUL;
  52   qed by 7,NSQRT_2_1`;;
  53
  54 (* ======== "automatically" converted from John's version ================== *)
  55
  56 let NSQRT_2_2 = thm `;
  57   now
  58     now
  59       let p q be num;
  60       assume !m q. m < p ==> m * m = 2 * q * q ==> q = 0 [1];
  61       assume p * p = 2 * q * q [2];
  62       now
  63         let m be num;
  64         assume !m' q. m' < 2 * m ==> m' * m' = 2 * q * q ==> q = 0 [3];
  65         assume (2 * m) * 2 * m = 2 * q * q [4];
  66         (2 * m) * 2 * m = 2 * q * q
  67             ==> (q < 2 * m ==> q * q = 2 * m * m ==> m = 0)
  68             ==> q = 0
  69           by TIMED_TAC 2 (CONV_TAC SOS_RULE);
  70         (q < 2 * m ==> q * q = 2 * m * m ==> m = 0) ==> q = 0
  71           by POP_ASSUM MP_TAC,4 from -;
  72         thus q = 0 by FIRST_X_ASSUM
  73           (MP_TAC o SPECL [parse_term "q:num"; parse_term "m:num"]),3,4;
  74       end;
  75       (?m. p = 2 * m) ==> q = 0
  76         by DISCH_THEN(X_CHOOSE_THEN (parse_term "m:num") SUBST_ALL_TAC),1,2;
  77       EVEN p ==> q = 0 by REWRITE_TAC[EVEN_EXISTS],1,2;
  78       (EVEN (p * p) <=> EVEN (2 * q * q)) ==> q = 0
  79         by REWRITE_TAC[EVEN_MULT; ARITH],1,2;
  80       thus q = 0 by FIRST_ASSUM(MP_TAC o AP_TERM (parse_term "EVEN")),1,2;
  81     end;
  82     !p q.
  83         (!m q. m < p ==> m * m = 2 * q * q ==> q = 0)
  84         ==> p * p = 2 * q * q
  85         ==> q = 0 by REPEAT STRIP_TAC;
  86     !p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0))
  87         ==> (!q. p * p = 2 * q * q ==> q = 0)
  88       by REWRITE_TAC[RIGHT_IMP_FORALL_THM];
  89     thus !p q. p * p = 2 * q * q ==> q = 0 by MATCH_MP_TAC num_WF;
  90   end`;;
  91
  92 let SQRT_2_IRRATIONAL_2 = thm `;
  93   now
  94     now
  95       let p q be num;
  96       now
  97         assume ~(q = 0) [1];
  98         ~(&2 * &q * &q = &p * &p)
  99           by ASM_MESON_TAC[NSQRT_2_2; REAL_OF_NUM_EQ; REAL_OF_NUM_MUL];
 100         ~((\x. x pow 2) (sqrt (&2)) = (\x. x pow 2) (&p / &q))
 101           by ASM_SIMP_TAC[SQRT_POW_2; REAL_POS; REAL_POW_DIV; REAL_POW_2;
 102             REAL_LT_SQUARE; REAL_OF_NUM_EQ; REAL_EQ_RDIV_EQ],1;
 103         thus ~(sqrt (&2) = &p / &q)
 104           by DISCH_THEN(MP_TAC o AP_TERM (parse_term "\\x. x pow 2")),1;
 105       end;
 106       thus ~(~(q = 0) /\ sqrt (&2) = &p / &q)
 107         by DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC);
 108     end;
 109     !p q. ~(~(q = 0) /\ sqrt (&2) = &p / &q) by REPEAT GEN_TAC;
 110     thus ~rational (sqrt (&2))
 111       by SIMP_TAC[rational; real_abs; SQRT_POS_LE; REAL_POS; NOT_EXISTS_THM];
 112   end`;;
 113
 114 (* ======== humanized version of John's version ============================ *)
 115
 116 let NSQRT_2_3 = thm `;
 117   !p q. p*p = 2*q*q ==> q = 0
 118   proof
 119     set P = \p. !q. p*p = 2*q*q ==> q = 0;
 120     now
 121       let p be num;
 122       assume !m. m < p ==> P m [1];
 123       let q be num;
 124       assume p*p = 2*q*q [2];
 125       EVEN(2*q*q) by REWRITE_TAC,EVEN_MULT,ARITH;
 126       EVEN p by 2,EVEN_MULT;
 127       consider m such that p = 2*m [3] by EVEN_EXISTS;
 128       (2*m)*2*m = 2*q*q /\ (q < 2*m /\ q*q = 2*m*m ==> m = 0) ==> q = 0
 129         from TIMED_TAC 2 (CONV_TAC SOS_RULE);
 130       thus q = 0 by 1,2,3;
 131     end;
 132   qed by MATCH_MP_TAC num_WF`;;
 133
 134 let SQRT_2_IRRATIONAL_3 = thm `;
 135   ~rational(sqrt(&2))
 136   proof
 137     assume rational(sqrt(&2));
 138     consider p q such that ~(q = 0) /\ sqrt(&2) = &p/ &q [1]
 139       by rational,real_abs,SQRT_POS_LE,REAL_POS;
 140     (&p* &p)/(&q* &q) = &2 [2] by SQRT_POW_2,REAL_POS,REAL_POW_DIV,REAL_POW_2;
 141     &0 < &q* &q by 1,REAL_LT_SQUARE,REAL_OF_NUM_EQ;
 142     &2*(&q* &q) = (&p* &p) by 2,REAL_EQ_RDIV_EQ;
 143   qed by 1,NSQRT_2_3,REAL_OF_NUM_EQ,REAL_OF_NUM_MUL`;;
 144