From 9b35adfc8c8b101f712d7db5671a98fde992da96 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 25 Dec 2016 12:47:17 -0800 Subject: [PATCH] feat(library/tactic/congruence/congruence_closure): add support for constructor equalities --- library/init/logic.lean | 3 ++ src/library/constants.cpp | 4 +++ src/library/constants.h | 1 + src/library/constants.txt | 1 + .../tactic/congruence/congruence_closure.cpp | 32 +++++++++++++----- .../tactic/congruence/congruence_closure.h | 2 +- tests/lean/run/cc_constructors.lean | 33 +++++++++++++++++++ 7 files changed, 66 insertions(+), 10 deletions(-) create mode 100644 tests/lean/run/cc_constructors.lean diff --git a/library/init/logic.lean b/library/init/logic.lean index 14b20606eb..2fd7c6ea35 100644 --- a/library/init/logic.lean +++ b/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⟩ diff --git a/src/library/constants.cpp b/src/library/constants.cpp index c20ee44eac..3f022d2e59 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index 88af109092..1fdcee1705 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 5a189e61f0..97eeb0ec5a 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp index e9ba0934f2..8450757a4b 100644 --- a/src/library/tactic/congruence/congruence_closure.cpp +++ b/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 c1 = is_constructor_app(env(), e1); + optional 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> implied_eqs; + lean_verify(mk_constructor_eq_constructor_implied_eqs(m_ctx, e1, e2, h, implied_eqs)); + for (std::tuple 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) { diff --git a/src/library/tactic/congruence/congruence_closure.h b/src/library/tactic/congruence/congruence_closure.h index d1f8c3cec4..0b2893f390 100644 --- a/src/library/tactic/congruence/congruence_closure.h +++ b/src/library/tactic/congruence/congruence_closure.h @@ -192,7 +192,7 @@ private: optional 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 const & added_prop, bool heq_proof); diff --git a/tests/lean/run/cc_constructors.lean b/tests/lean/run/cc_constructors.lean new file mode 100644 index 0000000000..81ac9764fc --- /dev/null +++ b/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