feat(library/simplifier): improve contextual simplifications

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/kernel.lean

@@ -339,6 +339,12 @@ theorem not_true : ¬ true ↔ false
 theorem not_false : ¬ false ↔ true
 := trivial
 
+theorem not_neq {A : TypeU} (a b : A) : ¬ (a ≠ b) ↔ a = b
+:= not_not_eq (a = b)
+
+theorem not_neq_elim {A : TypeU} {a b : A} (H : ¬ (a ≠ b)) : a = b
+:= (not_neq a b) ◂ H
+
 theorem not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b
 := case (λ x, ¬ (x ∧ b) ↔ ¬ x ∨ ¬ b)
         (case (λ y, ¬ (true ∧ y) ↔ ¬ true ∨ ¬ y)   trivial trivial b)

src/kernel/kernel_decls.cpp

@@ -97,6 +97,8 @@ MK_CONSTANT(imp_falser_fn, name("imp_falser"));
 MK_CONSTANT(imp_falsel_fn, name("imp_falsel"));
 MK_CONSTANT(not_true, name("not_true"));
 MK_CONSTANT(not_false, name("not_false"));
+MK_CONSTANT(not_neq_fn, name("not_neq"));
+MK_CONSTANT(not_neq_elim_fn, name("not_neq_elim"));
 MK_CONSTANT(not_and_fn, name("not_and"));
 MK_CONSTANT(not_and_elim_fn, name("not_and_elim"));
 MK_CONSTANT(not_or_fn, name("not_or"));

src/kernel/kernel_decls.h

@@ -282,6 +282,12 @@ expr mk_not_true();
 bool is_not_true(expr const & e);
 expr mk_not_false();
 bool is_not_false(expr const & e);
+expr mk_not_neq_fn();
+bool is_not_neq_fn(expr const & e);
+inline expr mk_not_neq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_neq_fn(), e1, e2, e3}); }
+expr mk_not_neq_elim_fn();
+bool is_not_neq_elim_fn(expr const & e);
+inline expr mk_not_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_not_neq_elim_fn(), e1, e2, e3, e4}); }
 expr mk_not_and_fn();
 bool is_not_and_fn(expr const & e);
 inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); }

src/library/simplifier/ceq.cpp

@@ -56,9 +56,16 @@ class to_ceqs_fn {
             return mk_singleton(new_e, new_H);
         } else if (is_not(e)) {
             expr a     = arg(e, 1);
-            expr new_e = mk_iff(a, False);
+            if (is_not(a)) {
-            expr new_H = mk_eqf_intro_th(a, H);
+                return apply(arg(a, 1), mk_not_not_elim_th(arg(a, 1), H));
-            return mk_singleton(new_e, new_H);
+            } else if (is_neq(a)) {
+                return mk_singleton(update_app(a, 0, mk_eq_fn()),
+                                    mk_not_neq_elim_th(arg(a, 1), arg(a, 2), arg(a, 3), H));
+            } else {
+                expr new_e = mk_iff(a, False);
+                expr new_H = mk_eqf_intro_th(a, H);
+                return mk_singleton(new_e, new_H);
+            }
         } else if (is_and(e)) {
             expr a1     = arg(e, 1);
             expr a2     = arg(e, 2);

tests/lean/simp14.lean

@@ -0,0 +1,16 @@
+rewrite_set simple
+add_rewrite and_truer and_truel and_falser and_falsel or_falsel : simple
+(*
+  add_congr_theorem("simple", "and_congr")
+  add_congr_theorem("simple", "or_congr")
+*)
+
+variables a b c : Nat
+
+(*
+local t = parse_lean([[a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a)]])
+local s, pr = simplify(t, "simple")
+print(s)
+print(pr)
+print(get_environment():type_check(pr))
+*)

tests/lean/simp14.lean.expected.out

@@ -0,0 +1,18 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+  Assumed: c
+a = 1 ∧ (¬ b = 0 ∨ c ≠ 0)
+and_congr
+    (refl (a = 1))
+    (λ C::1 : a = 1,
+       or_congr (refl (¬ b = 0))
+                (λ C::2 : ¬ ¬ b = 0,
+                   trans (or_congr (refl (c ≠ 0))
+                                   (λ C::3 : ¬ c ≠ 0,
+                                      congr (congr2 Nat::gt
+                                                    (congr (congr2 Nat::add (not_not_elim C::2)) (not_neq_elim C::3)))
+                                            C::1))
+                         (or_falsel (c ≠ 0))))
+a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a) ↔ a = 1 ∧ (¬ b = 0 ∨ c ≠ 0)