feat(library/tactic/simplify): simp reduces c a_1 ... a_n = c b_1 ... b_n into a_1 = b_1 /\ ... /\ a_n = b_n

doc/changes.md

@@ -97,6 +97,9 @@ master branch (aka work in progress branch)
 * `simp` now reduces equalities `c_1 ... = c_2 ...` to `false` if `c_1` and `c_2` are distinct
    constructors. This feature can be disabled using `simp {constructor_eq := ff}`.
 
+* `simp` now reduces equalities `c a_1 ... a_n = c b_1 ... b_n` to `a_1 = b_1 /\ ... /\ a_n = b_n` if `c` is a constructor.
+   This feature can be disabled using `simp {constructor_eq := ff}`.
+
 * `subst` and `subst_vars` now support heterogeneous equalities that are actually homogeneous
    (i.e., `@heq α a β b` where `α` and `β` are definitionally equal).
 

library/data/rbmap/default.lean

@@ -60,7 +60,7 @@ end
 lemma eq_some_of_to_value_eq_some {e : option (α × β)} {v : β} : to_value e = some v → ∃ k, e = some (k, v) :=
 begin
   cases e with val; simp [to_value],
-    { cases val, simp, intro h, injection h, subst v, constructor, refl }
+    { cases val, simp, intro h, subst v, constructor, refl }
 end
 
 lemma eq_none_of_to_value_eq_none {e : option (α × β)} : to_value e = none → e = none :=

library/data/rbtree/find.lean

@@ -114,7 +114,7 @@ begin
         { have hyx : lift lt (some y) (some x) := (range hs_hs₂ (mem_of_mem_exact hm)).1,
           simp [lift] at hyx,
           exact absurd hyx h.2 } },
