summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml155
-rw-r--r--backends/hol4/primitivesLib.sml23
2 files changed, 120 insertions, 58 deletions
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 1e874ad5..fe87e894 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -242,43 +242,53 @@ 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
+ [try_match] should return a list of instantiated theorems, as well as terms which
+ identify those 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).
It takes as input the set of bound variables (it should not perform
substitutions with variables belonging to this set).
*)
fun inst_match_in_terms
- (try_match: string Redblackset.set -> term -> term * thm)
+ (try_match: string Redblackset.set -> term -> (term * thm) list)
(tml : term list) : thm list =
let
(* 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_tm, inst_th) = try_match bvars t;
+ val matched_thms = try_match bvars t;
+ fun insert_th (inst_th_tm, inst_th) =
+ inst_thms := Redblackmap.insert (!inst_thms, inst_th_tm, inst_th)
in
- inst_thms := Redblackmap.insert (!inst_thms, inst_th_tm, inst_th)
+ List.app insert_th matched_thms
end
- handle HOL_ERR _ => ();
(* Explore the term *)
val _ = List.app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tml;
in
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
+(* Given a net of rewriting theorems [ths] which have premises, return all the
+ instantiations of those theorems which make its conclusion match subterms
in the provided list of term.
[keep]: if this function returns false on an instantiated theorem, ignore
the theorem.
+
+ The theorems in the Net should be of the shape:
+ {[
+ H0, ..., Hn ⊢ x = y
+ ]}
+ (no implications, no quantified variables)
+ For the above theorem, the key term used in the net should be ‘x’.
*)
-fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tml : term list) : thm list =
+fun inst_match_concl_in_terms (keep : thm -> bool) (ths : thm Net.net) (tml : term list) : thm list =
let
- val th = (UNDISCH_ALL o SPEC_ALL) th;
- fun try_match bvars t =
+ (* First, find potential matches in the net *)
+ fun find_thms (t : term) : thm list = Net.match t ths
+ (* Then, match more precisely for every theorem found *)
+ fun try_match (bvars : string Redblackset.set) t th =
let
val _ = print_dbg ("inst_match_concl_in_terms: " ^ term_to_string t ^ "\n")
val inst_th = inst_match_concl bvars th t
@@ -290,42 +300,72 @@ fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tml : term list)
else
let val _ = print_dbg ("inst_match_concl_in_terms: matched failed\n") in
failwith "inst_match_concl_in_terms: ignore theorem" end
- end;
+ end
+ (* Compose *)
+ fun try_match_on_thms bvars t =
+ let
+ val matched_thms = find_thms t
+ in
+ mapfilter (try_match bvars t) matched_thms
+ end
in
- inst_match_in_terms try_match tml
+ inst_match_in_terms try_match_on_thms tml
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 th = u32_to_int_int_to_u32
+val th = (UNDISCH_ALL o SPEC_ALL) th
+val ths = Net.insert ((lhs o concl) th, th) Net.empty
+val keep = fn _ => true
-val thms = inst_match_concl_in_terms int_to_u32_id [t]
+val thms = inst_match_concl_in_terms keep ths [t]
*)
-(* Given a theorem [th] which has premises, return all the
- instantiations of this theorem which make its first premise match subterms
+(* Given a net of theorems which have premises, return all the
+ instantiations of those theorems which make their first premise match subterms
in the provided list of term.
+
+ The theorems in the Net should be of the shape:
+ {[
+ ⊢ H0 => ... => Hn => H
+ ]}
+ (no quantified variables)
+ For the above theorem, the matching term used in the net should be ‘H0’.
*)
-fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tml : term list) : thm list =
+fun inst_match_first_premise_in_terms
+ (keep : thm -> bool) (ths : thm Net.net) (tml : term list) : thm list =
let
- val th = SPEC_ALL th;
- fun try_match bvars t =
+ (* First, find potential matches in the net *)
+ fun find_thms (t : term) : thm list = Net.match t ths
+ (* Then, match more precisely for every theorem found *)
+ fun try_match bvars t th =
let
val inst_th = inst_match_first_premise bvars th t;
in
if keep inst_th then ((fst o dest_imp o concl) inst_th, inst_th)
else failwith "inst_match_first_premise_in_terms: ignore theorem"
- end;
+ end
+ (* Compose *)
+ fun try_match_on_thms bvars t =
+ let
+ val matched_thms = find_thms t
+ in
+ mapfilter (try_match bvars t) matched_thms
+ end
in
- inst_match_in_terms try_match tml
+ inst_match_in_terms try_match_on_thms tml
end
(*
-val t = “x = y - 1 ==> T”
-val th = SPEC_ALL NUM_SUB_1_EQ
+val t = “n : int = m - 1 ==> T”
+val th = prove (“x: int = y - 1 ==> x + 1 = y”, COOPER_TAC)
+val th = SPEC_ALL th
+val ths = Net.insert ((fst o dest_imp o concl) th, th) Net.empty
+val keep = fn _ => true
-val thms = inst_match_first_premise_in_terms th [t]
+val thms = inst_match_first_premise_in_terms keep ths [t]
*)
@@ -333,39 +373,50 @@ val thms = inst_match_first_premise_in_terms th [t]
conclusion with subterms in the given list of terms.
Leaves the premises as subgoals if [prove_premise] doesn't prove them.
+
+ The theorems in the Net should be of the shape:
+ {[
+ H0, ..., Hn ⊢ x = y
+ ]}
+ (no implications, no quantified variables)
+ For the above theorem, the key term used in the net should be ‘x’.
*)
fun apply_dep_rewrites_match_concl_with_terms_tac
(prove_premise : tactic) (then_tac : thm_tactic)
(ignore_tml : term list)
- (tml : term list) (th : thm) : tactic =
+ (tml : term list) (ths : thm Net.net) : tactic =
let
val ignore = Redblackset.fromList Term.compare ignore_tml
fun keep th = not (Redblackset.member (ignore, concl th))
(* Discharge the assumptions so that the goal is one single term *)
- val thms = inst_match_concl_in_terms keep th tml
+ val thms = inst_match_concl_in_terms keep ths tml
val thms = map thm_to_conj_implies thms
in
- (* Apply each theorem *)
+ (* Try to prove each theorem, and insert the result in the subgoal *)
map_every_tac (try_tac o sg_premise_then prove_premise then_tac) thms
end
-(* Attempt to apply dependent rewrites with a theorem by matching its
+(* Attempt to apply dependent rewrites with theorems by matching their
conclusion with subterms of the goal (including the assumptions).
Leaves the premises as subgoals if [prove_premise] doesn't prove them.
+
+ See [apply_dep_rewrites_match_concl_with_terms_tac] for the shape of
+ the theorems used in the net.
*)
fun apply_dep_rewrites_match_concl_with_all_tac
- (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
+ (prove_premise : tactic) (then_tac : thm_tactic) (ths : thm Net.net) : tactic =
fn (asms, g) =>
- apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms (g :: asms) th (asms, g)
+ apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac
+ asms (g :: asms) ths (asms, g)
(* Same as {!apply_dep_rewrites_match_concl_with_all_tac} but we only match the
conclusion of the goal.
*)
fun apply_dep_rewrites_match_concl_with_goal_tac
- (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
+ (prove_premise : tactic) (then_tac : thm_tactic) (ths : thm Net.net) : tactic =
fn (asms, g) =>
- apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms [g] th (asms, g)
+ apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms [g] ths (asms, g)
(* A theorem might be of the shape: [H => A = B /\ C = D], in which
case we can split it into:
@@ -396,6 +447,21 @@ fun split_rewrite_thm (th : thm) : thm list =
map (transform_th o mk_th) tml
end
+(* Create a net from a list of rewriting theorems, from which we will match
+ the conclusion against various subterms. *)
+fun net_of_rewrite_thms (thml : thm list) : thm Net.net =
+ let
+ fun insert_th (th, net) =
+ let
+ val th = (UNDISCH_ALL o SPEC_ALL) th
+ val tm = (lhs o concl) th
+ in
+ Net.insert (tm, th) net
+ end
+ in
+ foldl insert_th Net.empty thml
+ end
+
(* A dependent rewrite tactic which introduces the premises in a new goal.
We try to apply dependent rewrites to the whole goal, including its assumptions.
@@ -407,8 +473,9 @@ fun sg_dep_rewrite_all_tac (th : thm) =
let
(* Split the theorem *)
val thml = split_rewrite_thm th
+ val ths = net_of_rewrite_thms thml
in
- MAP_EVERY (apply_dep_rewrites_match_concl_with_all_tac all_tac assume_tac) thml
+ apply_dep_rewrites_match_concl_with_all_tac all_tac assume_tac ths
end
(* Same as {!sg_dep_rewrite_tac} but this time we apply rewrites only in the conclusion
@@ -418,8 +485,9 @@ fun sg_dep_rewrite_goal_tac (th : thm) =
let
(* Split the theorem *)
val thml = split_rewrite_thm th
+ val ths = net_of_rewrite_thms thml
in
- MAP_EVERY (apply_dep_rewrites_match_concl_with_goal_tac all_tac assume_tac) thml
+ apply_dep_rewrites_match_concl_with_goal_tac all_tac assume_tac ths
end
(*
@@ -434,18 +502,18 @@ apply_dep_rewrites_match_concl_tac
int_to_u32_id
*)
-(* Attempt to apply dependent rewrites with a theorem by matching its
+(* Attempt to apply dependent rewrites with theorems by matching their
first premise with subterms of the goal.
Leaves the premises as subgoals if [prove_premise] doesn't prove them.
*)
fun apply_dep_rewrites_match_first_premise_with_all_tac
(keep : thm -> bool)
- (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
+ (prove_premise : tactic) (then_tac : thm_tactic) (ths : thm Net.net) : tactic =
fn (asms, g) =>
let
(* Discharge the assumptions so that the goal is one single term *)
- val thms = inst_match_first_premise_in_terms keep th (g :: asms);
+ val thms = inst_match_first_premise_in_terms keep ths (g :: asms);
val thms = map thm_to_conj_implies thms;
fun apply_tac th =
let
@@ -460,17 +528,6 @@ fun apply_dep_rewrites_match_first_premise_with_all_tac
val cooper_tac = COOPER_TAC
-(* TODO: COOPER_TAC fails in the proof below, because of x <> y. We should
- create an issue/PR for HOL4.
-
-Theorem cooper_fail:
- ∀(x y : 'a). x ≠ y ==> 0 ≤ i ==> i ≠ 0 ⇒ 0 < i
-Proof
- rw [] >> cooper_tac
-QED
-
-*)
-
(* Filter the assumptions in the goal *)
fun filter_assums_tac (keep : term -> bool) : tactic =
fn (asms, g) =>
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index 057c57bd..cf7368a6 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -150,6 +150,9 @@ val integer_conversion_lemmas_list = [
u128_to_int_int_to_u128
]
+(* Using a net for efficiency *)
+val integer_conversion_lemmas_net = net_of_rewrite_thms integer_conversion_lemmas_list
+
(* Look for conversions from integers to machine integers and back.
{[
u32_to_int (int_to_u32 x)
@@ -161,17 +164,19 @@ val integer_conversion_lemmas_list = [
]}
*)
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 integer_bounds_defs_list >> int_tac;
- val then_tac1 = (fn th => full_simp_tac simpLib.empty_ss [th]);
- val rewr_tac1 = apply_dep_rewrites_match_concl_with_all_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_with_all_tac (fn _ => true) prove_premise then_tac2;
+ val prove_premise = full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> int_tac
+ (* Rewriting based on matching the conclusion. *)
+ val then_tac1 = (fn th => full_simp_tac simpLib.empty_ss [th])
+ val rewr_tac1 = apply_dep_rewrites_match_concl_with_all_tac prove_premise then_tac1
+ (* Rewriting based on matching the first premise.
+ We're not trying to be smart: we just try to rewrite with each theorem at
+ a time.
+ Remark: this is not used for now. *)
+ val then_tac2 = (fn th => full_simp_tac simpLib.empty_ss [th])
+ val rewr_tac2 = apply_dep_rewrites_match_first_premise_with_all_tac (fn _ => true) prove_premise then_tac2
in
- map_every_tac rewr_tac1 integer_conversion_lemmas_list >>
- map_every_tac rewr_tac2 []
+ rewr_tac1 integer_conversion_lemmas_net
end
(* Massage a bit the goal, for instance by introducing integer bounds in the