max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/meta): add exception set to rsimp attributes, use iff lemmas

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-18 19:43:21 -08:00
parent 0626835530
commit 0a99910c52
5 changed files with 59 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/init/algebra/group.lean
View file

@ -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

8
library/init/meta/attribute.lean
View file

@ -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

21
library/init/meta/smt/ematch.lean
View file

@ -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

39
library/init/meta/smt/rsimp.lean
View file

@ -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

2
src/library/tactic/smt/hinst_lemmas.cpp
View file

@ -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 {