I ported the HOL Light tutorial's proof of the irrationality of sqrt{2}
(below). The tactics proof of NSQRT_2 (p 75) used the theorems
num_WF, RIGHT_IMP_FORALL_THM, EVEN_MULT, ARITH, EVEN_EXISTS, ARITH_RULE,
LE_MULT2, MULT_EQ_0; ARITH_RULE.
My miz3 port used all these theorems except RIGHT_IMP_FORALL_THM and ARITH. I
used in addition the theorems NUM_RING and LTE_CASES. Perhaps I needed the
last two because I didn't quite follow, or completely understand, John's
argument. But I have trouble seeing why I don't need NUM_RING, which I used to
prove that
p^2 = 2q^2 and p = 2m implies q^2 = 2m^2.
--
Best,
Bill
horizon := 0;;
timeout := 50;;
let SquareRoot2 = thm `;
thus ! p. ! q. p * p = 2 * q * q ==> q = 0
proof
consider P such that
P = \p. ! q. p * p = 2 * q * q ==> q = 0 [Pdef];
! p. (! m. m < p ==> P m) ==> P p
proof
let p be num;
assume ! m. m < p ==> P m [pInductStep];
! q. p * p = 2 * q * q ==> q = 0
proof
let q be num;
assume p * p = 2 * q * q [pq2];
EVEN p by -, EVEN_EXISTS, EVEN_MULT;
consider m such that
p = 2 * m by -, EVEN_EXISTS;
q * q = 2 * m * m [qmWorks] by -, pq2, NUM_RING;
! x. 2 * x <= x ==> x = 0 [Mult2LessZero] by ARITH_RULE;
q < p \/ q = 0 by LTE_CASES, pq2, LE_MULT2, Mult2LessZero,
MULT_EQ_0;
cases by -;
suppose q < p;
m = 0 by -, qmWorks, pInductStep, Pdef;
qed by -, qmWorks, MULT_0, MULT_EQ_0;
suppose q = 0;
qed by -;
end;
qed by -, Pdef;
qed by -, num_WF, Pdef;
`;;
------------------------------------------------------------------------------
Keep yourself connected to Go Parallel:
INSIGHTS What's next for parallel hardware, programming and related areas?
Interviews and blogs by thought leaders keep you ahead of the curve.
http://goparallel.sourceforge.net
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
