chore(builtin/kernel): add theorem for rewriter/simplifier

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

src/builtin/kernel.lean

@@ -213,6 +213,9 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
 theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false
 := eqf_intro H
 
+theorem eq_id {A : TypeU} (a : A) : (a = a) ↔ true
+:= eqt_intro (refl a)
+
 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

@@ -64,6 +64,7 @@ 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(eq_id_fn, name("eq_id"));
 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

@@ -183,6 +183,9 @@ inline expr mk_eqf_intro_th(expr const & e1, expr const & e2) { return mk_app({m
 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_eq_id_fn();
+bool is_eq_id_fn(expr const & e);
+inline expr mk_eq_id_th(expr const & e1, expr const & e2) { return mk_app({mk_eq_id_fn(), e1, e2}); }
 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}); }