Vince and Freek, I was wrong and you were right! First I used Vince's
let get = Obj.magic o Toploop.getvalue;;
but then I switched over to Freek's much more complicated exec_thm, as I could
not see how to test for theorems with get, as I didn't know how to handle a get
exception.
My low-tech solution using the reference theorems of database.ml fell apart as
soon as I wanted to refer to a theorem I proved. That would probably require
the techniques of update_database.ml, similar to yours and Freek's:
let exec = ignore o Toploop.execute_phrase false Format.std_formatter
o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
[...]
Obj.magic (Toploop.getvalue "buf__");;
[...]
let env = Obj.magic !Toploop.toplevel_env in
I'm including my new code, hoping that someone knows how to simplify Freek's
work with the simple get, and maybe to admit that my code might end up as
complicated as Freek's miz3.ml or John's mizar.ml. That's OK as long as I can
read it: my aim was only to get modify miz3 to use tactics proofs instead of
the unordered by list. Progress report: I still haven't coded up SUBGOAL_THEN,
needed when a proof is quite long, and haven't handled terms which are lists,
as they have semicolons. But I ported the first 185 lines of proofs in
RichterHilbertAxiomGeometry/FontHilbertAxiom.ml, so I think the code below is
solid.
--
Best,
Bill
#load "str.cma";;
(* ========================================================================= *)
(* Miz3 interface for tactics proof, so the syntax before the keyword "by" *)
(* emulates miz3.ml, with the aim of improved readability of formal proofs, *)
(* with few type annotations, doublequotes, backquotes and semicolons in *)
(* lists. Uses a version of INTRO_TAC, consider, case_split. Statements *)
(* to be proved are merely written, with the SUBGOAL_TAC hidden. Semicolons *)
(* are used essentially as THEN connecting tactics. THENL is currently *)
(* only allowed implicitly in case_split. More general tactics proofs could *)
(* be allowed than are presently, but allowing completely arbitrary proofs *)
(* will impede readability, so there's a tradeoff. An interactive mode is *)
(* useful in debugging proofs. An advantage over miz3 is that REWRITE_TAC *)
(* and SIMP_TAC can be used intelligently, as we have structured proofs, and *)
(* not an unordered commma separated "by" list. Miz3 proofs are primarily *)
(* done by MESON_TAC. Another advantage is that the semantics are obvious, *)
(* there's a straightforward translation to HOL Light tactics proofs. *)
(* parse_qproof uses system.ml quotexpander feature designed for miz3.ml to *)
(* turn backquoted expression `;[...]` into a string with no newline or *)
(* backslash problems. This miz3 emulation can not be used simultaneously *)
(* with miz3, which defines parse_qproof differently. *)
let parse_qproof s = (String.sub s 1 (String.length s - 1));;
(* exec_thm, taken from miz3.ml, maps a string to its theorem, and defines *)
(* the predicate is_thm which tests if a string represents a theorem. *)
let exec_phrase b s =
let lexbuf = Lexing.from_string s in
let ok = Toploop.execute_phrase b Format.std_formatter
(!Toploop.parse_toplevel_phrase lexbuf) in
Format.pp_print_flush Format.std_formatter ();
(ok,
let i = lexbuf.Lexing.lex_curr_pos in
String.sub lexbuf.Lexing.lex_buffer
i (lexbuf.Lexing.lex_buffer_len - i));;
let exec_thm_out = ref TRUTH;;
let exec_thm s =
try
let ok,rst = exec_phrase false
("exec_thm_out := (("^s^") : thm);;") in
if not ok or rst <> "" then raise Noparse;
!exec_thm_out
with _ -> raise Noparse;;
let exec_thmlist_tactic_out = ref REWRITE_TAC;;
let exec_thmlist_tactic s =
try
let ok,rst = exec_phrase false
("exec_thmlist_tactic_out := (("^s^") : thm list -> tactic);;") in
if not ok or rst <> "" then raise Noparse;
!exec_thmlist_tactic_out
with _ -> raise Noparse;;
let exec_thmtactic_out = ref MATCH_MP_TAC;;
let exec_thmtactic s =
try
let ok,rst = exec_phrase false
("exec_thmtactic_out := (("^s^") : thm -> tactic);;") in
if not ok or rst <> "" then raise Noparse;
!exec_thmtactic_out
with _ -> raise Noparse;;
let exec_tactic_out = ref ALL_TAC;;
let exec_tactic s =
try
let ok,rst = exec_phrase false
("exec_tactic_out := (("^s^") : tactic);;") in
if not ok or rst <> "" then raise Noparse;
!exec_tactic_out
with _ -> raise Noparse;;
let is_thm s =
try let thm = exec_thm s in true
with _ -> false;;
let is_tactic s =
try let tactic = exec_tactic s in true
with _ -> false;;
let is_thmtactic s =
try let ttac = exec_thmtactic s in true
with _ -> false;;
let is_thmlist_tactic s =
try let thmlist_tactic = exec_thmlist_tactic s in true
with _ -> false;;
(* make_env and parse_env_string, following Mizarlight/miz2a.ml and Vince *)
(* Aravantinos's https://github.com/aravantv/HOL-Light-Q, turn a string to a *)
(* term with types inferred by the goal and assumption list. The versions *)
(* of SUBGOAL_THEN, SUBGOAL_TAC, EXISTS_TAC, X_GEN_TAC, case_split and *)
(* consider can be used generally, especially with _split and consider use *)
(* DESTRUCT_TAC, so the labels sDestruct and lab must be nonempty strings; a *)
(* warning holds for case_split and consider in our miz3 emulation. *)
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 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 consider vars_t prfs lab =
let noSuchThat = Str.bounded_split (Str.regexp
"[ \t\n]+such[ \t\n]+that[ \t\n]+") vars_t 2 in
let vars = hd noSuchThat and
t = hd (tl noSuchThat) 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 raa lab st tac = subgoal_THEN (st ^ " ==> F") (LABEL_TAC lab) THENL
[INTRO_TAC lab; tac];;
(* Basically from the HOL Light tutorial "Towards more readable proofs." *)
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 fol = MESON_TAC;;
let arithmetic = ARITH_TAC;;
let set_RULE = CONV_TAC SET_RULE;;
(* Allows HOL4 and Isabelle style math characters, via parse_qproof. *)
let CleanMathFontsForHOL_Light s =
let rec clean s loStringPairs =
match loStringPairs with
[] -> s
| (hd :: tl) ->
let symbol = fst hd and ascii = snd hd in
let s = Str.global_replace (Str.regexp symbol) ascii s in
clean s tl in
clean s ["⇒","==>"; "⇔","<=>"; "∧","/\\ "; "∨","\\/"; "¬","~";
"∀","!"; "∃","?"; "∈","IN"; "∉","NOTIN";
"α","alpha"; "β","beta"; "γ","gamma"; "λ","\\"; "θ","theta"; "μ","mu";
"⊂","SUBSET"; "∩","INTER"; "∪","UNION"; "∅","{}"; "━","DELETE"];;
(* StringToTacticsProof uses regexp functions from the Str library to turn *)
(* string into a tactics proof. Most of the work is in ConvertToHOL, which *)
(* recognizes and converts pieces of the proof as string version of either: *)
(* a one-word tactic, e.g. ARITH_TAC; *)
(* a one-word thm_tactic and a thm, e.g. MATCH_MP_TAC num_WF; *)
(* intro_TAC followed by a nonempty comma-separated intro string; *)
(* exists_TAC term, the term of a string with few type annotations; *)
(* consider vars such that t [label] by tactic; *)
(* statement [label] by tactic; a typical proof of a statement or consider *)
(* thmlist->tactic labels [theorems], where the lists labels and theorems *)
(* are space- and comma-separated resp. Unlike miz3, there must be a label, *)
(* but the empty label [] is fine. The tactic obtained is *)
(* HYP thmlist->tactic "labels" [theorems] unless - occurs in labels, and *)
(* then so (using FIRST_ASSUM) references the previous statement. *)
let ws = "[ \t\n]+";;
let ws0 = "[ \t\n]*";;
let StringRegexpEqual r s = Str.string_match r s 0 &&
s = Str.matched_string s;;
let rec ConvertToHOL s =
if StringRegexpEqual (Str.regexp (ws0^ "\([^ \t\n]+\)" ^ws0)) s &&
is_tactic (Str.matched_group 1 s)
then
exec_tactic (Str.matched_group 1 s)
else
if StringRegexpEqual (Str.regexp
(ws0^ "\([^][ \t\n]+\)" ^ws0^ "\([^][ \t\n]+\)" ^ws0)) s &&
is_thmtactic (Str.matched_group 1 s) &&
is_thm (Str.matched_group 2 s)
then
let ttac = (Str.matched_group 1 s) and
thm = (Str.matched_group 2 s) in
(exec_thmtactic ttac) (exec_thm thm)
else
if Str.string_match (Str.regexp (ws0^ "intro_TAC" ^ws)) s 0
then
let intro_string = (Str.global_replace (Str.regexp ",") ";"
(Str.string_after s (String.length (Str.matched_string s)))) in
INTRO_TAC intro_string
else
if Str.string_match (Str.regexp (ws0^ "exists_TAC" ^ws)) s 0
then
exists_TAC (Str.string_after s (String.length (Str.matched_string s)))
else
if Str.string_match (Str.regexp (ws0^ "consider" ^ws^ "\(\(.\|\n\)+\)" ^ws^
"such"
^ws^ "that" ^ws^ "\(\(.\|\n\)+\)" ^ws^ "\[\(\(.\|\n\)*\)\]" ^ws^ "by" ^ws))
s 0
then
let vars = Str.matched_group 1 s and
t = Str.matched_group 3 s and
lab = Str.matched_group 5 s and
tac = Str.string_after s (String.length (Str.matched_string s)) in
subgoal_THEN ("?" ^ vars ^ ". " ^ t)
(DESTRUCT_TAC ("@" ^ vars ^ "." ^ lab)) THENL [ConvertToHOL tac; ALL_TAC]
else
if Str.string_match (Str.regexp
("\(\(.\|\n\)+\)\[\([^]]*\)\]" ^ws^ "by" ^ws)) s 0
then
let statement = Str.matched_group 1 s and
lab = Str.matched_group 3 s and
tac = (Str.string_after s (String.length (Str.matched_string s))) in
subgoal_TAC lab statement [ConvertToHOL tac]
else
if StringRegexpEqual (Str.regexp (ws0^ "\([^ \t\n]+\)\(" ^ws^ "[^[]*"
^ws0^ "\)\[\(\(.\|\n\)*\)\]" ^ws0)) s &&
is_thmlist_tactic (Str.matched_group 1 s)
then
try
let ttac = exec_thmlist_tactic (Str.matched_group 1 s) and
labs = Str.matched_group 2 s and
thms = Str.global_replace (Str.regexp ws) "" (Str.matched_group 3 s) in
let listofThms = map exec_thm (Str.split (Str.regexp ",") thms) in
if Str.string_match (Str.regexp ("[^-]*" ^ws^ "-" ^ws)) labs 0
then
let labs_minus = Str.global_replace (Str.regexp (ws^ "-")) "" labs in
so (HYP ttac labs_minus listofThms)
else HYP ttac labs listofThms
with _ -> warn (true) "square-brace following thm_list->tactic is not a
comma-separated list of theorems"; ALL_TAC
else ALL_TAC;;
let organizeTHEN s =
let rec THENify listofString =
match listofString with
[] -> ALL_TAC
| hd::tl -> (ConvertToHOL hd) THEN (THENify tl) in
THENify (Str.split (Str.regexp "[ \t\n]*;[ \t\n]*") s);;
(* StringToTacticsProof only handles case_split, which has semicolons: *)
(* case_split sDestruct by tactic; *)
(* suppose dj1; *)
(* <proof1> *)
(* suppose dj2; *)
(* <proof2> *)
(* ... *)
(* where tactic is a proof of the disjunction dj1 \/ dj2 \/ ..., and proof1 *)
(* is a proof of the goal with the added assumptions dj1, etc. *)
let StringToTacticsProof s =
try
let start = Str.search_forward (Str.regexp
(ws0^ "case_split" ^ws)) s 0 in
organizeTHEN (Str.string_before s start) THEN
let s = (Str.string_after s (Str.match_end())) in
let start = Str.search_forward (Str.regexp (ws ^ "by" ^ ws)) s 0 in
let sDestruct = (Str.string_before s start) and
rest = (Str.string_after s (Str.match_end())) in
let start = Str.search_forward (Str.regexp (";" ^ ws)) rest 0 in
let tac = (Str.string_before rest start) and
loCase = Str.split (Str.regexp ("suppose" ^ws))
(Str.string_after rest (Str.match_end())) in
let suppose_proof case =
let start = Str.search_forward (Str.regexp ";") case 0 in
(Str.string_before case start, Str.string_after case
(Str.match_end())) in
let pairCase = map suppose_proof loCase in
let listofDisj = map fst pairCase and
listofTac = map snd pairCase in
(case_split sDestruct listofDisj [ConvertToHOL tac])
THENL (map organizeTHEN listofTac)
with Not_found -> organizeTHEN s;;
let theorem s =
let s = CleanMathFontsForHOL_Light s in
let start = Str.search_forward (Str.regexp (ws ^ "proof" ^ ws)) s 0 in
let thm = (Str.string_before s start) and
proof = (Str.string_after s (Str.match_end())) in
prove (parse_env_string [] thm, StringToTacticsProof proof);;
let interactive_proof s =
let proof = CleanMathFontsForHOL_Light s in
e (StringToTacticsProof proof);;
let interactive_goal s =
let thm = CleanMathFontsForHOL_Light s in
g (parse_env_string [] thm);;
(* Two versions of proofs in the HOL Light tutorial. First from p 93, then
our version of the p 81 readable proof of the irrationality of sqrt 2. *)
let AXIOM_OF_CHOICE = theorem `;
∀P. (∀x. ∃y. P x y) ==> ∃f. ∀x. P x (f x)
proof
intro_TAC ∀P, H1;
exists_TAC \x. @y. P x y;
fol H1 [];
`;;
let NSQRT_2 = theorem `;
∀p q. p * p = 2 * q * q ⇒ q = 0
proof
MATCH_MP_TAC num_WF;
intro_TAC ∀p, A, ∀q, B;
EVEN(p * p) ⇔ EVEN(2 * q * q) [] by fol B [];
EVEN(p) [] by fol - [ARITH, EVEN_MULT];
consider m such that p = 2 * m [C] by fol - [EVEN_EXISTS];
case_split qp | pq by arithmetic;
suppose q < p;
q * q = 2 * m * m ⇒ m = 0 [] by fol qp A [];
NUM_RING_thmTAC - B C [];
suppose p <= q;
p * p <= q * q [] by fol - [LE_MULT2];
q * q = 0 [] by ARITH_thmTAC - B [];
NUM_RING_thmTAC - [];
`;;
interactive_goal `;∀p q. p * p = 2 * q * q ⇒ q = 0
`;;
interactive_proof `;
MATCH_MP_TAC num_WF;
intro_TAC ∀p, A, ∀q, B;
EVEN(p * p) ⇔ EVEN(2 * q * q) [] by fol B [];
EVEN(p) [] by fol - [ARITH, EVEN_MULT];
consider m such that p = 2 * m [C] by fol - [EVEN_EXISTS]
`;;
interactive_proof `;
case_split qp | pq by arithmetic;
suppose q < p;
q * q = 2 * m * m ⇒ m = 0 [] by fol qp A [];
NUM_RING_thmTAC - B C [];
suppose p <= q;
p * p <= q * q [] by fol - [LE_MULT2];
q * q = 0 [] by ARITH_thmTAC - B [];
NUM_RING_thmTAC - []
`;;
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and
their applications. This 200-page book is written by three acclaimed
leaders in the field. The early access version is available now.
Download your free book today! http://p.sf.net/sfu/neotech_d2d_may
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
