Thanks, Konrad and Mark! I sorta understood what you posted on my own, by
thinking about John & Freek's Mizar-like code. And thanks to Vince, as I now
have the type annotation reduction I wanted, using retypecheck code from
Freek's function parse_context_term from Mizarlight/miz2a.ml, which is
essentially the same as John's code typecheck_in_env in Examples/mizar.ml. Now
SUBGOAL_THEN (renamed subgoal_THEN) can take a string argument, and turn it
into a pristine preterm by
fst o parse_preterm o lex o explode
and turn that into a term by
term_of_preterm o retypecheck env,
where env is created by Konrad's dest_var and frees, which Petros taught me
about. Now SUBGOAL_TAC, consider and case_split are easily modified. The new
code removes 51 out of 75 type annotations from
Examples/inverse_bug_puzzle_tac.ml. I have two hazy beliefs I'd like you to
help me out with:
1) I believe that my environment is built from the goal as well as all the
assumptions. I'm guessing that w is the goal in the (asl,w) occurring so often
in tactics.ml. I think I have evidence from my rewrite of
inverse_bug_puzzle_tac.ml, which now reads
let reachableN_CLAUSES = prove
(`∀ p p'. (reachableN p p' 0 ⇔ p = p') ∧
∀ n. reachableN p p' (SUC n) ⇔ ∃ q. reachableN p q n ∧ move q p'`,
INTRO_TAC "∀p p'" THEN
consider `"s0 such that s0 = λm:num. p'` [...]
The evidence is that p' did not need the type annotation real^2#real^2#real^2,
which can be inferred from goal, which p' is free in after INTRO_TAC "∀p p'",
and
# type_of `reachableN`;;
val it : hol_type = `:real^2#real^2#real^2->real^2#real^2#real^2->num->bool`
2) I think we can't play (retypecheck env) games on a preterm that's created
with preterm_of_term, as too much type annotation has already taken place. We
need a pristine preterm created by fst o parse_preterm o lex o explode.
Vince, I easily could have used preterms entirely instead instead of strings,
and the only cost would be that consider would be look slightly worse. But I'm
hoping that strings will simplify the real goal, a miz3-type interface for HOL
Light.
John and Freek also remove type annotations from EXISTS_TAC and X_GEN_TAC, but
I haven't done that yet.
To run my code, modify quotexpander in system.ml as before as follows:
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)^"\"";;
Now restart HOL Light with
ocaml
#use "hol.ml";;
Here's my subgoal/consider/case_split code:
let (subgoal_THEN: string -> thm_tactic -> tactic) =
fun stm ttac (asl,w) ->
let env = map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var)
(freesl (w::(map (concl o snd) asl))) in
let wa = (term_of_preterm o retypecheck env)
((fst o parse_preterm o lex o explode) stm) in
let meta,gl,just = ttac (ASSUME wa) (asl,w) in
meta,(asl,wa)::gl,fun i l -> PROVE_HYP (hd l) (just i (tl l));;
let subgoal_TAC s stm prfs =
match prfs with
p::ps -> (warn (ps <> []) "subgoal_TAC: additional subproofs ignored";
subgoal_THEN stm (LABEL_TAC s) THENL [p; ALL_TAC])
| [] -> failwith "subgoal_TAC: no subproof given";;
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
match prfs with
p::ps -> (warn (ps <> []) "consider: additional subproofs ignored";
subgoal_THEN ("?" ^ vars ^ ". " ^ t)
(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
subgoal_TAC "" (list_mk_string_disj sDisjlist) tac THEN
FIRST_X_ASSUM (DESTRUCT_TAC sDestruct);;
(* Below is a version of the tutorial readable proof of the irrationality of
sqrt 2 illustrating the new code above.
--
Best,
Bill *)
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;;
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN
INTRO_TAC "!p; A; !q; B" THEN
subgoal_TAC "" `"EVEN(p * p) <=> EVEN(2 * q * q)`
[HYP MESON_TAC "B" []] THEN
subgoal_TAC "" `"EVEN(p)` [so (MESON_TAC [ARITH; EVEN_MULT])] THEN
consider `"m such that p = 2 * m`
[so (MESON_TAC [EVEN_EXISTS])] "C" THEN
case_split "qp | pq" [`"q < p`; `"p <= q`] [ARITH_TAC] THENL
[subgoal_TAC "" `"q * q = 2 * m * m ==> m = 0` [HYP MESON_TAC "qp A" []] THEN
so (HYP NUM_RING_thmTAC "B C" []);
subgoal_TAC "" `"p * p <= q * q` [so (MESON_TAC [LE_MULT2 ])] THEN
subgoal_TAC "" `"q * q = 0` [so (HYP ARITH_thmTAC "B" [])] THEN
so (NUM_RING_thmTAC [])]);;
------------------------------------------------------------------------------
Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET
Get 100% visibility into your production application - at no cost.
Code-level diagnostics for performance bottlenecks with <2% overhead
Download for free and get started troubleshooting in minutes.
http://p.sf.net/sfu/appdyn_d2d_ap1
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
