From 1ec8f9d536410c8b49c22e14bd3479ebb17155ee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Dec 2013 13:56:38 -0800
Subject: [PATCH] feat(kernel): add abstraction (aka function extensionality)
 axiom

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/notation.cpp   | 1 +
 src/kernel/builtin.cpp            | 5 +++++
 src/kernel/builtin.h              | 5 +++++
 tests/lean/abst.lean              | 5 +++++
 tests/lean/abst.lean.expected.out | 8 ++++++++
 5 files changed, 24 insertions(+)
 create mode 100644 tests/lean/abst.lean
 create mode 100644 tests/lean/abst.lean.expected.out

diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
index 99eb8becb0..a238f90db1 100644
--- a/src/frontends/lean/notation.cpp
+++ b/src/frontends/lean/notation.cpp
@@ -92,6 +92,7 @@ void init_builtin_notation(frontend & f) {
     f.mark_implicit_arguments("SubstP", {true, true, true, false, false, false});
     f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, true, false, false});
     f.mark_implicit_arguments(mk_eta_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_abst_fn(), {true, true, true, true, false});
     f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false});
     f.mark_implicit_arguments(mk_dom_inj_fn(), {true, true, true, true, false});
     f.mark_implicit_arguments(mk_ran_inj_fn(), {true, true, true, true, false, false});
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index da6fa2c21d..2fc764160c 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -203,6 +203,7 @@ MK_CONSTANT(trans_ext_fn,   name("TransExt"));
 MK_CONSTANT(subst_fn,       name("Subst"));
 MK_CONSTANT(eta_fn,         name("Eta"));
 MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
+MK_CONSTANT(abst_fn,        name("Abst"));
 
 void import_basic(environment & env) {
     if (!env.mark_builtin_imported("basic"))
@@ -213,6 +214,7 @@ void import_basic(environment & env) {
     expr p1        = Bool >> Bool;
     expr p2        = Bool >> p1;
     expr f         = Const("f");
+    expr g         = Const("g");
     expr a         = Const("a");
     expr b         = Const("b");
     expr c         = Const("c");
@@ -281,5 +283,8 @@ void import_basic(environment & env) {
 
     // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
     env.add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b)));
+
+    // Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g
+    env.add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g)));
 }
 }
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 05cbdea012..6bcb2701d1 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -181,6 +181,11 @@ expr mk_imp_antisym_fn();
 /** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */
 inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); }
 
+/** \brief Abstraction axiom */
+expr mk_abst_fn();
+/** \brief (Axiom) {A : Type u} {B : A -> Type u}, f g : {Pi x : A, B x}, H : (Pi x : A, (f x) = (g x)) |- Abst(A, B, f, g, H) : f = g */
+inline expr Abst(expr const & A, expr const & B, expr const & f, expr const & g, expr const & H) { return mk_app({mk_abst_fn(), A, B, f, g, H}); }
+
 class environment;
 /** \brief Initialize the environment with basic builtin declarations and axioms */
 void import_basic(environment & env);
diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean
new file mode 100644
index 0000000000..960f40e5e2
--- /dev/null
+++ b/tests/lean/abst.lean
@@ -0,0 +1,5 @@
+Axiom PlusComm(a b : Int) : a + b == b + a.
+Variable a : Int.
+Check (Abst (fun x : Int, (PlusComm a x))).
+Set pp::implicit true.
+Check (Abst (fun x : Int, (PlusComm a x))).
diff --git a/tests/lean/abst.lean.expected.out b/tests/lean/abst.lean.expected.out
new file mode 100644
index 0000000000..f89d91a491
--- /dev/null
+++ b/tests/lean/abst.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: PlusComm
+  Assumed: a
+Abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a)
+  Set: lean::pp::implicit
+Abst::explicit ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
+    (λ x : ℤ, a + x) == (λ x : ℤ, x + a)