feat(frontends/lean): allow → to be used in calc proofs

see issue #586

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

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) {

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; }

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();

src/library/constants.txt

@@ -28,6 +28,7 @@ heq.refl
 heq.to_eq
 iff
 iff.refl
+implies
 ite
 lift
 lift.down

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