feat(frontends/lean): add 'proof-qed' notation

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

src/emacs/lean-mode.el

@@ -24,7 +24,7 @@
 (define-generic-mode
     'lean-mode     ;; name of the mode to create
   '("--")          ;; comments start with
-  '("import" "abbreviation" "definition" "parameter" "parameters" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords
+  '("import" "abbreviation" "definition" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords
   '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
     ("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
     ("\"[^\"]*\"" . 'font-lock-string-face)

src/frontends/lean/builtin_exprs.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
+#include "library/tactic/tactic.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/token_table.h"
@@ -15,19 +16,11 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace notation {
-static name g_llevel_curly(".{");
-static name g_rcurly("}");
-static name g_in("in");
-static name g_colon(":");
-static name g_assign(":=");
-static name g_comma(",");
-static name g_fact("[fact]");
-static name g_inline("[inline]");
-static name g_from("from");
-static name g_using("using");
-static name g_then("then");
-static name g_have("have");
-static name g_by("by");
+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_take("take"), g_assume("assume"), g_show("show"), g_fun("fun");
+
 
 static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
     if (p.curr_is_token(g_llevel_curly)) {
@@ -138,6 +131,36 @@ 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> r;
+    while (true) {
+        bool use_exact = (p.curr_is_token(g_have) || p.curr_is_token(g_show) || p.curr_is_token(g_assume) ||
+                          p.curr_is_token(g_take) || p.curr_is_token(g_fun));
+        auto pos = p.pos();
+        expr tac = p.parse_expr();
+        if (use_exact)
+            tac = p.save_pos(mk_app(get_exact_tac_fn(), tac), pos);
+        if (pre_tac)
+            tac = p.save_pos(mk_app(get_and_then_tac_fn(), *pre_tac, tac), pos);
+        r = r ? p.save_pos(mk_app(get_and_then_tac_fn(), *r, tac), pos) : tac;
+        if (p.curr_is_token(g_qed)) {
+            auto pos = p.pos();
+            p.next();
+            return p.save_pos(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());
+        }
+    }
+}
+
 static expr parse_proof(parser & p, expr const & prop) {
     if (p.curr_is_token(g_from)) {
         // parse: 'from' expr
@@ -285,6 +308,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);
     return r;
 }
 

src/library/tactic/expr_to_tactic.cpp

@@ -82,13 +82,19 @@ 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));
+expr const & get_exact_tac_fn() { return g_exact_tac_fn; }
+expr const & get_and_then_tac_fn() { return g_and_then_tac_fn; }
 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(name(g_tac, "and_then"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
+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_tac reg_state(name(g_tac, "state"), [](type_checker &, expr const & e, pos_info_provider const * p) {

src/library/tactic/expr_to_tactic.h

@@ -29,6 +29,9 @@ struct register_unary_tac {
 };
 
 name const & get_exact_tac_name();
+name const & get_and_then_tac_name();
+expr const & get_exact_tac_fn();
+expr const & get_and_then_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/tactic13.lean

@@ -0,0 +1,12 @@
+import standard
+using tactic
+
+theorem tst (a b : Bool) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
+proof
+  apply and_intro,
+  apply not_intro,
+  assume Ha, or_elim H
+    (assume Hna, absurd Ha Hna)
+    (assume Hnb, absurd Hb Hnb),
+  assumption
+qed