diff options
| -rw-r--r-- | backends/hol4/Test.sml | 374 |
1 files changed, 347 insertions, 27 deletions
diff --git a/backends/hol4/Test.sml b/backends/hol4/Test.sml index 04bc3ec3..a01211d0 100644 --- a/backends/hol4/Test.sml +++ b/backends/hol4/Test.sml @@ -448,6 +448,7 @@ QED (* Add a list of theorems in the assumptions - TODO: move *) fun ASSUME_TACL (thms : thm list) : tactic = let + (* TODO: use MAP_EVERY *) fun t thms = case thms of [] => ALL_TAC @@ -456,6 +457,12 @@ fun ASSUME_TACL (thms : thm list) : tactic = t thms end +(* Drop/forget a theorem. + + To be used in conjunction with {!pop_assum} for instance. + *) +fun DROP_TAC (_ : thm) : tactic = ALL_TAC + (* The map from integer type to bounds lemmas *) val integer_bounds_lemmas = Redblackmap.fromList String.compare @@ -464,18 +471,81 @@ val integer_bounds_lemmas = ("i32", i32_to_int_bounds) ] +(* The map from integer type to conversion lemmas *) +val integer_conversion_lemmas = + Redblackmap.fromList String.compare + [ + ("u32", int_to_u32_id), + ("i32", int_to_i32_id) + ] + +val integer_conversion_lemmas_list = + map snd (Redblackmap.listItems integer_conversion_lemmas) + +(* Not sure how term nets work, nor how we are supposed to convert Term.term + to mlibTerm.term. + + TODO: it seems we need to explore the term and convert everything to strings. + *) +fun term_to_mlib_term (t : term) : mlibTerm.term = + mlibTerm.string_to_term (term_to_string t) + +(* +(* The lhs of the conclusion of the integer conversion lemmas - we use this for + pattern matching *) +val integer_conversion_lhs_concls = + let + val thms = map snd (Redblackmap.listItems integer_conversion_lemmas); + val concls = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms; + in concls end +*) + +(* +val integer_conversion_concls_net = + let + val maplets = map (fn x => fst (dest_eq x) |-> ()) integer_conversion_concls; + + val maplets = map (fn x => fst (mlibTerm.dest_eq x) |-> ()) integer_conversion_concls; + val maplets = map (fn x => fst (mlibThm.dest_unit_eq x) |-> ()) integer_conversion_concls; + val parameters = { fifo=false }; + in mlibTermnet.from_maplets parameters maplets end + +mlibTerm.string_to_term (term_to_string “u32_to_int (int_to_u32 n) = n”) +term_to_quote + +SIMP_CONV +mlibThm.dest_thm u32_to_int_bounds +mlibThm.dest_unit u32_to_int_bounds +*) + (* The integer types *) val integer_types_names = Redblackset.fromList String.compare (map fst (Redblackmap.listItems integer_bounds_lemmas)) +val all_integer_bounds = [ + u32_max_def, + i32_min_def, + i32_max_def +] + +(* Small utility: compute the set of assumptions in the context. + + We isolate this code in a utility in order to be able to improve it: + for now we simply put all the assumptions in a set, but in the future + we might want to split the assumptions which are conjunctions in order + to be more precise. + *) +fun compute_asms_set ((asms,g) : goal) : term Redblackset.set = + Redblackset.fromList Term.compare asms + (* See {!assume_bounds_for_all_int_vars}. This tactic is in charge of adding assumptions for one variable. *) fun assume_bounds_for_int_var - (asms: term Redblackset.set) (var : string) (ty : string) : + (asms_set: term Redblackset.set) (var : string) (ty : string) : tactic = let (* Lookup the lemma to apply *) @@ -495,12 +565,43 @@ fun assume_bounds_for_int_var (* Filter the conjuncts: some of them might already be in the context, we don't want to introduce them again, as it would pollute it. *) - val lemmas = filter (fn lem => not (Redblackset.member (asms, concl lem))) lemmas; + val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas; in (* Introduce the assumptions in the context *) ASSUME_TACL lemmas end +(* Destruct if possible a term of the shape: [x y], + where [x] is not a comb. + + Returns [(x, y)] + *) +fun dest_single_comb (t : term) : (term * term) option = + case strip_comb t of + (x, [y]) => SOME (x, y) + | _ => NONE + +(** Destruct if possible a term of the shape: [x (y z)]. + Returns [(x, y, z)] + *) +fun dest_single_comb_twice (t : term) : (term * term * term) option = + case dest_single_comb t of + NONE => NONE + | SOME (x, y) => + case dest_single_comb y of + NONE => NONE + | SOME (y, z) => SOME (x, y, z) + +(* A utility map to lookup integer conversion lemmas *) +val integer_conversion_pat_map = + let + val thms = map snd (Redblackmap.listItems integer_conversion_lemmas); + val tl = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms; + val tl = map (valOf o dest_single_comb_twice) tl; + val tl = map (fn (x, y, _) => (x, y)) tl; + val m = Redblackmap.fromList Term.compare tl + in m end + (* Introduce bound assumptions for all the machine integers in the context. Exemple: @@ -516,7 +617,7 @@ fun assume_bounds_for_all_int_vars (asms, g) = (* Compute the set of integer variables in the context *) val vars = free_varsl (g :: asms); (* Compute the set of assumptions already present in the context *) - val asms_set = Redblackset.fromList Term.compare vars; + val asms_set = compute_asms_set (asms, g); (* Filter the variables to keep only the ones with type machine integer, decompose the types at the same time *) fun decompose_var (v : term) : (string * string) = @@ -532,6 +633,7 @@ fun assume_bounds_for_all_int_vars (asms, g) = fun add_var_asm (v, ty) : tactic = assume_bounds_for_int_var asms_set v ty; (* Add assumptions for all the variables *) + (* TODO: use MAP_EVERY *) fun add_vars_asm vl : tactic = case vl of [] => ALL_TAC @@ -555,9 +657,232 @@ fun bounds_for_ints_in_list (vars : (string * hol_type) list) : tactic = FAIL_TAC "" val var = "x" val ty = "u32" + +val asms_set = Redblackset.fromList Term.compare asms; + +val x = “1: int” +val ty = "u32" + +val thm = lemma *) -val massage : tactic = assume_bounds_for_all_int_vars +(* Given a theorem of the shape: + {[ + A0, ..., An ⊢ B0 ==> ... ==> Bm ==> concl + ]} + + Rewrite it so that it has the shape: + {[ + ⊢ (A0 /\ ... /\ An /\ B0 /\ ... /\ Bm) ==> concl + ]} + *) +fun thm_to_conj_implies (thm : thm) : thm = + let + (* Discharge all the assumptions *) + val thm = DISCH_ALL thm; + (* Rewrite the implications as one conjunction *) + val thm = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] thm; + in thm end + +(* 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] + + 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 = + 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; + (* 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 + +(* Call a function on all the subterms of a term *) +fun dep_apply_in_subterms + (f : string Redblackset.set -> term -> unit) + (bound_vars : string Redblackset.set) + (t : term) : unit = + let + val dep = dep_apply_in_subterms f; + val _ = f bound_vars t; + in + case dest_term t of + VAR (name, ty) => () + | CONST {Name=name, Thy=thy, Ty=ty} => () + | COMB (app, arg) => + let + val _ = dep bound_vars app; + val _ = dep bound_vars arg; + in () end + | LAMB (bvar, body) => + let + val (varname, ty) = dest_var bvar; + val bound_vars = Redblackset.add (bound_vars, varname); + val _ = dep bound_vars body; + in () end + end + +(* Attempt to instantiate a rewrite theorem. + + Remark: this theorem should be of the form: + H ⊢ x = y + + (without quantified variables). + + **REMARK**: the function raises a HOL_ERR exception if it fails. + + [forbid_vars]: forbid substituting with those vars (typically because + they are bound elsewhere). +*) +fun instantiate_dep_rewrite (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm = + let + (* Retrieve the lhs of the conclusion of the theorem *) + val l = lhs (concl th); + (* Match this lhs with the term *) + val (var_s, ty_s) = match_term l t; + (* Check that we are allowed to perform the substitution *) + val free_vars = free_varsl (map (fn {redex=_, residue=x} => x) var_s); + val free_vars = map (fst o dest_var) free_vars; + val free_vars = Redblackset.fromList String.compare free_vars; + val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars)); + in + (* Perform the substitution *) + INST var_s (INST_TYPE ty_s th) + end + +(* +val forbid_vars = Redblackset.empty String.compare +val t = “u32_to_int (int_to_u32 x)” +val t = “u32_to_int (int_to_u32 3)” +val th = (UNDISCH_ALL o SPEC_ALL) int_to_u32_id +*) + +fun instantiate_dep_rewrites (th : thm) (t : term) : thm list = + let + val th = (UNDISCH_ALL o SPEC_ALL) th; + (* We use a map when storing the theorems, to avoid storing the same theorem twice *) + val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare); + fun try_instantiate bvars t = + let + val inst_th = instantiate_dep_rewrite bvars th t; + in + inst_thms := Redblackmap.insert (!inst_thms, lhs (concl inst_th), inst_th) + end + handle HOL_ERR _ => (); + (* Explore the term *) + val _ = dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare) t; + in + map snd (Redblackmap.listItems (!inst_thms)) + end + +(* +val t = “!x. u32_to_int (int_to_u32 x) = u32_to_int (int_to_u32 y)” +val th = int_to_u32_id + +val thms = instantiate_dep_rewrites int_to_u32_id + “!x. u32_to_int (int_to_u32 x) = u32_to_int (int_to_u32 y)” +*) + +(* Attempt to apply dependent rewrites with a theorem *) +fun apply_dep_rewrites_tac (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic = + fn (asms, g) => + let + (* Discharge the assumptions so that the goal is one single term *) + val dg = list_mk_imp (asms, g) + val thms = instantiate_dep_rewrites th dg; + val thms = map thm_to_conj_implies thms; + (* Apply each theorem *) + in + MAP_EVERY (prove_premise_then_apply prove_premise then_tac) thms (asms, g) + end + +(* +val (asms, g) = ([ + “u32_to_int z = u32_to_int i − u32_to_int (int_to_u32 1)”, + “u32_to_int (int_to_u32 2) = 2” +], “T”) + +apply_dep_rewrites_tac + (FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC) + (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]) + int_to_u32_id +*) + +(* See {!rewrite_all_int_conversion_ids}. + + Small utility which takes care of one rewriting. + + TODO: we actually don't use it. + *) +fun rewrite_int_conversion_id + (asms_set: term Redblackset.set) (x : term) (ty : string) : + tactic = + let + (* Lookup the theorem *) + val lemma = Redblackmap.find (integer_conversion_lemmas, ty); + (* Instantiate *) + val lemma = SPEC x lemma; + (* Rewrite the lemma. The lemma typically has the shape: + ⊢ u32_min <= x /\ x <= u32_max ==> u32_to_int (int_to_u32 x) = x + + Make sure the lemma has the proper shape, attempt to prove the premise, + then use the conclusion if it succeeds. + *) + val lemma = thm_to_conj_implies lemma; + (* Retrieve the conclusion of the lemma - we do this to check if it is not + already in the assumptions *) + val c = concl (UNDISCH_ALL lemma); + val already_in_asms = Redblackset.member (asms_set, c); + (* Small utility: the tactic to prove the premise *) + val prove_premise = + (* We might need to unfold the bound definitions, in particular if the + term is a constant (e.g., “3:int”) *) + FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> + COOPER_TAC; + (* Rewrite with a lemma, then assume it *) + fun rewrite_then_assum (thm : thm) : tactic = + FULL_SIMP_TAC simpLib.empty_ss [thm] >> assume_tac thm; + in + (* 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 + end + +(* Look for conversions from integers to machine integers and back. + {[ + u32_to_int (int_to_u32 x) + ]} + + Attempts to prove and apply equalities of the form: + {[ + u32_to_int (int_to_u32 x) = x + ]} + + **REMARK**: this function can fail, if it doesn't manage to prove the + premises of the theorem to apply. + *) +val rewrite_all_int_conversion_ids : tactic = + (* We're not trying to be smart: we just try to rewrite with each theorem at + a time *) + let + val prove_premise = FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC; + val then_tac = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]); + val rewr_tac = apply_dep_rewrites_tac prove_premise then_tac; + in + MAP_EVERY rewr_tac integer_conversion_lemmas_list + end + +(* Massage a bit the goal, for instance by introducing integer bounds in the + assumptions. +*) +val massage : tactic = assume_bounds_for_all_int_vars >> rewrite_all_int_conversion_ids Theorem nth_lem: !(ls : 't list_t) (i : u32). @@ -572,31 +897,26 @@ Proof 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)’ >-( - (* TODO: automate *) - DEP_ONCE_REWRITE_TAC [int_to_u32_id] >> - strip_tac >- (fs [u32_max_def] >> COOPER_TAC) >> - COOPER_TAC - ) >> - (* TODO: automate *) - imp_res_tac U32_SUB_EQ >> fs [st_ex_bind_def] >> - PURE_ONCE_REWRITE_TAC [list_t_v_def] >> rw [] >> - (* Automate this *) - sg ‘u32_to_int (int_to_u32 1) = 1’ >-( - DEP_ONCE_REWRITE_TAC [int_to_u32_id] >> - fs [u32_max_def] >> COOPER_TAC + massage >> COOPER_TAC ) >> - massage >> fs [] >> - (* TODO: automate this *) - qspec_then ‘u32_to_int z’ imp_res_tac NUM_SUB_1_EQ >> rw [] >> + (* 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 [] >> (* Finish the proof by recursion *) - pop_last_assum (qspec_then ‘z’ assume_tac) >> - pop_last_assum mp_tac >> - fs [list_t_v_def] >> - rw [] >> - fs [INT] >> - sg ‘u32_to_int z < &LENGTH (list_t_v ls)’ >- COOPER_TAC >> - (* Rem.: rfs! *) - rfs [] + (* TODO: automate (it should be in massage) *) + qspec_then ‘u32_to_int z’ imp_res_tac NUM_SUB_1_EQ >> rw [] >> rfs [] >> + (* 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 QED (*** |