From 52d4189805e76b608b4f891254894fdea185c930 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Jun 2017 17:09:44 -0700 Subject: [PATCH] feat(library/tactic): add `dsimp_config` configuration object for the `dsimp` tactic family 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 --- doc/changes.md | 2 + library/init/data/int/bitwise.lean | 2 +- library/init/data/list/lemmas.lean | 2 +- library/init/data/nat/bitwise.lean | 4 +- library/init/meta/interactive.lean | 15 ++-- library/init/meta/simp_tactic.lean | 52 +++++++------ library/smt/array.lean | 4 +- src/library/tactic/dsimplify.cpp | 97 ++++++++++++++++--------- src/library/tactic/dsimplify.h | 32 ++++++-- src/library/tactic/smt/hinst_lemmas.cpp | 10 ++- src/library/tactic/smt/smt_state.cpp | 9 ++- src/library/tactic/unfold_tactic.cpp | 14 ++-- tests/lean/1327.lean | 2 +- tests/lean/defeq_simp1.lean | 3 +- tests/lean/defeq_simp2.lean | 4 +- tests/lean/defeq_simp4.lean | 6 +- tests/lean/run/dsimp_at1.lean | 13 ---- 17 files changed, 160 insertions(+), 111 deletions(-) delete mode 100644 tests/lean/run/dsimp_at1.lean diff --git a/doc/changes.md b/doc/changes.md index d1b2487105..652a9b34f7 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -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) ------------- diff --git a/library/init/data/int/bitwise.lean b/library/init/data/int/bitwise.lean index 0aa7508c6d..2bca0f6bd3 100644 --- a/library/init/data/int/bitwise.lean +++ b/library/init/data/int/bitwise.lean @@ -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 diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index 4b51ef669b..fdbced6524 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -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 -/ diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index 24dbfc60a0..3cf887f709 100644 --- a/library/init/data/nat/bitwise.lean +++ b/library/init/data/nat/bitwise.lean @@ -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) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 94a26bce24..2e8b0a10be 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -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. diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 91473ec63b..fd1c9a552d 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -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 diff --git a/library/smt/array.lean b/library/smt/array.lean index e324f1bc0a..d647c6d1db 100644 --- a/library/smt/array.lean +++ b/library/smt/array.lean @@ -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 diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp index a8ca35da5a..9269856fe5 100644 --- a/src/library/tactic/dsimplify.cpp +++ b/src/library/tactic/dsimplify.cpp @@ -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> 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> 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> dsimplify_fn::pre(expr const & e) { optional> 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> 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>(); @@ -259,12 +283,9 @@ optional> dsimplify_fn::post(expr const & e) { return optional>(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::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::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() { diff --git a/src/library/tactic/dsimplify.h b/src/library/tactic/dsimplify.h index d53df72d17..f5d632e5c3 100644 --- a/src/library/tactic/dsimplify.h +++ b/src/library/tactic/dsimplify.h @@ -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 m_cache; unsigned m_num_steps; bool m_need_restart; - - unsigned m_max_steps; - bool m_visit_instances; + dsimp_config m_cfg; virtual optional> pre(expr const &); virtual optional> 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> pre(expr const & e) override; virtual optional> 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(); diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp index 6f261c246c..bdb12b1cf4 100644 --- a/src/library/tactic/smt/hinst_lemmas.cpp +++ b/src/library/tactic/smt/hinst_lemmas.cpp @@ -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 { diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index fb1945983b..256cb809aa 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -184,8 +184,9 @@ static pair 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) { diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp index ca9937d53b..5b4df64af1 100644 --- a/src/library/tactic/unfold_tactic.cpp +++ b/src/library/tactic/unfold_tactic.cpp @@ -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 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 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 const & cs): + unfold_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, list const & cs): unfold_core_fn(ctx, dcs, max_steps, cs) { } }; diff --git a/tests/lean/1327.lean b/tests/lean/1327.lean index dcee0c2055..ba1916c45f 100644 --- a/tests/lean/1327.lean +++ b/tests/lean/1327.lean @@ -1,4 +1,4 @@ example (n) : nat.pred n = n := begin - dsimp + dsimp {fail_if_unchaged := ff} end diff --git a/tests/lean/defeq_simp1.lean b/tests/lean/defeq_simp1.lean index 9f921819c1..d802dfe940 100644 --- a/tests/lean/defeq_simp1.lean +++ b/tests/lean/defeq_simp1.lean @@ -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, diff --git a/tests/lean/defeq_simp2.lean b/tests/lean/defeq_simp2.lean index bb1e03866a..3018163227 100644 --- a/tests/lean/defeq_simp2.lean +++ b/tests/lean/defeq_simp2.lean @@ -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 diff --git a/tests/lean/defeq_simp4.lean b/tests/lean/defeq_simp4.lean index 59455d1a63..8a92a37cea 100644 --- a/tests/lean/defeq_simp4.lean +++ b/tests/lean/defeq_simp4.lean @@ -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 diff --git a/tests/lean/run/dsimp_at1.lean b/tests/lean/run/dsimp_at1.lean deleted file mode 100644 index 1e077afe19..0000000000 --- a/tests/lean/run/dsimp_at1.lean +++ /dev/null @@ -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