Thanks, Vince! It look like your q.ml and the HOL4 version are both
counterexamples to what I've been posting, that the only place where
retypecheck is used with a nonempty environment is in John & Freek's Mizar-like
code. I'm really happy to have been wrong! I can definitely see some
similarities between my code and yours, e.g.
let CONTEXT_TAC ttac (asms,c as g) =
let vs = frees c @ freesl (map (concl o snd) asms) in
although I don't know how to run your code and can't really read it. Great!
Thanks for not telling me about this before, because I found writing my code to
be a very interesting exercise! I do prefer my code, at this point, maybe just
because I can read mine. Can you try to compare my code to yours? Does yours
do anything mine doesn't do, or vice versa? Did I not check for some important
error conditions? Are there bugs I will run into? I think you said that yours
isn't quite finished yet, and that you were going to do a great deal more. Can
you say anything about how you learned to write your code?
I looked at the HOL4 version
http://hol.sourceforge.net/kananaskis-8-helpdocs/help/src-sml/htmlsigs/Q.html
and can see some similarity:
fun EXISTS_TAC q (g as (asl, w)) =
let val ctxt = free_varsl (w::asl)
[...]
fun ptm_with_ctxtty ctxt ty q =
let val q' = QUOTE "(" :: (q @ [QUOTE "):", ANTIQUOTE(ty_antiq ty), QUOTE ""])
in Parse.parse_in_context ctxt (normalise_quotation q')
end
Perhaps you can help me with next stage of my project, to write a miz3-type
interface for general HOL Light code. The one thing I don't like about miz3 is
the "by" list, an unordered comma-separated list. Why not keep the rest of the
miz3 interface and use regular HOL Light proofs? It would be easier to write,
wouldn't it? I have a few questions and points:
1) Is there already an HOL4 version of anything like this?
2) Using my parser/`"[...]`/string idea, all I need is to write a function to
turn a huge string into from a miz3-looking proof to an HOL Light proof. It
seems to me that this an easy project if one has good regexp/replace functions,
and I think that's in the Ocaml str library, described e.g. in Chapter 24 of
the official ocaml manual. I don't believe that str is ever used in HOL Light.
Do you know why that is? Does HOL4 use any fancy SML regexp/replace
functions? If we don't use str, I suspect the plan is to to use (lex o
explode) and then play lex games. I already did something like that in a
different version of the code, something that borrows from Marco's code:
map (fun l -> match l with
Ident s -> s
| _ -> raise Noparse) ((lex o explode) vars)
Do you have advice on how to learn more about how to use lexcode lists to turn
one type of proof to another?
3) Your (asms,c as g) looks a lot like things I saw in tactics.ml. Does this
mean that g is equal to the ordered pair (asms,c)? Do you know where that
feature of "as" is explained?
4) How can we debug code that explicitly uses the goal, as you do with (g as
(asl, w))?
Below is a version of my code, with examples, that doesn't involve rewriting
quotexpander, but borrows Freek's `;[...]` feature.
--
Best,
Bill
let parse_qproof s = (String.sub s 1 (String.length s - 1));;
let (make_env: goal -> (string * pretype) list) =
fun (asl,w) -> map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var)
(freesl (w::(map (concl o snd) asl)));;
let parse_env_string env s = (term_of_preterm o retypecheck env)
((fst o parse_preterm o lex o explode) s);;
let (subgoal_THEN: string -> thm_tactic -> tactic) =
fun stm ttac (asl,w) ->
let wa = parse_env_string (make_env (asl,w)) 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 (exists_TAC: string -> tactic) =
fun stm (asl,w) -> let env = make_env (asl,w) in
EXISTS_TAC (parse_env_string env stm) (asl,w);;
let (X_gen_TAC: string -> tactic) =
fun svar (asl,w) ->
let vartype = (snd o dest_var o fst o dest_forall) w in
X_GEN_TAC (mk_var (svar,vartype)) (asl,w);;
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);;
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;;
(* from the HOL Light tutorial, followed by a version with no type annotations
*)
let AXIOM_OF_CHOICE = prove
(`(!x:A. ?y:B. P x y) ==> ?f. !x. P x (f x)`,
STRIP_TAC THEN EXISTS_TAC `\x:A. @y:B. P x y` THEN ASM_MESON_TAC[]);;
let AXIOM_OF_CHOICE = prove
(`(!x. ?y. P x y) ==> ?f. !x. P x (f x)`,
INTRO_TAC "H1" THEN exists_TAC `;\x. @y. P x y` THEN
HYP MESON_TAC "H1" []);;
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN
X_gen_TAC "p" THEN INTRO_TAC "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
