diff options
| -rw-r--r-- | backends/hol4/Test.sml | 372 |
1 files changed, 339 insertions, 33 deletions
diff --git a/backends/hol4/Test.sml b/backends/hol4/Test.sml index c10d64ce..55915fbc 100644 --- a/backends/hol4/Test.sml +++ b/backends/hol4/Test.sml @@ -27,6 +27,8 @@ val st_ex_bind_def = Define ` | Fail e => Fail e | Loop => Loop`; +val bind_name = fst (dest_const “st_ex_bind”) + val st_ex_return_def = Define ` (st_ex_return : 'a -> 'a M) x = Return x`; @@ -713,25 +715,43 @@ fun thm_to_conj_implies (thm : thm) : thm = val thm = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] thm; in thm end + +(* Like THEN1 and >-, but doesn't fail if the first subgoal is not completely + solved. + + TODO: how to get the notation right? + *) +fun op PARTIAL_THEN1 (tac1: tactic) (tac2: tactic) : tactic = tac1 THEN_LT (NTH_GOAL tac2 1) + (* If the current goal is [asms ⊢ g], and given a lemma of the form [⊢ H ==> C], do the following: - - attempt to prove [asms ⊢ H] using the given tactic - - if it succeeds, call the theorem tactic with the theorem [asms ⊢ C] + - introduce [asms ⊢ H] as a subgoal and apply the given tactic on it + - also calls the theorem tactic with the theorem [asms ⊢ C] If the lemma is not an implication, we directly call the theorem tactic. *) -fun prove_premise_then_apply (prove_hyp: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = +fun intro_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = let val c = concl thm; (* First case: there is a premise to prove *) fun prove_premise_then (h : term) = - SUBGOAL_THEN h (fn h_thm => then_tac (MP thm h_thm)) >- prove_hyp; + PARTIAL_THEN1 (SUBGOAL_THEN h (fn h_thm => then_tac (MP thm h_thm))) premise_tac; (* Second case: no premise to prove *) val no_prove_premise_then = then_tac thm; in if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then end +(* Same as {!intro_premise_then} but fails if the premise_tac fails to prove the premise *) +fun prove_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = + intro_premise_then + (premise_tac >> FAIL_TAC "prove_premise_then: could not prove premise") + then_tac thm + +(* +val thm = th +*) + (* Call a function on all the subterms of a term *) fun dep_apply_in_subterms (f : string Redblackset.set -> term -> unit) @@ -923,7 +943,7 @@ fun apply_dep_rewrites_match_concl_tac val thms = map thm_to_conj_implies thms; in (* Apply each theorem *) - MAP_EVERY (prove_premise_then_apply prove_premise then_tac) thms (asms, g) + MAP_EVERY (prove_premise_then prove_premise then_tac) thms (asms, g) end (* @@ -952,7 +972,7 @@ fun apply_dep_rewrites_match_first_premise_tac let val th = thm_to_conj_implies th; in - prove_premise_then_apply prove_premise then_tac th + prove_premise_then prove_premise then_tac th end; in (* Apply each theorem *) @@ -997,7 +1017,7 @@ fun rewrite_int_conversion_id (* If the conclusion is not already in the assumptions, prove it, use it to rewrite the goal and add it in the assumptions, otherwise do nothing *) if already_in_asms then ALL_TAC - else prove_premise_then_apply prove_premise rewrite_then_assum lemma + else prove_premise_then prove_premise rewrite_then_assum lemma end (* Look for conversions from integers to machine integers and back. @@ -1034,7 +1054,7 @@ apply_dep_rewrites_match_first_premise_tac prove_premise then_tac NUM_SUB_1_EQ sg ‘u32_to_int z = u32_to_int i − 1 /\ 0 ≤ u32_to_int z’ >- prove_premise -prove_premise_then_apply prove_premise +prove_premise_then prove_premise val thm = thm_to_conj_implies (SPECL [“u32_to_int z”, “u32_to_int i”] NUM_SUB_1_EQ) @@ -1048,13 +1068,315 @@ val massage : tactic = assume_bounds_for_all_int_vars >> rewrite_with_dep_int_lemmas +(* Lexicographic order over pairs *) +fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order) + ((p1, p2) : (('a * 'b) * ('a * 'b))) : order = + let + val (x1, y1) = p1; + val (x2, y2) = p2; + in + case comp1 (x1, x2) of + LESS => LESS + | GREATER => GREATER + | EQUAL => comp2 (y1, y2) + end + +(* A constant name (theory, constant name) *) +type const_name = string * string + +val const_name_compare = pair_compare String.compare String.compare + +(* The registered spec theorems, that {!progress} will automatically apply. + + The keys are the function names (it is a pair, because constant names + are made of the theory name and the name of the constant itself). + + Also note that we can store several specs per definition (in practice, when + looking up specs, we will try them all one by one, in a LIFO order). + + We store theorems where all the premises are in the goal, with implications + (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not [H0, ..., Hn ⊢ H]). + + We do this because, when doing proofs by induction, {!progress} might have to + handle *unregistered* theorems coming the current goal assumptions and of the shape + (the conclusion of the theorem is an assumption, and we want to ignore this assumption): + {[ + [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ + case nth ls i of + Return x => ... + | ... => ...] + ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ + case nth ls i of + Return x => ... + | ... => ... + ]} + *) +val reg_spec_thms: (const_name, thm) Redblackmap.dict ref = + ref (Redblackmap.mkDict const_name_compare) + +(* Retrieve the specified application in a spec theorem. + + A spec theorem for a function [f] typically has the shape: + {[ + !x0 ... xn. + H0 ==> ... Hm ==> + (exists ... + (exists ... . f y0 ... yp = ... /\ ...) \/ + (exists ... . f y0 ... yp = ... /\ ...) \/ + ... + ]} + + Or: + {[ + !x0 ... xn. + H0 ==> ... Hm ==> + case f y0 ... yp of + ... => ... + | ... => ... + ]} + + We return: [f y0 ... yp] +*) +fun get_spec_app (t : term) : term = + let + (* Remove the universally quantified variables, the premises and + the existentially quantified variables *) + val t = (snd o strip_exists o snd o strip_imp o snd o strip_forall) t; + (* Remove the exists, take the first disjunct *) + val t = (hd o strip_disj o snd o strip_exists) t; + (* Split the conjunctions and take the first conjunct *) + val t = (hd o strip_conj) t; + (* Remove the case if there is, otherwise destruct the equality *) + val t = + if TypeBase.is_case t then let val (_, t, _) = TypeBase.dest_case t in t end + else (fst o dest_eq) t; + in t end + +(* Given a function call [f y0 ... yn] return the name of the function *) +fun get_fun_name_from_app (t : term) : const_name = + let + val f = (fst o strip_comb) t; + val {Name=name, Thy=thy, Ty=_} = dest_thy_const f; + val cn = (thy, name); + in cn end + +(* Register a spec theorem in the spec database. + + For the shape of spec theorems, see {!get_spec_thm_app}. + *) +fun register_spec_thm (th: thm) : unit = + let + (* Transform the theroem a bit before storing it *) + val th = SPEC_ALL th; + (* Retrieve the app ([f x0 ... xn]) *) + val f = get_spec_app (concl th); + (* Retrieve the function name *) + val cn = get_fun_name_from_app f; + in + (* Store *) + reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th) + end + +(* TODO: I32_SUB_EQ *) +val _ = app register_spec_thm [U32_ADD_EQ, U32_SUB_EQ, I32_ADD_EQ] + +(* +app register_spec_thm [U32_ADD_EQ, U32_SUB_EQ, I32_ADD_EQ] +Redblackmap.listItems (!reg_spec_thms) +*) + +(* +(* TODO: remove? *) +datatype monadic_app_kind = + Call | Bind | Case +*) + +(* Repeatedly destruct cases and return the last scrutinee we get *) +fun strip_all_cases_get_scrutinee (t : term) : term = + if TypeBase.is_case t + then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t + else t + +(* +TypeBase.dest_case “case ls of [] => T | _ => F” +TypeBase.strip_case “case ls of [] => T | _ => F” +TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F” +TypeBase.strip_case “3” +TypeBase.dest_case “3” + +strip_all_cases_get_scrutinee “case ls of [] => T | _ => F” +strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F” +strip_all_cases_get_scrutinee “3” +*) + + +(* Provided the goal contains a call to a monadic function, return this function call. + + The goal should be of the shape: + 1. + {[ + case (* potentially expanded function body *) of + ... => ... + | ... => ... + ]} + + 2. Or: + {[ + exists ... . + ... (* potentially expanded function body *) = Return ... /\ + ... (* Various properties *) + ]} + + 3. Or a disjunction of cases like the one above, below existential binders + (actually: note sure this last case exists in practice): + {[ + exists ... . + (exists ... . (* body *) = Return ... /\ ...) \/ + ... + ]} + + The function body should be of the shape: + {[ + x <- f y0 ... yn; + ... + ]} + + Or (typically if we expanded the monadic binds): + {[ + case f y0 ... yn of + ... + ]} + + Or simply (typically if we reached the end of the function we're analyzing): + {[ + f y0 ... yn + ]} + + For all the above cases we would return [f y0 ... yn]. + *) +fun get_monadic_app_call (t : term) : term = + (* We do something slightly imprecise but hopefully general and robut *) + let + (* Case 3.: strip the existential binders, and take the first disjuntion *) + val t = (hd o strip_disj o snd o strip_exists) t; + (* Case 2.: strip the existential binders, and take the first conjunction *) + val t = (hd o strip_conj o snd o strip_exists) t; + (* If it is an equality, take the lhs *) + val t = if is_eq t then lhs t else t; + (* Expand the binders to transform them to cases *) + val t = + (rhs o concl) (REWRITE_CONV [st_ex_bind_def] t) + handle UNCHANGED => t; + (* Strip all the cases *) + val t = strip_all_cases_get_scrutinee t; + in t end + +(* Use the given theorem to progress by one step (we use this when + analyzing a function body: this goes forward by one call to a monadic function). + + We transform the goal by: + - pushing the theorem premises to a subgoal + - adding the theorem conclusion in the assumptions in another goal, and + getting rid of the monadic call + + Then [then_tac] receives as paramter the monadic call on which we applied + the lemma. This can be useful, for instance, to make a case disjunction. + + This function is the most primitive of the [progress...] functions. + *) +fun pure_progress_with (premise_tac : tactic) + (then_tac : term -> thm_tactic) (th : thm) : tactic = + fn (asms,g) => + let + (* Remove all the universally quantified variables from the theorem *) + val th = SPEC_ALL th; + (* Retrieve the monadic call from the goal *) + val fgoal = get_monadic_app_call g; + (* Retrieve the app call from the theroem *) + val gth = get_spec_app (concl th); + (* Match and instantiate *) + val (var_s, ty_s) = match_term gth fgoal; + (* Instantiate the theorem *) + val th = INST var_s (INST_TYPE ty_s th); + (* Retrieve the premises of the theorem *) + val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th; + in + (* Apply the theorem *) + intro_premise_then premise_tac (then_tac fgoal) th (asms, g) + end + (* -SIMP_CONV arith_ss [ADD] “1 + (x : num)” -SIMP_CONV list_ss [ADD, EL] “EL (Num (1+x)) (t::list_t_v ls)” +val (asms, g) = top_goal () +val t = g + +val th = U32_SUB_EQ + +val premise_tac = massage >> TRY COOPER_TAC +fun then_tac fgoal = + fn thm => ASSUME_TAC thm >> Cases_on ‘^fgoal’ >> + rw [] >> fs [st_ex_bind_def] >> massage >> fs [] + +pure_progress_with premise_tac then_tac th +*) + +fun progress_with (th : thm) : tactic = + let + val premise_tac = massage >> fs [] >> rw [] >> TRY COOPER_TAC; + fun then_tac fgoal thm = + ASSUME_TAC thm >> Cases_on ‘^fgoal’ >> + rw [] >> fs [st_ex_bind_def] >> massage >> fs []; + in + pure_progress_with premise_tac then_tac th + end + +(* +progress_with U32_SUB_EQ +*) + +(* This function lookups the theorem to use to make progress *) +val progress : tactic = + fn (asms, g) => + let + (* Retrieve the monadic call from the goal *) + val fgoal = get_monadic_app_call g; + val fname = get_fun_name_from_app fgoal; + (* Lookup the theorem: first look in the assumptions (we might want to + use the inductive hypothesis for instance) *) + fun asm_to_spec asm = + let + (* Fail if there are no universal quantifiers *) + val _ = + if is_forall asm then asm + else assert is_forall ((snd o strip_imp) asm); + val asm_fname = (get_fun_name_from_app o get_spec_app) asm; + (* Fail if the name is not the one we're looking for *) + val _ = assert (fn n => fname = n) asm_fname; + in + ASSUME asm + end + val asms_thl = mapfilter asm_to_spec asms; + (* Lookup a spec in the database *) + val thl = + case Redblackmap.peek (!reg_spec_thms, fname) of + NONE => asms_thl + | SOME spec => spec :: asms_thl; + val _ = + if null thl then + raise (failwith "progress: could not find a suitable theorem to apply") + else (); + in + (* Attempt to use the theorems one by one *) + MAP_FIRST progress_with thl (asms, g) + end -m “1 + x = SUC x” +(* +val (asms, g) = top_goal () *) +(* TODO: no exfalso tactic?? *) +val EX_FALSO : tactic = + SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[]) + Theorem nth_lem: !(ls : 't list_t) (i : u32). u32_to_int i < int_of_num (LENGTH (list_t_v ls)) ==> @@ -1063,30 +1385,14 @@ Theorem nth_lem: | Fail _ => F | Loop => F Proof - Induct_on ‘ls’ >> fs [list_t_v_def, HD] >~ [‘ListNil’] >> - rpt strip_tac >> massage >> - PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >-(intLib.COOPER_TAC) >> - (* TODO: we need specialized tactics here - first: subgoal *) - sg ‘0 <= u32_to_int i - u32_to_int (int_to_u32 1)’ >-( - massage >> COOPER_TAC - ) >> - (* TODO: automate (should be in a massage) *) - imp_res_tac U32_SUB_EQ >> fs [st_ex_bind_def, list_t_v_def] >> rw [] >> - massage >> fs [] >> rw [] >> - (* TODO: automate this: we should be able to analyze the ‘nth ls z’, - notice there is a quantified assumption in the context, - and instantiate it properly. - - Remark: we can apply the resulting theorem only after rewriting it. - Possibility: - - do some default rewriting and try to apply it - - if it fails, simply add it in the assumptions for the user - *) - pop_last_assum (qspec_then ‘z’ assume_tac) >> rfs [] >> - pop_assum irule >> - COOPER_TAC + Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] + >-(massage >> EX_FALSO >> COOPER_TAC) >> + PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >> + progress >> progress QED +(* *) + (*** * Example of how to get rid of the fuel in practice *) |