feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81

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

src/frontends/lean/CMakeLists.txt

@@ -3,7 +3,7 @@ scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
 parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 server.cpp notation_cmd.cpp calc.cpp
 decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
-dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp
+dependencies.cpp parser_bindings.cpp begin_end_ext.cpp
 class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp noinfo.cpp)
 

src/frontends/lean/begin_end_ext.cpp

@@ -14,22 +14,22 @@ Author: Leonardo de Moura
 
 namespace lean {
 // This (scoped) environment extension allows us to set a tactic to be applied before every element
-// in a <tt>proof ... qed</tt> block
-struct pq_entry {
+// in a <tt>begin ... end</tt> block
+struct be_entry {
     bool m_accumulate; // if true, then accumulate the new tactic, if false replace
     expr m_tac;
-    pq_entry():m_accumulate(false) {}
-    pq_entry(bool a, expr const & t):m_accumulate(a), m_tac(t) {}
+    be_entry():m_accumulate(false) {}
+    be_entry(bool a, expr const & t):m_accumulate(a), m_tac(t) {}
 };
 
-struct pq_state {
+struct be_state {
     optional<expr> m_pre_tac;
     optional<expr> m_pre_tac_body;
 };
 
-struct pq_config {
-    typedef pq_state state;
-    typedef pq_entry entry;
+struct be_config {
+    typedef be_state state;
+    typedef be_entry entry;
     static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
         if (e.m_accumulate) {
             if (s.m_pre_tac_body)
@@ -44,11 +44,11 @@ struct pq_config {
         }
     }
     static name const & get_class_name() {
-        static name g_class_name("proof_qed");
+        static name g_class_name("begin_end");
         return g_class_name;
     }
     static std::string const & get_serialization_key() {
-        static std::string g_key("pq_pre_tac");
+        static std::string g_key("be_pre_tac");
         return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
@@ -61,42 +61,42 @@ struct pq_config {
     }
 };
 
-template class scoped_ext<pq_config>;
-typedef scoped_ext<pq_config> proof_qed_ext;
+template class scoped_ext<be_config>;
+typedef scoped_ext<be_config> begin_end_ext;
 
 static void check_valid_tactic(environment const & env, expr const & pre_tac) {
     type_checker tc(env);
     if (!tc.is_def_eq(tc.infer(pre_tac).first, get_tactic_type()).first)
-        throw exception("invalid proof-qed pre-tactic update, argument is not a tactic");
+        throw exception("invalid begin-end pre-tactic update, argument is not a tactic");
 }
 
-environment add_proof_qed_pre_tactic(environment const & env, expr const & pre_tac) {
+environment add_begin_end_pre_tactic(environment const & env, expr const & pre_tac) {
     check_valid_tactic(env, pre_tac);
-    return proof_qed_ext::add_entry(env, get_dummy_ios(), pq_entry(true, pre_tac));
+    return begin_end_ext::add_entry(env, get_dummy_ios(), be_entry(true, pre_tac));
 }
 
-environment set_proof_qed_pre_tactic(environment const & env, expr const & pre_tac) {
+environment set_begin_end_pre_tactic(environment const & env, expr const & pre_tac) {
     check_valid_tactic(env, pre_tac);
-    return proof_qed_ext::add_entry(env, get_dummy_ios(), pq_entry(false, pre_tac));
+    return begin_end_ext::add_entry(env, get_dummy_ios(), be_entry(false, pre_tac));
 }
 
-optional<expr> get_proof_qed_pre_tactic(environment const & env) {
-    pq_state const & s = proof_qed_ext::get_state(env);
+optional<expr> get_begin_end_pre_tactic(environment const & env) {
+    be_state const & s = begin_end_ext::get_state(env);
     return s.m_pre_tac;
 }
 
-environment add_proof_qed_cmd(parser & p) {
-    return add_proof_qed_pre_tactic(p.env(), parse_tactic_name(p));
+environment add_begin_end_cmd(parser & p) {
+    return add_begin_end_pre_tactic(p.env(), parse_tactic_name(p));
 }
 
-environment set_proof_qed_cmd(parser & p) {
-    return set_proof_qed_pre_tactic(p.env(), parse_tactic_name(p));
+environment set_begin_end_cmd(parser & p) {
+    return set_begin_end_pre_tactic(p.env(), parse_tactic_name(p));
 }
 
-void register_proof_qed_cmds(cmd_table & r) {
-    add_cmd(r, cmd_info("add_proof_qed", "add a new tactic to be automatically applied before every component in a 'proof-qed' block",
-                        add_proof_qed_cmd));
-    add_cmd(r, cmd_info("set_proof_qed", "reset the tactic that is automatically applied before every component in a 'proof-qed' block",
-                        set_proof_qed_cmd));
+void register_begin_end_cmds(cmd_table & r) {
+    add_cmd(r, cmd_info("add_begin_end_tactic", "add a new tactic to be automatically applied before every component in a 'begin-end' block",
+                        add_begin_end_cmd));
+    add_cmd(r, cmd_info("set_begin_end_tactic", "reset the tactic that is automatically applied before every component in a 'begin-end' block",
+                        set_begin_end_cmd));
 }
 }

src/frontends/lean/begin_end_ext.h

@@ -9,8 +9,8 @@ Author: Leonardo de Moura
 #include "frontends/lean/cmd_table.h"
 
 namespace lean {
-environment add_proof_qed_pre_tactic(environment const & env, expr const & pre_tac);
-environment reset_proof_qed_pre_tactic(environment const & env, expr const & pre_tac);
-optional<expr> get_proof_qed_pre_tactic(environment const & env);
-void register_proof_qed_cmds(cmd_table & r);
+environment add_begin_end_pre_tactic(environment const & env, expr const & pre_tac);
+environment reset_begin_end_pre_tactic(environment const & env, expr const & pre_tac);
+optional<expr> get_begin_end_pre_tactic(environment const & env);
+void register_begin_end_cmds(cmd_table & r);
 }

src/frontends/lean/builtin_cmds.cpp

@@ -22,7 +22,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/inductive_cmd.h"
 #include "frontends/lean/structure_cmd.h"
-#include "frontends/lean/proof_qed_ext.h"
+#include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/class.h"
 #include "frontends/lean/tactic_hint.h"
@@ -312,7 +312,7 @@ cmd_table init_cmd_table() {
     register_structure_cmd(r);
     register_notation_cmds(r);
     register_calc_cmds(r);
-    register_proof_qed_cmds(r);
+    register_begin_end_cmds(r);
     register_class_cmds(r);
     register_tactic_hint_cmd(r);
     return r;

src/frontends/lean/builtin_exprs.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
-#include "frontends/lean/proof_qed_ext.h"
+#include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 
@@ -22,7 +22,7 @@ namespace lean {
 namespace notation {
 static name g_llevel_curly(".{"), g_rcurly("}"), g_in("in"), g_colon(":"), g_assign(":=");
 static name g_comma(","), g_fact("[fact]"), g_inline("[inline]"), g_from("from"), g_using("using");
-static name g_then("then"), g_have("have"), g_by("by"), g_qed("qed");
+static name g_then("then"), g_have("have"), g_by("by"), g_qed("qed"), g_end("end");
 static name g_take("take"), g_assume("assume"), g_show("show"), g_fun("fun");
 
 static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
@@ -138,10 +138,10 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     return p.mk_by(t, pos);
 }
 
-static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const & pos) {
+static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
     if (!p.has_tactic_decls())
-        throw parser_error("invalid 'proof' expression, tactic module has not been imported", pos);
-    optional<expr> pre_tac = get_proof_qed_pre_tactic(p.env());
+        throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", pos);
+    optional<expr> pre_tac = get_begin_end_pre_tactic(p.env());
     optional<expr> r;
     while (true) {
         bool use_exact = (p.curr_is_token(g_have) || p.curr_is_token(g_show) || p.curr_is_token(g_assume) ||
@@ -154,14 +154,14 @@ static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const &
             tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
         tac = p.mk_app(get_determ_tac_fn(), tac, pos);
         r = r ? p.mk_app({get_and_then_tac_fn(), *r, tac}, pos) : tac;
-        if (p.curr_is_token(g_qed)) {
+        if (p.curr_is_token(g_end)) {
             auto pos = p.pos();
             p.next();
             return p.mk_by(*r, pos);
         } else if (p.curr_is_token(g_comma)) {
             p.next();
         } else {
-            throw parser_error("invalid proof-qed, ',' or 'qed' expected", p.pos());
+            throw parser_error("invalid begin-end, ',' or 'end' expected", p.pos());
         }
     }
 }
@@ -387,7 +387,7 @@ parse_table init_nud_table() {
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
-    r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0);
+    r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0);
     r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0);
     r = r.add({transition("including", mk_ext_action(parse_including_expr))}, x0);
     return r;

src/frontends/lean/token_table.cpp

@@ -70,7 +70,7 @@ token_table init_token_table() {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec},
          {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
+         {"(*", 0}, {"(--", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",
@@ -79,7 +79,7 @@ token_table init_token_table() {
                                "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
                                "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
-                               "add_proof_qed", "set_proof_qed", "instance", "#erase_cache", nullptr};
+                               "add_begin_end_tactic", "set_begin_end_tactic", "instance", "#erase_cache", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

tests/lean/run/tactic13.lean

@@ -2,11 +2,11 @@ import standard
 using tactic
 
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
-proof
+begin
   apply and_intro,
   apply not_intro,
   assume Ha, or_elim H
     (assume Hna, absurd Ha Hna)
     (assume Hnb, absurd Hb Hnb),
   assumption
-qed
+end

tests/lean/run/tactic14.lean

@@ -4,11 +4,11 @@ using tactic
 definition basic_tac : tactic
 := repeat [apply @and_intro | assumption]
 
-set_proof_qed basic_tac -- basic_tac is automatically applied to each element of a proof-qed block
+set_begin_end_tactic basic_tac -- basic_tac is automatically applied to each element of a proof-qed block
 
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
-proof
+begin
   assume Ha, or_elim H
     (assume Hna, absurd Ha Hna)
     (assume Hnb, absurd Hb Hnb)
-qed
+end