From aff9257c7233381abe7aa58352a88535118f5cc3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 May 2015 12:28:47 -0700
Subject: [PATCH] =?UTF-8?q?feat(frontends/lean):=20allow=20=E2=86=92=20to?=
 =?UTF-8?q?=20be=20used=20in=20calc=20proofs?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

see issue #586
---
 library/init/logic.lean      |  5 +++++
 src/frontends/lean/calc.cpp  | 17 ++++++++++++++++-
 src/library/constants.cpp    |  4 ++++
 src/library/constants.h      |  1 +
 src/library/constants.txt    |  1 +
 tests/lean/run/calc_imp.lean |  4 ++++
 6 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/calc_imp.lean

diff --git a/library/init/logic.lean b/library/init/logic.lean
index 5381988282..23a777e706 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -10,6 +10,11 @@ import init.datatypes init.reserved_notation
 
 /- implication -/
 
+definition implies (a b : Prop) := a → b
+
+lemma implies.trans [trans] {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
+assume hp, h₂ (h₁ hp)
+
 definition trivial := true.intro
 
 definition not (a : Prop) := a → false
diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp
index d4718641c8..b37810164d 100644
--- a/src/frontends/lean/calc.cpp
+++ b/src/frontends/lean/calc.cpp
@@ -174,12 +174,19 @@ static void join(parser & p, std::vector<calc_step> const & steps1, std::vector<
     }
 }
 
+static expr mk_implies(parser & p, expr const & lhs, expr const & rhs, pos_info const & pos) {
+    return p.mk_app(p.mk_app(p.save_pos(mk_constant(get_implies_name()), pos), lhs, pos), rhs, pos);
+}
+
 expr parse_calc(parser & p) {
     buffer<calc_pred> preds, new_preds;
     buffer<expr>      rhss;
     std::vector<calc_step> steps, new_steps, next_steps;
     auto pos             = p.pos();
+    bool is_std          = is_standard(p.env());
     expr first_pred      = p.parse_expr();
+    if (is_std && is_arrow(first_pred))
+        first_pred = mk_implies(p, binding_domain(first_pred), binding_body(first_pred), pos);
     decode_expr(first_pred, preds, pos);
     parse_calc_proof(p, preds, steps);
     bool single    = true; // true if calc has only one step
@@ -188,7 +195,15 @@ expr parse_calc(parser & p) {
         single = false;
         pos    = p.pos();
         p.next();
-        decode_expr(p.parse_led(dummy), preds, pos);
+        expr next_pred;
+        if (is_std && p.curr_is_token(get_arrow_tk())) {
+            p.next();
+            expr rhs  = p.parse_expr();
+            next_pred = mk_implies(p, dummy, rhs, pos);
+        } else {
+            next_pred = p.parse_led(dummy);
+        }
+        decode_expr(next_pred, preds, pos);
         collect_rhss(steps, rhss);
         new_steps.clear();
         for (auto const & pred : preds) {
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index cda7dfce32..d7e22e6508 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -33,6 +33,7 @@ name const * g_heq_refl = nullptr;
 name const * g_heq_to_eq = nullptr;
 name const * g_iff = nullptr;
 name const * g_iff_refl = nullptr;
+name const * g_implies = nullptr;
 name const * g_ite = nullptr;
 name const * g_lift = nullptr;
 name const * g_lift_down = nullptr;
@@ -160,6 +161,7 @@ void initialize_constants() {
     g_heq_to_eq = new name{"heq", "to_eq"};
     g_iff = new name{"iff"};
     g_iff_refl = new name{"iff", "refl"};
+    g_implies = new name{"implies"};
     g_ite = new name{"ite"};
     g_lift = new name{"lift"};
     g_lift_down = new name{"lift", "down"};
@@ -288,6 +290,7 @@ void finalize_constants() {
     delete g_heq_to_eq;
     delete g_iff;
     delete g_iff_refl;
+    delete g_implies;
     delete g_ite;
     delete g_lift;
     delete g_lift_down;
@@ -415,6 +418,7 @@ name const & get_heq_refl_name() { return *g_heq_refl; }
 name const & get_heq_to_eq_name() { return *g_heq_to_eq; }
 name const & get_iff_name() { return *g_iff; }
 name const & get_iff_refl_name() { return *g_iff_refl; }
+name const & get_implies_name() { return *g_implies; }
 name const & get_ite_name() { return *g_ite; }
 name const & get_lift_name() { return *g_lift; }
 name const & get_lift_down_name() { return *g_lift_down; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 33ed641017..f175b95e06 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -35,6 +35,7 @@ name const & get_heq_refl_name();
 name const & get_heq_to_eq_name();
 name const & get_iff_name();
 name const & get_iff_refl_name();
+name const & get_implies_name();
 name const & get_ite_name();
 name const & get_lift_name();
 name const & get_lift_down_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index ca951ad6ec..9af3dfe526 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -28,6 +28,7 @@ heq.refl
 heq.to_eq
 iff
 iff.refl
+implies
 ite
 lift
 lift.down
diff --git a/tests/lean/run/calc_imp.lean b/tests/lean/run/calc_imp.lean
new file mode 100644
index 0000000000..3b90350d48
--- /dev/null
+++ b/tests/lean/run/calc_imp.lean
@@ -0,0 +1,4 @@
+example (A B C D : Prop) (h1 : A → B) (h2 : B → C) (h3 : C → D) : A → D :=
+calc A → B : h1
+   ... → C : h2
+   ... → D : h3