feat(frontends/lean): new 'have' expression

Add 'have' notation suggested by Jeremy Avigad.
Add his example to the test suite.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser_expr.cpp

@@ -1002,6 +1002,34 @@ expr parser_imp::parse_show_expr() {
     }
 }
 
+/** \brief Parse <tt>'have' Id ':' expr, 'from' expr, expr</tt> and
+                 <tt>'have' Id ':' expr, 'by' expr, expr</tt>
+*/
+expr parser_imp::parse_have_expr() {
+    auto p = pos();
+    next();
+    mk_scope scope(*this);
+    name id  = check_identifier_next("invalid 'have' expression, identifier expected");
+    check_colon_next("invalid 'have' expression, ':' expected");
+    expr t   = parse_expr();
+    check_comma_next("invalid 'have' expression, ',' expected");
+    expr val;
+    if (curr() == scanner::token::By) {
+        next();
+        tactic tac = parse_tactic_expr();
+        expr r = mk_placeholder(some_expr(t));
+        m_tactic_hints.insert(mk_pair(r, tac));
+        val = save(r, p);
+    } else if (curr_is_identifier() && curr_name() == g_from) {
+        next();
+        val = parse_expr();
+    }
+    check_comma_next("invalid 'have' expression, ',' expected");
+    register_binding(id);
+    expr body = parse_expr();
+    return mk_let(id, t, val, body);
+}
+
 /** \brief Parse <tt>'by' tactic</tt> */
 expr parser_imp::parse_by_expr() {
     auto p = pos();
@@ -1030,10 +1058,11 @@ expr parser_imp::parse_nud() {
     case scanner::token::Placeholder: return parse_placeholder();
     case scanner::token::Type:        return parse_type(false);
     case scanner::token::Show:        return parse_show_expr();
+    case scanner::token::Have:        return parse_have_expr();
+    case scanner::token::By:          return parse_by_expr();
     case scanner::token::Tuple:       return parse_tuple();
     case scanner::token::Proj1:       return parse_proj(true);
     case scanner::token::Proj2:       return parse_proj(false);
-    case scanner::token::By:          return parse_by_expr();
     default:
         throw parser_error("invalid expression, unexpected token", pos());
     }

src/frontends/lean/parser_imp.h

@@ -320,6 +320,7 @@ private:
     expr parse_proj(bool first);
     tactic parse_tactic_macro(name tac_id, pos_info const & p);
     expr parse_show_expr();
+    expr parse_have_expr();
     expr parse_calc();
     expr parse_nud_id();
     expr parse_nud();

tests/lean/j2.lean

@@ -0,0 +1,33 @@
+import macros
+import tactic
+using Nat
+
+definition dvd (a b : Nat) : Bool := ∃ c, a * c = b
+
+infix 50 | : dvd
+
+theorem dvd_trans {a b c} (H1 : a | b) (H2 : b | c) : a | c
+:= obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1,
+   obtain (w2 : Nat) (Hw2 : b * w2 = c), from H2,
+     exists_intro (w1 * w2)
+       (calc a * (w1 * w2) = a * w1 * w2 : symm (mul_assoc a w1 w2)
+                       ... = b * w2 : { Hw1 }
+                       ... = c : Hw2)
+
+definition prime p := p ≥ 2 ∧ forall m, m | p → m = 1 ∨ m = p
+
+theorem not_prime_eq (n : Nat) (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n
+:= have H3 : ¬ n ≥ 2 ∨ ¬ (∀ m : Nat, m | n → m = 1 ∨ m = n),
+     from (not_and _ _ ◂ H2),
+   have H4 : ¬ ¬ n ≥ 2,
+     from ((symm (not_not_eq _)) ◂ H1),
+   obtain (m : Nat) (H5 :  ¬ (m | n → m = 1 ∨ m = n)),
+     from (not_forall_elim (resolve1 H3 H4)),
+   have H6 : m | n ∧ ¬ (m = 1 ∨ m = n),
+     from ((not_implies _ _) ◂ H5),
+   have H7 : ¬ (m = 1 ∨ m = n) ↔ (m ≠ 1 ∧ m ≠ n),
+     from (not_or (m = 1) (m = n)),
+   have H8 : m | n ∧ m ≠ 1 ∧ m ≠ n,
+     from subst H6 H7,
+   show ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n,
+     from exists_intro m H8

tests/lean/j2.lean.expected.out

@@ -0,0 +1,9 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'macros'
+  Imported 'tactic'
+  Using: Nat
+  Defined: dvd
+  Proved: dvd_trans
+  Defined: prime
+  Proved: not_prime_eq