feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'

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

src/frontends/lean/frontend_elaborator.cpp

@@ -123,7 +123,7 @@ class frontend_elaborator::imp {
 
         virtual expr visit_constant(expr const & e, context const & ctx) {
             if (is_placeholder(e)) {
-                expr m = m_ref.m_menv.mk_metavar(ctx);
+                expr m = m_ref.m_menv.mk_metavar(ctx, const_type(e));
                 m_ref.m_trace[m] = e;
                 return m;
             } else {

src/frontends/lean/parser.cpp

@@ -134,6 +134,7 @@ class parser::imp {
     typedef std::unordered_map<name, expr, name_hash, name_eq>  builtins;
     typedef std::pair<unsigned, unsigned> pos_info;
     typedef expr_map<pos_info> expr_pos_info;
+    typedef expr_map<tactic>   tactic_hints; // a mapping from placeholder to tactic
     typedef buffer<std::tuple<pos_info, name, expr, bool>> bindings_buffer;
     frontend &          m_frontend;
     scanner             m_scanner;
@@ -148,6 +149,7 @@ class parser::imp {
     expr_pos_info       m_expr_pos_info;
     pos_info            m_last_cmd_pos;
     pos_info            m_last_script_pos;
+    tactic_hints        m_tactic_hints;
 
     script_state *      m_script_state;
 
@@ -1122,6 +1124,72 @@ class parser::imp {
         return save(mk_placeholder(), p);
     }
 
+    /** \brief Parse a tactic expression, it can be
+
+        1) A Lua Script Block expression that returns a tactic
+        2) '(' expr ')' where expr is a proof term
+        3) identifier that is the name of a tactic or proof term.
+    */
+    tactic parse_tactic_expr() {
+        auto p = pos();
+        tactic t;
+        if (curr() == scanner::token::ScriptBlock) {
+            parse_script_expr();
+            using_script([&](lua_State * L) {
+                    try {
+                        t = to_tactic_ext(L, -1);
+                    } catch (...) {
+                        throw parser_error("invalid script-block, it must return a tactic", p);
+                    }
+                });
+        } else if (curr_is_lparen()) {
+            next();
+            expr pr      = parse_expr();
+            check_rparen_next("invalid apply command, ')' expected");
+            expr pr_type = m_type_inferer(pr);
+            t = apply_tactic(pr, pr_type);
+        } else {
+           name n = check_identifier_next("invalid apply command, identifier, '(' expr ')', or 'script-block' expected");
+            object const & o = m_frontend.find_object(n);
+            if (o && (o.is_theorem() || o.is_axiom())) {
+                t = apply_tactic(n);
+            } else {
+                using_script([&](lua_State * L) {
+                        lua_getglobal(L, n.to_string().c_str());
+                        try {
+                            t = to_tactic_ext(L, -1);
+                        } catch (...) {
+                            throw parser_error(sstream() << "unknown tactic '" << n << "'", p);
+                        }
+                        lua_pop(L, 1);
+                    });
+            }
+        }
+        return t;
+    }
+
+    /** \brief Parse <tt>'show' expr 'by' tactic</tt> */
+    expr parse_show_expr() {
+        auto p = pos();
+        next();
+        expr t = parse_expr();
+        check_next(scanner::token::By, "invalid 'show _ by _' expression, 'by' expected");
+        tactic tac = parse_tactic_expr();
+        expr r = mk_placeholder(t);
+        m_tactic_hints[r] = tac;
+        return save(r, p);
+    }
+
+    /** \brief Parse <tt>'by' tactic</tt> */
+    expr parse_by_expr() {
+        auto p = pos();
+        next();
+        tactic tac = parse_tactic_expr();
+        expr r = mk_placeholder();
+        m_tactic_hints[r] = tac;
+        return save(r, p);
+    }
+
     /**
        \brief Auxiliary method used when processing the beginning of an expression.
     */
@@ -1139,6 +1207,8 @@ class parser::imp {
         case scanner::token::StringVal:   return parse_string();
         case scanner::token::Placeholder: return parse_placeholder();
         case scanner::token::Type:        return parse_type();
+        case scanner::token::Show:        return parse_show_expr();
+        case scanner::token::By:          return parse_by_expr();
         default:
             throw parser_error("invalid expression, unexpected token", pos());
         }
@@ -1260,7 +1330,7 @@ class parser::imp {
         throw tactic_cmd_error("failed to backtrack", p, s);
     }
 
-    void tactic_apply(proof_state_seq_stack & stack, proof_state & s, tactic const & t, pos_info const & tac_pos) {
+    void tactic_apply(proof_state_seq_stack & stack, proof_state & s, tactic const & t, pos_info const & p) {
         proof_state_seq::maybe_pair r;
         code_with_callbacks([&]() {
                 // t may have call-backs we should set ios in the script_state
@@ -1271,46 +1341,20 @@ class parser::imp {
             s = r->first;
             stack.push_back(r->second);
         } else {
-            throw tactic_cmd_error("tactic failed", tac_pos, s);
+            throw tactic_cmd_error("tactic failed", p, s);
         }
     }
 
+    proof_state tactic_apply(proof_state s, tactic const & t, pos_info const & p) {
+        proof_state_seq_stack stack;
+        tactic_apply(stack, s, t, p);
+        return s;
+    }
+
     void tactic_apply(proof_state_seq_stack & stack, proof_state & s) {
         auto tac_pos = pos();
         next();
-        tactic t;
+        tactic t = parse_tactic_expr();
-        if (curr() == scanner::token::ScriptBlock) {
-            parse_script_expr();
-            using_script([&](lua_State * L) {
-                    try {
-                        t = to_tactic_ext(L, -1);
-                    } catch (...) {
-                        throw tactic_cmd_error(sstream() << "invalid script-block, it must return a tactic", tac_pos, s);
-                    }
-                });
-        } else if (curr_is_lparen()) {
-            next();
-            expr pr      = parse_expr();
-            check_rparen_next("invalid apply command, ')' expected");
-            expr pr_type = m_type_inferer(pr);
-            t = apply_tactic(pr, pr_type);
-        } else {
-           name n = check_identifier_next("invalid apply command, identifier, '(' expr ')', or 'script-block' expected");
-            object const & o = m_frontend.find_object(n);
-            if (o && (o.is_theorem() || o.is_axiom())) {
-                t = apply_tactic(n);
-            } else {
-                using_script([&](lua_State * L) {
-                        lua_getglobal(L, n.to_string().c_str());
-                        try {
-                            t = to_tactic_ext(L, -1);
-                        } catch (...) {
-                            throw tactic_cmd_error(sstream() << "unknown tactic '" << n << "'", tac_pos, s);
-                        }
-                        lua_pop(L, 1);
-                    });
-            }
-        }
         tactic_apply(stack, s, t, tac_pos);
     }
 
@@ -1320,9 +1364,7 @@ class parser::imp {
         tactic_apply(stack, s, assumption_tactic(), tac_pos);
     }
 
-    expr tactic_done(proof_state const & s) {
+    expr mk_proof_for(proof_state const & s, pos_info const & p) {
-        auto p = pos();
-        next();
         if (s.is_proof_final_state()) {
             assignment a(s.get_menv());
             proof_map  m;
@@ -1336,6 +1378,12 @@ class parser::imp {
         }
     }
 
+    expr tactic_done(proof_state const & s) {
+        auto p = pos();
+        next();
+        return mk_proof_for(s, p);
+    }
+
     bool curr_is_tactic_cmd() {
         if (curr_is_identifier()) {
             name const & id = curr_name();
@@ -1420,16 +1468,38 @@ class parser::imp {
         }
     }
 
-    expr parse_tactic(expr const & type, expr const & val, metavar_env & menv) {
+    /**
+       \brief Return a 'hint' tactic (if it exists) for the given metavariable.
+       If the metavariable is not associated with any hint, then return the
+       null tactic. The method also returns the position of the hint.
+    */
+    std::pair<tactic, pos_info> get_tactic_tactic_for(expr const & mvar) {
+        expr placeholder = m_elaborator.get_original(mvar);
+        auto it = m_tactic_hints.find(placeholder);
+        if (it != m_tactic_hints.end()) {
+            return mk_pair(it->second, pos_of(placeholder, pos()));
+        } else {
+            return mk_pair(tactic(), pos_of(placeholder, pos()));
+        }
+    }
+
+    expr apply_tactics(expr const & type, expr const & val, metavar_env & menv) {
         if (is_metavar(val)) {
             // simple case
             if (!m_type_inferer.is_proposition(type))
                 throw exception("failed to synthesize metavar, its type is not a proposition");
             proof_state s = to_proof_state(m_frontend, context(), type);
-            display_proof_state_if_interactive(s);
+            std::pair<tactic, pos_info> hint_and_pos = get_tactic_tactic_for(val);
-            show_tactic_prompt();
+            if (hint_and_pos.first) {
-            check_period_next("invalid theorem, '.' expected before tactical proof");
+                // metavariable has an associated tactic hint
-            return parse_tactic(s);
+                s = tactic_apply(s, hint_and_pos.first, hint_and_pos.second);
+                return mk_proof_for(s, hint_and_pos.second);
+            } else {
+                display_proof_state_if_interactive(s);
+                show_tactic_prompt();
+                check_period_next("invalid theorem, '.' expected before tactical proof");
+                return parse_tactic(s);
+            }
         } else {
             buffer<expr> mvars;
             for_each(val, [&](expr const & e, unsigned) {
@@ -1453,14 +1523,21 @@ class parser::imp {
                 if (!m_type_inferer.is_proposition(mvar_type, mvar_ctx))
                     throw exception("failed to synthesize metavar, its type is not a proposition");
                 proof_state s = to_proof_state(m_frontend, mvar_ctx, mvar_type);
-                if (curr_is_period()) {
+                std::pair<tactic, pos_info> hint_and_pos = get_tactic_tactic_for(mvar);
-                    display_proof_state_if_interactive(s);
+                if (hint_and_pos.first) {
-                    show_tactic_prompt();
+                    // metavariable has an associated tactic hint
-                    next();
+                    s = tactic_apply(s, hint_and_pos.first, hint_and_pos.second);
+                    menv.assign(mvar, mk_proof_for(s, hint_and_pos.second));
+                } else {
+                    if (curr_is_period()) {
+                        display_proof_state_if_interactive(s);
+                        show_tactic_prompt();
+                        next();
+                    }
+                    expr mvar_val = parse_tactic(s);
+                    if (mvar_val)
+                        menv.assign(mvar, mvar_val);
                 }
-                expr mvar_val = parse_tactic(s);
-                if (mvar_val)
-                    menv.assign(mvar, mvar_val);
             }
             return instantiate_metavars(val, menv);
         }
@@ -1507,7 +1584,7 @@ class parser::imp {
         if (has_metavar(type))
             throw exception("invalid definition, type still contains metavariables after elaboration");
         if (!is_definition && has_metavar(val)) {
-            val = parse_tactic(type, val, menv);
+            val = apply_tactics(type, val, menv);
         }
         if (has_metavar(val))
             throw exception("invalid definition, value still contains metavariables after elaboration");
@@ -1915,6 +1992,7 @@ class parser::imp {
     bool parse_command() {
         m_elaborator.clear();
         m_expr_pos_info.clear();
+        m_tactic_hints.clear();
         m_last_cmd_pos = pos();
         name const & cmd_id = curr_name();
         if (cmd_id == g_definition_kwd) {

src/frontends/lean/scanner.cpp

@@ -28,6 +28,8 @@ static name g_forall_unicode("\u2200");
 static name g_exists_name("exists");
 static name g_exists_unicode("\u2203");
 static name g_placeholder_name("_");
+static name g_show_name("show");
+static name g_by_name("by");
 
 static char g_normalized[256];
 
@@ -219,6 +221,10 @@ scanner::token scanner::read_a_symbol() {
                 return token::In;
             else if (m_name_val == g_placeholder_name)
                 return token::Placeholder;
+            else if (m_name_val == g_show_name)
+                return token::Show;
+            else if (m_name_val == g_by_name)
+                return token::By;
             else
                 return is_command(m_name_val) ? token::CommandId : token::Id;
         }
@@ -446,6 +452,8 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::Type:              out << "Type"; break;
     case scanner::token::Placeholder:       out << "_"; break;
     case scanner::token::ScriptBlock:       out << "Script"; break;
+    case scanner::token::Show:              out << "show"; break;
+    case scanner::token::By:                out << "by"; break;
     case scanner::token::Eof:               out << "EOF"; break;
     }
     return out;

src/frontends/lean/scanner.h

@@ -21,7 +21,7 @@ public:
     enum class token {
         LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
         Let, In, Forall, Exists, Id, CommandId, NatVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder,
-        ScriptBlock, Eof
+        Show, By, ScriptBlock, Eof
     };
 protected:
     int                m_spos; // position in the current line of the stream

src/library/placeholder.cpp

@@ -12,8 +12,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_placeholder_name("_");
-expr mk_placeholder() {
+expr mk_placeholder(expr const & t) {
-    return mk_constant(g_placeholder_name);
+    return mk_constant(g_placeholder_name, t);
 }
 
 bool is_placeholder(expr const & e) {
@@ -30,7 +30,7 @@ class replace_placeholders_with_metavars_proc : public replace_visitor {
 protected:
     expr visit_constant(expr const & e, context const & c) {
         if (is_placeholder(e)) {
-            return m_menv.mk_metavar(c);
+            return m_menv.mk_metavar(c, const_type(e));
         } else {
             return e;
         }

src/library/placeholder.h

@@ -11,10 +11,11 @@ Author: Leonardo de Moura
 namespace lean {
 class metavar_env;
 /**
-    \brief Return a new placeholder expression. To be able to track location,
+    \brief Return a new placeholder expression (with an optional
-    a new constant for each placeholder.
+    type). To be able to track location, a new constant for each
+    placeholder.
 */
-expr mk_placeholder();
+expr mk_placeholder(expr const & t = expr());
 
 /**
     \brief Return true iff the given expression is a placeholder.

tests/lean/interactive/t1.lean.expected.out

@@ -11,9 +11,7 @@ Proof state:
 a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
 ## Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Error (line: 8, pos: 0) unknown tactic 'imp_tac2'
+## Error (line: 8, pos: 6) unknown tactic 'imp_tac2'
-Proof state:
-H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
 ## Error (line: 9, pos: 0) invalid tactic command 'foo'
 Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b

tests/lean/interactive/t10.lean.expected.out

@@ -7,9 +7,7 @@ A : Bool, B : Bool, H : A ∧ B ⊢ A
 no goals
 ## Proof state:
 A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
-## Error (line: 15, pos: 3) unknown tactic 'simple2_tac'
+## Error (line: 15, pos: 9) unknown tactic 'simple2_tac'
-Proof state:
-A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
 ## Error (line: 15, pos: 22) invalid 'done' command, proof cannot be produced from this state
 Proof state:
 A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B

tests/lean/interactive/t12.lean

@@ -0,0 +1,58 @@
+(**
+-- Define a simple tactic using Lua
+auto = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
+**)
+
+(*
+The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it.
+The "hint" is a tactic that should be used to fill the "hole".
+In the following example, we use the tactic "auto" defined by the Lua code above.
+
+The (show [expr] by [tactic]) expression is also creating a "hole" and associating a "hint" to it.
+The expression [expr] after the shows is fixing the type of the "hole"
+*)
+Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
+     fun assumption : A /\ B,
+          let lemma1     : A      := (by auto),
+              lemma2     : B      := (by auto)
+          in (show B /\ A by auto)
+
+(*
+When hints are not provided, the user must fill the (remaining) holes using tactic command sequences.
+Each hole must be filled with a tactic command sequence that terminates with the command 'done' and
+successfully produces a proof term for filling the hole. Here is the same example without hints
+This style is more convenient for interactive proofs
+*)
+Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
+     fun assumption : A /\ B,
+          let lemma1     : A      := _,  (* first hole *)
+              lemma2     : B      := _   (* second hole *)
+          in _. (* third hole *)
+   apply auto. done. (* tactic command sequence for the first hole *)
+   apply auto. done. (* tactic command sequence for the second hole *)
+   apply auto. done. (* tactic command sequence for the third hole *)
+
+(*
+In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
+*)
+Theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
+     fun assumption : A /\ B,
+          let lemma1     : A      := _,  (* first hole *)
+              lemma2     : B      := _   (* second hole *)
+          in _. (* third hole *)
+   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the first hole *)
+   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the second hole *)
+   apply conj_tac. apply assumption_tac. done.      (* tactic command sequence for the third hole *)
+
+(*
+We can also mix the two styles (hints and command sequences)
+*)
+Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
+     fun assumption : A /\ B,
+          let lemma1     : A      := _,  (* first hole *)
+              lemma2     : B      := _   (* second hole *)
+          in (show B /\ A by auto).
+   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the first hole *)
+   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the second hole *)
+
+

tests/lean/interactive/t12.lean.expected.out

@@ -0,0 +1,51 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+  Proved: T1
+Proof state:
+A : Bool, B : Bool, assumption : A ∧ B ⊢ A
+## Proof state:
+no goals
+## Proof state:
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A ⊢ B
+## Proof state:
+no goals
+## Proof state:
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A, lemma2 : B ⊢ B ∧ A
+## Proof state:
+no goals
+##   Proved: T2
+# Proof state:
+A : Bool, B : Bool, assumption : A ∧ B ⊢ A
+## Proof state:
+A : Bool, B : Bool, assumption::1 : A, assumption::2 : B ⊢ A
+## Proof state:
+no goals
+## Proof state:
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A ⊢ B
+## Proof state:
+A : Bool, B : Bool, assumption::1 : A, assumption::2 : B, lemma1 : A ⊢ B
+## Proof state:
+no goals
+## Proof state:
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A, lemma2 : B ⊢ B ∧ A
+## Proof state:
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A, lemma2 : B ⊢ B
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A, lemma2 : B ⊢ A
+## Proof state:
+no goals
+##   Proved: T3
+# Proof state:
+A : Bool, B : Bool, assumption : A ∧ B ⊢ A
+## Proof state:
+A : Bool, B : Bool, assumption::1 : A, assumption::2 : B ⊢ A
+## Proof state:
+no goals
+## Proof state:
+A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A ⊢ B
+## Proof state:
+A : Bool, B : Bool, assumption::1 : A, assumption::2 : B, lemma1 : A ⊢ B
+## Proof state:
+no goals
+##   Proved: T4
+# 

tests/lean/interactive/t2.lean.expected.out

@@ -5,9 +5,7 @@ Proof state:
 a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
 ## Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Error (line: 6, pos: 0) unknown tactic 'imp_tac2'
+## Error (line: 6, pos: 6) unknown tactic 'imp_tac2'
-Proof state:
-H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
 ## Error (line: 7, pos: 0) invalid tactic command 'foo'
 Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b