From 28a5ca5809176c560f6df4cd96fc25383f3c5b54 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 18 Sep 2015 07:51:02 -0700
Subject: [PATCH] fix(frontends/lean): fixes #830

---
 src/frontends/lean/builtin_exprs.cpp |  8 ++++----
 src/frontends/lean/tokens.cpp        |  4 ++++
 src/frontends/lean/tokens.h          |  1 +
 src/frontends/lean/tokens.txt        |  1 +
 tests/lean/run/830.lean              | 30 ++++++++++++++++++++++++++++
 5 files changed, 40 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/830.lean

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index cbd0912c9..7c5e1ed0c 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -383,11 +383,11 @@ static expr parse_proof(parser & p, expr const & prop) {
         auto pos = p.pos();
         return parse_begin_end_core(p, pos, get_end_tk(), true);
     } else if (p.curr_is_token(get_by_tk())) {
-        // parse: 'by' tactic
         auto pos = p.pos();
-        p.next();
-        expr t = p.parse_tactic();
-        return p.mk_by(t, pos);
+        return parse_by(p, 0, nullptr, pos);
+    } else if (p.curr_is_token(get_by_plus_tk())) {
+        auto pos = p.pos();
+        return parse_by_plus(p, 0, nullptr, pos);
     } else if (p.curr_is_token(get_using_tk())) {
         // parse: 'using' locals* ',' proof
         auto using_pos = p.pos();
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index c212c5d06..8a63075e2 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -81,6 +81,7 @@ static name const * g_using_tk = nullptr;
 static name const * g_then_tk = nullptr;
 static name const * g_else_tk = nullptr;
 static name const * g_by_tk = nullptr;
+static name const * g_by_plus_tk = nullptr;
 static name const * g_rewrite_tk = nullptr;
 static name const * g_proof_tk = nullptr;
 static name const * g_qed_tk = nullptr;
@@ -233,6 +234,7 @@ void initialize_tokens() {
     g_then_tk = new name{"then"};
     g_else_tk = new name{"else"};
     g_by_tk = new name{"by"};
+    g_by_plus_tk = new name{"by+"};
     g_rewrite_tk = new name{"rewrite"};
     g_proof_tk = new name{"proof"};
     g_qed_tk = new name{"qed"};
@@ -386,6 +388,7 @@ void finalize_tokens() {
     delete g_then_tk;
     delete g_else_tk;
     delete g_by_tk;
+    delete g_by_plus_tk;
     delete g_rewrite_tk;
     delete g_proof_tk;
     delete g_qed_tk;
@@ -538,6 +541,7 @@ name const & get_using_tk() { return *g_using_tk; }
 name const & get_then_tk() { return *g_then_tk; }
 name const & get_else_tk() { return *g_else_tk; }
 name const & get_by_tk() { return *g_by_tk; }
+name const & get_by_plus_tk() { return *g_by_plus_tk; }
 name const & get_rewrite_tk() { return *g_rewrite_tk; }
 name const & get_proof_tk() { return *g_proof_tk; }
 name const & get_qed_tk() { return *g_qed_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index e8d58538a..db7868b59 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -83,6 +83,7 @@ name const & get_using_tk();
 name const & get_then_tk();
 name const & get_else_tk();
 name const & get_by_tk();
+name const & get_by_plus_tk();
 name const & get_rewrite_tk();
 name const & get_proof_tk();
 name const & get_qed_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index 0d50302bf..67b635c42 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -76,6 +76,7 @@ using        using
 then         then
 else         else
 by           by
+by_plus      by+
 rewrite      rewrite
 proof        proof
 qed          qed
diff --git a/tests/lean/run/830.lean b/tests/lean/run/830.lean
new file mode 100644
index 000000000..634bff9b8
--- /dev/null
+++ b/tests/lean/run/830.lean
@@ -0,0 +1,30 @@
+variable P : Prop
+premise HP : P
+
+example : P :=
+have H : P, from HP,
+H
+
+example : P :=
+have H : P, from HP,
+show P, from H
+
+example : P :=
+have H : P, from HP,
+by+ exact H
+
+example : P :=
+have H : P, from HP,
+show P, by+ exact H
+
+example : P :=
+have H : P, from HP,
+show P, begin+ exact H end
+
+example : P :=
+have H : P, from HP,
+show P, using H, by exact H
+
+example : P :=
+assert H : P, from HP,
+show P, by exact H