diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index afe510421..4956b2af9 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/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 { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 722e9362b..b8ebc5f16 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -134,6 +134,7 @@ class parser::imp { typedef std::unordered_map builtins; typedef std::pair pos_info; typedef expr_map expr_pos_info; + typedef expr_map tactic_hints; // a mapping from placeholder to tactic typedef buffer> 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 'show' expr 'by' tactic */ + 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 'by' tactic */ + 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; - 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 t = parse_tactic_expr(); 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) { - auto p = pos(); - next(); + expr mk_proof_for(proof_state const & s, pos_info const & p) { 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 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); - show_tactic_prompt(); - check_period_next("invalid theorem, '.' expected before tactical proof"); - return parse_tactic(s); + std::pair hint_and_pos = get_tactic_tactic_for(val); + if (hint_and_pos.first) { + // metavariable has an associated tactic hint + 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 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()) { - display_proof_state_if_interactive(s); - show_tactic_prompt(); - next(); + std::pair hint_and_pos = get_tactic_tactic_for(mvar); + if (hint_and_pos.first) { + // metavariable has an associated tactic hint + 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) { diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index d13c34f7e..470f9b299 100644 --- a/src/frontends/lean/scanner.cpp +++ b/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; diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index b5b6a4bf4..994f26b92 100644 --- a/src/frontends/lean/scanner.h +++ b/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 diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index 5ef37e050..54d2b0fe1 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -12,8 +12,8 @@ Author: Leonardo de Moura namespace lean { static name g_placeholder_name("_"); -expr mk_placeholder() { - return mk_constant(g_placeholder_name); +expr mk_placeholder(expr const & t) { + 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; } diff --git a/src/library/placeholder.h b/src/library/placeholder.h index 6d0939e4b..15254a42e 100644 --- a/src/library/placeholder.h +++ b/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, - a new constant for each placeholder. + \brief Return a new placeholder expression (with an optional + 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. diff --git a/tests/lean/interactive/t1.lean.expected.out b/tests/lean/interactive/t1.lean.expected.out index 06f0b0a73..847e0f943 100644 --- a/tests/lean/interactive/t1.lean.expected.out +++ b/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' -Proof state: -H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b +## Error (line: 8, pos: 6) unknown tactic 'imp_tac2' ## Error (line: 9, pos: 0) invalid tactic command 'foo' Proof state: H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b diff --git a/tests/lean/interactive/t10.lean.expected.out b/tests/lean/interactive/t10.lean.expected.out index 043995204..846e416ce 100644 --- a/tests/lean/interactive/t10.lean.expected.out +++ 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' -Proof state: -A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B +## Error (line: 15, pos: 9) unknown tactic 'simple2_tac' ## 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 diff --git a/tests/lean/interactive/t12.lean b/tests/lean/interactive/t12.lean new file mode 100644 index 000000000..ac4b1c42a --- /dev/null +++ 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 *) + + diff --git a/tests/lean/interactive/t12.lean.expected.out b/tests/lean/interactive/t12.lean.expected.out new file mode 100644 index 000000000..bb47b4776 --- /dev/null +++ b/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 +# \ No newline at end of file diff --git a/tests/lean/interactive/t2.lean.expected.out b/tests/lean/interactive/t2.lean.expected.out index 25c2a63d6..d7366ef7a 100644 --- a/tests/lean/interactive/t2.lean.expected.out +++ b/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' -Proof state: -H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b +## Error (line: 6, pos: 6) unknown tactic 'imp_tac2' ## Error (line: 7, pos: 0) invalid tactic command 'foo' Proof state: H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b