Add homogeneous equality

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

examples/ex14.lean

@@ -0,0 +1,9 @@
+Variable N : Type
+Variable a : N
+Variable b : N
+Show a ≃ b
+Check a ≃ b
+Set lean::pp::implicit true
+Show a ≃ b
+Show (Type 1) ≃ (Type 1)
+Show true ≃ false

src/frontends/lean/lean_frontend.cpp

@@ -283,8 +283,8 @@ struct frontend::imp {
 };
 
 frontend::frontend():m_imp(new imp(*this)) {
-    init_builtin_notation(*this);
     init_toplevel(m_imp->m_env);
+    init_builtin_notation(*this);
     m_imp->m_state.set_formatter(mk_pp_formatter(*this));
 }
 frontend::frontend(imp * new_ptr):m_imp(new_ptr) {

src/frontends/lean/lean_notation.cpp

@@ -12,6 +12,10 @@ namespace lean {
    \brief Initialize builtin notation.
 */
 void init_builtin_notation(frontend & f) {
+    f.mark_implicit_arguments("heq", {true, false, false});
+    f.add_infix("==", 50, mk_homo_eq_fn());
+    f.add_infix("≃",  50, mk_homo_eq_fn());
+
     f.add_prefix("\u00ac", 40, mk_not_fn());     // "¬"
     f.add_infixr("&&", 35, mk_and_fn());         // "&&"
     f.add_infixr("/\\", 35, mk_and_fn());        // "/\"

src/kernel/builtin.cpp

@@ -183,6 +183,7 @@ MK_CONSTANT(or_fn,      name("or"));
 MK_CONSTANT(not_fn,     name("not"));
 MK_CONSTANT(forall_fn,  name("forall"));
 MK_CONSTANT(exists_fn,  name("exists"));
+MK_CONSTANT(homo_eq_fn, name("heq"));
 
 // Axioms
 MK_CONSTANT(mp_fn,          name("MP"));
@@ -238,6 +239,9 @@ void add_basic_theory(environment & env) {
     // TODO: introduce epsilon
     env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
 
+    // homogeneous equality
+    env.add_definition(homo_eq_fn_name, Pi({A,TypeU}, A >> (A >> Bool)), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
+
     // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
     env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
 

src/kernel/builtin.h

@@ -109,6 +109,12 @@ expr mk_exists_fn();
 inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); }
 inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
 
+/** \brief Homogeneous equality. It has type: <tt>Pi (A : Type), A -> A -> Bool */
+expr mk_homo_eq_fn();
+/** \brief Return the term (homo_eq A l r) */
+inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }
+inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); }
+
 /** \brief Modus Ponens axiom */
 expr mk_mp_fn();
 /** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : a |- MP(a, b, H1, H2) : b */

src/shell/CMakeLists.txt

@@ -14,3 +14,5 @@ add_test(lean9 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/
 add_test(lean10 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex10.lean")
 add_test(lean11 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex11.lean")
 add_test(lean12 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex12.lean")
+add_test(lean13 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex13.lean")
+add_test(lean14 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex14.lean")