From 4ef46551830defe8d849ac34266d1a1cfc2bee23 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Aug 2013 14:26:12 -0700
Subject: [PATCH] Add homogeneous equality

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/ex14.lean                   | 9 +++++++++
 src/frontends/lean/lean_frontend.cpp | 2 +-
 src/frontends/lean/lean_notation.cpp | 4 ++++
 src/kernel/builtin.cpp               | 4 ++++
 src/kernel/builtin.h                 | 6 ++++++
 src/shell/CMakeLists.txt             | 2 ++
 6 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 examples/ex14.lean

diff --git a/examples/ex14.lean b/examples/ex14.lean
new file mode 100644
index 000000000..11444d46c
--- /dev/null
+++ b/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
diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp
index c1bb8bc3f..e71c92f1d 100644
--- a/src/frontends/lean/lean_frontend.cpp
+++ b/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) {
diff --git a/src/frontends/lean/lean_notation.cpp b/src/frontends/lean/lean_notation.cpp
index 87c17f9f8..5aff2c48f 100644
--- a/src/frontends/lean/lean_notation.cpp
+++ b/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());        // "/\"
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index db4be7f41..e6b4acb4b 100644
--- a/src/kernel/builtin.cpp
+++ b/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));
 
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 3616230c0..3a3f37644 100644
--- a/src/kernel/builtin.h
+++ 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 */
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index d1e0f7302..9e37aece2 100644
--- a/src/shell/CMakeLists.txt
+++ 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")