feat(frontends/lean): add nameless 'have' expression

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

src/frontends/lean/builtin_exprs.cpp

@@ -146,24 +146,35 @@ static expr parse_proof(parser & p, expr const & prop) {
     }
 }
 
-static void parse_have_modifiers(parser & p, bool & is_fact) {
+static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> const & prev_local) {
+    auto id_pos       = p.pos();
+    bool is_fact      = false;
+    name id;
+    expr prop;
     if (p.curr_is_token(g_fact)) {
         p.next();
-        is_fact = true;
-    }
-}
-
-static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> const & prev_local) {
-    auto id_pos  = p.pos();
-    bool is_fact = false;
-    name id      = p.check_id_next("invalid 'have' declaration, identifier expected");
-    parse_have_modifiers(p, is_fact);
-    expr prop;
-    if (p.curr_is_token(g_colon)) {
+        is_fact       = true;
+        id            = p.mk_fresh_name();
+        prop          = p.parse_expr();
+    } else if (p.curr_is_identifier()) {
+        id = p.get_name_val();
         p.next();
-        prop  = p.parse_expr();
+        if (p.curr_is_token(g_fact)) {
+            p.next();
+            p.check_token_next(g_colon, "invalid 'have' declaration, ':' expected");
+            is_fact   = true;
+            prop      = p.parse_expr();
+        } else if (p.curr_is_token(g_colon)) {
+            p.next();
+            prop      = p.parse_expr();
+        } else {
+            expr left = p.id_to_expr(id, id_pos);
+            id        = p.mk_fresh_name();
+            prop      = p.parse_led(left);
+        }
     } else {
-        prop  = p.save_pos(mk_expr_placeholder(), id_pos);
+        id            = p.mk_fresh_name();
+        prop          = p.parse_expr();
     }
     p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
     expr proof;

src/frontends/lean/parser.cpp

@@ -109,12 +109,14 @@ struct scoped_set_parser {
     }
 };
 
+static name g_tmp_prefix = name::mk_internal_unique_name();
+
 parser::parser(environment const & env, io_state const & ios,
                std::istream & strm, char const * strm_name,
                bool use_exceptions, unsigned num_threads,
                local_level_decls const & lds, local_expr_decls const & eds,
                unsigned line):
-    m_env(env), m_ios(ios),
+    m_env(env), m_ios(ios), m_ngen(g_tmp_prefix),
     m_verbose(true), m_use_exceptions(use_exceptions),
     m_scanner(strm, strm_name), m_local_level_decls(lds), m_local_decls(eds),
     m_pos_table(std::make_shared<pos_info_table>()) {
@@ -796,10 +798,7 @@ expr parser::parse_led_notation(expr left) {
         return mk_app(left, parse_nud_notation(), pos_of(left));
 }
 
-expr parser::parse_id() {
-    auto p  = pos();
-    name id = get_name_val();
-    next();
+expr parser::id_to_expr(name const & id, pos_info const & p) {
     buffer<level> lvl_buffer;
     levels ls;
     if (curr_is_token(g_llevel_curly)) {
@@ -835,6 +834,13 @@ expr parser::parse_id() {
     return *r;
 }
 
+expr parser::parse_id() {
+    auto p  = pos();
+    name id = get_name_val();
+    next();
+    return id_to_expr(id, p);
+}
+
 expr parser::parse_numeral_expr() {
     // TODO(Leo)
     return expr();

src/frontends/lean/parser.h

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "util/thread_script_state.h"
 #include "util/script_exception.h"
+#include "util/name_generator.h"
 #include "kernel/environment.h"
 #include "kernel/expr_maps.h"
 #include "library/io_state.h"
@@ -43,11 +44,11 @@ typedef std::unordered_map<unsigned, tactic> hint_table;
 class parser {
     environment             m_env;
     io_state                m_ios;
+    name_generator          m_ngen;
     bool                    m_verbose;
     bool                    m_use_exceptions;
     bool                    m_show_errors;
     unsigned                m_num_threads;
-
     scanner                 m_scanner;
     scanner::token_kind     m_curr;
     local_level_decls       m_local_level_decls;
@@ -143,6 +144,8 @@ public:
     void updt_options();
     template<typename T> void set_option(name const & n, T const & v) { m_ios.set_option(n, v); }
 
+    name mk_fresh_name() { return m_ngen.next(); }
+
     /** \brief Return the current position information */
     pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }
     expr save_pos(expr e, pos_info p);
@@ -203,6 +206,9 @@ public:
     parameter parse_binder();
     local_environment parse_binders(buffer<parameter> & r);
 
+    /** \brief Convert an identifier into an expression (constant or local constant) based on the current scope */
+    expr id_to_expr(name const & id, pos_info const & p);
+
     expr parse_expr(unsigned rbp = 0);
     expr parse_led(expr left);
     expr parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp = 0);

tests/lean/run/have6.lean

@@ -0,0 +1,18 @@
+abbreviation Bool : Type.{1} := Type.{0}
+variable and : Bool → Bool → Bool
+infixl `∧` 25 := and
+variable and_intro : forall (a b : Bool), a → b → a ∧ b
+variables a b c d : Bool
+axiom Ha : a
+axiom Hb : b
+axiom Hc : c
+check
+  have a ∧ b, from and_intro a b Ha Hb,
+  have [fact] b ∧ a, from and_intro b a Hb Ha,
+  have H : a ∧ b, from and_intro a b Ha Hb,
+  have H [fact] : a ∧ b, from and_intro a b Ha Hb,
+  then have a ∧ b, from and_intro a b Ha Hb,
+  then have [fact] b ∧ a, from and_intro b a Hb Ha,
+  then have H : a ∧ b, from and_intro a b Ha Hb,
+  then have H [fact] : a ∧ b, from and_intro a b Ha Hb,
+    Ha