1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
(* Example proof by Konrad Slind. See http://www.cs.kun.nl/~freek/comparison/
Taken from HOL4 distribution hol98/examples/root2.sml *)
(*---------------------------------------------------------------------------*)
(* Challenge from Freek Wiedijk: the square root of two is not rational. *)
(* I've adapted a proof in HOL Light by John Harrison. *)
(*---------------------------------------------------------------------------*)
load "transcTheory"; open arithmeticTheory BasicProvers;
(*---------------------------------------------------------------------------*)
(* Need a predicate on reals that picks out the rational ones *)
(*---------------------------------------------------------------------------*)
val Rational_def = Define `Rational r = ?p q. ~(q=0) /\ (abs(r) = &p / &q)`;
(*---------------------------------------------------------------------------*)
(* Trivial lemmas *)
(*---------------------------------------------------------------------------*)
val EXP_2 = Q.prove(`!n:num. n**2 = n*n`,
REWRITE_TAC [TWO,ONE,EXP] THEN RW_TAC arith_ss []);
val EXP2_LEM = Q.prove(`!x y:num. ((2*x)**2 = 2*(y**2)) = (2*(x**2) = y**2)`,
REWRITE_TAC [TWO,EXP_2]
THEN PROVE_TAC [MULT_MONO_EQ,MULT_ASSOC,MULT_SYM]);
(*---------------------------------------------------------------------------*)
(* Lemma: squares are not doublings of squares, except trivially. *)
(*---------------------------------------------------------------------------*)
val lemma = Q.prove
(`!m n. (m**2 = 2 * n**2) ==> (m=0) /\ (n=0)`,
completeInduct_on `m` THEN NTAC 2 STRIP_TAC THEN
`?k. m = 2*k` by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT,EVEN_EXISTS]
THEN VAR_EQ_TAC THEN
`?p. n = 2*p` by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT,
EVEN_EXISTS,EXP2_LEM]
THEN VAR_EQ_TAC THEN
`k**2 = 2*(p**2)` by PROVE_TAC [EXP2_LEM] THEN
`(k=0) \/ k < 2*k` by numLib.ARITH_TAC
THENL [FULL_SIMP_TAC arith_ss [EXP_2],
PROVE_TAC [MULT_EQ_0, DECIDE (Term `~(2 = 0n)`)]]);
(*---------------------------------------------------------------------------*)
(* The proof moves the problem from R to N, then uses lemma *)
(*---------------------------------------------------------------------------*)
local open realTheory transcTheory
in
val SQRT_2_IRRATIONAL = Q.prove
(`~Rational (sqrt 2r)`,
RW_TAC std_ss [Rational_def,abs,SQRT_POS_LE,REAL_POS]
THEN Cases_on `q = 0` THEN ASM_REWRITE_TAC []
THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `\x. x pow 2`)
THEN RW_TAC arith_ss [SQRT_POW_2, REAL_POS, REAL_POW_DIV,
REAL_EQ_RDIV_EQ,REAL_LT, REAL_POW_LT]
THEN REWRITE_TAC [REAL_OF_NUM_POW, REAL_MUL, REAL_INJ]
THEN PROVE_TAC [lemma])
end;
(*---------------------------------------------------------------------------*)
(* The following is a bit more declarative *)
(*---------------------------------------------------------------------------*)
infix THEN1;
fun ie q tac = Q_TAC SUFF_TAC q THEN1 tac;
local open realTheory transcTheory
in
val SQRT_2_IRRATIONAL = Q.prove
(`~Rational (sqrt 2r)`,
ie `!p q. ~(q=0) ==> ~(sqrt 2 = & p / & q)`
(RW_TAC std_ss [Rational_def,abs,SQRT_POS_LE,REAL_POS]
THEN PROVE_TAC[]) THEN RW_TAC std_ss [] THEN
ie `~(sqrt 2 = & p / & q)` (PROVE_TAC []) THEN
ie `~(2 * q**2 = p**2)`
(DISCH_TAC THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `\x. x pow 2`)
THEN RW_TAC arith_ss [SQRT_POW_2,REAL_POS,
REAL_POW_DIV,REAL_EQ_RDIV_EQ,REAL_LT, REAL_POW_LT]
THEN ASM_REWRITE_TAC [REAL_OF_NUM_POW, REAL_MUL,REAL_INJ])
THEN PROVE_TAC [lemma])
end;
|
