Here's a reasonable version of a miz3 interface for HOL Light. Thanks to
Vince, Freek and Petros for helping me out!
I believe this is the end of this parser-based discussion, so allow me to
summarize. It's good for formal proofs to readable, especially if you want to
attract mathematicians. John has always pushed for readable proofs, and writes
in his purple FOL book that we should really be doing both declarative and
procedural proofs, as neither is powerful enough. But it's also be nice for
the Ocaml interface code to be readable, so it can be modified. I think my
code below is much more readable that John's mizar.ml or Freek's masterpiece
miz3.ml, whose interface I have tried to emulate.
--
Best,
Bill
#load "str.cma";;
let parse_qproof s = (String.sub s 1 (String.length s - 1));;
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 thmlist_tactics = ref([]:(string*(thm list -> tactic))list);;
let thm_tactics = ref([]:(string*thm_tactic)list);;
let tactics = ref([]:(string*tactic)list);;
let tac_tactics = ref([]:(string*(tactic -> tactic))list);;
thmlist_tactics := [
"fol",MESON_TAC;
"SIMP_TAC",SIMP_TAC;
"REWRITE_TAC",REWRITE_TAC;
"SET_TAC",SET_TAC;
"NUM_RING_thmTAC",NUM_RING_thmTAC;
"ARITH_thmTAC",ARITH_thmTAC
];;
thm_tactics := [
"MATCH_MP_TAC",MATCH_MP_TAC;
"MP_TAC",MP_TAC;
];;
tactics := [
"arithmetic",ARITH_TAC;
"REAL_ARITH_TAC",REAL_ARITH_TAC
];;
tac_tactics := [
"so",so
];;
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 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 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 raa lab st tac = subgoal_THEN (st ^ " ==> F") (LABEL_TAC lab) THENL
[INTRO_TAC lab; tac];;
let CleanMathFontsForHOL_Light s =
let s = Str.global_replace (Str.regexp "⇒") "==>" s in
let s = Str.global_replace (Str.regexp "⇔") "<=>" s in
let s = Str.global_replace (Str.regexp "∧ ") "/\\ " s in
let s = Str.global_replace (Str.regexp "∨") "\\/" s in
let s = Str.global_replace (Str.regexp "¬") "~" s in
let s = Str.global_replace (Str.regexp "∀") "!" s in
let s = Str.global_replace (Str.regexp "∃") "?" s in
Str.global_replace (Str.regexp "λ") "\\" s;;
let StringRegexpEqual r s = Str.string_match r s 0 &&
s = Str.matched_string s;;
let rec ConvertToHOL s =
if StringRegexpEqual (Str.regexp "[ \t\n]*\([^ \t\n]*\)[ \t\n]*") s
then
let tac = (Str.matched_group 1 s) in
assoc tac !tactics
else
if StringRegexpEqual (Str.regexp
"[ \t\n]*\([^ \t\n]*\)[ \t\n]*\([^ \t\n]*\)[ \t\n]*") s
then
let ttac = (Str.matched_group 1 s) and
thm = (Str.matched_group 2 s) in
if mem ttac (map fst !thm_tactics) && mem thm (map fst !theorems)
then (assoc ttac !thm_tactics) (assoc thm !theorems)
else if mem ttac (map fst !tac_tactics) && mem thm (map fst !tactics)
then (assoc ttac !tac_tactics) (assoc thm !tactics)
else ALL_TAC
else
if StringRegexpEqual (Str.regexp "[ \t\n]*INTRO_TAC \([^][]*\)") s
then
let labstring = (Str.matched_group 1 s) in
INTRO_TAC (Str.global_replace (Str.regexp ",") ";" labstring)
else
if StringRegexpEqual (Str.regexp "[ \t\n]*exists_TAC \([^][]*\)") s
then
exists_TAC (Str.matched_group 1 s)
else
if StringRegexpEqual (Str.regexp
"[ \t\n]*consider[ \t\n]+\([^][]+[ \t\n]+such[ \t\n]+that[ \t\n]+[^][]+[
\t\n]+\)\[\([^][]*\)\][ \t\n]+by[ \t\n]+\([^!]*\)[ \t\n]*") s
then
let vars_t = Str.matched_group 1 s and
lab = Str.matched_group 2 s and
tac = Str.matched_group 3 s in
consider vars_t [ConvertToHOL tac] lab
else
if StringRegexpEqual (Str.regexp
"[ \t\n]*\([^ \t\n]+\)\([ \t\n]+[^[]+[ \t\n]+\)\[\([^]]*\)\][ \t\n]*") s &&
mem (Str.matched_group 1 s) (map fst !thmlist_tactics)
then
let ttac = assoc (Str.matched_group 1 s) !thmlist_tactics and
labs = Str.matched_group 2 s and
listofThms = map (fun ts -> assoc ts !theorems)
(Str.split (Str.regexp "[ \t\n]*,[ \t\n]*") (Str.matched_group 3 s)) in
if Str.string_match (Str.regexp "[^-]*[ \t\n]+-[ \t\n]+") labs 0
then
let labs_minus = Str.global_replace (Str.regexp "[ \t\n]+-") "" labs in
so (HYP ttac labs_minus listofThms)
else HYP ttac labs listofThms
else
if StringRegexpEqual (Str.regexp
"\([^][]+\)\[\([^][]*\)\][ \t\n]+by[ \t\n]+\([^!]+\)[ \t\n]*") s
then
let statement = Str.matched_group 1 s and
lab = Str.matched_group 2 s and
tac = Str.matched_group 3 s in
subgoal_TAC lab statement [ConvertToHOL 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);;
let StringToTacticsProof s =
try
let start = Str.search_forward (Str.regexp
"[ \t\n]*case_split[ \t\n]+") s 0 in
organizeTHEN (Str.string_before s start) THEN
let s = (Str.string_after s (Str.match_end())) in
if StringRegexpEqual (Str.regexp
"\([^][]+\)[ \t\n]+\[\([^][]+\)\][ \t\n]+by[ \t\n]+\([^!]+\)![
\t\n]+suppose[ \t\n]+\(\(.\|\n\)+\)") s
then
let sDestruct = Str.matched_group 1 s and
disjs = Str.matched_group 2 s and
tac = Str.matched_group 3 s and
tacs = Str.matched_group 4 s in
let listofDisj = Str.split (Str.regexp "[ \t\n]*!,[ \t\n]*") disjs and
listofTac = Str.split (Str.regexp "[ \t\n]*suppose[ \t\n]*") tacs in
(case_split sDestruct listofDisj [ConvertToHOL tac])
THENL (map organizeTHEN listofTac)
else ALL_TAC
with Not_found -> organizeTHEN s;;
let theorem s =
let sl = Str.split (Str.regexp "[ \t\n]*proof[ \t\n]*")
(CleanMathFontsForHOL_Light s) in
prove (parse_env_string [] (hd sl), StringToTacticsProof (hd (tl sl)));;
(* Two versions of proofs in the HOL Light tutorial: the axiom of choice on p
93, then 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 [q < p !, p <= q] by arithmetic!
suppose
q * q = 2 * m * m ⇒ m = 0 [] by fol qp A [];
NUM_RING_thmTAC - B C []
suppose
p * p <= q * q [] by fol - [LE_MULT2];
q * q = 0 [] by ARITH_thmTAC - B [];
NUM_RING_thmTAC - []
`;;
(* tutorial proofs for comparison:
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 NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
suffices_to_prove
`!p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0))
==> (!q. p * p = 2 * q * q ==> q = 0)`
(MATCH_ACCEPT_TAC num_WF) THEN
fix [`p:num`] THEN
assume("A") `!m. m < p ==> !q. m * m = 2 * q * q ==> q = 0` THEN
fix [`q:num`] THEN
assume("B") `p * p = 2 * q * q` THEN
so have `EVEN(p * p) <=> EVEN(2 * q * q)` (trivial) THEN
so have `EVEN(p)` (using [ARITH; EVEN_MULT] trivial) THEN
so consider (`m:num`,"C",`p = 2 * m`) (using [EVEN_EXISTS] trivial) THEN
cases ("D",`q < p \/ p <= q`) (arithmetic) THENL
[so have `q * q = 2 * m * m ==> m = 0` (by ["A"] trivial) THEN
so we’re finished (by ["B"; "C"] algebra);
so have `p * p <= q * q` (using [LE_MULT2] trivial) THEN
so have `q * q = 0` (by ["B"] arithmetic) THEN
so we’re finished (algebra)]);;
*)
------------------------------------------------------------------------------
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
