Vince, I think you just explained to me that I've been misunderstanding HOL all
along! What I'd been asking about environment and scope of variable sounds now
like the simple fact that HOL allows free variables. I think that means that
FOL is actually quite different than the way mathematicians think, even though
it amounts to the same proofs.
I still don't understand why you want to avoid preterms.
Let me answer this question, and then explain my HOL misunderstanding, by going
back to my earlier post about quotexpander. It's worth going through again to
highlight John's related preterm code.
You proposed a modification of quotexpander in system.ml using "." at the start
indicate a preterm. I got a lot out of your proposal, and came up with my own
modification, where "\"" at the start indicates a string:
let quotexpander s =
if s = "" then failwith "Empty quotation" else
let c = String.sub s 0 1 in
if c = "\"" then
"\""^(String.escaped (String.sub s 1 (String.length s - 1)))^"\"" else
if c = ":" then
"parse_type \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else if c = ";" then "parse_qproof \""^(String.escaped s)^"\""
else "parse_term \""^(String.escaped s)^"\"";;
Modify quotexpander this way and then start a new HOL Light process by
ocaml
#use "hol.ml";;
Then the code included below works. The definitions of consider and case_split
there are quite simple.
But I can also define case_split using preterms, with this code:
let parse_qproof s = (fst o parse_preterm o lex o explode)
(String.sub s 1 (String.length s - 1));;
let case_split sDestruct pretermDisjlist tac =
let disjthm = (term_of_preterm o (retypecheck [])) (end_itlist
(fun pt1 pt2 -> (Combp (Combp (`;\/`, pt1), pt2))) pretermDisjlist) in
SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
(DESTRUCT_TAC sDestruct);;
I think that's a lot more complicated than my string version below, and I could
not define consider using preterms.
However, I realized last night that John did more complicated preterm stunts in
Examples/mizar.ml
(* ------------------------------------------------------------------------- *)
(* Some preterm operations we need. *)
(* ------------------------------------------------------------------------- *)
let rec split_ppair ptm =
match ptm with
Combp(Combp(Varp(",",dpty),ptm1),ptm2) -> ptm1::(split_ppair ptm2)
| _ -> [ptm];;
let pmk_conj(ptm1,ptm2) =
Combp(Combp(Varp("/\\",dpty),ptm1),ptm2);;
let pmk_exists(v,ptm) =
Combp(Varp("?",dpty),Absp(v,ptm));;
John's version of consider there is better than mine, but it's a lot more
complicated. BTW let me say that John's mizar.ml predates Freek's Mizar-like
code written, and it's only 682 lines long, and I counted 160 of those lines as
defining John's Mizar-like by justification, and I don't want that. So that's
only 522 of code that I have to understand. I can't believe it's that hard to
understand?
Maybe I don't get your question here, because it looks more complex
than I thought.
Maybe I've been misunderstanding HOL Light! I've been thinking that various
occurences of the same variable had the same value, but maybe I had it all
wrong. Let's go through the code below, which is my version of the tutorial
proof of the irrationality of sqrt.
After the first 3 lines, we have fixed the variables p & q (of type num), the
goal is
q = 0
and we have two labeled assumptions
0 [`!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0)`] (A)
1 [`p * p = 2 * q * q`] (B)
Now a mathematicians would think this means that we have chosen arbitrary
elements of the set that num denotes, and that the variables p and q will refer
to these fixed, but arbitrary, elements from now on. But I think that's not
what HOL is doing! I think HOL is just saying that the assumptions and the
goals are now written in terms of the free variables p & q. And I guess HOL
and FOL are designed this way because that's the way math works, but I never
saw that before.
The next SUBGOAL_TAC command uses assumption B and easily gives as a new
assumption
2 [`EVEN (p * p) <=> EVEN (2 * q * q)`]
The next SUBGOAL_TAC command uses this last assumption, theorems ARITH and
EVEN_MULT to prove the new assumption
3 [`EVEN p`]
I guess that's true for any free variables p & q of type num! The next
consider command fixes the variable m of type num and gives us the labeled
assumption
4 [`p = 2 * m`] (C)
Basically MESON proved that such an m exists using theorem EVEN_EXISTS. So now
we have three free variables p, q, and m which all have type num, and 5
assumptions about p, q, and m, but I think now that p, q, and m are just free
variables. Now I have a question for you:
I bet the information that p, q, and m have type num is stored somewhere. I
know we can infer the type num from the assumptions, but that's not always
true. Can you tell me where this type information is stored?
Now I do
e(case_split "qp | pq" [`"(q:num) < p`; `"p <= q`] [ARITH_TAC]);;
This gives two cases, with labels qp and pq, and I can do this because
ARITH_TAC proves that for all p & q of type num, either q < p or p <= q. I
think now that there's no connection here between this p & q and the p & q
above that I think are "fixed". Since my proof is interactive, I now work the
first case, which has a new assumption
5 [`q < p`] (qp)
The next SUBGOAL_TAC command gives us the new assumption
6 [`q * q = 2 * m * m ==> m = 0`]
I think MESON's proof only needs the two free variables p and q and the
assumptions qp and A. I think MESON just instantiates the !m. m < p of
assumption A with m = q, which is true by assumption qp. Then the consequent
of assumption A becomes, after an alpha conversion
(!z. q * q = 2 * z * z ==> z = 0)
and MESON can then instantiate z with m to get our assumption 6 above. Note
that this entire argument has nothing to do with any "fact" that p, q and m
denote fixed elements of the set denoted by the type num. It's just FOL using
the free variables p, q & m, promoted to HOL by the typing, and assumptions qp
and A. Wow. How could I have misunderstood this all along!
Let's see how the next NUM_RING_thmTAC command proves the goal q = 0 using
these 3 assumptions:
1 [`p * p = 2 * q * q`] (B)
4 [`p = 2 * m`] (C)
6 [`q * q = 2 * m * m ==> m = 0`]
We have free variables p, q and m and these 3 statements. B and C give p^2 =
2q^2 and p = 2m, so
4 m^2 = 2 q^2
q^2 = 2 m^2
Assumption 6 then gives m = 0. By C, p = 0 and then by B,
2 q^2 = 0,
so q = 0. NUM_RING can perform this sort of nonlinear deduction. Now we're
working the other case
5 [`p <= q`] (pq)
The next SUBGOAL_TAC command uses this last assumption and the theorem LE_MULT2
to prove
6 [`p * p <= q * q`]
and surely this is true for any free variables p and q of type num. There's no
reason to think that HOL Light is remembering that p and q denote fixed natural
numbers that we've been using all along!
The next SUBGOAL_TAC command deduces
7 [`q * q = 0`]
from this last assumption and B:
1 [`p * p = 2 * q * q`] (B)
6 [`p * p <= q * q`]
That is, ARITH_TAC can prove that for any free variables p & q, that if
2 q^2 <= q^2
then q = 0. Nothing about HOL Light is remembering our fixed natural numbers p
& q!
Now NUM_RING proves the goal. But surely we believe that for any free variable
q of type num that
q = 0
if q^2 = 0.
--
Best,
Bill
let consider vars_t prfs lab =
let len = String.length vars_t in
let rec findSuchThat = function
n -> if String.sub vars_t n 9 = "such that" then n
else findSuchThat (n + 1) in
let n = findSuchThat 1 in
let vars = String.sub vars_t 0 (n - 1) and
t = String.sub vars_t (n + 9) (len - n - 9) in
let tm = parse_term ("?" ^ vars ^ ". " ^ t) in
match prfs with
p::ps -> (warn (ps <> []) "Consider: additional subproofs ignored";
SUBGOAL_THEN tm (DESTRUCT_TAC ("@" ^ vars ^ "." ^ lab))
THENL [p; ALL_TAC])
| [] -> failwith "Consider: no subproof given";;
let case_split sDestruct sDisjlist tac =
let rec list_mk_string_disj = function
[] -> ""
| s::[] -> "(" ^ s ^ ")"
| s::ls -> "(" ^ s ^ ") \\/ " ^ list_mk_string_disj ls in
let disjthm = parse_term (list_mk_string_disj sDisjlist) in
SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
(DESTRUCT_TAC sDestruct);;
let TACtoThmTactic tac = fun ths -> MAP_EVERY MP_TAC ths THEN tac;;
let NUM_RING_thmTAC = TACtoThmTactic (CONV_TAC NUM_RING);;
let ARITH_thmTAC = TACtoThmTactic ARITH_TAC;;
let so = fun tac -> FIRST_ASSUM MP_TAC THEN tac;;
g `!p q. p * p = 2 * q * q ==> q = 0`;;
e(MATCH_MP_TAC num_WF);;
e(INTRO_TAC "!p; A; !q; B");;
e(SUBGOAL_TAC "" `EVEN(p * p) <=> EVEN(2 * q * q)`
[HYP MESON_TAC "B" []]);;
e(SUBGOAL_TAC "" `EVEN(p)` [so (MESON_TAC [ARITH; EVEN_MULT])]);;
e(consider `"m such that p = 2 * m`
[so (MESON_TAC [EVEN_EXISTS])] "C");;
e(case_split "qp | pq" [`"(q:num) < p`; `"p <= q`] [ARITH_TAC]);;
e(SUBGOAL_TAC "" `q * q = 2 * m * m ==> m = 0` [HYP MESON_TAC "qp A" []]);;
e(so (HYP NUM_RING_thmTAC "B C" []));;
e(SUBGOAL_TAC "" `p * p <= (q:num) * q` [so (MESON_TAC [LE_MULT2 ])]);;
e(SUBGOAL_TAC "" `q * q = 0` [so (HYP ARITH_thmTAC "B" [])]);;
e(so (NUM_RING_thmTAC []));;
let NSQRT_2 = top_thm();;
------------------------------------------------------------------------------
Try New Relic Now & We'll Send You this Cool Shirt
New Relic is the only SaaS-based application performance monitoring service
that delivers powerful full stack analytics. Optimize and monitor your
browser, app, & servers with just a few lines of code. Try New Relic
and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
