feat(library/tactic/simplify): add simp!

doc/changes.md

@@ -115,6 +115,14 @@ master branch (aka work in progress branch)
   number of constants used in a goal. For example, we plan to
   add the lemma `f <$> x = x >>= pure ∘ f` to `[norm]`.
 
+* Add `iota_eqn : bool` field to `simp_config`. `simp {iota_eqn := tt}` uses
+  all non trivial equation lemmas generated by equation/pattern-matching compiler.
+  A lemma is considered non trivial if it is not of the form `forall x_1 ... x_n, f x_1 ... x_n = t` and
+  a proof by reflexivity. `simp!` is a shorthand for `simp {iota_eqn := tt}`.
+  For example, given the goal `... |- [1,2].map nat.succ = t`, `simp!` reduces the left-hand-side
+  of the equation to `[nat.succ 1, nat.succ 2]`. In this example, `simp!` is equivalent to
+  `simp [list.map]`.
+
 *Changes*
 
 * Replace `inout` modifier in type class declarations with `out_param` modifier.

library/data/rbtree/insert.lean

@@ -110,7 +110,7 @@ by apply balance.cases l y r; intros; simp [*]; is_searchable_tactic
 
 lemma is_searchable_balance1_node {t} [is_trans α lt] : ∀ {y s lo hi}, is_searchable lt t lo (some y) → is_searchable lt s (some y) hi → is_searchable lt (balance1_node t y s) lo hi :=
 begin
-  cases t; simp [balance1_node]; intros; is_searchable_tactic,
+  cases t; simp!; intros; is_searchable_tactic,
   { cases lo,
     { apply is_searchable_none_low_of_is_searchable_some_low, assumption },
     { simp at *, apply is_searchable_some_low_of_is_searchable_of_lt; assumption } },
@@ -122,7 +122,7 @@ by apply balance.cases l y r; intros; simp [*]; is_searchable_tactic
 
 lemma is_searchable_balance2_node {t} [is_trans α lt] : ∀ {y s lo hi}, is_searchable lt s lo (some y) → is_searchable lt t (some y) hi → is_searchable lt (balance2_node t y s) lo hi :=
 begin
