feat(library/tactic/congruence/congruence_closure): hard code support for ne

src/library/constants.cpp

@@ -229,6 +229,7 @@ name const * g_nat_one_lt_bit0 = nullptr;
 name const * g_nat_one_lt_bit1 = nullptr;
 name const * g_nat_le_of_lt = nullptr;
 name const * g_nat_le_refl = nullptr;
+name const * g_ne = nullptr;
 name const * g_neg = nullptr;
 name const * g_neq_of_not_iff = nullptr;
 name const * g_norm_num_add1 = nullptr;
@@ -659,6 +660,7 @@ void initialize_constants() {
     g_nat_one_lt_bit1 = new name{"nat", "one_lt_bit1"};
     g_nat_le_of_lt = new name{"nat", "le_of_lt"};
     g_nat_le_refl = new name{"nat", "le_refl"};
+    g_ne = new name{"ne"};
     g_neg = new name{"neg"};
     g_neq_of_not_iff = new name{"neq_of_not_iff"};
     g_norm_num_add1 = new name{"norm_num", "add1"};
@@ -1090,6 +1092,7 @@ void finalize_constants() {
     delete g_nat_one_lt_bit1;
     delete g_nat_le_of_lt;
     delete g_nat_le_refl;
+    delete g_ne;
     delete g_neg;
     delete g_neq_of_not_iff;
     delete g_norm_num_add1;
@@ -1520,6 +1523,7 @@ name const & get_nat_one_lt_bit0_name() { return *g_nat_one_lt_bit0; }
 name const & get_nat_one_lt_bit1_name() { return *g_nat_one_lt_bit1; }
 name const & get_nat_le_of_lt_name() { return *g_nat_le_of_lt; }
 name const & get_nat_le_refl_name() { return *g_nat_le_refl; }
+name const & get_ne_name() { return *g_ne; }
 name const & get_neg_name() { return *g_neg; }
 name const & get_neq_of_not_iff_name() { return *g_neq_of_not_iff; }
 name const & get_norm_num_add1_name() { return *g_norm_num_add1; }

src/library/constants.h

@@ -231,6 +231,7 @@ name const & get_nat_one_lt_bit0_name();
 name const & get_nat_one_lt_bit1_name();
 name const & get_nat_le_of_lt_name();
 name const & get_nat_le_refl_name();
+name const & get_ne_name();
 name const & get_neg_name();
 name const & get_neq_of_not_iff_name();
 name const & get_norm_num_add1_name();

src/library/constants.txt

@@ -224,6 +224,7 @@ nat.one_lt_bit0
 nat.one_lt_bit1
 nat.le_of_lt
 nat.le_refl
+ne
 neg
 neq_of_not_iff
 norm_num.add1

src/library/tactic/congruence/congruence_closure.cpp

@@ -1215,7 +1215,7 @@ void congruence_closure::add(expr const & type, expr const & proof) {
     flet<congruence_closure *> set_cc(g_cc, this);
     m_todo.clear();
     expr p      = type;
-    bool is_neg = is_not(type, p);
+    bool is_neg = is_not_or_ne(type, p);
     expr lhs, rhs;
     if (is_eq(type, lhs, rhs) || is_heq(type, lhs, rhs)) {
         if (is_neg) {

src/library/util.cpp

@@ -740,15 +740,10 @@ bool is_or(expr const & e, expr & A, expr & B) {
 }
 
 bool is_not(expr const & e, expr & a) {
-    if (is_app(e)) {
-        expr const & f = app_fn(e);
-        if (!is_constant(f) || const_name(f) != get_not_name())
-            return false;
+    if (is_app_of(e, get_not_name(), 1)) {
         a = app_arg(e);
         return true;
-    } else if (is_pi(e)) {
-        if (!is_false(binding_body(e)))
-            return false;
+    } else if (is_pi(e) && is_false(binding_body(e))) {
         a = binding_domain(e);
         return true;
     } else {
@@ -756,6 +751,20 @@ bool is_not(expr const & e, expr & a) {
     }
 }
 
+bool is_not_or_ne(expr const & e, expr & a) {
+    if (is_not(e, a)) {
+        return true;
+    } else if (is_app_of(e, get_ne_name(), 3)) {
+        buffer<expr> args;
+        expr const & fn = get_app_args(e, args);
+        expr new_fn     = mk_constant(get_eq_name(), const_levels(fn));
+        a               = mk_app(new_fn, args);
+        return true;
+    } else {
+        return false;
+    }
+}
+
 expr mk_not(expr const & e) {
     return mk_app(mk_constant(get_not_name()), e);
 }

src/library/util.h

@@ -232,9 +232,11 @@ expr mk_false_rec(abstract_type_context & ctx, expr const & f, expr const & t);
 bool is_or(expr const & e);
 bool is_or(expr const & e, expr & A, expr & B);
 
-/** \brief Return true if \c e is of the form <tt>(not arg)</tt>, and store \c arg in \c a.
+/** \brief Return true if \c e is of the form <tt>(not arg)</tt> or <tt>arg -> false</tt>, and store \c arg in \c a.
      Return false otherwise */
 bool is_not(expr const & e, expr & a);
+/** \brief Extends is_not to handle (lhs ≠ rhs). In the new case, it stores (lhs = rhs) in \c a. */
+bool is_not_or_ne(expr const & e, expr & a);
 expr mk_not(expr const & e);
 
 /** \brief Create the term <tt>absurd e not_e : t</tt>. */