feat(library/tactic/congruence/congruence_closure): add support for constructor equalities

library/init/logic.lean

@@ -387,6 +387,9 @@ assume h, iff.mp h trivial
 lemma false_of_true_eq_false : (true = false) → false :=
 assume h, h ▸ trivial
 
+lemma true_eq_false_of_false : false → (true = false) :=
+false.elim
+
 /- and simp rules -/
 lemma and.imp (hac : a → c) (hbd : b → d) : a ∧ b → c ∧ d :=
 assume ⟨ha, hb⟩, ⟨hac ha, hbd hb⟩

src/library/constants.cpp

@@ -79,6 +79,7 @@ name const * g_functor = nullptr;
 name const * g_false = nullptr;
 name const * g_false_of_true_iff_false = nullptr;
 name const * g_false_of_true_eq_false = nullptr;
+name const * g_true_eq_false_of_false = nullptr;
 name const * g_false_rec = nullptr;
 name const * g_field = nullptr;
 name const * g_fin = nullptr;
@@ -528,6 +529,7 @@ void initialize_constants() {
     g_false = new name{"false"};
     g_false_of_true_iff_false = new name{"false_of_true_iff_false"};
     g_false_of_true_eq_false = new name{"false_of_true_eq_false"};
+    g_true_eq_false_of_false = new name{"true_eq_false_of_false"};
     g_false_rec = new name{"false", "rec"};
     g_field = new name{"field"};
     g_fin = new name{"fin"};
@@ -978,6 +980,7 @@ void finalize_constants() {
     delete g_false;
     delete g_false_of_true_iff_false;
     delete g_false_of_true_eq_false;
+    delete g_true_eq_false_of_false;
     delete g_false_rec;
     delete g_field;
     delete g_fin;
@@ -1427,6 +1430,7 @@ name const & get_functor_name() { return *g_functor; }
 name const & get_false_name() { return *g_false; }
 name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; }
 name const & get_false_of_true_eq_false_name() { return *g_false_of_true_eq_false; }
+name const & get_true_eq_false_of_false_name() { return *g_true_eq_false_of_false; }
 name const & get_false_rec_name() { return *g_false_rec; }
 name const & get_field_name() { return *g_field; }
 name const & get_fin_name() { return *g_fin; }

src/library/constants.h

@@ -81,6 +81,7 @@ name const & get_functor_name();
 name const & get_false_name();
 name const & get_false_of_true_iff_false_name();
 name const & get_false_of_true_eq_false_name();
+name const & get_true_eq_false_of_false_name();
 name const & get_false_rec_name();
 name const & get_field_name();
 name const & get_fin_name();

src/library/constants.txt

@@ -74,6 +74,7 @@ functor
 false
 false_of_true_iff_false
 false_of_true_eq_false
+true_eq_false_of_false
 false.rec
 field
 fin

src/library/tactic/congruence/congruence_closure.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/comp_val.h"
 #include "library/app_builder.h"
 #include "library/defeq_canonizer.h"
+#include "library/constructions/constructor.h"
 #include "library/tactic/congruence/congruence_closure.h"
 
 namespace lean {
@@ -1145,12 +1146,26 @@ void congruence_closure::check_new_subsingleton_eq(expr const & old_root, expr c
     }
 }
 
-void congruence_closure::propagate_no_confusion_eq(expr const & e1, expr const & e2) {
-    lean_assert(is_constructor_app(env(), e1));
-    lean_assert(is_constructor_app(env(), e2));
+void congruence_closure::propagate_constructor_eq(expr const & e1, expr const & e2) {
+    optional<name> c1 = is_constructor_app(env(), e1);
+    optional<name> c2 = is_constructor_app(env(), e2);
+    lean_assert(c1 && c2);
     expr type       = mk_eq(m_ctx, e1, e2);
-    expr pr         = *get_eq_proof(e1, e2);
-    /* TODO(Leo): use no_confusion to build proofs for arguments */
+    expr h          = *get_eq_proof(e1, e2);
+    bool heq_proof  = false;
+    if (*c1 == *c2) {
+        buffer<std::tuple<expr, expr, expr>> implied_eqs;
+        lean_verify(mk_constructor_eq_constructor_implied_eqs(m_ctx, e1, e2, h, implied_eqs));
+        for (std::tuple<expr, expr, expr> const & t : implied_eqs) {
+            expr lhs, rhs, H;
+            std::tie(lhs, rhs, H) = t;
+            push_todo(lhs, rhs, H, heq_proof);
+        }
+    } else {
+        expr false_pr = *mk_constructor_eq_constructor_inconsistency_proof(m_ctx, e1, e2, h);
+        expr H        = mk_app(mk_constant(get_true_eq_false_of_false_name()), false_pr);
+        push_todo(mk_true(), mk_false(), H, heq_proof);
+    }
 }
 
 void congruence_closure::propagate_value_inconsistency(expr const & e1, expr const & e2) {
@@ -1216,8 +1231,7 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H,
         }
     }
 
-    bool use_no_confusion = r1->m_constructor && r2->m_constructor;
-
+    bool constructor_eq = r1->m_constructor && r2->m_constructor;
     expr e1_root   = n1->m_root;
     expr e2_root   = n2->m_root;
     entry new_n1   = *n1;
@@ -1292,8 +1306,8 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H,
         */
     }
 
