feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component

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

src/frontends/lean/CMakeLists.txt

@@ -3,6 +3,6 @@ scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
 parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 interactive.cpp notation_cmd.cpp calc.cpp
 decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
-dependencies.cpp parser_bindings.cpp)
+dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_cmds.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/calc.h"
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/inductive_cmd.h"
+#include "frontends/lean/proof_qed_ext.h"
 #include "frontends/lean/decl_cmds.h"
 
 namespace lean {
@@ -246,6 +247,7 @@ cmd_table init_cmd_table() {
     register_inductive_cmd(r);
     register_notation_cmds(r);
     register_calc_cmds(r);
+    register_proof_qed_cmds(r);
     return r;
 }
 

src/frontends/lean/builtin_exprs.cpp

@@ -12,6 +12,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/parser.h"
 
 namespace lean {
@@ -131,13 +132,8 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     return p.save_pos(mk_by(t), pos);
 }
 
-static optional<expr> get_proof_qed_pre_tac(environment const & /* env */) {
-    // TODO(Leo)
-    return none_expr();
-}
-
 static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const &) {
-    optional<expr> pre_tac = get_proof_qed_pre_tac(p.env());
+    optional<expr> pre_tac = get_proof_qed_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) ||

src/frontends/lean/elaborator.cpp

@@ -645,7 +645,7 @@ public:
     void check_exact_tacs(expr const & pre_tac, substitution const & s) {
         for_each(pre_tac, [&](expr const & e, unsigned) {
                 expr const & f = get_app_fn(e);
-                if (is_constant(f) && const_name(f) == get_exact_tac_name()) {
+                if (is_constant(f) && const_name(f) == const_name(get_exact_tac_fn())) {
                     display_unassigned_mvars(e, s);
                     return false;
                 } else {

src/frontends/lean/proof_qed_ext.cpp

@@ -0,0 +1,107 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "kernel/type_checker.h"
+#include "library/scoped_ext.h"
+#include "library/kernel_serializer.h"
+#include "library/tactic/expr_to_tactic.h"
+#include "frontends/lean/parser.h"
+
+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 {
+    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) {}
+};
+
+struct pq_state {
+    optional<expr> m_pre_tac;
+    optional<expr> m_pre_tac_body;
+};
+
+struct pq_config {
+    typedef pq_state state;
+    typedef pq_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)
+                s.m_pre_tac_body = mk_app(get_or_else_tac_fn(), *s.m_pre_tac_body, e.m_tac);
+            else
+                s.m_pre_tac_body = e.m_tac;
+            s.m_pre_tac = mk_app(get_repeat_tac_fn(), *s.m_pre_tac_body);
+        } else {
+            // reset
+            s.m_pre_tac      = e.m_tac;
+            s.m_pre_tac_body = e.m_tac;
+        }
+    }
+    static name const & get_class_name() {
+        static name g_class_name("proof_qed");
+        return g_class_name;
+    }
+    static std::string const & get_serialization_key() {
+        static std::string g_key("pq_pre_tac");
+        return g_key;
+    }
+    static void  write_entry(serializer & s, entry const & e) {
+        s << e.m_accumulate << e.m_tac;
+    }
+    static entry read_entry(deserializer & d) {
+        entry e;
+        d >> e.m_accumulate >> e.m_tac;
+        return e;
+    }
+};
+
+template class scoped_ext<pq_config>;
+typedef scoped_ext<pq_config> proof_qed_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), get_tactic_type()))
+        throw exception("invalid proof-qed pre-tactic update, argument is not a tactic");
+}
+
+environment add_proof_qed_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));
+}
+
+environment reset_proof_qed_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));
+}
+
+optional<expr> get_proof_qed_pre_tactic(environment const & env) {
+    pq_state const & s = proof_qed_ext::get_state(env);
+    return s.m_pre_tac;
+}
+
+static expr parse_tactic_name(parser & p) {
+    auto pos = p.pos();
+    name id  = p.check_id_next("invalid proof_qed configuration command, indentifier expected");
+    return p.id_to_expr(id, pos);
+}
+
+environment add_proof_qed_cmd(parser & p) {
+    return add_proof_qed_pre_tactic(p.env(), parse_tactic_name(p));
+}
+
+environment reset_proof_qed_cmd(parser & p) {
+    return reset_proof_qed_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("reset_proof_qed", "reset the tactic that is automatically applied before every component in a 'proof-qed' block",
+                        reset_proof_qed_cmd));
+}
+}

src/frontends/lean/proof_qed_ext.h

@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+#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);
+}

src/frontends/lean/token_table.cpp