-      { intro hm, injection hm, simp [*] } },
+      { intro hm, simp [*] } },
     {
       cases hs,
       apply iff.intro,
@@ -137,7 +137,7 @@ begin
   apply find.induction lt t x; intros; simp only [mem, find, *] at *,
   iterate 2 {
     { cases hs, exact ih hs_hs₁ rfl },
-    { injection he, subst y, simp at h, exact h },
+    { subst y, simp at h, exact h },
     { cases hs, exact ih hs_hs₂ rfl } }
 end
 

library/data/rbtree/min_max.lean

@@ -15,7 +15,7 @@ begin
    { intros, contradiction },
    all_goals {
      cases t_lchild; simp [rbnode.min]; intro h,
-     { injection h, subst t_val, simp [mem, irrefl_of lt a] },
+     { subst t_val, simp [mem, irrefl_of lt a] },
      all_goals { rw [mem], simp [t_ih_lchild h] } }
 end
 
@@ -25,7 +25,7 @@ begin
    { intros, contradiction },
    all_goals {
      cases t_rchild; simp [rbnode.max]; intro h,
-     { injection h, subst t_val, simp [mem, irrefl_of lt a] },
+     { subst t_val, simp [mem, irrefl_of lt a] },
      all_goals { rw [mem], simp [t_ih_rchild h] } }
 end
 
@@ -55,7 +55,7 @@ begin
   { simp [strict_weak_order.equiv], intros _ _ hs hmin b, contradiction },
   all_goals {
     cases t_lchild; intros lo hi hs hmin b hmem,
-    { simp [rbnode.min] at hmin, injection hmin, subst t_val,
+    { simp [rbnode.min] at hmin, subst t_val,
       simp [mem] at hmem, cases hmem with heqv hmem,
       { left, exact heqv.swap },
       { have := lt_of_mem_right hs (by constructor) hmem,
@@ -80,7 +80,7 @@ begin
   { simp [strict_weak_order.equiv], intros _ _ hs hmax b, contradiction },
   all_goals {
     cases t_rchild; intros lo hi hs hmax b hmem,
-    { simp [rbnode.max] at hmax, injection hmax, subst t_val,
+    { simp [rbnode.max] at hmax, subst t_val,
       simp [mem] at hmem, cases hmem with hmem heqv,
       { have := lt_of_mem_left hs (by constructor) hmem,
         right, assumption },

library/data/stream.lean

@@ -464,7 +464,7 @@ theorem take_theorem (s₁ s₂ : stream α) : (∀ (n : nat), approx n s₁ = a
 begin
   intro h, apply stream.ext, intro n,
   induction n with n ih,
-  { have aux := h 1, unfold approx at aux, injection aux },
+  { have aux := h 1, simp [approx] at aux, exact aux },
   { have h₁ : some (nth (succ n) s₁) = some (nth (succ n) s₂),
     { rw [← nth_approx, ← nth_approx, h (succ (succ n))] },
     injection h₁ }

library/init/data/nat/lemmas.lean

@@ -47,7 +47,7 @@ left_comm nat.add nat.add_comm nat.add_assoc
 protected lemma add_left_cancel : ∀ {n m k : ℕ}, n + m = n + k → m = k
 | 0        m k := by simp [nat.zero_add] {contextual := tt}
 | (succ n) m k := λ h,
-  have n+m = n+k, by simp [succ_add] at h; injection h,
+  have n+m = n+k, by { simp [succ_add] at h, assumption },
   add_left_cancel this
 
 protected lemma add_right_cancel {n m k : ℕ} (h : n + m = k + m) : n = k :=
@@ -427,14 +427,14 @@ protected lemma bit0_inj : ∀ {n m : ℕ}, bit0 n = bit0 m → n = m
 | (n+1) 0     h := by contradiction
 | (n+1) (m+1) h :=
   have succ (succ (n + n)) = succ (succ (m + m)),
-  begin unfold bit0 at h, simp [add_one, add_succ, succ_add] at h, exact h end,
+  begin unfold bit0 at h, simp [add_one, add_succ, succ_add] at h, rw h end,
   have n + n = m + m, by iterate { injection this with this },
   have n = m, from bit0_inj this,
   by rw this
 
 protected lemma bit1_inj : ∀ {n m : ℕ}, bit1 n = bit1 m → n = m :=
 λ n m h,
-have succ (bit0 n) = succ (bit0 m), begin simp [nat.bit1_eq_succ_bit0] at h, assumption end,
+have succ (bit0 n) = succ (bit0 m), begin simp [nat.bit1_eq_succ_bit0] at h, rw h end,
 have bit0 n = bit0 m, by injection this,
 nat.bit0_inj this
 

library/init/meta/interactive.lean

@@ -1390,6 +1390,7 @@ structure unfold_config extends simp_config :=
 (proj               := ff)
 (eta                := ff)
 (canonize_instances := ff)
+(constructor_eq     := ff)
 
 namespace interactive
 open interactive interactive.types expr
@@ -1630,7 +1631,7 @@ by tactic.mk_inj_eq
 lemma psigma.mk.inj_eq {α : Sort u} {β : α → Sort v} (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) : (psigma.mk a₁ b₁ = psigma.mk a₂ b₂) = (a₁ = a₂ ∧ b₁ == b₂) :=
 by tactic.mk_inj_eq
 
-lemma subtype.mk.inj_eq {α : Type u} {p : α → Prop} (a₁ : α) (h₁ : p a₁) (a₂ : α) (h₂ : p a₂) : (subtype.mk a₁ h₁ = subtype.mk a₂ h₂) = (a₁ = a₂) :=
+lemma subtype.mk.inj_eq {α : Sort u} {p : α → Prop} (a₁ : α) (h₁ : p a₁) (a₂ : α) (h₂ : p a₂) : (subtype.mk a₁ h₁ = subtype.mk a₂ h₂) = (a₁ = a₂) :=
 by tactic.mk_inj_eq
 
 lemma option.some.inj_eq {α : Type u} (a₁ a₂ : α) : (some a₁ = some a₂) = (a₁ = a₂) :=

library/init/native/result.lean

@@ -67,7 +67,7 @@ section resultT
    bind_assoc := begin
      intros,
      cases x, simp,
-     apply congr_arg, rw [monad.bind_assoc],
+     rw [monad.bind_assoc],
      apply congr_arg, funext,
      cases x with e a; simp,
      { cases f a, refl },

src/library/inductive_compiler/nested.cpp

@@ -1554,6 +1554,7 @@ class add_nested_inductive_decl_fn {
         cfg.m_canonize_proofs    = false;
         cfg.m_use_axioms         = false;
         cfg.m_zeta               = false;
+        cfg.m_constructor_eq     = false;
         return cfg;
     }
 

src/library/tactic/simplify.cpp

@@ -34,6 +34,7 @@ Author: Daniel Selsam, Leonardo de Moura
 #include "library/congr_lemma.h"
 #include "library/fun_info.h"
 #include "library/constructions/constructor.h"
+#include "library/constructions/injective.h"
 #include "library/inductive_compiler/ginductive.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_option.h"
@@ -671,10 +672,10 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
             break;
         }
 
-        if (m_cfg.m_constructor_eq)
-            new_result = simplify_constructor_eq_constructor(new_result);
-
-        if (auto r2 = post(new_result.get_new(), parent)) {
+        if (m_cfg.m_constructor_eq && simplify_constructor_eq_constructor(new_result)) {
+            curr_result = new_result;
+            /* continue simplifying */
+        } else if (auto r2 = post(new_result.get_new(), parent)) {
             if (!r2->second) {
                 curr_result = join(new_result, r2->first);
                 break;
@@ -770,28 +771,60 @@ simp_result simplify_core_fn::visit_app(expr const & _e) {
     return simp_result(e);
 }
 
-simp_result simplify_core_fn::simplify_constructor_eq_constructor(simp_result const & r) {
+bool simplify_core_fn::simplify_constructor_eq_constructor(simp_result & r) {
     if (m_rel != get_eq_name())
-        return r; /* TODO(Leo): we can add support for <-> */
-    expr lhs, rhs;
-    if (!is_eq(r.get_new(), lhs, rhs))
-        return r;
+        return false; /* TODO(Leo): we can add support for <-> */
+    expr A, lhs, rhs;
+    if (!is_eq(r.get_new(), A, lhs, rhs))
+        return false;
     optional<name> c1 = is_gintro_rule_app(m_ctx.env(), lhs);
-    if (!c1) return r;
+    if (!c1) return false;
     optional<name> c2 = is_gintro_rule_app(m_ctx.env(), rhs);
-    if (!c2) return r;
+    if (!c2) return false;
 
     if (*c1 != *c2) {
         if (optional<expr> not_eq_prf = mk_constructor_ne_constructor_proof(m_ctx, lhs, rhs)) {
             expr eq_false_prf = mk_app(m_ctx, get_eq_false_intro_name(), *not_eq_prf);
             simp_result new_r(mk_false(), eq_false_prf);
-            return join_eq(m_ctx, r, new_r);
+            r = join_eq(m_ctx, r, new_r);
+            return true;
         } else {
-            return r;
+            return false;
         }
     } else {
-        /* TODO(Leo) */
-        return r;
+        A = whnf_ginductive(m_ctx, A);
+        expr const & A_fn   = get_app_fn(A);
+        if (!is_constant(A_fn) || !is_ginductive(m_ctx.env(), const_name(A_fn)))
+            return false;
+        unsigned A_nparams = get_ginductive_num_params(m_ctx.env(), const_name(A_fn));
+        if (get_app_num_args(lhs) <= A_nparams)
+            return false;
+        name inj_eq_name = mk_injective_eq_name(*c1);
+        optional<declaration> inj_eq_decl = m_ctx.env().find(inj_eq_name);
+        if (!inj_eq_decl)
+            return false;
+        /* We use the `*.inj` lemma for computing the arguments for `*.inj_eq` lemma. */
+        try {
+            name inj_name = mk_injective_name(*c1);
+            optional<declaration> inj_decl = m_ctx.env().find(inj_name);
+            if (!inj_decl)
+                return false;
+            unsigned inj_arity = get_arity(inj_decl->get_type());
+            type_context::tmp_locals locals(m_ctx);
+            expr H   = locals.push_local("_h", r.get_new());
+            expr inj = mk_app(m_ctx, inj_name, inj_arity, H);
+            buffer<expr> inj_args;
+            expr const & inj_fn = get_app_args(inj, inj_args);
+            expr inj_eq_pr = mk_app(mk_constant(inj_eq_name, const_levels(inj_fn)), inj_args.size() - 1, inj_args.data());
+            expr inj_eq    = m_ctx.infer(inj_eq_pr);
+            expr new_lhs, new_rhs;
+            lean_verify(is_eq(inj_eq, new_lhs, new_rhs));
+            simp_result new_r(new_rhs, inj_eq_pr);
+            r = join_eq(m_ctx, r, new_r);
+            return true;
+        } catch (exception &) {
+            return false;
+        }
     }
 }
 

src/library/tactic/simplify.h

@@ -121,8 +121,10 @@ protected:
     simp_result propext_rewrite(expr const & e);
 
     /* Simplify equalities of the form (c ... = c' ...) where `c` and `c'` are
-       constructors. */
-    simp_result simplify_constructor_eq_constructor(simp_result const & r);
+       constructors.
+
+       Return true if `r` was simplified. */
+    bool simplify_constructor_eq_constructor(simp_result & r);
 
     /* Visitors */
     virtual optional<pair<simp_result, bool>> pre(expr const & e, optional<expr> const & parent);

tests/lean/run/simp_constructor.lean

@@ -11,8 +11,6 @@ end
 example : ¬ term.var "a" = term.app "f" [] :=
 by simp
 
-#check @term.app.inj_eq
-
 universes u
 
 inductive vec (α : Type u) : nat → Type u
@@ -35,3 +33,21 @@ with Expr_list : Type
 | cons : Expr → Expr_list → Expr_list
 
 #check @Expr.app.inj_eq
+
+example {α : Type u} (n : nat) (a₁ a₂ : α) (t : vec α n) (h : vec.cons a₁ t = vec.cons a₂ t) : a₁ = a₂ :=
+begin
+  simp at h,
+  exact h
+end
+
+example (a₁ a₂ : nat) (h₁ : a₁ > 0) (h₂ : a₂ > 0) (h : a₁ = a₂) : subtype.mk a₁ h₁ = subtype.mk a₂ h₂ :=
+begin
+  simp,
+  exact h
+end
+
+example (a₁ a₂ : nat) (h₁ : a₁ > 0) (h₂ : a₂ > 0) (h : subtype.mk a₁ h₁ = subtype.mk a₂ h₂) : a₁ = a₂ :=
+begin
+  simp at h,
+  exact h
+end