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

feat(library/tactic): add dsimp_config configuration object for the dsimp tactic family

Browse source 
Now, `dsimp` fails if the goal did not change.
We can use the config object to obtain the previous behavior:
```
dsimp {fail_if_unchaged := ff}
```
See comment https://github.com/leanprover/lean/issues/1694#issuecomment-310956315
at issue #1694
This commit is contained in:
Leonardo de Moura 2017-06-30 17:09:44 -07:00
parent 19f65b3b8a
commit 52d4189805
17 changed files with 160 additions and 111 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/changes.md
View file

@ -44,6 +44,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
* Add configuration object `rewrite_cfg` to `rw`/`rewrite` tactic. It now has support for `auto_param` and `opt_param`.
The new goals are ordered using the same strategies available for `apply`.
* All `dsimp` tactics fail if they did not change anything. We can simulate the v3.2.0 by using `dsimp {fail_if_unchaged := ff}`.
v3.2.0 (18 June 2017)
-------------

2
library/init/data/int/bitwise.lean
View file

@ -152,7 +152,7 @@ namespace int
cases m with m m; cases n with n n; try {refl},
all_goals {
apply congr_arg of_nat <|> apply congr_arg neg_succ_of_nat,
dsimp [nat.land, nat.ldiff, nat.lor],
try {dsimp [nat.land, nat.ldiff, nat.lor]},
try {rw [
show nat.bitwise (λ a b, a && bnot b) n m =
nat.bitwise (λ a b, b && bnot a) m n, from

2
library/init/data/list/lemmas.lean
View file

@ -461,7 +461,7 @@ lemma exists_of_mem_join {a : α} {L : list (list α)} : a ∈ join L → ∃ l,
mem_join_iff.1
lemma mem_join {a : α} {L : list (list α)} {l} (lL : l ∈ L) (al : a ∈ l) : a ∈ join L :=
mem_join_iff.2 ⟨l, lL, al⟩
mem_join_iff.2 ⟨l, lL, al⟩
/- list subset -/

4
library/init/data/nat/bitwise.lean
View file

@ -154,7 +154,7 @@ namespace nat
lemma shiftr_eq_div_pow (m) : ∀ n, shiftr m n = m / 2 ^ n
| 0 := (nat.div_one _).symm
| (k+1) := (congr_arg div2 (shiftr_eq_div_pow k)).trans $
by dsimp; rw [div2_val, nat.div_div_eq_div_mul]; refl
by rw [div2_val, nat.div_div_eq_div_mul]; refl
@[simp] lemma zero_shiftr (n) : shiftr 0 n = 0 :=
(shiftr_eq_div_pow _ _).trans (nat.zero_div _)
@ -175,7 +175,7 @@ namespace nat
(lt_of_le_of_ne (zero_le _) (ne.symm n0)),
rwa mul_one at this
end,
by rw [-show bit (bodd n) n' = n, from bit_decomp n]; exact
by rw [-show bit (bodd n) n' = n, from bit_decomp n]; exact
f (bodd n) n' (binary_rec n')
def size : ℕ → ℕ := binary_rec 0 (λ_ _, succ)

15
library/init/meta/interactive.lean
View file

@ -800,17 +800,20 @@ do s ← mk_simp_set no_dflt attr_names hs wo_ids,
end,
try triv >> try (reflexivity reducible)
private meta def dsimp_hyps (s : simp_lemmas) (hs : list name) : tactic unit :=
hs.mfor' (λ h, get_local h >>= dsimp_at_core s)
private meta def dsimp_hyps (s : simp_lemmas) (hs : list name) (cfg : dsimp_config := {}) : tactic unit :=
hs.mfor' (λ h_name, do h ← get_local h_name, dsimp_at_core s h cfg)
meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : parse location → tactic unit
| (loc.ns []) := do s ← mk_simp_set no_dflt attr_names es ids, tactic.dsimp_core s
| (loc.ns hs) := do s ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s hs
meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list)
(ids : parse without_ident_list) (l : parse location) (cfg : dsimp_config := {}) : tactic unit :=
match l with
| (loc.ns []) := do s ← mk_simp_set no_dflt attr_names es ids, tactic.dsimp_core s cfg
| (loc.ns hs) := do s ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s hs cfg
| (loc.wildcard) := do ls ← local_context,
n ← revert_lst ls,
s ← mk_simp_set no_dflt attr_names es ids,
tactic.dsimp_core s,
tactic.dsimp_core s cfg,
intron n
end
/--
This tactic applies to a goal that has the form `t ~ u` where `~` is a reflexive relation.

52
library/init/meta/simp_tactic.lean
View file

@ -55,18 +55,11 @@ meta constant simp_lemmas.drewrite_core : transparency → simp_lemmas → expr
meta def simp_lemmas.drewrite : simp_lemmas → expr → tactic expr :=
simp_lemmas.drewrite_core reducible
/-- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
The resulting expression is definitionally equal to the input. -/
meta constant simp_lemmas.dsimplify_core (max_steps : nat) (visit_instances : bool) : simp_lemmas → expr → tactic expr
meta constant is_valid_simp_lemma_cnst : transparency → name → tactic bool
meta constant is_valid_simp_lemma : transparency → expr → tactic bool
def default_max_steps := 10000000
meta def simp_lemmas.dsimplify : simp_lemmas → expr → tactic expr :=
simp_lemmas.dsimplify_core default_max_steps ff
meta constant simp_lemmas.pp : simp_lemmas → tactic format
namespace tactic
@ -74,15 +67,26 @@ namespace tactic
If deps is tt, then lemmas for automatically generated auxiliary declarations used to define d are also included. -/
meta constant get_eqn_lemmas_for : bool → name → tactic (list name)
structure dsimp_config :=
(md := reducible)
(max_steps : nat := default_max_steps)
(canonize_instances : bool := tt)
(single_pass : bool := ff)
(fail_if_unchaged := tt)
(eta := tt)
end tactic
/-- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
The resulting expression is definitionally equal to the input. -/
meta constant simp_lemmas.dsimplify (s : simp_lemmas) (e : expr) (cfg : tactic.dsimp_config := {}) : tactic expr
namespace tactic
/- Remark: the configuration parameters `cfg.md` and `cfg.eta` are ignored by this tactic. -/
meta constant dsimplify_core
/- The user state type. -/
{α : Type}
/- Initial user data -/
(a : α)
(max_steps : nat)
/- If visit_instances = ff, then instance implicit arguments are not visited, but
tactic will canonize them. -/
(visit_instances : bool)
/- (pre a e) is invoked before visiting the children of subterm 'e',
if it succeeds the result (new_a, new_e, flag) where
- 'new_a' is the new value for the user data
@ -93,13 +97,15 @@ meta constant dsimplify_core
The output is similar to (pre a e), but the 'flag' indicates whether
the new expression should be revisited or not. -/
(post : α → expr → tactic (α × expr × bool))
: expr → tactic (α × expr)
(e : expr)
(cfg : dsimp_config := {})
: tactic (α × expr)
meta def dsimplify
(pre : expr → tactic (expr × bool))
(post : expr → tactic (expr × bool))
: expr → tactic expr :=
λ e, do (a, new_e) ← dsimplify_core () default_max_steps ff
λ e, do (a, new_e) ← dsimplify_core ()
(λ u e, do r ← pre e, return (u, r))
(λ u e, do r ← post e, return (u, r)) e,
return new_e
@ -170,7 +176,7 @@ let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
new_f ← decl.instantiate_value_univ_params f_lvls,
new_e ← head_beta (expr.mk_app new_f e.get_app_args),
return (u, new_e, tt)
in do (c, new_e) ← dsimplify_core () cfg.max_steps cfg.visit_instances (λ c e, failed) unfold e,
in do (c, new_e) ← dsimplify_core () (λ c e, failed) unfold e {max_steps := cfg.max_steps, canonize_instances := cfg.visit_instances},
return new_e
meta def delta (cs : list name) : tactic unit :=
@ -183,7 +189,7 @@ meta def unfold_projections_core (m : transparency) (max_steps : nat) (e : expr)
let unfold (changed : bool) (e : expr) : tactic (bool × expr × bool) := do
new_e ← unfold_projection_core m e,
return (tt, new_e, tt)
in do (tt, new_e) ← dsimplify_core ff default_max_steps tt (λ c e, failed) unfold e | fail "no projections to unfold",
in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e | fail "no projections to unfold",
return new_e
meta def unfold_projections : tactic unit :=
@ -260,17 +266,17 @@ do S ← simp_lemmas.mk_default,
S ← S.append hs,
simplify_goal S cfg >> try triv
meta def dsimp_core (s : simp_lemmas) : tactic unit :=
target >>= s.dsimplify >>= unsafe_change
meta def dsimp_core (s : simp_lemmas) (cfg : dsimp_config := {}) : tactic unit :=
do t ← target, s.dsimplify t cfg >>= unsafe_change
meta def dsimp : tactic unit :=
simp_lemmas.mk_default >>= dsimp_core
meta def dsimp (cfg : dsimp_config := {}) : tactic unit :=
do s ← simp_lemmas.mk_default, dsimp_core s cfg
meta def dsimp_at_core (s : simp_lemmas) : expr → tactic unit :=
revert_and_transform s.dsimplify
meta def dsimp_at_core (s : simp_lemmas) (h : expr) (cfg : dsimp_config := {}) : tactic unit :=
revert_and_transform (λ e, s.dsimplify e cfg) h
meta def dsimp_at (h : expr) : tactic unit :=
do s ← simp_lemmas.mk_default, dsimp_at_core s h
meta def dsimp_at (h : expr) (cfg : dsimp_config := {}) : tactic unit :=
do s ← simp_lemmas.mk_default, dsimp_at_core s h cfg
private meta def is_equation : expr → bool
| (expr.pi n bi d b) := is_equation b

4
library/smt/array.lean
View file

@ -22,9 +22,9 @@ def store (a : array α β) (i : α) (v : β) : array α β :=
λ j, if j = i then v else select a j
@[simp] lemma select_store (a : array α β) (i : α) (v : β) : select (store a i v) i = v :=
by unfold smt.store smt.select; dsimp; rewrite if_pos; reflexivity
by unfold smt.store smt.select; rewrite if_pos; reflexivity
@[simp] lemma select_store_ne (a : array α β) (i j : α) (v : β) : j ≠ i → select (store a i v) j = select a j :=
by intros; unfold smt.store smt.select; dsimp; rewrite if_neg; assumption
by intros; unfold smt.store smt.select; rewrite if_neg; assumption
end smt

97
src/library/tactic/dsimplify.cpp
View file

@ -19,7 +19,28 @@ Author: Leonardo de Moura
#include "library/tactic/simp_lemmas.h"
#include "library/tactic/tactic_state.h"
#ifndef LEAN_DEFAULT_DSIMPLIFY_MAX_STEPS
#define LEAN_DEFAULT_DSIMPLIFY_MAX_STEPS 1000000
#endif
namespace lean {
dsimp_config::dsimp_config():
m_md(transparency_mode::Reducible),
m_max_steps(LEAN_DEFAULT_DSIMPLIFY_MAX_STEPS),
m_canonize_instances(true),
m_single_pass(false),
m_fail_if_unchanged(true),
m_eta(false) {
}
dsimp_config::dsimp_config(vm_obj const & o) {
m_md = to_transparency_mode(cfield(o, 0));
m_max_steps = force_to_unsigned(cfield(o, 1));
m_canonize_instances = to_bool(cfield(o, 2));
m_single_pass = to_bool(cfield(o, 3));
m_fail_if_unchanged = to_bool(cfield(o, 4));
m_eta = to_bool(cfield(o, 5));
}
#define lean_dsimp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
optional<pair<expr, bool>> dsimplify_core_fn::pre(expr const &) {
@ -85,7 +106,7 @@ expr dsimplify_core_fn::visit_app(expr const & e) {
bool modified = false;
expr f = get_app_args(e, args);
unsigned i = 0;
if (!m_visit_instances) {
if (!m_cfg.m_canonize_instances) {
fun_info info = get_fun_info(m_ctx, f, args.size());
for (param_info const & pinfo : info.get_params_info()) {
lean_assert(i < args.size());
@ -119,7 +140,7 @@ expr dsimplify_core_fn::visit_meta(expr const & e) {
void dsimplify_core_fn::inc_num_steps() {
m_num_steps++;
if (m_num_steps > m_max_steps)
if (m_num_steps > m_cfg.m_max_steps)
throw exception("dsimplify failed, maximum number of steps exceeded");
}
@ -177,6 +198,8 @@ expr dsimplify_core_fn::visit(expr const & e) {
break;
}
curr_e = p2->first;
if (m_cfg.m_single_pass)
break;
} else {
curr_e = new_e;
break;
@ -186,15 +209,14 @@ expr dsimplify_core_fn::visit(expr const & e) {
return curr_e;
}
dsimplify_core_fn::dsimplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, bool visit_instances):
m_ctx(ctx), m_defeq_canonizer(ctx, dcs), m_num_steps(0), m_need_restart(false),
m_max_steps(max_steps), m_visit_instances(visit_instances) {}
dsimplify_core_fn::dsimplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, dsimp_config const & cfg):
m_ctx(ctx), m_defeq_canonizer(ctx, dcs), m_num_steps(0), m_need_restart(false), m_cfg(cfg) {}
expr dsimplify_core_fn::operator()(expr e) {
while (true) {
m_need_restart = false;
e = visit(e);
if (!m_need_restart)
if (!m_need_restart || m_cfg.m_single_pass)
return e;
m_cache.clear();
}
@ -206,13 +228,13 @@ metavar_context const & dsimplify_core_fn::mctx() const {
expr dsimplify_fn::whnf(expr const & e) {
expr new_e = m_ctx.whnf(e);
if (m_use_eta)
if (m_cfg.m_eta)
new_e = try_eta(new_e);
return new_e;
}
optional<pair<expr, bool>> dsimplify_fn::pre(expr const & e) {
type_context::transparency_scope s(m_ctx, m_md);
type_context::transparency_scope s(m_ctx, m_cfg.m_md);
expr new_e = whnf(e);
if (new_e != e) {
lean_dsimp_trace(m_ctx, "dsimplify", tout() << "whnf\n" << e << "\n==>\n" << new_e << "\n";);
@ -225,7 +247,7 @@ optional<pair<expr, bool>> dsimplify_fn::pre(expr const & e) {
optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
expr curr_e;
{
type_context::transparency_scope s(m_ctx, m_md);
type_context::transparency_scope s(m_ctx, m_cfg.m_md);
curr_e = whnf(e);
if (curr_e != e) {
lean_dsimp_trace(m_ctx, "dsimplify", tout() << "whnf\n" << e << "\n==>\n" << curr_e << "\n";);
@ -252,6 +274,8 @@ optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
if (new_e == curr_e) break;
lean_dsimp_trace(m_ctx, "dsimplify", tout() << "rewrite\n" << curr_e << "\n==>\n" << new_e << "\n";);
curr_e = new_e;
if (m_cfg.m_single_pass)
break;
}
if (curr_e == e)
return optional<pair<expr, bool>>();
@ -259,12 +283,9 @@ optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
return optional<pair<expr, bool>>(curr_e, true);
}
dsimplify_fn::dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, bool visit_instances, simp_lemmas_for const & lemmas,
bool use_eta, transparency_mode md):
dsimplify_core_fn(ctx, dcs, max_steps, visit_instances),
m_simp_lemmas(lemmas),
m_use_eta(use_eta),
m_md(md) {
dsimplify_fn::dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas_for const & lemmas, dsimp_config const & cfg):
dsimplify_core_fn(ctx, dcs, cfg),
m_simp_lemmas(lemmas) {
}
class tactic_dsimplify_fn : public dsimplify_core_fn {
@ -300,9 +321,10 @@ class tactic_dsimplify_fn : public dsimplify_core_fn {
}
public:
tactic_dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, bool visit_instances,
vm_obj const & a, vm_obj const & pre, vm_obj const & post, tactic_state const & s):
dsimplify_core_fn(ctx, dcs, max_steps, visit_instances),
tactic_dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs,
vm_obj const & a, vm_obj const & pre, vm_obj const & post,
tactic_state const & s, dsimp_config const & cfg):
dsimplify_core_fn(ctx, dcs, cfg),
m_a(a),
m_pre(pre),
m_post(post),
@ -313,37 +335,43 @@ public:
};
vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a,
vm_obj const & max_steps, vm_obj const & visit_instances,
vm_obj const & pre, vm_obj const & post, vm_obj const & e, vm_obj const & _s) {
vm_obj const & pre, vm_obj const & post, vm_obj const & e,
vm_obj const & _cfg, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
dsimp_config cfg(_cfg);
try {
type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
type_context ctx = mk_type_context_for(s, cfg.m_md);
defeq_can_state dcs = s.dcs();
tactic_dsimplify_fn F(ctx, dcs, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
to_bool(visit_instances), a, pre, post, s);
tactic_dsimplify_fn F(ctx, dcs, a, pre, post, s, cfg);
expr new_e = F(to_expr(e));
tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs);
return tactic::mk_success(mk_vm_pair(F.get_a(), to_obj(new_e)), new_s);
if (cfg.m_fail_if_unchanged && to_expr(e) == new_e) {
return tactic::mk_exception("dsimplify tactic failed to simplify", s);
} else {
tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs);
return tactic::mk_success(mk_vm_pair(F.get_a(), to_obj(new_e)), new_s);
}
} catch (exception & ex) {
return tactic::mk_exception(ex, s);
}
}
vm_obj simp_lemmas_dsimplify_core(vm_obj const & max_steps, vm_obj const & visit_instances, vm_obj const & lemmas,
vm_obj const & e, vm_obj const & _s) {
vm_obj simp_lemmas_dsimplify(vm_obj const & lemmas, vm_obj const & e, vm_obj const & _cfg, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
dsimp_config cfg(_cfg);
try {
type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
type_context ctx = mk_type_context_for(s, cfg.m_md);
defeq_can_state dcs = s.dcs();
simp_lemmas_for dlemmas;
if (auto * dls = to_simp_lemmas(lemmas).find(get_eq_name()))
dlemmas = *dls;
bool use_eta = true; /* TODO(Leo): expose flag in the Lean API */
dsimplify_fn F(ctx, dcs, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
to_bool(visit_instances), dlemmas, use_eta);
dsimplify_fn F(ctx, dcs, dlemmas, cfg);
expr new_e = F(to_expr(e));
tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs);
return tactic::mk_success(to_obj(new_e), new_s);
if (cfg.m_fail_if_unchanged && to_expr(e) == new_e) {
return tactic::mk_exception("dsimplify tactic failed to simplify", s);
} else {
tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs);
return tactic::mk_success(to_obj(new_e), new_s);
}
} catch (exception & ex) {
return tactic::mk_exception(ex, s);
}
@ -352,9 +380,8 @@ vm_obj simp_lemmas_dsimplify_core(vm_obj const & max_steps, vm_obj const & visit
void initialize_dsimplify() {
register_trace_class("dsimplify");
register_trace_class(name{"debug", "dsimplify"});
DECLARE_VM_BUILTIN(name({"tactic", "dsimplify_core"}), tactic_dsimplify_core);
DECLARE_VM_BUILTIN(name({"simp_lemmas", "dsimplify_core"}), simp_lemmas_dsimplify_core);
DECLARE_VM_BUILTIN(name({"simp_lemmas", "dsimplify"}), simp_lemmas_dsimplify);
}
void finalize_dsimplify() {

32
src/library/tactic/dsimplify.h
View file

@ -10,6 +10,27 @@ Author: Leonardo de Moura
#include "library/tactic/simp_lemmas.h"
namespace lean {
/*
structure dsimp_config :=
(md := reducible)
(max_steps : nat := default_max_steps)
(canonize_instances : bool := tt)
(canonize_proofs : bool := ff)
(single_pass : bool := ff)
(fail_if_unchaged := tt)
(eta := ff)
*/
struct dsimp_config {
transparency_mode m_md;
unsigned m_max_steps;
bool m_canonize_instances;
bool m_single_pass;
bool m_fail_if_unchanged;
bool m_eta;
dsimp_config();
dsimp_config(vm_obj const & o);
};
class dsimplify_core_fn {
protected:
type_context & m_ctx;
@ -17,9 +38,7 @@ protected:
expr_struct_map<expr> m_cache;
unsigned m_num_steps;
bool m_need_restart;
unsigned m_max_steps;
bool m_visit_instances;
dsimp_config m_cfg;
virtual optional<pair<expr, bool>> pre(expr const &);
virtual optional<pair<expr, bool>> post(expr const &);
@ -33,22 +52,19 @@ protected:
expr visit(expr const & e);
public:
dsimplify_core_fn(type_context & ctx, defeq_canonizer::state & s, unsigned max_steps, bool visit_instances);
dsimplify_core_fn(type_context & ctx, defeq_canonizer::state & s, dsimp_config const & cfg);
expr operator()(expr e);
metavar_context const & mctx() const;
};
class dsimplify_fn : public dsimplify_core_fn {
simp_lemmas_for m_simp_lemmas;
bool m_use_eta;
transparency_mode m_md;
expr whnf(expr const & e);
virtual optional<pair<expr, bool>> pre(expr const & e) override;
virtual optional<pair<expr, bool>> post(expr const & e) override;
public:
dsimplify_fn(type_context & ctx, defeq_canonizer::state & s,
unsigned max_steps, bool visit_instances, simp_lemmas_for const & lemmas,
bool use_eta, transparency_mode md = transparency_mode::Reducible);
simp_lemmas_for const & lemmas, dsimp_config const & cfg);
};
void initialize_dsimplify();

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

@ -251,10 +251,12 @@ static expr dsimp(type_context & ctx, transparency_mode md, expr const & e) {
See discussion at ring.lean.
*/
defeq_can_state dcs;
bool visit_instances = false;
unsigned max_steps = 1000000; /* TODO(Leo): add parameter? */
bool use_eta = true;
return dsimplify_fn(ctx, dcs, max_steps, visit_instances, simp_lemmas_for(), use_eta, md)(e);
dsimp_config cfg;
cfg.m_md = md;
cfg.m_canonize_instances = false;
cfg.m_max_steps = 1000000; /* TODO(Leo): add parameter? */
cfg.m_eta = true;
return dsimplify_fn(ctx, dcs, simp_lemmas_for(), cfg)(e);
}
struct mk_hinst_lemma_fn {

9
src/library/tactic/smt/smt_state.cpp
View file

@ -184,8 +184,9 @@ static pair<tactic_state, unsigned> revert_all(tactic_state const & s) {
}
static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) {
unsigned max_steps = cfg.m_max_steps;
bool visit_instances = false;
dsimp_config dcfg;
dcfg.m_max_steps = cfg.m_max_steps;
dcfg.m_canonize_instances = false;
/* We use eta reduction to make sure terms such as (fun x, list x) are reduced to list.
Given (a : nat) (l : list nat) (a ∈ a::l), the elaborator produces
@ -202,11 +203,11 @@ static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_
This is not an issue in this module since it assumes goals do not contain metavariables.
*/
bool use_eta = true;
dcfg.m_eta = true;
simp_lemmas_for eq_lemmas;
if (auto r = cfg.m_simp_lemmas.find(get_eq_name()))
eq_lemmas = *r;
return dsimplify_fn(ctx, dcs, max_steps, visit_instances, eq_lemmas, use_eta);
return dsimplify_fn(ctx, dcs, eq_lemmas, dcfg);
}
static simplify_fn mk_simp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) {

14
src/library/tactic/unfold_tactic.cpp
View file

@ -90,6 +90,12 @@ vm_obj tactic_dunfold_expr_core(vm_obj const & m, vm_obj const & _e, vm_obj cons
}
}
static dsimp_config mk_dsimp_cfg(unsigned max_steps) {
dsimp_config cfg;
cfg.m_max_steps = max_steps;
return cfg;
}
class unfold_core_fn : public dsimplify_core_fn {
protected:
name_set m_cs;
@ -123,9 +129,8 @@ protected:
}
public:
unfold_core_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps,
list<name> const & cs):
dsimplify_core_fn(ctx, dcs, max_steps, true /* visit_instances */),
unfold_core_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, list<name> const & cs):
dsimplify_core_fn(ctx, dcs, mk_dsimp_cfg(max_steps)),
m_cs(to_name_set(cs)) {
}
};
@ -135,8 +140,7 @@ class unfold_fn : public unfold_core_fn {
return unfold_step(e);
}
public:
unfold_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps,
list<name> const & cs):
unfold_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, list<name> const & cs):
unfold_core_fn(ctx, dcs, max_steps, cs) {
}
};

2
tests/lean/1327.lean
View file

@ -1,4 +1,4 @@
example (n) : nat.pred n = n :=
begin
dsimp
dsimp {fail_if_unchaged := ff}
end

3
tests/lean/defeq_simp1.lean
View file

@ -5,14 +5,13 @@ def nat_has_add2 : has_add nat :=
set_option pp.all true
open tactic
local attribute [-simp] id.def
example (a b : nat) (H : @has_add.add nat (id (id nat.has_add)) a b = @has_add.add nat nat_has_add2 a b) : true :=
by do
s ← simp_lemmas.mk_default,
get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
constructor
example (a b : nat) (H : (λ x : nat, @has_add.add nat (id (id nat.has_add)) a b) = (λ x : nat, @has_add.add nat nat_has_add2 a x)) : true :=
by do
s ← simp_lemmas.mk_default,

4
tests/lean/defeq_simp2.lean
View file

@ -10,7 +10,7 @@ axiom foo3 (n : nat) : n ≥ 0
example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
by do
s ← simp_lemmas.mk_default,
get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchaged := ff} >>= trace,
constructor
constant x1 : nat -- update the environment to force defeq_canonize cache to be reset
@ -18,7 +18,7 @@ constant x1 : nat -- update the environment to force defeq_canonize cache to be
example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
by do
s ← simp_lemmas.mk_default,
get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchaged := ff} >>= trace,
constructor
constant x2 : nat -- update the environment to force defeq_canonize cache to be reset

6
tests/lean/defeq_simp4.lean
View file

@ -16,8 +16,10 @@ set_option pp.all true
example (a b : nat) (H : (λ x : nat, @has_add.add nat (nat_has_add3 x) a b) = (λ x : nat, @has_add.add nat nat_has_add2 a x)) : true :=
by do
s ← simp_lemmas.mk_default,
get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchaged := ff} >>= trace,
trace "---------",
-- The following should work
get_local `H >>= infer_type >>= s^.dsimplify >>= s^.dsimplify >>= trace,
e ← get_local `H >>= infer_type,
e ← s^.dsimplify e {fail_if_unchaged := ff},
s^.dsimplify e {fail_if_unchaged := ff} >>= trace,
constructor

13
tests/lean/run/dsimp_at1.lean
View file

@ -1,13 +0,0 @@
open tactic
constants (A : Type.{1}) (x y : A)
noncomputable definition f (z : A) : A := z
@[simp] definition f.def (z:A) : f z = z := rfl
definition foo (z₁ z₂ : A) : f z₁ = f z₂ → z₁ = z₂ :=
by do H ← intro `H,
trace_state,
dsimp_at H,
trace_state,
assumption