feat(library/simplifier): convert disequalities (a ≠ b) into equations '(a = b) = false'

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

src/builtin/kernel.lean

@@ -214,6 +214,9 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
 := boolext (assume H1 : a,     absurd H1 H)
            (assume H2 : false, false_elim a H2)
 
+theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : (a = b) = false
+:= eqf_intro H
+
 theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a)
 := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a))
            (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b))

src/kernel/kernel_decls.cpp

@@ -63,6 +63,7 @@ MK_CONSTANT(boolext_fn, name("boolext"));
 MK_CONSTANT(iff_intro_fn, name("iff_intro"));
 MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));
 MK_CONSTANT(eqf_intro_fn, name("eqf_intro"));
+MK_CONSTANT(neq_elim_fn, name("neq_elim"));
 MK_CONSTANT(or_comm_fn, name("or_comm"));
 MK_CONSTANT(or_assoc_fn, name("or_assoc"));
 MK_CONSTANT(or_id_fn, name("or_id"));

src/kernel/kernel_decls.h

@@ -180,6 +180,9 @@ inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({m
 expr mk_eqf_intro_fn();
 bool is_eqf_intro_fn(expr const & e);
 inline expr mk_eqf_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqf_intro_fn(), e1, e2}); }
+expr mk_neq_elim_fn();
+bool is_neq_elim_fn(expr const & e);
+inline expr mk_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_neq_elim_fn(), e1, e2, e3, e4}); }
 expr mk_or_comm_fn();
 bool is_or_comm_fn(expr const & e);
 inline expr mk_or_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_or_comm_fn(), e1, e2}); }

src/library/simplifier/ceq.cpp

@@ -46,6 +46,13 @@ class to_ceqs_fn {
     list<expr_pair> apply(expr const & e, expr const & H) {
         if (is_eq(e)) {
             return mk_singleton(e, H);
+        } else if (is_neq(e)) {
+            expr T   = arg(e, 1);
+            expr lhs = arg(e, 2);
+            expr rhs = arg(e, 3);
+            expr new_e = mk_eq(Bool, mk_eq(T, lhs, rhs), False);
+            expr new_H = mk_neq_elim_th(T, lhs, rhs, H);
+            return mk_singleton(new_e, new_H);
         } else if (is_not(e)) {
             expr a     = arg(e, 1);
             expr new_e = mk_eq(Bool, a, False);

src/library/simplifier/ceq.h

@@ -19,6 +19,7 @@ namespace lean {
    [if P then Q else R] --->   P -> [Q],  not P -> [Q]
    [P -> Q]             --->   P -> [Q]
    [forall x : A, P]    --->   forall x : A, [P]
+   [a ≠ b]              --->   (a = b) = false
 
    P                    --->   P = true   (if none of the rules above apply and P is not an equality)
 

tests/lua/ceq1.lua

@@ -1,4 +1,5 @@
 local env  = get_environment()
+assert(env:find_object("neq_elim"))
 
 function show_ceqs(ceqs)
    for i = 1, #ceqs do
@@ -24,6 +25,7 @@ parse_lean_cmds([[
    axiom Ax3 : forall x : Nat, not (x = 1) -> if (x < 0) then (g x x = 0) else (g x x < 0 /\ g x 0 = 1 /\ g 0 x = 2)
    axiom Ax4 : forall x y : Nat, f x = x
    axiom Ax5 : forall x y : Nat, f x = y /\ g x y = x
+   axiom Ax6 : forall x : Nat, f x ≠ 0
 ]])
 
 test_ceq("Ax1", 2)
@@ -31,6 +33,7 @@ test_ceq("Ax2", 1)
 test_ceq("Ax3", 4)
 test_ceq("Ax4", 0)
 test_ceq("Ax5", 1)
+test_ceq("Ax6", 1)
 -- test_ceq("eta", 1)
 test_ceq("not_not_eq", 1)
 test_ceq("or_comm", 1)