From 032f5cd7b3e7a30dd7a9af21c8cd8e4db83a149e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Oct 2013 10:45:34 -0700
Subject: [PATCH] feat(frontends/lean): make the 'expression template' argument
 in Subst implicit because higher-order matching can infer it.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/notation.cpp    |  9 ++++++++-
 tests/lean/bad5.lean               |  2 +-
 tests/lean/bad5.lean.expected.out  |  2 +-
 tests/lean/ho.lean                 |  2 +-
 tests/lean/ho.lean.expected.out    |  2 +-
 tests/lean/subst.lean              |  9 +++++++++
 tests/lean/subst.lean.expected.out | 12 ++++++++++++
 7 files changed, 33 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/subst.lean
 create mode 100644 tests/lean/subst.lean.expected.out

diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
index 5466161bc1..70b834dcdf 100644
--- a/src/frontends/lean/notation.cpp
+++ b/src/frontends/lean/notation.cpp
@@ -11,6 +11,11 @@ Author: Leonardo de Moura
 #include "frontends/lean/frontend.h"
 
 namespace lean {
+void add_alias(frontend & f, name const & n, name const & m) {
+    object const & obj = f.get_object(n);
+    f.add_definition(m, obj.get_type(), mk_constant(n));
+}
+
 /**
    \brief Initialize builtin notation.
 */
@@ -80,7 +85,9 @@ void init_builtin_notation(frontend & f) {
     f.mark_implicit_arguments(mk_mp_fn(), {true, true, false, false});
     f.mark_implicit_arguments(mk_discharge_fn(), {true, true, false});
     f.mark_implicit_arguments(mk_refl_fn(), {true, false});
-    f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, false, false, false});
+    f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, true, false, false});
+    add_alias(f, "Subst", "SubstP");
+    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_imp_antisym_fn(), {true, true, false, false});
diff --git a/tests/lean/bad5.lean b/tests/lean/bad5.lean
index 8ec9ccc516..f89a711d10 100644
--- a/tests/lean/bad5.lean
+++ b/tests/lean/bad5.lean
@@ -3,5 +3,5 @@ Variable a : Int
 Variable b : Int
 Axiom H1 : a = b
 Axiom H2 : (g a) > 0
-Theorem T1 : (g b) > 0 := Subst (λ x, (g x) > 0) H2 H1
+Theorem T1 : (g b) > 0 := SubstP (λ x, (g x) > 0) H2 H1
 Show Environment 2
diff --git a/tests/lean/bad5.lean.expected.out b/tests/lean/bad5.lean.expected.out
index ed9eae9370..5ecf8b7ed7 100644
--- a/tests/lean/bad5.lean.expected.out
+++ b/tests/lean/bad5.lean.expected.out
@@ -7,4 +7,4 @@
   Assumed: H2
   Proved: T1
 Axiom H2 : (g a) > 0
-Theorem T1 : (g b) > 0 := Subst (λ x : ℤ, (g x) > 0) H2 H1
+Theorem T1 : (g b) > 0 := SubstP (λ x : ℤ, (g x) > 0) H2 H1
diff --git a/tests/lean/ho.lean b/tests/lean/ho.lean
index e17e19e570..b756407ec9 100644
--- a/tests/lean/ho.lean
+++ b/tests/lean/ho.lean
@@ -3,5 +3,5 @@ Variable a : Int
 Variable b : Int
 Axiom H1 : a = b
 Axiom H2 : (g a) > 0
-Theorem T1 : (g b) > 0 := Subst _ H2 H1
+Theorem T1 : (g b) > 0 := Subst H2 H1
 Show Environment 2
diff --git a/tests/lean/ho.lean.expected.out b/tests/lean/ho.lean.expected.out
index 324be8ef8a..95b4520ac7 100644
--- a/tests/lean/ho.lean.expected.out
+++ b/tests/lean/ho.lean.expected.out
@@ -7,4 +7,4 @@
   Assumed: H2
   Proved: T1
 Axiom H2 : (g a) > 0
-Theorem T1 : (g b) > 0 := Subst (λ x : ℤ, if ((g x) ≤ 0) ⊥ ⊤) H2 H1
+Theorem T1 : (g b) > 0 := Subst H2 H1
diff --git a/tests/lean/subst.lean b/tests/lean/subst.lean
new file mode 100644
index 0000000000..afbac2cd36
--- /dev/null
+++ b/tests/lean/subst.lean
@@ -0,0 +1,9 @@
+Variable a : Int
+Variable n : Nat
+Axiom H1 : a + a + a = 10
+Axiom H2 : a = n
+Theorem T : a + n + a = 10 := Subst H1 H2
+Set pp::coercion true
+Set pp::notation false
+Set pp::implicit true
+Show Environment 1.
diff --git a/tests/lean/subst.lean.expected.out b/tests/lean/subst.lean.expected.out
new file mode 100644
index 0000000000..8c36261b2e
--- /dev/null
+++ b/tests/lean/subst.lean.expected.out
@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: n
+  Assumed: H1
+  Assumed: H2
+  Proved: T
+  Set: lean::pp::coercion
+  Set: lean::pp::notation
+  Set: lean::pp::implicit
+Theorem T : eq::explicit ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) :=
+    Subst::explicit ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == 10) H1 H2