diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean index e603c0c5f9..93d9903eb8 100644 --- a/library/init/algebra/group.lean +++ b/library/init/algebra/group.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura -/ prelude -import init.logic init.algebra.ac init.meta init.meta.decl_cmds +import init.logic init.algebra.ac init.meta init.meta.decl_cmds init.meta.smt.rsimp /- Make sure instances defined in this file have lower priority than the ones defined for concrete structures -/ @@ -401,3 +401,8 @@ by simp lemma neg_neg_sub_neg [add_comm_group α] (a b : α) : - (-a - -b) = a - b := by simp + +/- The following lemmas generate too many instances for rsimp -/ +attribute [no_rsimp] + mul_assoc mul_comm mul_left_comm + add_assoc add_comm add_left_comm diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean index 37fbb2c27c..b8479bc2c7 100644 --- a/library/init/meta/attribute.lean +++ b/library/init/meta/attribute.lean @@ -29,7 +29,13 @@ meta def mk_name_set_attr (attr_name : name) : command := do t ← to_expr ``(caching_user_attribute name_set), v ← to_expr ``({name := %%(quote attr_name), descr := "name_set attribute", - mk_cache := name_set.of_list, + mk_cache := λ ns, return $ name_set.of_list ns, dependencies := [] } : caching_user_attribute name_set), add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff), attribute.register attr_name + +meta def get_name_set_for_attr (attr_name : name) : tactic name_set := +do + cnst ← return (expr.const attr_name []), + attr ← eval_expr (caching_user_attribute name_set) cnst, + caching_user_attribute.get_cache attr diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean index 1a3bf463db..0d5eb2c7ff 100644 --- a/library/init/meta/smt/ematch.lean +++ b/library/init/meta/smt/ematch.lean @@ -54,14 +54,13 @@ meta instance : has_to_tactic_format hinst_lemmas := open tactic -private meta def add_lemma (m : transparency) (ignore_errors : bool) (as_simp : bool) (h : name) (hs : hinst_lemmas) : tactic hinst_lemmas := -if ignore_errors then (do h ← hinst_lemma.mk_from_decl_core m h as_simp, return $ hs^.add h) <|> return hs -else (do h ← hinst_lemma.mk_from_decl_core m h as_simp, return $ hs^.add h) +private meta def add_lemma (m : transparency) (as_simp : bool) (h : name) (hs : hinst_lemmas) : tactic hinst_lemmas := +do h ← hinst_lemma.mk_from_decl_core m h as_simp, return $ hs^.add h -meta def to_hinst_lemmas_core (m : transparency) (ignore_errors : bool) : bool → list name → hinst_lemmas → tactic hinst_lemmas +meta def to_hinst_lemmas_core (m : transparency) : bool → list name → hinst_lemmas → tactic hinst_lemmas | as_simp [] hs := return hs | as_simp (n::ns) hs := - let add n := add_lemma m ignore_errors as_simp n hs >>= to_hinst_lemmas_core as_simp ns + let add n := add_lemma m as_simp n hs >>= to_hinst_lemmas_core as_simp ns in do /- First check if n is the name of a function with equational lemmas associated with it -/ eqns ← tactic.get_eqn_lemmas_for tt n, @@ -84,7 +83,7 @@ do t ← to_expr ``(caching_user_attribute hinst_lemmas), b ← if as_simp then to_expr ``(tt) else to_expr ``(ff), v ← to_expr ``({name := %%a, descr := "hinst_lemma attribute", - mk_cache := λ ns, to_hinst_lemmas_core reducible ff %%b ns hinst_lemmas.mk, + mk_cache := λ ns, to_hinst_lemmas_core reducible %%b ns hinst_lemmas.mk, dependencies := [`reducibility] } : caching_user_attribute hinst_lemmas), add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff), attribute.register attr_name @@ -100,11 +99,11 @@ meta def mk_hinst_lemma_attrs_core (as_simp : bool) : list name → command <|> fail ("failed to create hinst_lemma attribute '" ++ n^.to_string ++ "', declaration already exists and has different type.")), mk_hinst_lemma_attrs_core ns) -meta def merge_hinst_lemma_attrs (m : transparency) (ignore_errors as_simp : bool) : list name → hinst_lemmas → tactic hinst_lemmas +meta def merge_hinst_lemma_attrs (m : transparency) (as_simp : bool) : list name → hinst_lemmas → tactic hinst_lemmas | [] hs := return hs | (attr::attrs) hs := do ns ← attribute.get_instances attr, - new_hs ← to_hinst_lemmas_core m ignore_errors as_simp ns hs, + new_hs ← to_hinst_lemmas_core m as_simp ns hs, merge_hinst_lemma_attrs attrs new_hs /-- @@ -127,9 +126,9 @@ do mk_hinst_lemma_attrs_core ff attr_names, let aux1 : list name := %%l1, aux2 : list name := %%l2 in do { - hs₁ ← to_hinst_lemmas_core reducible ff ff ns hinst_lemmas.mk, - hs₂ ← merge_hinst_lemma_attrs reducible ff ff aux1 hs₁, - merge_hinst_lemma_attrs reducible ff tt aux2 hs₂}, + hs₁ ← to_hinst_lemmas_core reducible ff ns hinst_lemmas.mk, + hs₂ ← merge_hinst_lemma_attrs reducible ff aux1 hs₁, + merge_hinst_lemma_attrs reducible tt aux2 hs₂}, dependencies := [`reducibility] ++ %%l1 ++ %%l2 } : caching_user_attribute hinst_lemmas), add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff), attribute.register attr_name diff --git a/library/init/meta/smt/rsimp.lean b/library/init/meta/smt/rsimp.lean index baffb8ee1d..dfedee7824 100644 --- a/library/init/meta/smt/rsimp.lean +++ b/library/init/meta/smt/rsimp.lean @@ -8,22 +8,53 @@ import init.meta.smt.smt_tactic init.meta.fun_info init.meta.rb_map open tactic -meta def mk_hinst_lemma_attr_from_simp_attr (attr_decl_name attr_name : name) (simp_attr_name : name) : command := +private meta def add_lemma (m : transparency) (h : name) (hs : hinst_lemmas) : tactic hinst_lemmas := +(do h ← hinst_lemma.mk_from_decl_core m h tt, return $ hs^.add h) <|> return hs + +private meta def to_hinst_lemmas (m : transparency) (ex : name_set) : list name → hinst_lemmas → tactic hinst_lemmas +| [] hs := return hs +| (n::ns) hs := + if ex^.contains n then to_hinst_lemmas ns hs else + let add n := add_lemma m n hs >>= to_hinst_lemmas ns + in do eqns ← tactic.get_eqn_lemmas_for tt n, + match eqns with + | [] := add n + | _ := mcond (is_prop_decl n) (add n) (to_hinst_lemmas eqns hs >>= to_hinst_lemmas ns) + end + +/-- Create a rsimp attribute named `attr_name`, the attribute declaration is named `attr_decl_name`. + The cached hinst_lemmas structure is built using the lemmas marked with simp attribute `simp_attr_name`, + but *not* marked with `ex_attr_name`. + + We say `ex_attr_name` is the "exception set". It is useful for excluding lemmas in `simp_attr_name` + which are not good or redundant for ematching. -/ +meta def mk_hinst_lemma_attr_from_simp_attr (attr_decl_name attr_name : name) (simp_attr_name : name) (ex_attr_name : name) : command := do t ← to_expr `(caching_user_attribute hinst_lemmas), v ← to_expr `({ name := %%(quote attr_name), descr := "hinst_lemma attribute derived from '" ++ to_string %%(quote simp_attr_name) ++ "'", mk_cache := λ ns, let aux := %%(quote simp_attr_name) in + let ex_attr := %%(quote ex_attr_name) in do { - hs ← to_hinst_lemmas_core reducible tt tt ns hinst_lemmas.mk, + hs ← to_hinst_lemmas reducible mk_name_set ns hinst_lemmas.mk, ss ← attribute.get_instances aux, - to_hinst_lemmas_core reducible tt tt ss hs + ex ← get_name_set_for_attr ex_attr, + to_hinst_lemmas reducible ex ss hs }, dependencies := [`reducibility, %%(quote simp_attr_name)]} : caching_user_attribute hinst_lemmas), add_decl (declaration.defn attr_decl_name [] t v reducibility_hints.abbrev ff), attribute.register attr_decl_name -run_command mk_hinst_lemma_attr_from_simp_attr `rsimp_attr `rsimp `simp +run_command mk_name_set_attr `no_rsimp +run_command mk_hinst_lemma_attr_from_simp_attr `rsimp_attr `rsimp `simp `no_rsimp + +/- The following lemmas are not needed by rsimp, and they actually hurt performance since they generate a lot of + instances. -/ +attribute [no_rsimp] + id.def ne.def not_true not_false_iff ne_self_iff_false eq_self_iff_true heq_self_iff_true iff_not_self not_iff_self + true_iff_false false_iff_true and.comm and.assoc and.left_comm and_true true_and and_false false_and not_and_self and_not_self + and_self or.comm or.assoc or.left_comm or_true true_or or_false false_or or_self iff_true true_iff iff_false false_iff + iff_self implies_true_iff false_implies_iff if_t_t if_true if_false namespace rsimp diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp index be8cdbbd0b..d8b6b526c6 100644 --- a/src/library/tactic/smt/hinst_lemmas.cpp +++ b/src/library/tactic/smt/hinst_lemmas.cpp @@ -405,7 +405,7 @@ struct mk_hinst_lemma_fn { m_candidates = candidate_set(); if (m_simp) { expr lhs, rhs; - if (is_eq(a, lhs, rhs) || is_heq(a, lhs, rhs)) { + if (is_eq(a, lhs, rhs) || is_heq(a, lhs, rhs) || is_iff(a, lhs, rhs)) { m_candidates.insert(candidate(normalize(lhs))); } } else {