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

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

tests/lean/tactic11.lean.expected.out

@@ -1 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
   Proved: T

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.

tests/lean/tactic12.lean.expected.out

@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Proved: T
+  Assumed: p
+  Assumed: q
+  Proved: T2