From dd62af164175717865b63236e16891ef10308ae8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Dec 2013 08:20:13 -0800
Subject: [PATCH] feat(frontends/parser): simplified theorem definition using
 tactical proof

When using tactics for proving theorems, a common pattern is

     Theorem T : <proposition> := _.
          apply <tactic>.
          ...
          done.

This commit allows the user to write the simplified form:

     Theorem T : <proposition>.
          apply <tactic>.
          ...
          done.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp         | 18 +++++++++++++-----
 tests/lean/tactic11.lean.expected.out |  2 ++
 tests/lean/tactic12.lean              | 13 +++++++++++++
 tests/lean/tactic12.lean.expected.out |  6 ++++++
 4 files changed, 34 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/tactic12.lean
 create mode 100644 tests/lean/tactic12.lean.expected.out

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 093f7c408..9f7c17f84 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1183,8 +1183,12 @@ class parser::imp {
         if (curr_is_colon()) {
             next();
             pre_type = parse_expr();
-            check_assign_next("invalid definition, ':=' expected");
-            pre_val  = parse_expr();
+            if (!is_definition && curr_is_period()) {
+                pre_val  = save(mk_placholder(), pos());
+            } else {
+                check_assign_next("invalid definition, ':=' expected");
+                pre_val  = parse_expr();
+            }
         } else if (is_definition && curr_is_assign()) {
             auto p   = pos();
             next();
@@ -1195,10 +1199,14 @@ class parser::imp {
             parse_object_bindings(bindings);
             check_colon_next("invalid definition, ':' expected");
             expr type_body = parse_expr();
-            check_assign_next("invalid definition, ':=' expected");
-            expr val_body  = parse_expr();
             pre_type  = mk_abstraction(false, bindings, type_body);
-            pre_val   = mk_abstraction(true, bindings, val_body);
+            if (!is_definition && curr_is_period()) {
+                pre_val = mk_abstraction(true, bindings, mk_placholder());
+            } else {
+                check_assign_next("invalid definition, ':=' expected");
+                expr val_body  = parse_expr();
+                pre_val   = mk_abstraction(true, bindings, val_body);
+            }
         }
         auto r = m_elaborator(id, pre_type, pre_val);
         expr type = std::get<0>(r);
diff --git a/tests/lean/tactic11.lean.expected.out b/tests/lean/tactic11.lean.expected.out
index 01bc4d73f..ed7015541 100644
--- a/tests/lean/tactic11.lean.expected.out
+++ b/tests/lean/tactic11.lean.expected.out
@@ -1 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
   Proved: T
diff --git a/tests/lean/tactic12.lean b/tests/lean/tactic12.lean
new file mode 100644
index 000000000..eea54de00
--- /dev/null
+++ b/tests/lean/tactic12.lean
@@ -0,0 +1,13 @@
+Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a).
+   apply beta_tactic.
+   apply imp_tactic.
+   apply conj_hyp_tactic.
+   apply assumption_tactic.
+   done.
+
+Variables p q : Bool.
+Theorem T2 : p /\ q => q.
+   apply imp_tactic.
+   apply conj_hyp_tactic.
+   apply assumption_tactic.
+   done.
\ No newline at end of file
diff --git a/tests/lean/tactic12.lean.expected.out b/tests/lean/tactic12.lean.expected.out
new file mode 100644
index 000000000..83c468786
--- /dev/null
+++ b/tests/lean/tactic12.lean.expected.out
@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Proved: T
+  Assumed: p
+  Assumed: q
+  Proved: T2