(* ========================================================================= *) (* Miz3 interface for readable HOL Light tactics formal proofs *) (* *) (* (c) Copyright, Bill Richter 2013 *) (* Distributed under the same license as HOL Light *) (* *) (* The primary meaning of readability is explained in the HOL Light tutorial *) (* on page 81 after the proof of NSQRT_2 (ported below), *) (* "We would like to claim that this proof can be read in isolation, without *) (* running it in HOL. For each step, every fact we used is clearly labelled *) (* somewhere else in the proof, and every assumption is given explicitly." *) (* However readability is often improved by using tactics constructs like *) (* SIMP_TAC and MATCH_MP_TAC, which allow facts and assumptions to not be *) (* given explicitly, so as to not lose sight of the proof. Readability is *) (* improved by a miz3 interface with few type annotations, back-quotes or *) (* double-quotes, and allowing HOL4/Isabelle math characters, e.g. *) (* â‡’ â‡” âˆ§ âˆ¨ Â¬ âˆ€ âˆƒ âˆˆ âˆ‰ Î± Î² Î³ Î» Î¸ Î¼ âŠ‚ âˆ© âˆª âˆ… â” â‰¡ â‰… âˆ¡ âˆ¥ âˆ âˆ˜ â†’ â•ª . *) (* We use ideas for readable formal proofs due to John Harrison ("Towards *) (* more readable proofs" of the tutorial and Examples/mizar.ml), Freek *) (* Wiedijk (Mizarlight/miz2a.ml, miz3/miz3.ml and arxiv.org/pdf/1201.3601 *) (* "A Synthesis of Procedural and Declarative Styles of Interactive *) (* Theorem Proving"), Marco Maggesi (author of tactic constructs *) (* INTRO_TAC, DESTRUCT_TAC & HYP), Petros Papapanagiotou (coauthor of *) (* Isabelle Light), Vincent Aravantinos (author of the Q-module *) (* https://github.com/aravantv/HOL-Light-Q) and Mark Adams (author of HOL *) (* Zero and Tactician). These readability ideas yield the miz3-type *) (* declarative constructs assume, consider and case_split. The semantics of *) (* readable.ml is clear from an obvious translation to HOL Light proofs. An *) (* interactive mode is useful in writing, debugging and displaying proofs. *) (* *) (* The construct "case_split" reducing the goal to various cases given by *) (* "suppose" clauses. The construct "proof" [...] "qed" allows arbitrarily *) (* long proofs, which can be arbitrarily nested with other case_split and *) (* proof/qed constructs. THENL is only implemented implicitly in case_split *) (* (also eq_tac and conj_tac), and this requires adjustments, such as using *) (* MATCH_MP_TAC num_INDUCTION instead of INDUCT_TAC. *) (* ========================================================================= *) (* The Str library defines regexp functions needed to process strings. *) #load "str.cma";; (* parse_qproof uses system.ml quotexpander feature designed for miz3.ml to *) (* turn backquoted expression `;[...]` into a string with no newline or *) (* backslash problems. Note that miz3.ml defines parse_qproof differently. *) let parse_qproof s = (String.sub s 1 (String.length s - 1));; (* Allows HOL4 and Isabelle style math characters. *) let CleanMathFontsForHOL_Light s = let rec clean s loStringPairs = match loStringPairs with | [] -> s | hd :: tl -> let s = Str.global_replace (Str.regexp (fst hd)) (snd hd) s in clean s tl in clean s ["â‡’","==>"; "â‡”","<=>"; "âˆ§","/\\ "; "âˆ¨","\\/"; "Â¬","~"; "âˆ€","!"; "âˆƒ","?"; "âˆˆ","IN"; "âˆ‰","NOTIN"; "Î±","alpha"; "Î²","beta"; "Î³","gamma"; "Î»","\\ "; "Î¸","theta"; "Î¼","mu"; "âŠ‚","SUBSET"; "âˆ©","INTER"; "âˆª","UNION"; "âˆ…","{}"; "â”","DIFF"; "â‰¡","==="; "â‰…","cong"; "âˆ¡","angle"; "âˆ¥","parallel"; "âˆ","prod"; "âˆ˜","_o_"; "â†’","--->"; "â•ª","INSERT"];; (* printReadExn prints uncluttered error messages via Readable_fail. This *) (* is due to Mark Adams, who also explained Roland Zumkeller's exec below. *) exception Readable_fail of string;; let printReadExn e = match e with | Readable_fail s -> print_string s | _ -> print_string (Printexc.to_string e);; #install_printer printReadExn;; (* From update_database.ml: Execute any OCaml expression given as a string. *) let exec = ignore o Toploop.execute_phrase false Format.std_formatter o !Toploop.parse_toplevel_phrase o Lexing.from_string;; (* Following miz3.ml, exec_thm returns the theorem representing a string, so *) (* exec_thm "FORALL_PAIR_THM";; returns *) (* val it : thm = |- !P. (!p. P p) <=> (!p1 p2. P (p1,p2)) *) (* Extra error-checking is done to rule out the possibility of the theorem *) (* string ending with a semicolon. *) let thm_ref = ref TRUTH;; let tactic_ref = ref ALL_TAC;; let thmtactic_ref = ref MATCH_MP_TAC;; let thmlist_tactic_ref = ref REWRITE_TAC;; let termlist_thm_thm_ref = ref SPECL;; let thm_thm_ref = ref GSYM;; let term_thm_ref = ref ARITH_RULE;; let thmlist_term_thm_ref = ref MESON;; let exec_thm s = if Str.string_match (Str.regexp "[^;]*;") s 0 then raise Noparse else try exec ("thm_ref := (("^ s ^"): thm);;"); !thm_ref with _ -> raise Noparse;; let exec_tactic s = try exec ("tactic_ref := (("^ s ^"): tactic);;"); !tactic_ref with _ -> raise Noparse;; let exec_thmlist_tactic s = try exec ("thmlist_tactic_ref := (("^ s ^"): thm list -> tactic);;"); !thmlist_tactic_ref with _ -> raise Noparse;; let exec_thmtactic s = try exec ("thmtactic_ref := (("^ s ^"): thm -> tactic);;"); !thmtactic_ref with _ -> raise Noparse;; let exec_termlist_thm_thm s = try exec ("termlist_thm_thm_ref := (("^ s ^"): (term list -> thm -> thm));;"); !termlist_thm_thm_ref with _ -> raise Noparse;; let exec_thm_thm s = try exec ("thm_thm_ref := (("^ s ^"): (thm -> thm));;"); !thm_thm_ref with _ -> raise Noparse;; let exec_term_thm s = try exec ("term_thm_ref := (("^ s ^"): (term -> thm));;"); !term_thm_ref with _ -> raise Noparse;; let exec_thmlist_term_thm s = try exec ("thmlist_term_thm_ref := (("^ s ^"): (thm list ->term -> thm));;"); !thmlist_term_thm_ref with _ -> raise Noparse;; (* make_env and parse_env_string (following parse_term from parser.ml, *) (* Mizarlight/miz2a.ml and https://github.com/aravantv/HOL-Light-Q) turn a *) (* string into a term with types inferred by the goal and assumption list. *) 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 = let (ptm, l) = (parse_preterm o lex o explode) s in if l = [] then (term_of_preterm o retypecheck env) ptm else raise (Readable_fail ("Unparsed input at the end of the term\n" ^ s));; (* versions of new_constant, parse_as_infix, new_definition and new_axiom *) let NewConstant (x, y) = new_constant(CleanMathFontsForHOL_Light x, y);; let ParseAsInfix (x, y) = parse_as_infix (CleanMathFontsForHOL_Light x, y);; let NewDefinition s = new_definition (parse_env_string [] (CleanMathFontsForHOL_Light s));; let NewAxiom s = new_axiom (parse_env_string [] (CleanMathFontsForHOL_Light s));; (* String versions without type annotations of SUBGOAL_THEN, SUBGOAL_TAC, *) (* intro_TAC, EXISTS_TAC, X_GEN_TAC, and EXISTS_TAC, and also new miz3-type *) (* tactic constructs assume, consider and case_split. *) (* subgoal_THEN stm ttac gl = (SUBGOAL_THEN t ttac) gl, *) (* where stm is a string that turned into a statement t by make_env and *) (* parse_env_string, using the goal gl. We call stm a string statement. *) (* ttac is often the thm_tactic (LABEL_TAC string) or (DESTRUCT_TAC string). *) let subgoal_THEN stm ttac gl = SUBGOAL_THEN (parse_env_string (make_env gl) stm) ttac gl;; (* subgoal_TAC stm lab tac gl = (SUBGOAL_TAC lab t [tac]) gl, *) (* exists_TAC stm gl = (EXISTS_TAC t) gl, and *) (* X_gen_TAC svar gl = (X_GEN_TAC v) gl, where *) (* stm is a string statement which is turned into a statement t by make_env, *) (* parse_env_string and the goal gl. Similarly string svar is turned into a *) (* variable v. *) (* X_genl_TAC combines X_gen_TAC and GENL. Since below in StepToTactic the *) (* string-term list uses whitespace as the delimiter and no braces, there is *) (* no reason in readable.ml proofs to use X_gen_TAC instead X_genl_TAC. *) (* intro_TAC is INTRO_TAC with the delimiter ";" replaced with",". *) (* eq_tac string tac *) (* requires the goal to be an iff statement of the form x â‡” y and then *) (* performs an EQ_TAC. If string = "Right", then the tactic tac proves the *) (* implication y â‡’ x, and the goal becomes the other implication x â‡’ y. *) (* If string = "Left", then tac proves x â‡’ y and the goal becomes y â‡’ x. *) (* conj_tac string tac *) (* requires the goal to be a conjunction statement x âˆ§ y and then performs a *) (* CONJ_TAC. If string = "Left" then the tactic tac proves x, and the goal *) (* becomes y. If string = "Right", tac proves y and the new goal is x. *) (* consider svars stm lab tac *) (* defines new variables given by the string svars = "v1 v2 ... vn" and the *) (* string statement stm, which subgoal_THEN turns into statement t, labeled *) (* by lab. The tactic tac proves the existential statement ?v1 ... vn. t. *) (* case_split sDestruct tac listofDisj listofTac *) (* reduces the goal to n cases which are solved separately. listofDisj is a *) (* list of strings [st_1;...; st_n] whose disjunction st_1 \/...\/ st_n is a *) (* string statement proved by tactic tac. listofTac is a list of tactics *) (* [tac_1;...; tac_n] which prove the statements st_1,..., st_n. The string *) (* sDestruct must have the form "lab_1 |...| lab_n", and lab_i is a label *) (* used by tac_i to prove st_i. Each lab_i must be a nonempty string. *) (* assume *) (* is a version of ASM_CASES_TAC, and performs proofs by contradiction and *) (* binary case_splits where one of the forks has a short proof. In general, *) (* assume statement lab tac *) (* turns the string statement into a term t, with the tactic tac a proof of *) (* Â¬t â‡’ w, where w is the goal. There is a new assumption t labeled lab, and *) (* the new goal is the result of applying the tactic SIMP_TAC [t] to w. *) (* It's recommended to only use assume with a short proof tac. Three uses *) (* of assume arise when t = Â¬w or t = Â¬Î±, with w = Î± âˆ¨ Î² or w = Î² âˆ¨ Î±. *) (* In all three cases write *) (* assume statement [lab] by fol; *) (* and the new goal will be F (false) or Î² respectively, as a result of the *) (* SIMP_TAC [t]. So do not use assume if SIMP_TAC [t] is disadvantageous. *) let subgoal_TAC stm lab tac gl = SUBGOAL_TAC lab (parse_env_string (make_env gl) stm) [tac] gl;; let exists_TAC stm gl = EXISTS_TAC (parse_env_string (make_env gl) stm) gl;; let X_gen_TAC svar (asl, w as gl) = let vartype = (snd o dest_var o fst o dest_forall) w in X_GEN_TAC (mk_var (svar, vartype)) gl;; let X_genl_TAC svarlist = MAP_EVERY X_gen_TAC svarlist;; let intro_TAC s = INTRO_TAC (Str.global_replace (Str.regexp ",") ";" s);; let assume statement lab tac (asl, w as gl) = let t = parse_env_string (make_env gl) statement in (DISJ_CASES_THEN (LABEL_TAC lab) (SPEC t EXCLUDED_MIDDLE) THENL [ALL_TAC; FIRST_ASSUM MP_TAC THEN tac] THEN HYP SIMP_TAC lab []) gl;; let eq_tac string tac = if string = "Right" then CONV_TAC SYM_CONV THEN EQ_TAC THENL [tac; ALL_TAC] else if string = "Left" then EQ_TAC THENL [tac; ALL_TAC] else raise (Readable_fail ("eq_tac requires " ^ string ^" to be either Left or Right"));; let conj_tac string tac = if string = "Right" then ONCE_REWRITE_TAC [CONJ_SYM] THEN CONJ_TAC THENL [tac; ALL_TAC] else if string = "Left" then CONJ_TAC THENL [tac; ALL_TAC] else raise (Readable_fail ("conj_tac requires " ^ string ^" to be either Left or Right"));; let consider svars stm lab tac = subgoal_THEN ("?"^ svars ^ ". "^ stm) (DESTRUCT_TAC ("@"^ svars ^ "."^ lab)) THENL [tac; ALL_TAC];; let case_split sDestruct tac listofDisj listofTac = let disjunction = itlist (fun s t -> if t = "" then "("^ s ^")" else "("^ s ^") \\/ "^ t) listofDisj "" in subgoal_TAC disjunction "" tac THEN FIRST_X_ASSUM (DESTRUCT_TAC sDestruct) THENL listofTac;; (* Following the HOL Light tutorial section "Towards more readable proofs." *) let fol = MESON_TAC;; let rewrite = REWRITE_TAC;; let simplify = SIMP_TAC;; let set = SET_TAC;; let rewriteR = GEN_REWRITE_TAC (RAND_CONV);; let rewriteL = GEN_REWRITE_TAC (LAND_CONV);; let rewriteI = GEN_REWRITE_TAC I;; let rewriteRLDepth = GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o DEPTH_CONV);; let TACtoThmTactic tac = fun ths -> MAP_EVERY MP_TAC ths THEN tac;; let arithmetic = TACtoThmTactic ARITH_TAC;; let real_arithmetic = TACtoThmTactic REAL_ARITH_TAC;; let num_ring = TACtoThmTactic (CONV_TAC NUM_RING);; let real_ring = TACtoThmTactic (CONV_TAC REAL_RING);; let ws = "[ \t\n]+";; let ws0 = "[ \t\n]*";; let StringRegexpEqual r s = Str.string_match r s 0 && s = Str.matched_string s;; (* FindMatch sleft sright s *) (* turns strings sleft and sright into regexps, recursively searches string *) (* s for matched pairs of substrings matching sleft and sright, and returns *) (* the position after the first substring matched by sright which is not *) (* paired with an sleft-matching substring. Often here sleft ends with *) (* whitespace (ws) while sright begins with ws. The "degenerate" case of *) (* X^ws^Y where X^ws matches sleft and ws^Y matches sright is handled by *) (* backing up a character after an sleft match if the last character is ws. *) let FindMatch sleft sright s = let test = Str.regexp ("\("^ sleft ^"\|"^ sright ^"\)") and left = Str.regexp sleft in let rec FindMatchPosition s count = if count = 1 then 0 else try ignore(Str.search_forward test s 0); let TestMatch = Str.matched_group 1 s and AfterTest = Str.match_end() in let LastChar = Str.last_chars (Str.string_before s AfterTest) 1 in let endpos = if Str.string_match (Str.regexp ws) LastChar 0 then AfterTest - 1 else AfterTest in let rest = Str.string_after s endpos and increment = if StringRegexpEqual left TestMatch then -1 else 1 in endpos + (FindMatchPosition rest (count + increment)) with Not_found -> raise (Readable_fail ("No matching right bracket operator "^ sright ^ " to left bracket operator "^ sleft ^" in "^ s)) in FindMatchPosition s 0;; (* FindSemicolon uses FindMatch to find the position before the next *) (* semicolon which is not a delimiter of a list. *) let rec FindSemicolon s = try let rec FindMatchPosition s pos = let start = Str.search_forward (Str.regexp ";\|\[") s pos in if Str.matched_string s = ";" then start else let rest = Str.string_after s (start + 1) in let MatchingSquareBrace = FindMatch "\[" "\]" rest in let newpos = start + 1 + MatchingSquareBrace in FindMatchPosition s newpos in FindMatchPosition s 0 with Not_found -> raise (Readable_fail ("No final semicolon in "^ s));; (* FindCases uses FindMatch to take a string *) (* "suppose" proof_1 "end;" ... "suppose" proof_n "end;" *) (* and return the list [proof_1; proof_2; ... ; proof_n]. *) let rec FindCases s = let sleftCase, srightCase = ws^ "suppose"^ws, ws^ "end" ^ws0^ ";" in if Str.string_match (Str.regexp sleftCase) s 0 then let CaseEndRest = Str.string_after s (Str.match_end()) in let PosAfterEnd = FindMatch sleftCase srightCase CaseEndRest in let pos = Str.search_backward (Str.regexp srightCase) CaseEndRest PosAfterEnd in let case = Str.string_before CaseEndRest pos and rest = Str.string_after CaseEndRest PosAfterEnd in case :: (FindCases rest) else [];; (* StringToList uses FindSemicolon to turns a string into the list of *) (* substrings delimited by the semicolons which are not captured in lists. *) let rec StringToList s = if StringRegexpEqual (Str.regexp ws0) s then [] else if Str.string_match (Str.regexp "[^;]*;") s 0 then let pos = FindSemicolon s in let head = Str.string_before s pos in head :: (StringToList (Str.string_after s (pos + 1))) else [s];; (* ExtractWsStringList string = (["l1"; "l2"; ...; "ln"], rest), *) (* if string = ws ^ "[l1; l2; ...; ln]" ^ rest. Raises Not_found otherwise. *) let ExtractWsStringList string = if Str.string_match (Str.regexp (ws^ "\[")) string 0 then let listRest = Str.string_after string (Str.match_end()) in let RightBrace = FindMatch "\[" "\]" listRest in let rest = Str.string_after listRest RightBrace and list = Str.string_before listRest (RightBrace - 1) in (StringToList list, rest) else raise Not_found;; (* theoremify string goal returns a pair (thm, rest), *) (* where thm is the first theorem found on string, using goal if needed, and *) (* rest is the remainder of string. Theoremify uses 3 helping functions: *) (* 1) CombTermThm_Term, which produces a combination of a term->thm *) (* (e.g. ARITH_RULE) with a term, *) (* 2) CombThmlistTermThm_Thmlist_Term, which combines a thmlist->term->thm *) (* (e.g. MESON) with a thmlist and a term, and *) (* 3) CombTermlistThmThm_Termlist, which combines a termlist->thm->thm *) (* (e.g. SPECL) with a termlist and a thm produced by theoremify. *) (* Similar functions CombThmtactic_Thm and CombThmlisttactic_Thmlist are *) (* used below, along with theoremify, by StringToTactic. *) let CombTermThm_Term word rest gl = let TermThm = exec_term_thm word in try let (stermlist, wsRest) = ExtractWsStringList rest in if length stermlist = 1 then let term = (parse_env_string (make_env gl)) (hd stermlist) in (TermThm term, wsRest) else raise (Readable_fail ("term->thm "^ word ^" not followed by length 1 term list, but instead the list \n["^ String.concat ";" stermlist ^"]")) with Not_found -> raise (Readable_fail ("term->thm "^ word ^" not followed by term list, but instead \n"^ rest));; let rec theoremify string gl = if Str.string_match (Str.regexp (ws^ "\([^][ \t\n]+\)")) string 0 then let word = Str.matched_group 1 string and rest = Str.string_after string (Str.match_end()) in if word = "-" then (snd (hd (fst gl)), rest) else try (exec_thm word, rest) with _ -> try (assoc word (fst gl), rest) with _ -> try firstPairMult (exec_thm_thm word) (theoremify rest gl) with _ -> try CombTermThm_Term word rest gl with Noparse -> try CombThmlistTermThm_Thmlist_Term word rest gl with Noparse -> try CombTermlistThmThm_Termlist word rest gl with Noparse -> raise (Readable_fail ("Not a theorem:\n"^ string)) else raise (Readable_fail ("Empty theorem:\n"^ string)) and firstPairMult f (a, b) = (f a, b) and CombTermlistThmThm_Termlist word rest gl = let TermlistThmThm = exec_termlist_thm_thm word in try let (stermlist, WsThm) = ExtractWsStringList rest in let termlist = map (parse_env_string (make_env gl)) stermlist in firstPairMult (TermlistThmThm termlist) (theoremify WsThm gl) with Not_found -> raise (Readable_fail ("termlist->thm->thm "^ word ^"\n not followed by term list in\n"^ rest)) and CombThmlistTermThm_Thmlist_Term word rest gl = let thm_create sthm = let (thm, rest) = theoremify (" "^ sthm) gl in if rest = "" then thm else raise (Readable_fail ("an argument of thmlist->term->thm "^ word ^ "\n is not a theorem, but instead \n"^ sthm)) in let ThmlistTermThm = exec_thmlist_term_thm word in try let (stermlist, wsTermRest) = ExtractWsStringList rest in let thmlist = map thm_create stermlist in if Str.string_match (Str.regexp (ws^ "\[")) wsTermRest 0 then let termRest = Str.string_after wsTermRest (Str.match_end()) in let RightBrace = FindMatch "\[" "\]" termRest in let rest = Str.string_after termRest RightBrace and sterm = Str.string_before termRest (RightBrace - 1) in let term = parse_env_string (make_env gl) sterm in (ThmlistTermThm thmlist term, rest) else raise (Readable_fail ("thmlist->term->thm "^ word ^" followed by list of theorems ["^ String.concat ";" stermlist ^"] not followed by term in\n"^ wsTermRest)) with Not_found -> raise (Readable_fail ("thmlist->term->thm "^ word ^" not followed by thm list in\n"^ rest));; let CombThmtactic_Thm step = if Str.string_match (Str.regexp (ws^ "\([a-zA-Z0-9_]+\)")) step 0 then let sthm_tactic = Str.matched_group 1 step and sthm = Str.string_after step (Str.match_end()) in let thm_tactic = exec_thmtactic sthm_tactic in fun gl -> let (thm, rest) = theoremify sthm gl in if rest = "" then thm_tactic thm gl else raise (Readable_fail ("thm_tactic "^ sthm_tactic ^" not followed by a theorem, but instead\n"^ sthm)) else raise Not_found;; let CombThmlisttactic_Thmlist step = let rec makeThmListAccum string list gl = if StringRegexpEqual (Str.regexp ws0) string then list else let (thm, rest) = theoremify string gl in makeThmListAccum rest (thm :: list) gl in if Str.string_match (Str.regexp (ws^ "\([a-zA-Z0-9_]+\)")) step 0 then let ttac = exec_thmlist_tactic (Str.matched_group 1 step) and LabThmString = Str.string_after step (Str.match_end()) in fun gl -> let LabThmList = List.rev (makeThmListAccum LabThmString [] gl) in ttac LabThmList gl else raise Not_found;; (* StringToTactic uses regexp functions from the Str library to transform a *) (* string into a tactic. The allowable tactics are written in BNF form as *) (* *) (* Tactic := ALL_TAC | Tactic THEN Tactic | thm->tactic Thm | *) (* one-word-tactic (e.g. ARITH_TAC) | thmlist->tactic Thm-list | *) (* intro_TAC string | exists_TAC term | X_genl_TAC term-list | *) (* case_split string Tactic statement-list Tactic-list | *) (* consider variable-list statement label Tactic | *) (* eq_tac (Right | Left) Tactic | conj_tac (Right | Left) Tactic | *) (* (assume | subgoal_TAC) statement label Tactic *) (* *) (* Thm := theorem-name | label | - [i.e. last assumption] | thm->thm Thm | *) (* term->thm term | thmlist->term->thm Thm-list term | *) (* termlist->thm->thm term-list Thm *) (* *) (* The string proofs allowed by StringToTactic are written in BNF form as *) (* *) (* Proof := Proof THEN Proof | case_split destruct_string ByProofQed *) (* suppose statement; Proof end; ... suppose statement; Proof end; | *) (* OneStepProof; | consider variable-list statement [label] ByProofQed | *) (* eq_tac [Right|Left] ByProofQed | conj_tac [Right|Left] ByProofQed | *) (* (assume | ) statement [label] ByProofQed *) (* *) (* OneStepProof := one-word-tactic | thm->tactic Thm | intro_TAC string | *) (* exists_TAC term-string | X_genl_TAC variable-string-list | *) (* thmlist->tactic Thm-list *) (* *) (* ByProofQed := by OneStepProof; | proof Proof Proof ... Proof qed; *) (* *) (* theorem is a version of prove based on the miz3.ml thm, with argument *) (* statement ByProofQed *) let rec StringToTactic s = if StringRegexpEqual (Str.regexp ws0) s then ALL_TAC else try makeCaseSplit s with _ -> let pos = FindSemicolon s in let step, rest = Str.string_before s pos, Str.string_after s (pos + 1) in try let tactic = StepToTactic step in tactic THEN StringToTactic rest with Not_found -> let (tactic, rest) = BigStepToTactic s step in tactic THEN StringToTactic rest and GetProof ByProof s = if ByProof = "by" then let pos = FindSemicolon s in let step, rest = Str.string_before s pos, Str.string_after s (pos + 1) in (StepToTactic step, rest) else let pos_after_qed = FindMatch (ws^"proof"^ws) (ws^"qed"^ws0^";") s in let pos = Str.search_backward (Str.regexp "qed") s pos_after_qed in let proof = StringToTactic (Str.string_before s pos) in (proof, Str.string_after s pos_after_qed) and makeCaseSplit s = if Str.string_match (Str.regexp (ws^ "case_split" ^ws^ "\([^;]+\)" ^ws^ "\(by\|proof\)" ^ws)) s 0 then let sDestruct = Str.matched_group 1 s and (proof, rest) = GetProof (Str.matched_group 2 s) (Str.string_after s (Str.group_end 2)) and SplitAtSemicolon case = let pos = FindSemicolon case in [Str.string_before case pos; Str.string_after case (pos + 1)] in let list2Case = map SplitAtSemicolon (FindCases rest) in let listofDisj = map hd list2Case and listofTac = map (StringToTactic o hd o tl) list2Case in case_split sDestruct proof listofDisj listofTac else raise Not_found and StepToTactic step = try if StringRegexpEqual (Str.regexp (ws^ "\([^ \t\n]+\)" ^ws0)) step then exec_tactic (Str.matched_group 1 step) else raise Not_found with _ -> try CombThmtactic_Thm step with _ -> try CombThmlisttactic_Thmlist step with _ -> if Str.string_match (Str.regexp (ws^ "intro_TAC" ^ws)) step 0 then let intro_string = Str.string_after step (Str.match_end()) in intro_TAC intro_string else if Str.string_match (Str.regexp (ws^ "exists_TAC" ^ws)) step 0 then let exists_string = Str.string_after step (Str.match_end()) in exists_TAC exists_string else if Str.string_match (Str.regexp (ws^ "X_genl_TAC" ^ws)) step 0 then let genl_string = Str.string_after step (Str.match_end()) in let svarlist = Str.split (Str.regexp ws) genl_string in X_genl_TAC svarlist else raise Not_found and BigStepToTactic s step = if Str.string_match (Str.regexp (ws^ "consider" ^ws^ "\(\(.\|\n\)+\)" ^ws^ "such" ^ws^ "that" ^ws^ "\(\(.\|\n\)+\)" ^ws^ "\[\(\(.\|\n\)*\)\]" ^ws^ "\(by\|proof\)" ^ws)) step 0 then let vars, t = Str.matched_group 1 step, Str.matched_group 3 step and lab = Str.matched_group 5 step and KeyWord, endKeyWord = Str.matched_group 7 step, (Str.group_end 7) in let (proof, rest) = GetProof KeyWord (Str.string_after s endKeyWord) in (consider vars t lab proof, rest) else try let start = Str.search_forward (Str.regexp (ws^ "\[\([^]]*\)\]" ^ws^ "\(by\|proof\)" ^ws)) step 0 in let statement = Str.string_before step start and lab = Str.matched_group 1 step and KeyWord = Str.matched_group 2 step and AfterWord = Str.string_after s (Str.group_end 2) in let (proof, rest) = GetProof KeyWord AfterWord in if StringRegexpEqual (Str.regexp (ws^ "eq_tac")) statement then (eq_tac lab proof, rest) else if StringRegexpEqual (Str.regexp (ws^ "conj_tac")) statement then (conj_tac lab proof, rest) else if Str.string_match (Str.regexp (ws^ "\(assume\)" ^ws)) statement 0 then let statement = Str.string_after statement (Str.match_end()) in (assume statement lab proof, rest) else (subgoal_TAC statement lab proof, rest) with Not_found -> raise (Readable_fail ("Can't parse as a Proof:\n"^ step));; let theorem s = let s = CleanMathFontsForHOL_Light s in try let start = Str.search_forward (Str.regexp (ws^ "proof\(" ^ws^ "\(.\|\n\)*\)" ^ws ^ "qed" ^ws0^ ";" ^ws0)) s 0 in let thm = Str.string_before s start and proof = Str.matched_group 1 s and rest = Str.string_after s (Str.match_end()) in if rest = "" then prove (parse_env_string [] thm, StringToTactic proof) else raise (Readable_fail ("Trailing garbage after the proof...qed:\n" ^ rest)) with Not_found -> try let start = Str.search_forward (Str.regexp (ws^ "by")) s 0 in let thm = Str.string_before s start and proof = Str.string_after s (Str.match_end()) in try prove (parse_env_string [] thm, StepToTactic proof) with Not_found -> raise (Readable_fail ("Not a proof:\n" ^ proof)) with Not_found -> raise (Readable_fail ("Missing initial \"proof\", \"by\", or final \"qed;\" in\n" ^ s));; let interactive_goal s = let thm = CleanMathFontsForHOL_Light s in g (parse_env_string [] thm);; let interactive_proof s = let proof = CleanMathFontsForHOL_Light s in e (StringToTactic proof);; (* Two examples illustrating intro_TAC, eq_tac, exists_TAC MP_TAC and SPECL, *) (* then a port of the HOL Light tutorial proof that sqrt 2 is irrational. *) let SKOLEM_THM_GEN = theorem `; âˆ€P R. (âˆ€x. P x â‡’ âˆƒy. R x y) â‡” âˆƒf. âˆ€x. P x â‡’ R x (f x) proof intro_TAC âˆ€P R; eq_tac [Right] by fol; intro_TAC H1; exists_TAC Î»x. @y. R x y; fol H1; qed; `;; let MOD_MOD_REFL = theorem `; âˆ€m n. Â¬(n = 0) â‡’ ((m MOD n) MOD n = m MOD n) proof intro_TAC !m n, H1; MP_TAC SPECL [m; n; 1] MOD_MOD; fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC; qed; `;; 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 - EVEN_DOUBLE 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 - B C; end; suppose p <= q; p * p <= q * q [] by fol - LE_MULT2; q * q = 0 [] by arithmetic - B; num_ring -; end; qed; `;; (* The following interactive version of the above proof shows a feature of *) (* proof/qed and case_split/suppose. You can evaluate an incomplete proof *) (* of a statement in an interactive_proof and complete the proof afterward, *) (* as indicated below. The "suppose" clauses of a case_split can also be *) (* incomplete. Do not include code below the incomplete proof or case_split *) (* in an interactive_proof body, for the usual THEN vs THENL reason. *) 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) [] proof qed; `;; interactive_proof `; fol B; `;; interactive_proof `; EVEN(p) [] by fol - EVEN_DOUBLE EVEN_MULT; consider m such that p = 2 * m [C] proof fol - EVEN_EXISTS; qed; `;; interactive_proof `; case_split qp | pq by arithmetic; suppose q < p; end; suppose p <= q; end; `;; interactive_proof `; q * q = 2 * m * m â‡’ m = 0 [] by fol qp A; num_ring - B C; `;; interactive_proof `; p * p <= q * q [] by fol - LE_MULT2; q * q = 0 [] by arithmetic - B; num_ring -; `;; let NSQRT_2 = top_thm();; (* An port from arith.ml uses by instead of proof...qed; in a short proof: *) let EXP_2 = theorem `; âˆ€n:num. n EXP 2 = n * n by rewrite BIT0_THM BIT1_THM EXP EXP_ADD MULT_CLAUSES ADD_CLAUSES`;; (* An example using GSYM, ARITH_RULE, MESON and GEN_REWRITE_TAC, reproving *) (* the binomial theorem from sec 13.1--2 of the HOL Light tutorial. *)let BINOM_LT = theorem `; âˆ€n k. n < k â‡’ binom(n,k) = 0 proof INDUCT_TAC; INDUCT_TAC; rewrite binom ARITH LT_SUC LT; ASM_SIMP_TAC ARITH_RULE [n < k ==> n < SUC(k)] ARITH; qed; `;; let BINOMIAL_THEOREM = theorem `; âˆ€n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k)) proof âˆ€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; MATCH_MP_TAC num_INDUCTION; simplify EXP NSUM_SING_NUMSEG binom SUB_0 MULT_CLAUSES; intro_TAC âˆ€n, nThm; rewrite Nsum0SUC binom RIGHT_ADD_DISTRIB NSUM_ADD_NUMSEG GSYM NSUM_LMUL ADD_ASSOC; rewriteR ADD_SYM; rewriteRLDepth SUB_SUC EXP; rewrite MULT_AC EQ_ADD_LCANCEL MESON [binom] [1 = binom(n, 0)] GSYM Nsum0SUC; simplify NSUM_CLAUSES_RIGHT ARITH_RULE [0 < SUC n âˆ§ 0 <= SUC n] LT BINOM_LT MULT_CLAUSES ADD_CLAUSES SUC_SUB1; simplify ARITH_RULE [k <= n â‡’ SUC n - k = SUC(n - k)] EXP MULT_AC; qed; `;;let binom = define `(!n. binom(n,0) = 1) /\ (!k. binom(0,SUC(k)) = 0) /\ (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;