-    if (use_no_confusion) {
-        propagate_no_confusion_eq(e1_root, e2_root);
+    if (constructor_eq) {
+        propagate_constructor_eq(e1_root, e2_root);
     }
 
     if (value_inconsistency) {

src/library/tactic/congruence/congruence_closure.h

@@ -192,7 +192,7 @@ private:
     optional<expr> get_eq_proof_core(expr const & e1, expr const & e2, bool as_heq) const;
     void push_subsingleton_eq(expr const & a, expr const & b);
     void check_new_subsingleton_eq(expr const & old_root, expr const & new_root);
-    void propagate_no_confusion_eq(expr const & e1, expr const & e2);
+    void propagate_constructor_eq(expr const & e1, expr const & e2);
     void propagate_value_inconsistency(expr const & e1, expr const & e2);
     void add_eqv_step(expr e1, expr e2, expr const & H,
                       optional<expr> const & added_prop, bool heq_proof);

tests/lean/run/cc_constructors.lean

@@ -0,0 +1,33 @@
+open tactic
+
+example (a b : nat) (s t : list nat) : a::s = b::t → a ≠ b → false :=
+by cc
+
+example (a b : nat) (s t : list nat) : a::s = b::t → t ≠ s → false :=
+by cc
+
+example (a c b : nat) (s t : list nat) : a::s = b::t → a ≠ c → c = b → false :=
+by cc
+
+example (a c b : nat) (s t : list nat) : a::a::s = a::b::t → a ≠ c → c = b → false :=
+by cc
+
+example (a b : nat) (s t r : list nat) : a::s = r → r = b::t → a ≠ b → false :=
+by cc
+
+example (a b : nat) (s t r : list nat) : a::s = r → r = b::t → a = b :=
+by cc
+
+universe variables u
+inductive Vec (α : Type u) : nat → Type (max 1 u)
+| nil  : Vec 0
+| cons : ∀ {n}, α → Vec n → Vec (nat.succ n)
+
+example (α : Type u) (a b c d : α) (n : nat) (s t : Vec α n) : Vec.cons a s = Vec.cons b t → a ≠ b → false :=
+by cc
+
+example (α : Type u) (a b c d : α) (n : nat) (s t : Vec α n) : Vec.cons a s = Vec.cons b t → t ≠ s → false :=
+by cc
+
+example (α : Type u) (a b c d : α) (n : nat) (s t : Vec α n) : Vec.cons a (Vec.cons a s) = Vec.cons a (Vec.cons b t) → b ≠ c → c = a → false :=
+by cc