-  induction t; simp [balance2_node]; intros; is_searchable_tactic,
+  induction t; simp!; intros; is_searchable_tactic,
   { cases hi,
     { apply is_searchable_none_high_of_is_searchable_some_high, assumption },
     { simp at *, apply is_searchable_some_high_of_is_searchable_of_lt, assumption' } },
@@ -131,7 +131,7 @@ end
 
 lemma is_searchable_ins {t x} [is_strict_weak_order α lt] : ∀ {lo hi} (h : is_searchable lt t lo hi), lift lt lo (some x) → lift lt (some x) hi → is_searchable lt (ins lt t x) lo hi :=
 begin
-  with_cases { apply ins.induction lt t x; intros; simp [ins, *] at * {eta := ff}; is_searchable_tactic },
+  with_cases { apply ins.induction lt t x; intros; simp! [*] at * {eta := ff}; is_searchable_tactic },
   case is_red_lt { apply ih h_hs₁, assumption, simp [*] },
   case is_red_eq hs₁ { apply is_searchable_of_is_searchable_of_incomp hc, assumption },
   case is_red_eq hs₂ { apply is_searchable_of_incomp_of_is_searchable hc, assumption },

library/init/meta/interactive.lean

@@ -1206,8 +1206,9 @@ The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
 
 `simp with attr₁ ... attrₙ` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr₁]`, ..., `[attrₙ]` or `[simp]`.
 -/
-meta def simp (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
+meta def simp (use_iota_eqn : parse $ (tk "!")?) (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
               (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit :=
+let cfg := if use_iota_eqn.is_none then cfg else {iota_eqn := tt, ..cfg} in
 propagate_tags (simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat)
 
 /--

library/init/meta/simp_tactic.lean

@@ -213,6 +213,7 @@ structure simp_config :=
 (eta  : bool               := tt)
 (proj : bool               := tt) -- reduce projections
 (iota : bool               := tt)
+(iota_eqn : bool           := ff) -- reduce using all equation lemmas generated by equation/pattern-matching compiler
 (constructor_eq : bool     := tt)
 (single_pass : bool        := ff)
 (fail_if_unchanged         := tt)

library/init/meta/smt/interactive.lean

@@ -236,9 +236,9 @@ slift (tactic.interactive.induction p rec_name ids revert)
 open tactic
 
 /-- Simplify the target type of the main goal. -/
-meta def simp (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
-              (cfg : simp_config_ext := {}) : smt_tactic unit :=
-tactic.interactive.simp no_dflt hs attr_names (loc.ns [none]) cfg
+meta def simp (use_iota_eqn : parse $ (tk "!")?) (no_dflt : parse only_flag) (hs : parse simp_arg_list)
+              (attr_names : parse with_ident_list) (cfg : simp_config_ext := {}) : smt_tactic unit :=
+tactic.interactive.simp use_iota_eqn no_dflt hs attr_names (loc.ns [none]) cfg
 
 meta def dsimp (no_dflt : parse only_flag) (es : parse simp_arg_list) (attr_names : parse with_ident_list) : smt_tactic unit :=
 tactic.interactive.dsimp no_dflt es attr_names (loc.ns [none])

src/library/tactic/simplify.cpp

@@ -77,6 +77,7 @@ simp_config::simp_config():
     m_eta(true),
     m_proj(true),
     m_iota(true),
+    m_iota_eqn(false),
     m_constructor_eq(true),
     m_single_pass(false),
     m_fail_if_unchanged(true),
@@ -95,10 +96,11 @@ simp_config::simp_config(vm_obj const & obj) {
     m_eta                = to_bool(cfield(obj, 8));
     m_proj               = to_bool(cfield(obj, 9));
     m_iota               = to_bool(cfield(obj, 10));
-    m_constructor_eq     = to_bool(cfield(obj, 11));
-    m_single_pass        = to_bool(cfield(obj, 12));
-    m_fail_if_unchanged  = to_bool(cfield(obj, 13));
-    m_memoize            = to_bool(cfield(obj, 14));
+    m_iota_eqn           = to_bool(cfield(obj, 11));
+    m_constructor_eq     = to_bool(cfield(obj, 12));
+    m_single_pass        = to_bool(cfield(obj, 13));
+    m_fail_if_unchanged  = to_bool(cfield(obj, 14));
+    m_memoize            = to_bool(cfield(obj, 15));
 }
 
 /* -----------------------------------
@@ -1089,9 +1091,23 @@ optional<pair<simp_result, bool>> simplify_fn::pre(expr const &, optional<expr>
     return no_ext_result();
 }
 
+// TODO(Leo): move to a different file
+static optional<expr> unfold_using_nontrivial_eqns(type_context & ctx, expr const & e) {
+    if (!is_app(e)) return none_expr();
+    expr const & f = get_app_fn(e);
+    if (!is_constant(f)) return none_expr();
+    if (has_simple_eqn_lemma(ctx.env(), const_name(f))) return none_expr();
+    type_context::transparency_scope scope(ctx, transparency_mode::Semireducible);
+    return ctx.unfold_definition(e);
+}
+
 optional<pair<simp_result, bool>> simplify_fn::post(expr const & e, optional<expr> const &) {
     if (auto r = unfold_step(m_ctx, e, m_to_unfold, false))
         return to_ext_result(simp_result(*r));
+    if (m_cfg.m_iota_eqn) {
+        if (auto r = unfold_using_nontrivial_eqns(m_ctx, e))
+            return to_ext_result(simp_result(*r));
+    }
     simp_result r = rewrite(e);
     if (r.get_new() != e) {
         return to_ext_result(r);

src/library/tactic/simplify.h

@@ -26,6 +26,7 @@ structure simp_config :=
 (eta  : bool)
 (proj : bool)
 (iota : bool)
+(iota_eqn : bool)
 (constructor_eq : bool)
 (single_pass : bool)
 (fail_if_unchaged : bool)
@@ -43,6 +44,7 @@ struct simp_config {
     bool                      m_eta;
     bool                      m_proj;
     bool                      m_iota;
+    bool                      m_iota_eqn;
     bool                      m_constructor_eq;
     bool                      m_single_pass;
     bool                      m_fail_if_unchanged;

src/library/type_context.h

@@ -758,6 +758,8 @@ class type_context : public abstract_type_context {
     virtual expr relaxed_whnf(expr const & e) override;
     virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) override;
 
+    optional<expr> unfold_definition(expr const & e);
+
     /** Non destructive is_def_eq (i.e., metavariables cannot be assigned) */
     bool pure_is_def_eq(level const & l1, level const & l2) {
         flet<bool> no_update_left(m_update_left, false);
@@ -965,7 +967,6 @@ class type_context : public abstract_type_context {
 private:
     void init_core(transparency_mode m);
     optional<expr> unfold_definition_core(expr const & e);
-    optional<expr> unfold_definition(expr const & e);
     bool should_unfold_macro(expr const & e);
     expr whnf_core(expr const & e, bool iota_proj_reduce);
     optional<declaration> is_transparent(transparency_mode m, name const & n);

tests/lean/run/simp_iota_eqn.lean

@@ -0,0 +1,29 @@
+def f {α : Type} (a : α) : α :=
+a
+
+example (a : nat) (h : a = 3) : [1,2].map nat.succ = [2, f a] :=
+begin
+  simp!,
+  guard_target nat.succ 2 = f a,
+  simp [f, h]
+end
+
+def foo : bool → bool → bool
+| tt tt := tt
+| ff ff := tt
+| _  _  := ff
+
+example : foo tt tt = f tt :=
+begin
+  simp!,
+  guard_target tt = f tt,
+  simp [f]
+end
+
+example (b : bool) (h : b = tt) : foo b tt = f tt :=
+begin
+  fail_if_success { simp! },
+  simp! [h],
+  guard_target tt = f tt,
+  simp [f]
+end