@@ -67,7 +67,8 @@ token_table init_token_table() {
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "set_option",
-                               "using", "calc_subst", "calc_refl", "calc_trans", "#setline", nullptr};
+                               "using", "calc_subst", "calc_refl", "calc_trans", "add_proof_qed", "reset_proof_qed",
+                               "#setline", nullptr};
 
     std::pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

src/kernel/type_checker.cpp

@@ -430,7 +430,7 @@ static void check_no_local(environment const & env, expr const & e) {
         throw_kernel_exception(env, "failed to add declaration to environment, it contains local constants", e);
 }
 
-static void check_no_mlocal(environment const & env, name const & n, expr const & e, bool is_type) {
+void check_no_mlocal(environment const & env, name const & n, expr const & e, bool is_type) {
     check_no_metavar(env, n, e, is_type);
     check_no_local(env, e);
 }

src/library/tactic/expr_to_tactic.cpp

@@ -24,7 +24,7 @@ void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn) {
 }
 
 tactic expr_to_tactic(type_checker & tc, expr const & e, pos_info_provider const * p) {
-    expr const & f = get_app_fn(tc.whnf(e));
+    expr f = get_app_fn(tc.whnf(e));
     if (is_constant(f)) {
         auto const & map = get_expr_to_tactic_map();
         auto it = map.find(const_name(f));
@@ -80,23 +80,25 @@ register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tact
         });
 }
 
-static name g_tac("tactic");
-static name g_exact_tac_name(g_tac, "exact");
-static name g_and_then_tac_name(g_tac, "and_then");
-name const & get_exact_tac_name() { return g_exact_tac_name; }
-name const & get_and_then_tac_name() { return g_and_then_tac_name; }
-static expr g_exact_tac_fn(Const(g_exact_tac_name));
-static expr g_and_then_tac_fn(Const(g_and_then_tac_name));
+static name g_tac("tactic"), g_tac_name(g_tac, "tactic"), g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then");
+static name g_or_else_tac_name(g_tac, "or_else"), g_repeat_tac_name(g_tac, "repeat");
+static expr g_exact_tac_fn(Const(g_exact_tac_name)), g_and_then_tac_fn(Const(g_and_then_tac_name));
+static expr g_or_else_tac_fn(Const(g_or_else_tac_name)), g_repeat_tac_fn(Const(g_repeat_tac_name));
+static expr g_tac_type(Const(g_tac_name));
 expr const & get_exact_tac_fn() { return g_exact_tac_fn; }
 expr const & get_and_then_tac_fn() { return g_and_then_tac_fn; }
+expr const & get_or_else_tac_fn() { return g_or_else_tac_fn; }
+expr const & get_repeat_tac_fn() { return g_repeat_tac_fn; }
+expr const & get_tactic_type() { return g_tac_type; }
+
 static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); });
 static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); });
 static register_simple_tac reg_assumption(name(g_tac, "assumption"), []() { return assumption_tactic(); });
 static register_simple_tac reg_fail(name(g_tac, "fail"), []() { return fail_tactic(); });
 static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tactic(); });
 static register_bin_tac reg_then(g_and_then_tac_name, [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
-static register_bin_tac reg_orelse(name(g_tac, "or_else"), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
-static register_unary_tac reg_repeat(name(g_tac, "repeat"), [](tactic const & t1) { return repeat(t1); });
+static register_bin_tac reg_orelse(g_or_else_tac_name, [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
+static register_unary_tac reg_repeat(g_repeat_tac_name, [](tactic const & t1) { return repeat(t1); });
 static register_tac reg_state(name(g_tac, "state"), [](type_checker &, expr const & e, pos_info_provider const * p) {
         if (p)
             return trace_state_tactic(std::string(p->get_file_name()), p->get_pos_info(e));

src/library/tactic/expr_to_tactic.h

@@ -28,10 +28,11 @@ struct register_unary_tac {
     register_unary_tac(name const & n, std::function<tactic(tactic const &)> f);
 };
 
-name const & get_exact_tac_name();
-name const & get_and_then_tac_name();
+expr const & get_tactic_type();
 expr const & get_exact_tac_fn();
 expr const & get_and_then_tac_fn();
+expr const & get_or_else_tac_fn();
+expr const & get_repeat_tac_fn();
 
 tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p);
 expr mk_by(expr const & e);

tests/lean/run/tactic14.lean

@@ -0,0 +1,14 @@
+import standard
+using tactic
+
+definition basic_tac : tactic
+:= repeat (apply @and_intro | apply @not_intro | assumption)
+
+reset_proof_qed basic_tac -- basic_tac is automatically applied to each element of a proof-qed block
+
+theorem tst (a b : Bool) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
+proof
+  assume Ha, or_elim H
+    (assume Hna, absurd Ha Hna)
+    (assume Hnb, absurd Hb Hnb)
+qed