1 (* ========================================================================= *)
2 (* Miz3 interface for readable HOL Light tactics formal proofs *)
4 (* (c) Copyright, Bill Richter 2013 *)
5 (* Distributed under the same license as HOL Light *)
7 (* The primary meaning of readability is explained in the HOL Light tutorial *)
8 (* on page 81 after the proof of NSQRT_2 (ported below), *)
9 (* "We would like to claim that this proof can be read in isolation, without *)
10 (* running it in HOL. For each step, every fact we used is clearly labelled *)
11 (* somewhere else in the proof, and every assumption is given explicitly." *)
12 (* However readability is often improved by using tactics constructs like *)
13 (* SIMP_TAC and MATCH_MP_TAC, which allow facts and assumptions to not be *)
14 (* given explicitly, so as to not lose sight of the proof. Readability is *)
15 (* improved by a miz3 interface with few type annotations, back-quotes or *)
16 (* double-quotes, and allowing HOL4/Isabelle math characters, e.g. *)
17 (* ⇒ ⇔ ∧ ∨ ¬ ∀ ∃ ∈ ∉ α β γ λ θ μ ⊂ ∩ ∪ ∅ ━ ≡ ≅ ∡ ∥ ∏ ∘ → ╪ . *)
18 (* We use ideas for readable formal proofs due to John Harrison ("Towards *)
19 (* more readable proofs" of the tutorial and Examples/mizar.ml), Freek *)
20 (* Wiedijk (Mizarlight/miz2a.ml, miz3/miz3.ml and arxiv.org/pdf/1201.3601 *)
21 (* "A Synthesis of Procedural and Declarative Styles of Interactive *)
22 (* Theorem Proving"), Marco Maggesi (author of tactic constructs *)
23 (* INTRO_TAC, DESTRUCT_TAC & HYP), Petros Papapanagiotou (coauthor of *)
24 (* Isabelle Light), Vincent Aravantinos (author of the Q-module *)
25 (* https://github.com/aravantv/HOL-Light-Q) and Mark Adams (author of HOL *)
26 (* Zero and Tactician). These readability ideas yield the miz3-type *)
27 (* declarative constructs assume, consider and case_split. The semantics of *)
28 (* readable.ml is clear from an obvious translation to HOL Light proofs. An *)
29 (* interactive mode is useful in writing, debugging and displaying proofs. *)
31 (* The construct "case_split" reducing the goal to various cases given by *)
32 (* "suppose" clauses. The construct "proof" [...] "qed" allows arbitrarily *)
33 (* long proofs, which can be arbitrarily nested with other case_split and *)
34 (* proof/qed constructs. THENL is only implemented implicitly in case_split *)
35 (* (also eq_tac and conj_tac), and this requires adjustments, such as using *)
36 (* MATCH_MP_TAC num_INDUCTION instead of INDUCT_TAC. *)
37 (* ========================================================================= *)
39 (* The Str library defines regexp functions needed to process strings. *)
43 (* parse_qproof uses system.ml quotexpander feature designed for miz3.ml to *)
44 (* turn backquoted expression `;[...]` into a string with no newline or *)
45 (* backslash problems. Note that miz3.ml defines parse_qproof differently. *)
47 let parse_qproof s = (String.sub s 1 (String.length s - 1));;
49 (* Allows HOL4 and Isabelle style math characters. *)
51 let CleanMathFontsForHOL_Light s =
52 let rec clean s loStringPairs =
53 match loStringPairs with
56 let s = Str.global_replace (Str.regexp (fst hd)) (snd hd) s in
58 clean s ["⇒","==>"; "⇔","<=>"; "∧","/\\ "; "∨","\\/"; "¬","~";
59 "∀","!"; "∃","?"; "∈","IN"; "∉","NOTIN";
60 "α","alpha"; "β","beta"; "γ","gamma"; "λ","\\ "; "θ","theta"; "μ","mu";
61 "⊂","SUBSET"; "∩","INTER"; "∪","UNION"; "∅","{}"; "━","DIFF";
62 "≡","==="; "≅","cong"; "∡","angle"; "∥","parallel";
63 "∏","prod"; "∘","_o_"; "→","--->"; "╪","INSERT"];;
65 (* printReadExn prints uncluttered error messages via Readable_fail. This *)
66 (* is due to Mark Adams, who also explained Roland Zumkeller's exec below. *)
68 exception Readable_fail of string;;
74 | _ -> print_string (Printexc.to_string e);;
76 #install_printer printReadExn;;
78 (* From update_database.ml: Execute any OCaml expression given as a string. *)
80 let exec = ignore o Toploop.execute_phrase false Format.std_formatter
81 o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
83 (* Following miz3.ml, exec_thm returns the theorem representing a string, so *)
84 (* exec_thm "FORALL_PAIR_THM";; returns *)
85 (* val it : thm = |- !P. (!p. P p) <=> (!p1 p2. P (p1,p2)) *)
86 (* Extra error-checking is done to rule out the possibility of the theorem *)
87 (* string ending with a semicolon. *)
89 let thm_ref = ref TRUTH;;
90 let tactic_ref = ref ALL_TAC;;
91 let thmtactic_ref = ref MATCH_MP_TAC;;
92 let thmlist_tactic_ref = ref REWRITE_TAC;;
93 let termlist_thm_thm_ref = ref SPECL;;
94 let thm_thm_ref = ref GSYM;;
95 let term_thm_ref = ref ARITH_RULE;;
96 let thmlist_term_thm_ref = ref MESON;;
99 if Str.string_match (Str.regexp "[^;]*;") s 0 then raise Noparse
101 try exec ("thm_ref := (("^ s ^"): thm);;");
103 with _ -> raise Noparse;;
106 try exec ("tactic_ref := (("^ s ^"): tactic);;"); !tactic_ref
107 with _ -> raise Noparse;;
109 let exec_thmlist_tactic s =
111 exec ("thmlist_tactic_ref := (("^ s ^"): thm list -> tactic);;");
113 with _ -> raise Noparse;;
115 let exec_thmtactic s =
116 try exec ("thmtactic_ref := (("^ s ^"): thm -> tactic);;"); !thmtactic_ref
117 with _ -> raise Noparse;;
119 let exec_termlist_thm_thm s =
120 try exec ("termlist_thm_thm_ref := (("^ s ^"): (term list -> thm -> thm));;");
121 !termlist_thm_thm_ref
122 with _ -> raise Noparse;;
125 try exec ("thm_thm_ref := (("^ s ^"): (thm -> thm));;");
127 with _ -> raise Noparse;;
129 let exec_term_thm s =
130 try exec ("term_thm_ref := (("^ s ^"): (term -> thm));;");
132 with _ -> raise Noparse;;
134 let exec_thmlist_term_thm s =
135 try exec ("thmlist_term_thm_ref := (("^ s ^"): (thm list ->term -> thm));;");
136 !thmlist_term_thm_ref
137 with _ -> raise Noparse;;
139 (* make_env and parse_env_string (following parse_term from parser.ml, *)
140 (* Mizarlight/miz2a.ml and https://github.com/aravantv/HOL-Light-Q) turn a *)
141 (* string into a term with types inferred by the goal and assumption list. *)
143 let (make_env: goal -> (string * pretype) list) =
144 fun (asl, w) -> map ((fun (s, ty) -> (s, pretype_of_type ty)) o dest_var)
145 (freesl (w::(map (concl o snd) asl)));;
147 let parse_env_string env s =
148 let (ptm, l) = (parse_preterm o lex o explode) s in
149 if l = [] then (term_of_preterm o retypecheck env) ptm
150 else raise (Readable_fail
151 ("Unparsed input at the end of the term\n" ^ s));;
153 (* versions of new_constant, parse_as_infix, new_definition and new_axiom *)
155 let NewConstant (x, y) = new_constant(CleanMathFontsForHOL_Light x, y);;
157 let ParseAsInfix (x, y) = parse_as_infix (CleanMathFontsForHOL_Light x, y);;
159 let NewDefinition s =
160 new_definition (parse_env_string [] (CleanMathFontsForHOL_Light s));;
163 new_axiom (parse_env_string [] (CleanMathFontsForHOL_Light s));;
165 (* String versions without type annotations of SUBGOAL_THEN, SUBGOAL_TAC, *)
166 (* intro_TAC, EXISTS_TAC, X_GEN_TAC, and EXISTS_TAC, and also new miz3-type *)
167 (* tactic constructs assume, consider and case_split. *)
169 (* subgoal_THEN stm ttac gl = (SUBGOAL_THEN t ttac) gl, *)
170 (* where stm is a string that turned into a statement t by make_env and *)
171 (* parse_env_string, using the goal gl. We call stm a string statement. *)
172 (* ttac is often the thm_tactic (LABEL_TAC string) or (DESTRUCT_TAC string). *)
174 let subgoal_THEN stm ttac gl =
175 SUBGOAL_THEN (parse_env_string (make_env gl) stm) ttac gl;;
177 (* subgoal_TAC stm lab tac gl = (SUBGOAL_TAC lab t [tac]) gl, *)
178 (* exists_TAC stm gl = (EXISTS_TAC t) gl, and *)
179 (* X_gen_TAC svar gl = (X_GEN_TAC v) gl, where *)
180 (* stm is a string statement which is turned into a statement t by make_env, *)
181 (* parse_env_string and the goal gl. Similarly string svar is turned into a *)
183 (* X_genl_TAC combines X_gen_TAC and GENL. Since below in StepToTactic the *)
184 (* string-term list uses whitespace as the delimiter and no braces, there is *)
185 (* no reason in readable.ml proofs to use X_gen_TAC instead X_genl_TAC. *)
186 (* intro_TAC is INTRO_TAC with the delimiter ";" replaced with",". *)
187 (* eq_tac string tac *)
188 (* requires the goal to be an iff statement of the form x ⇔ y and then *)
189 (* performs an EQ_TAC. If string = "Right", then the tactic tac proves the *)
190 (* implication y ⇒ x, and the goal becomes the other implication x ⇒ y. *)
191 (* If string = "Left", then tac proves x ⇒ y and the goal becomes y ⇒ x. *)
192 (* conj_tac string tac *)
193 (* requires the goal to be a conjunction statement x ∧ y and then performs a *)
194 (* CONJ_TAC. If string = "Left" then the tactic tac proves x, and the goal *)
195 (* becomes y. If string = "Right", tac proves y and the new goal is x. *)
196 (* consider svars stm lab tac *)
197 (* defines new variables given by the string svars = "v1 v2 ... vn" and the *)
198 (* string statement stm, which subgoal_THEN turns into statement t, labeled *)
199 (* by lab. The tactic tac proves the existential statement ?v1 ... vn. t. *)
200 (* case_split sDestruct tac listofDisj listofTac *)
201 (* reduces the goal to n cases which are solved separately. listofDisj is a *)
202 (* list of strings [st_1;...; st_n] whose disjunction st_1 \/...\/ st_n is a *)
203 (* string statement proved by tactic tac. listofTac is a list of tactics *)
204 (* [tac_1;...; tac_n] which prove the statements st_1,..., st_n. The string *)
205 (* sDestruct must have the form "lab_1 |...| lab_n", and lab_i is a label *)
206 (* used by tac_i to prove st_i. Each lab_i must be a nonempty string. *)
208 (* is a version of ASM_CASES_TAC, and performs proofs by contradiction and *)
209 (* binary case_splits where one of the forks has a short proof. In general, *)
210 (* assume statement lab tac *)
211 (* turns the string statement into a term t, with the tactic tac a proof of *)
212 (* ¬t ⇒ w, where w is the goal. There is a new assumption t labeled lab, and *)
213 (* the new goal is the result of applying the tactic SIMP_TAC [t] to w. *)
214 (* It's recommended to only use assume with a short proof tac. Three uses *)
215 (* of assume arise when t = ¬w or t = ¬α, with w = α ∨ β or w = β ∨ α. *)
216 (* In all three cases write *)
217 (* assume statement [lab] by fol; *)
218 (* and the new goal will be F (false) or β respectively, as a result of the *)
219 (* SIMP_TAC [t]. So do not use assume if SIMP_TAC [t] is disadvantageous. *)
221 let subgoal_TAC stm lab tac gl =
222 SUBGOAL_TAC lab (parse_env_string (make_env gl) stm) [tac] gl;;
224 let exists_TAC stm gl =
225 EXISTS_TAC (parse_env_string (make_env gl) stm) gl;;
227 let X_gen_TAC svar (asl, w as gl) =
228 let vartype = (snd o dest_var o fst o dest_forall) w in
229 X_GEN_TAC (mk_var (svar, vartype)) gl;;
231 let X_genl_TAC svarlist = MAP_EVERY X_gen_TAC svarlist;;
233 let intro_TAC s = INTRO_TAC (Str.global_replace (Str.regexp ",") ";" s);;
235 let assume statement lab tac (asl, w as gl) =
236 let t = parse_env_string (make_env gl) statement in
237 (DISJ_CASES_THEN (LABEL_TAC lab) (SPEC t EXCLUDED_MIDDLE) THENL
238 [ALL_TAC; FIRST_ASSUM MP_TAC THEN tac] THEN HYP SIMP_TAC lab []) gl;;
240 let eq_tac string tac =
241 if string = "Right" then CONV_TAC SYM_CONV THEN EQ_TAC THENL [tac; ALL_TAC]
242 else if string = "Left" then EQ_TAC THENL [tac; ALL_TAC]
243 else raise (Readable_fail
244 ("eq_tac requires " ^ string ^" to be either Left or Right"));;
246 let conj_tac string tac =
247 if string = "Right" then ONCE_REWRITE_TAC [CONJ_SYM] THEN
248 CONJ_TAC THENL [tac; ALL_TAC]
249 else if string = "Left" then CONJ_TAC THENL [tac; ALL_TAC]
250 else raise (Readable_fail
251 ("conj_tac requires " ^ string ^" to be either Left or Right"));;
253 let consider svars stm lab tac =
254 subgoal_THEN ("?"^ svars ^ ". "^ stm)
255 (DESTRUCT_TAC ("@"^ svars ^ "."^ lab)) THENL [tac; ALL_TAC];;
257 let case_split sDestruct tac listofDisj listofTac =
258 let disjunction = itlist
259 (fun s t -> if t = "" then "("^ s ^")" else "("^ s ^") \\/ "^ t)
261 subgoal_TAC disjunction "" tac THEN
262 FIRST_X_ASSUM (DESTRUCT_TAC sDestruct) THENL listofTac;;
264 (* Following the HOL Light tutorial section "Towards more readable proofs." *)
266 let fol = MESON_TAC;;
267 let rewrite = REWRITE_TAC;;
268 let simplify = SIMP_TAC;;
270 let rewriteR = GEN_REWRITE_TAC (RAND_CONV);;
271 let rewriteL = GEN_REWRITE_TAC (LAND_CONV);;
272 let rewriteI = GEN_REWRITE_TAC I;;
273 let rewriteRLDepth = GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o DEPTH_CONV);;
274 let TACtoThmTactic tac = fun ths -> MAP_EVERY MP_TAC ths THEN tac;;
275 let arithmetic = TACtoThmTactic ARITH_TAC;;
276 let real_arithmetic = TACtoThmTactic REAL_ARITH_TAC;;
277 let num_ring = TACtoThmTactic (CONV_TAC NUM_RING);;
278 let real_ring = TACtoThmTactic (CONV_TAC REAL_RING);;
280 let ws = "[ \t\n]+";;
281 let ws0 = "[ \t\n]*";;
283 let StringRegexpEqual r s = Str.string_match r s 0 &&
284 s = Str.matched_string s;;
286 (* FindMatch sleft sright s *)
287 (* turns strings sleft and sright into regexps, recursively searches string *)
288 (* s for matched pairs of substrings matching sleft and sright, and returns *)
289 (* the position after the first substring matched by sright which is not *)
290 (* paired with an sleft-matching substring. Often here sleft ends with *)
291 (* whitespace (ws) while sright begins with ws. The "degenerate" case of *)
292 (* X^ws^Y where X^ws matches sleft and ws^Y matches sright is handled by *)
293 (* backing up a character after an sleft match if the last character is ws. *)
295 let FindMatch sleft sright s =
296 let test = Str.regexp ("\("^ sleft ^"\|"^ sright ^"\)")
297 and left = Str.regexp sleft in
298 let rec FindMatchPosition s count =
302 ignore(Str.search_forward test s 0);
303 let TestMatch = Str.matched_group 1 s
304 and AfterTest = Str.match_end() in
305 let LastChar = Str.last_chars (Str.string_before s AfterTest) 1 in
307 if Str.string_match (Str.regexp ws) LastChar 0
308 then AfterTest - 1 else AfterTest in
309 let rest = Str.string_after s endpos
311 if StringRegexpEqual left TestMatch then -1 else 1 in
312 endpos + (FindMatchPosition rest (count + increment))
313 with Not_found -> raise (Readable_fail
314 ("No matching right bracket operator "^ sright ^
315 " to left bracket operator "^ sleft ^" in "^ s)) in
316 FindMatchPosition s 0;;
318 (* FindSemicolon uses FindMatch to find the position before the next *)
319 (* semicolon which is not a delimiter of a list. *)
321 let rec FindSemicolon s =
323 let rec FindMatchPosition s pos =
324 let start = Str.search_forward (Str.regexp ";\|\[") s pos in
325 if Str.matched_string s = ";" then start
327 let rest = Str.string_after s (start + 1) in
328 let MatchingSquareBrace = FindMatch "\[" "\]" rest in
329 let newpos = start + 1 + MatchingSquareBrace in
330 FindMatchPosition s newpos in
331 FindMatchPosition s 0
332 with Not_found -> raise (Readable_fail ("No final semicolon in "^ s));;
334 (* FindCases uses FindMatch to take a string *)
335 (* "suppose" proof_1 "end;" ... "suppose" proof_n "end;" *)
336 (* and return the list [proof_1; proof_2; ... ; proof_n]. *)
338 let rec FindCases s =
339 let sleftCase, srightCase = ws^ "suppose"^ws, ws^ "end" ^ws0^ ";" in
340 if Str.string_match (Str.regexp sleftCase) s 0 then
341 let CaseEndRest = Str.string_after s (Str.match_end()) in
342 let PosAfterEnd = FindMatch sleftCase srightCase CaseEndRest in
343 let pos = Str.search_backward (Str.regexp srightCase)
344 CaseEndRest PosAfterEnd in
345 let case = Str.string_before CaseEndRest pos
346 and rest = Str.string_after CaseEndRest PosAfterEnd in
347 case :: (FindCases rest)
350 (* StringToList uses FindSemicolon to turns a string into the list of *)
351 (* substrings delimited by the semicolons which are not captured in lists. *)
353 let rec StringToList s =
354 if StringRegexpEqual (Str.regexp ws0) s then [] else
355 if Str.string_match (Str.regexp "[^;]*;") s 0 then
356 let pos = FindSemicolon s in
357 let head = Str.string_before s pos in
358 head :: (StringToList (Str.string_after s (pos + 1)))
361 (* ExtractWsStringList string = (["l1"; "l2"; ...; "ln"], rest), *)
362 (* if string = ws ^ "[l1; l2; ...; ln]" ^ rest. Raises Not_found otherwise. *)
364 let ExtractWsStringList string =
365 if Str.string_match (Str.regexp (ws^ "\[")) string 0 then
366 let listRest = Str.string_after string (Str.match_end()) in
367 let RightBrace = FindMatch "\[" "\]" listRest in
368 let rest = Str.string_after listRest RightBrace
369 and list = Str.string_before listRest (RightBrace - 1) in
370 (StringToList list, rest)
371 else raise Not_found;;
373 (* theoremify string goal returns a pair (thm, rest), *)
374 (* where thm is the first theorem found on string, using goal if needed, and *)
375 (* rest is the remainder of string. Theoremify uses 3 helping functions: *)
376 (* 1) CombTermThm_Term, which produces a combination of a term->thm *)
377 (* (e.g. ARITH_RULE) with a term, *)
378 (* 2) CombThmlistTermThm_Thmlist_Term, which combines a thmlist->term->thm *)
379 (* (e.g. MESON) with a thmlist and a term, and *)
380 (* 3) CombTermlistThmThm_Termlist, which combines a termlist->thm->thm *)
381 (* (e.g. SPECL) with a termlist and a thm produced by theoremify. *)
382 (* Similar functions CombThmtactic_Thm and CombThmlisttactic_Thmlist are *)
383 (* used below, along with theoremify, by StringToTactic. *)
385 let CombTermThm_Term word rest gl =
386 let TermThm = exec_term_thm word in
388 let (stermlist, wsRest) = ExtractWsStringList rest in
389 if length stermlist = 1 then
390 let term = (parse_env_string (make_env gl)) (hd stermlist) in
391 (TermThm term, wsRest)
392 else raise (Readable_fail ("term->thm "^ word
393 ^" not followed by length 1 term list, but instead the list \n["^
394 String.concat ";" stermlist ^"]"))
395 with Not_found -> raise (Readable_fail ("term->thm "^ word
396 ^" not followed by term list, but instead \n"^ rest));;
398 let rec theoremify string gl =
399 if Str.string_match (Str.regexp (ws^ "\([^][ \t\n]+\)")) string 0 then
400 let word = Str.matched_group 1 string
401 and rest = Str.string_after string (Str.match_end()) in
402 if word = "-" then (snd (hd (fst gl)), rest) else
403 try (exec_thm word, rest)
405 try (assoc word (fst gl), rest)
407 try firstPairMult (exec_thm_thm word) (theoremify rest gl)
409 try CombTermThm_Term word rest gl
411 try CombThmlistTermThm_Thmlist_Term word rest gl
413 try CombTermlistThmThm_Termlist word rest gl
414 with Noparse -> raise (Readable_fail ("Not a theorem:\n"^ string))
415 else raise (Readable_fail ("Empty theorem:\n"^ string))
417 firstPairMult f (a, b) = (f a, b)
419 CombTermlistThmThm_Termlist word rest gl =
420 let TermlistThmThm = exec_termlist_thm_thm word in
422 let (stermlist, WsThm) = ExtractWsStringList rest in
423 let termlist = map (parse_env_string (make_env gl)) stermlist in
424 firstPairMult (TermlistThmThm termlist) (theoremify WsThm gl)
425 with Not_found -> raise (Readable_fail ("termlist->thm->thm "^ word
426 ^"\n not followed by term list in\n"^ rest))
428 CombThmlistTermThm_Thmlist_Term word rest gl =
429 let thm_create sthm =
430 let (thm, rest) = theoremify (" "^ sthm) gl in
431 if rest = "" then thm
432 else raise (Readable_fail ("an argument of thmlist->term->thm "^ word ^
433 "\n is not a theorem, but instead \n"^ sthm)) in
434 let ThmlistTermThm = exec_thmlist_term_thm word in
436 let (stermlist, wsTermRest) = ExtractWsStringList rest in
437 let thmlist = map thm_create stermlist in
438 if Str.string_match (Str.regexp (ws^ "\[")) wsTermRest 0 then
439 let termRest = Str.string_after wsTermRest (Str.match_end()) in
440 let RightBrace = FindMatch "\[" "\]" termRest in
441 let rest = Str.string_after termRest RightBrace
442 and sterm = Str.string_before termRest (RightBrace - 1) in
443 let term = parse_env_string (make_env gl) sterm in
444 (ThmlistTermThm thmlist term, rest)
445 else raise (Readable_fail ("thmlist->term->thm "^ word
446 ^" followed by list of theorems ["^ String.concat ";" stermlist ^"]
447 not followed by term in\n"^ wsTermRest))
448 with Not_found -> raise (Readable_fail ("thmlist->term->thm "^ word
449 ^" not followed by thm list in\n"^ rest));;
451 let CombThmtactic_Thm step =
452 if Str.string_match (Str.regexp (ws^ "\([a-zA-Z0-9_]+\)")) step 0 then
453 let sthm_tactic = Str.matched_group 1 step
454 and sthm = Str.string_after step (Str.match_end()) in
455 let thm_tactic = exec_thmtactic sthm_tactic in
457 let (thm, rest) = theoremify sthm gl in
458 if rest = "" then thm_tactic thm gl
459 else raise (Readable_fail ("thm_tactic "^ sthm_tactic
460 ^" not followed by a theorem, but instead\n"^ sthm))
461 else raise Not_found;;
463 let CombThmlisttactic_Thmlist step =
464 let rec makeThmListAccum string list gl =
465 if StringRegexpEqual (Str.regexp ws0) string then list else
466 let (thm, rest) = theoremify string gl in
467 makeThmListAccum rest (thm :: list) gl in
468 if Str.string_match (Str.regexp (ws^ "\([a-zA-Z0-9_]+\)")) step 0 then
469 let ttac = exec_thmlist_tactic (Str.matched_group 1 step)
470 and LabThmString = Str.string_after step (Str.match_end()) in
472 let LabThmList = List.rev (makeThmListAccum LabThmString [] gl) in
474 else raise Not_found;;
476 (* StringToTactic uses regexp functions from the Str library to transform a *)
477 (* string into a tactic. The allowable tactics are written in BNF form as *)
479 (* Tactic := ALL_TAC | Tactic THEN Tactic | thm->tactic Thm | *)
480 (* one-word-tactic (e.g. ARITH_TAC) | thmlist->tactic Thm-list | *)
481 (* intro_TAC string | exists_TAC term | X_genl_TAC term-list | *)
482 (* case_split string Tactic statement-list Tactic-list | *)
483 (* consider variable-list statement label Tactic | *)
484 (* eq_tac (Right | Left) Tactic | conj_tac (Right | Left) Tactic | *)
485 (* (assume | subgoal_TAC) statement label Tactic *)
487 (* Thm := theorem-name | label | - [i.e. last assumption] | thm->thm Thm | *)
488 (* term->thm term | thmlist->term->thm Thm-list term | *)
489 (* termlist->thm->thm term-list Thm *)
491 (* The string proofs allowed by StringToTactic are written in BNF form as *)
493 (* Proof := Proof THEN Proof | case_split destruct_string ByProofQed *)
494 (* suppose statement; Proof end; ... suppose statement; Proof end; | *)
495 (* OneStepProof; | consider variable-list statement [label] ByProofQed | *)
496 (* eq_tac [Right|Left] ByProofQed | conj_tac [Right|Left] ByProofQed | *)
497 (* (assume | ) statement [label] ByProofQed *)
499 (* OneStepProof := one-word-tactic | thm->tactic Thm | intro_TAC string | *)
500 (* exists_TAC term-string | X_genl_TAC variable-string-list | *)
501 (* thmlist->tactic Thm-list *)
503 (* ByProofQed := by OneStepProof; | proof Proof Proof ... Proof qed; *)
505 (* theorem is a version of prove based on the miz3.ml thm, with argument *)
506 (* statement ByProofQed *)
508 let rec StringToTactic s =
509 if StringRegexpEqual (Str.regexp ws0) s then ALL_TAC
513 let pos = FindSemicolon s in
514 let step, rest = Str.string_before s pos, Str.string_after s (pos + 1) in
516 let tactic = StepToTactic step in
517 tactic THEN StringToTactic rest
519 let (tactic, rest) = BigStepToTactic s step in
520 tactic THEN StringToTactic rest
523 if ByProof = "by" then
524 let pos = FindSemicolon s in
525 let step, rest = Str.string_before s pos, Str.string_after s (pos + 1) in
526 (StepToTactic step, rest)
528 let pos_after_qed = FindMatch (ws^"proof"^ws) (ws^"qed"^ws0^";") s in
529 let pos = Str.search_backward (Str.regexp "qed") s pos_after_qed in
530 let proof = StringToTactic (Str.string_before s pos) in
531 (proof, Str.string_after s pos_after_qed)
534 if Str.string_match (Str.regexp (ws^ "case_split" ^ws^ "\([^;]+\)" ^ws^
535 "\(by\|proof\)" ^ws)) s 0 then
536 let sDestruct = Str.matched_group 1 s
537 and (proof, rest) = GetProof (Str.matched_group 2 s)
538 (Str.string_after s (Str.group_end 2))
539 and SplitAtSemicolon case =
540 let pos = FindSemicolon case in
541 [Str.string_before case pos; Str.string_after case (pos + 1)] in
542 let list2Case = map SplitAtSemicolon (FindCases rest) in
543 let listofDisj = map hd list2Case
544 and listofTac = map (StringToTactic o hd o tl) list2Case in
545 case_split sDestruct proof listofDisj listofTac
550 if StringRegexpEqual (Str.regexp (ws^ "\([^ \t\n]+\)" ^ws0)) step then
551 exec_tactic (Str.matched_group 1 step)
554 try CombThmtactic_Thm step
556 try CombThmlisttactic_Thmlist step
558 if Str.string_match (Str.regexp (ws^ "intro_TAC" ^ws)) step 0 then
559 let intro_string = Str.string_after step (Str.match_end()) in
560 intro_TAC intro_string
561 else if Str.string_match (Str.regexp (ws^ "exists_TAC" ^ws)) step 0 then
562 let exists_string = Str.string_after step (Str.match_end()) in
563 exists_TAC exists_string
564 else if Str.string_match (Str.regexp (ws^ "X_genl_TAC" ^ws)) step 0 then
565 let genl_string = Str.string_after step (Str.match_end()) in
566 let svarlist = Str.split (Str.regexp ws) genl_string in
570 BigStepToTactic s step =
571 if Str.string_match (Str.regexp (ws^ "consider" ^ws^ "\(\(.\|\n\)+\)" ^ws^
572 "such" ^ws^ "that" ^ws^ "\(\(.\|\n\)+\)" ^ws^ "\[\(\(.\|\n\)*\)\]" ^ws^
573 "\(by\|proof\)" ^ws)) step 0 then
574 let vars, t = Str.matched_group 1 step, Str.matched_group 3 step
575 and lab = Str.matched_group 5 step
576 and KeyWord, endKeyWord = Str.matched_group 7 step, (Str.group_end 7) in
577 let (proof, rest) = GetProof KeyWord (Str.string_after s endKeyWord) in
578 (consider vars t lab proof, rest)
581 let start = Str.search_forward (Str.regexp
582 (ws^ "\[\([^]]*\)\]" ^ws^ "\(by\|proof\)" ^ws)) step 0 in
583 let statement = Str.string_before step start
584 and lab = Str.matched_group 1 step
585 and KeyWord = Str.matched_group 2 step
586 and AfterWord = Str.string_after s (Str.group_end 2) in
587 let (proof, rest) = GetProof KeyWord AfterWord in
588 if StringRegexpEqual (Str.regexp (ws^ "eq_tac")) statement
589 then (eq_tac lab proof, rest)
590 else if StringRegexpEqual (Str.regexp (ws^ "conj_tac")) statement
591 then (conj_tac lab proof, rest)
593 Str.string_match (Str.regexp (ws^ "\(assume\)" ^ws)) statement 0
595 let statement = Str.string_after statement (Str.match_end()) in
596 (assume statement lab proof, rest)
597 else (subgoal_TAC statement lab proof, rest)
598 with Not_found -> raise (Readable_fail
599 ("Can't parse as a Proof:\n"^ step));;
602 let s = CleanMathFontsForHOL_Light s in
604 let start = Str.search_forward (Str.regexp
605 (ws^ "proof\(" ^ws^ "\(.\|\n\)*\)" ^ws ^ "qed" ^ws0^ ";" ^ws0)) s 0 in
606 let thm = Str.string_before s start
607 and proof = Str.matched_group 1 s
608 and rest = Str.string_after s (Str.match_end()) in
609 if rest = "" then prove (parse_env_string [] thm, StringToTactic proof)
610 else raise (Readable_fail
611 ("Trailing garbage after the proof...qed:\n" ^ rest))
614 let start = Str.search_forward (Str.regexp (ws^ "by")) s 0 in
615 let thm = Str.string_before s start
616 and proof = Str.string_after s (Str.match_end()) in
618 prove (parse_env_string [] thm, StepToTactic proof)
619 with Not_found -> raise (Readable_fail ("Not a proof:\n" ^ proof))
620 with Not_found -> raise (Readable_fail
621 ("Missing initial \"proof\", \"by\", or final \"qed;\" in\n" ^ s));;
623 let interactive_goal s =
624 let thm = CleanMathFontsForHOL_Light s in
625 g (parse_env_string [] thm);;
627 let interactive_proof s =
628 let proof = CleanMathFontsForHOL_Light s in
629 e (StringToTactic proof);;
631 (* Two examples illustrating intro_TAC, eq_tac, exists_TAC MP_TAC and SPECL, *)
632 (* then a port of the HOL Light tutorial proof that sqrt 2 is irrational. *)
634 let SKOLEM_THM_GEN = theorem `;
635 ∀P R. (∀x. P x ⇒ ∃y. R x y) ⇔ ∃f. ∀x. P x ⇒ R x (f x)
639 eq_tac [Right] by fol;
641 exists_TAC λx. @y. R x y;
646 let MOD_MOD_REFL = theorem `;
647 ∀m n. ¬(n = 0) ⇒ ((m MOD n) MOD n = m MOD n)
651 MP_TAC SPECL [m; n; 1] MOD_MOD;
652 fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
656 let NSQRT_2 = theorem `;
657 ∀p q. p * p = 2 * q * q ⇒ q = 0
661 intro_TAC ∀p, A, ∀q, B;
662 EVEN(p * p) ⇔ EVEN(2 * q * q) [] by fol B;
663 EVEN(p) [] by fol - EVEN_DOUBLE EVEN_MULT;
664 consider m such that p = 2 * m [C] by fol - EVEN_EXISTS;
665 case_split qp | pq by arithmetic;
667 q * q = 2 * m * m ⇒ m = 0 [] by fol qp A;
671 p * p <= q * q [] by fol - LE_MULT2;
672 q * q = 0 [] by arithmetic - B;
678 (* The following interactive version of the above proof shows a feature of *)
679 (* proof/qed and case_split/suppose. You can evaluate an incomplete proof *)
680 (* of a statement in an interactive_proof and complete the proof afterward, *)
681 (* as indicated below. The "suppose" clauses of a case_split can also be *)
682 (* incomplete. Do not include code below the incomplete proof or case_split *)
683 (* in an interactive_proof body, for the usual THEN vs THENL reason. *)
685 interactive_goal `;∀p q. p * p = 2 * q * q ⇒ q = 0
689 intro_TAC ∀p, A, ∀q, B;
690 EVEN(p * p) ⇔ EVEN(2 * q * q) [] proof qed;
696 EVEN(p) [] by fol - EVEN_DOUBLE EVEN_MULT;
697 consider m such that p = 2 * m [C] proof fol - EVEN_EXISTS; qed;
700 case_split qp | pq by arithmetic;
707 q * q = 2 * m * m ⇒ m = 0 [] by fol qp A;
711 p * p <= q * q [] by fol - LE_MULT2;
712 q * q = 0 [] by arithmetic - B;
715 let NSQRT_2 = top_thm();;
717 (* An port from arith.ml uses by instead of proof...qed; in a short proof: *)
719 let EXP_2 = theorem `;
720 ∀n:num. n EXP 2 = n * n
721 by rewrite BIT0_THM BIT1_THM EXP EXP_ADD MULT_CLAUSES ADD_CLAUSES`;;
723 (* An example using GSYM, ARITH_RULE, MESON and GEN_REWRITE_TAC, reproving *)
724 (* the binomial theorem from sec 13.1--2 of the HOL Light tutorial. *)
727 `(!n. binom(n,0) = 1) /\
728 (!k. binom(0,SUC(k)) = 0) /\
729 (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;
731 let BINOM_LT = theorem `;
732 ∀n k. n < k ⇒ binom(n,k) = 0
735 INDUCT_TAC; INDUCT_TAC;
736 rewrite binom ARITH LT_SUC LT;
737 ASM_SIMP_TAC ARITH_RULE [n < k ==> n < SUC(k)] ARITH;
741 let BINOMIAL_THEOREM = theorem `;
742 ∀n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))
745 ∀f n. nsum (0.. SUC n) f = f(0) + nsum (0..n) (λi. f (SUC i)) [Nsum0SUC] by simplify LE_0 ADD1 NSUM_CLAUSES_LEFT NSUM_OFFSET;
746 MATCH_MP_TAC num_INDUCTION;
747 simplify EXP NSUM_SING_NUMSEG binom SUB_0 MULT_CLAUSES;
749 rewrite Nsum0SUC binom RIGHT_ADD_DISTRIB NSUM_ADD_NUMSEG GSYM NSUM_LMUL ADD_ASSOC;
751 rewriteRLDepth SUB_SUC EXP;
752 rewrite MULT_AC EQ_ADD_LCANCEL MESON [binom] [1 = binom(n, 0)] GSYM Nsum0SUC;
753 simplify NSUM_CLAUSES_RIGHT ARITH_RULE [0 < SUC n ∧ 0 <= SUC n] LT BINOM_LT MULT_CLAUSES ADD_CLAUSES SUC_SUB1;
754 simplify ARITH_RULE [k <= n ⇒ SUC n - k = SUC(n - k)] EXP MULT_AC;