(* ------------------------------------------------------------------------- *) (* More "manual" proof of main lemma avoiding SOS_RULE. *) (* ------------------------------------------------------------------------- *) let NSQRT_2 = prove (`!p q. p * p = 2 * q * q ==> q = 0`, MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN ONCE_REWRITE_TAC[ARITH_RULE `q * q = 2 * m * m <=> (2 * m) * (2 * m) = 2 * q * q`] THEN ASM_REWRITE_TAC[ARITH_RULE `(q < 2 * m ==> m = 0) <=> 2 * m <= q`] THEN DISCH_THEN(MP_TAC o MATCH_MP LE_MULT2 o W CONJ) THEN ASM_REWRITE_TAC[ARITH_RULE `2 * x <= x <=> x = 0`; MULT_EQ_0]);; (* ------------------------------------------------------------------------- *) (* A slicker proof avoiding odd/even case analysis. *) (* ------------------------------------------------------------------------- *) let LEMMA_1 = SOS_RULE `p EXP 2 = 2 * q EXP 2 ==> (q = 0 \/ 2 * q - p < p /\ ~(p - q = 0)) /\ (2 * q - p) EXP 2 = 2 * (p - q) EXP 2`;; let NSQRT_2 = prove (`!p q. p * p = 2 * q * q ==> q = 0`, REWRITE_TAC[GSYM EXP_2] THEN MATCH_MP_TAC num_WF THEN MESON_TAC[LEMMA_1]);;