feat(library/simplifier): improve contextual simplifications

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

src/library/simplifier/ceq.cpp

@@ -61,6 +61,9 @@ class to_ceqs_fn {
             } 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 if (is_or(a)) {
+                return apply(mk_and(mk_not(arg(a, 1)), mk_not(arg(a, 2))),
+                             mk_not_or_elim_th(arg(a, 1), arg(a, 2), H));
             } else {
                 expr new_e = mk_iff(a, False);
                 expr new_H = mk_eqf_intro_th(a, H);

tests/lean/simp16.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 ≠ b) ∨ b + c > a)]])
+local s, pr = simplify(t, "simple")
+print(s)
+print(pr)
+print(get_environment():type_check(pr))
+*)

tests/lean/simp16.lean.expected.out

@@ -0,0 +1,17 @@
+  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,
+       trans (or_congr (or_congr (refl (¬ b = 0)) (λ C::2 : ¬ ¬ b = 0, congr2 (neq c) (not_not_elim C::2)))
+                       (λ C::2 : ¬ (¬ b = 0 ∨ c ≠ 0),
+                          congr (congr2 Nat::gt
+                                        (congr (congr2 Nat::add (not_not_elim (and_eliml (not_or_elim C::2))))
+                                               (not_neq_elim (and_elimr (not_or_elim C::2)))))
+                                C::1))
+             (or_falsel (¬ b = 0 ∨ c ≠ 0)))
+a = 1 ∧ ((¬ b = 0 ∨ c ≠ b) ∨ b + c > a) ↔ a = 1 ∧ (¬ b = 0 ∨ c ≠ 0)