diff options
Diffstat (limited to 'backends/hol4')
| -rw-r--r-- | backends/hol4/Test.sml | 250 |
1 files changed, 199 insertions, 51 deletions
diff --git a/backends/hol4/Test.sml b/backends/hol4/Test.sml index ef110cb1..c10d64ce 100644 --- a/backends/hol4/Test.sml +++ b/backends/hol4/Test.sml @@ -414,6 +414,13 @@ val list_t_v_def = Define ‘ open dep_rewrite open integerTheory +(* Ignore a theorem. + + To be used in conjunction with {!pop_assum} for instance. + *) +fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC + + Theorem INT_OF_NUM_INJ: !n m. &n = &m ==> n = m Proof @@ -421,7 +428,35 @@ Proof fs [Num] QED +Theorem NUM_SUB_EQ: + !(x y z : int). x = y - z ==> 0 <= x ==> 0 <= z ==> Num y = Num z + Num x +Proof + rpt strip_tac >> + sg ‘0 <= y’ >- COOPER_TAC >> + rfs [] >> + (* Convert to integers *) + irule INT_OF_NUM_INJ >> + imp_res_tac (GSYM INT_OF_NUM) >> + (* Associativity of & *) + PURE_REWRITE_TAC [GSYM INT_ADD] >> + fs [] +QED + Theorem NUM_SUB_1_EQ: + !(x y : int). x = y - 1 ==> 0 <= x ==> Num y = SUC (Num x) +Proof + rpt strip_tac >> + (* Get rid of the SUC *) + sg ‘SUC (Num x) = 1 + Num x’ >-(rw [ADD]) >> rw [] >> + (* Massage a bit the goal *) + qsuff_tac ‘Num y = Num (y − 1) + Num 1’ >- COOPER_TAC >> + (* Apply the general theorem *) + irule NUM_SUB_EQ >> + COOPER_TAC +QED + +(* TODO: remove *) +Theorem NUM_SUB_1_EQ1: !i. 0 <= i - 1 ==> Num i = SUC (Num (i-1)) Proof rpt strip_tac >> @@ -457,12 +492,6 @@ 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 @@ -728,6 +757,14 @@ fun dep_apply_in_subterms in () end end +(* Return the set of free variables appearing in the residues of a term substitution *) +fun free_vars_in_subst_residue (s: (term, term) Term.subst) : string Redblackset.set = + let + val free_vars = free_varsl (map (fn {redex=_, residue=x} => x) s); + val free_vars = map (fst o dest_var) free_vars; + val free_vars = Redblackset.fromList String.compare free_vars; + in free_vars end + (* Attempt to instantiate a rewrite theorem. Remark: this theorem should be of the form: @@ -738,19 +775,18 @@ fun dep_apply_in_subterms **REMARK**: the function raises a HOL_ERR exception if it fails. [forbid_vars]: forbid substituting with those vars (typically because - they are bound elsewhere). + we are maching in a subterm under lambdas, and some of those variables + are bounds in the outer lambdas). *) -fun instantiate_dep_rewrite (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm = +fun inst_match_concl (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)); + (* 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_vars_in_subst_residue var_s; + val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars)); in (* Perform the substitution *) INST var_s (INST_TYPE ty_s th) @@ -763,16 +799,61 @@ val t = “u32_to_int (int_to_u32 3)” val th = (UNDISCH_ALL o SPEC_ALL) int_to_u32_id *) -fun instantiate_dep_rewrites_in_terms (th : thm) (tl : term list) : thm list = +(* Attempt to instantiate a theorem by matching its first premise. + + Note that we make the hypothesis tha all the free variables which need + to be instantiated appear in the first premise, of course (the caller should + enforce this). + + Remark: this theorem should be of the form: + ⊢ H0 ==> ... ==> Hn ==> H + + (without quantified variables). + + **REMARK**: the function raises a HOL_ERR exception if it fails. + + [forbid_vars]: see [inst_match_concl] +*) +fun inst_match_first_premise + (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm = + let + (* Retrieve the first premise *) + val l = (fst o dest_imp o concl) th; + (* Match this 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_vars_in_subst_residue var_s; + 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 z = u32_to_int i − 1” +val th = SPEC_ALL NUM_SUB_1_EQ +*) + +(* Call a matching function on all the subterms in the provided list of term. + This is a generic function. + + [try_match] should return an instantiated theorem, as well as a term which + identifies this theorem (the lhs of the equality, if this is a rewriting + theorem for instance - we use this to check for collisions, and discard + redundant instantiations). + *) +fun inst_match_in_terms + (try_match: string Redblackset.set -> term -> term * thm) + (tl : term list) : 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; + val (inst_th_tm, inst_th) = try_match bvars t; in - inst_thms := Redblackmap.insert (!inst_thms, lhs (concl inst_th), inst_th) + inst_thms := Redblackmap.insert (!inst_thms, inst_th_tm, inst_th) end handle HOL_ERR _ => (); (* Explore the term *) @@ -781,23 +862,67 @@ fun instantiate_dep_rewrites_in_terms (th : thm) (tl : term list) : thm list = map snd (Redblackmap.listItems (!inst_thms)) end +(* Given a rewriting theorem [th] which has premises, return all the + instantiations of this theorem which make its conclusion match subterms + in the provided list of term. + *) +fun inst_match_concl_in_terms (th : thm) (tl : term list) : thm list = + let + val th = (UNDISCH_ALL o SPEC_ALL) th; + fun try_match bvars t = + let + val inst_th = inst_match_concl bvars th t; + in + (lhs (concl inst_th), inst_th) + end; + in + inst_match_in_terms try_match tl + 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)” +val thms = inst_match_concl_in_terms int_to_u32_id [t] +*) + + +(* Given a theorem [th] which has premises, return all the + instantiations of this theorem which make its first premise match subterms + in the provided list of term. + *) +fun inst_match_first_premise_in_terms (th : thm) (tl : term list) : thm list = + let + val th = SPEC_ALL th; + fun try_match bvars t = + let + val inst_th = inst_match_first_premise bvars th t; + in + ((fst o dest_imp o concl) inst_th, inst_th) + end; + in + inst_match_in_terms try_match tl + end + +(* +val t = “x = y - 1 ==> T” +val th = SPEC_ALL NUM_SUB_1_EQ + +val thms = inst_match_first_premise_in_terms th [t] *) -(* Attempt to apply dependent rewrites with a theorem *) -fun apply_dep_rewrites_tac (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic = +(* Attempt to apply dependent rewrites with a theorem by matching its + conclusion with subterms of the goal. + *) +fun apply_dep_rewrites_match_concl_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 thms = instantiate_dep_rewrites_in_terms th (g :: asms); + val thms = inst_match_concl_in_terms th (g :: asms); val thms = map thm_to_conj_implies thms; - (* Apply each theorem *) in + (* Apply each theorem *) MAP_EVERY (prove_premise_then_apply prove_premise then_tac) thms (asms, g) end @@ -807,17 +932,38 @@ val (asms, g) = ([ “u32_to_int (int_to_u32 2) = 2” ], “T”) -apply_dep_rewrites_tac +apply_dep_rewrites_match_concl_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 *) +(* Attempt to apply dependent rewrites with a theorem by matching its + first premise with subterms of the goal. + *) +fun apply_dep_rewrites_match_first_premise_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 thms = inst_match_first_premise_in_terms th (g :: asms); + val thms = map thm_to_conj_implies thms; + fun apply_tac th = + let + val th = thm_to_conj_implies th; + in + prove_premise_then_apply prove_premise then_tac th + end; + in + (* Apply each theorem *) + MAP_EVERY apply_tac thms (asms, g) + end + (* See {!rewrite_all_int_conversion_ids}. Small utility which takes care of one rewriting. - TODO: we actually don't use it. + TODO: we actually don't use it. REMOVE? *) fun rewrite_int_conversion_id (asms_set: term Redblackset.set) (x : term) (ty : string) : @@ -866,22 +1012,41 @@ fun rewrite_int_conversion_id **REMARK**: this function can fail, if it doesn't manage to prove the premises of the theorem to apply. + + TODO: update *) -val rewrite_all_int_conversion_ids : tactic = +val rewrite_with_dep_int_lemmas : 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; + val then_tac1 = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]); + val rewr_tac1 = apply_dep_rewrites_match_concl_tac prove_premise then_tac1; + val then_tac2 = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]); + val rewr_tac2 = apply_dep_rewrites_match_first_premise_tac prove_premise then_tac2; in - MAP_EVERY rewr_tac integer_conversion_lemmas_list + MAP_EVERY rewr_tac1 integer_conversion_lemmas_list >> + MAP_EVERY rewr_tac2 [NUM_SUB_1_EQ] end +(* +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 + +val thm = thm_to_conj_implies (SPECL [“u32_to_int z”, “u32_to_int i”] NUM_SUB_1_EQ) + +val h = “u32_to_int z = u32_to_int i − 1 ∧ 0 ≤ u32_to_int z” +*) + (* 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 +val massage : tactic = + assume_bounds_for_all_int_vars >> + rewrite_with_dep_int_lemmas (* SIMP_CONV arith_ss [ADD] “1 + (x : num)” @@ -908,23 +1073,6 @@ Proof (* 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 *) - (* TODO: automate (it should be in massage). - - Steps: - - rewrite: x = y - 1 => Num y = SUC x - - TODO: generalize? - - x = y - z ==> 0 <= x ==> Num y = z + x - - then apply rewriting such as ADD (1 + ...)? - - or: two versions of the theorem, and we prioritize the first one: - x = y - 1 ==> 0 <= x ==> Num y = SUC z - x = y - z ==> 0 <= x ==> Num y = y - z - - or: EL (x + 1) ls = EL (SUC x) ls - (and other theorems like this) - (but there will be a loooot of theorems) - *) - 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. |