feat(frontends/lean): add proof-qed expression

Remark: we still have to add support to it in the elaborator.
Right now, it is just an embellished parenthesis.

src/emacs/lean-syntax.el

@@ -80,6 +80,8 @@
      (,(rx symbol-start (or "bool" "int" "nat" "real" "Prop" "Type" "ℕ" "ℤ") symbol-end) . 'font-lock-type-face)
      ;; sorry
      (,(rx symbol-start "sorry" symbol-end) . 'font-lock-warning-face)
+     ;; extra-keywords
+     (,(rx (or "∎")) . 'font-lock-keyword-face)
      ;; lean-keywords
      (, (concat "\\(" (regexp-opt lean-keywords 'words) "\\)")
         (1 'font-lock-keyword-face)))))

src/frontends/lean/builtin_exprs.cpp

@@ -26,7 +26,7 @@ namespace lean {
 namespace notation {
 static name g_llevel_curly(".{"), g_rcurly("}"), g_in("in"), g_colon(":"), g_assign(":=");
 static name g_comma(","), g_visible("[visible]"), g_from("from"), g_using("using");
-static name g_then("then"), g_have("have"), g_by("by"), g_qed("qed"), g_end("end");
+static name g_then("then"), g_have("have"), g_by("by"), g_proof("proof"), 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) {
@@ -153,11 +153,21 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
     }
 }
 
+static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
+    expr r = p.save_pos(mk_proof_qed_annotation(p.parse_expr()), pos);
+    p.check_token_next(g_qed, "invalid proof-qed, 'qed' expected");
+    return r;
+}
+
 static expr parse_proof(parser & p, expr const & prop) {
     if (p.curr_is_token(g_from)) {
         // parse: 'from' expr
         p.next();
         return p.parse_expr();
+    } else if (p.curr_is_token(g_proof)) {
+        auto pos = p.pos();
+        p.next();
+        return parse_proof_qed_core(p, pos);
     } else if (p.curr_is_token(g_by)) {
         // parse: 'by' tactic
         auto pos = p.pos();
@@ -369,6 +379,10 @@ static expr parse_rparen(parser & p, unsigned, expr const * args, pos_info const
         return args[0];
 }
 
+static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return parse_proof_qed_core(p, pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -390,6 +404,7 @@ parse_table init_nud_table() {
     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("begin", mk_ext_action(parse_begin_end))}, x0);
+    r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, 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/elaborator.cpp

@@ -315,6 +315,8 @@ public:
             return visit_choice(e, some_expr(t), cs);
         } else if (is_by(e)) {
             return visit_by(e, some_expr(t), cs);
+        } else if (is_proof_qed_annotation(e)) {
+            return visit_proof_qed(e, some_expr(t), cs);
         } else {
             return visit(e, cs);
         }
@@ -343,6 +345,12 @@ public:
         return m;
     }
 
+    expr visit_proof_qed(expr const & e, optional<expr> const & /* t */, constraint_seq & cs) {
+        lean_assert(is_proof_qed_annotation(e));
+        // TODO(Leo)
+        return visit(get_annotation_arg(e), cs);
+    }
+
     /** \brief Make sure \c f is really a function, if it is not, try to apply coercions.
         The result is a pair <tt>new_f, f_type</tt>, where new_f is the new value for \c f,
         and \c f_type is its type (and a Pi-expression)
@@ -693,6 +701,8 @@ public:
             return visit_let_value(e, cs);
         } else if (is_by(e)) {
             return visit_by(e, none_expr(), cs);
+        } else if (is_proof_qed_annotation(e)) {
+            return visit_proof_qed(e, none_expr(), cs);
         } else if (is_no_info(e)) {
             flet<bool> let(m_no_info, true);
             return visit(get_annotation_arg(e), cs);

src/frontends/lean/token_table.cpp

@@ -65,6 +65,7 @@ static char const * g_pi_unicode     = "\u03A0";
 static char const * g_forall_unicode = "\u2200";
 static char const * g_arrow_unicode  = "\u2192";
 static char const * g_cup            = "\u2294";
+static char const * g_qed_unicode    = "∎";
 
 token_table init_token_table() {
     token_table t;
@@ -87,7 +88,7 @@ token_table init_token_table() {
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
-         {nullptr, nullptr}};
+         {g_qed_unicode, "qed"}, {nullptr, nullptr}};
 
     pair<char const *, char const *> cmd_aliases[] =
         {{"parameter", "variable"}, {"parameters", "variables"}, {"lemma", "theorem"},

src/library/annotation.cpp

@@ -136,11 +136,20 @@ name const & get_show_name() {
     return g_show;
 }
 
+name const & get_proof_qed_name() {
+    static name g_proof_qed("proof-qed");
+    static register_annotation_fn g_proof_qed_annotation(g_proof_qed);
+    return g_proof_qed;
+}
+
 static name g_have_name = get_have_name(); // force 'have' annotation to be registered
 static name g_show_name = get_show_name(); // force 'show' annotation to be registered
+static name g_proof_qed_name = get_proof_qed_name(); // force 'proof-qed' annotation to be registered
 
 expr mk_have_annotation(expr const & e) { return mk_annotation(get_have_name(), e); }
 expr mk_show_annotation(expr const & e) { return mk_annotation(get_show_name(), e); }
+expr mk_proof_qed_annotation(expr const & e) { return mk_annotation(get_proof_qed_name(), e); }
 bool is_have_annotation(expr const & e) { return is_annotation(e, get_have_name()); }
 bool is_show_annotation(expr const & e) { return is_annotation(e, get_show_name()); }
+bool is_proof_qed_annotation(expr const & e) { return is_annotation(e, get_proof_qed_name()); }
 }

src/library/annotation.h

@@ -60,10 +60,14 @@ expr copy_annotations(expr const & from, expr const & to);
 expr mk_have_annotation(expr const & e);
 /** \brief Tag \c e as a 'show'-expression. 'show' is a pre-registered annotation. */
 expr mk_show_annotation(expr const & e);
+/** \brief Tag \c e as a 'proof-qed'-expression. 'proof-qed' is a pre-registered annotation. */
+expr mk_proof_qed_annotation(expr const & e);
 /** \brief Return true iff \c e was created using #mk_have_annotation. */
 bool is_have_annotation(expr const & e);
 /** \brief Return true iff \c e was created using #mk_show_annotation. */
 bool is_show_annotation(expr const & e);
+/** \brief Return true iff \c e was created using #mk_proof_qed_annotation. */
+bool is_proof_qed_annotation(expr const & e);
 
 /** \brief Return the serialization 'opcode' for annotation macros. */
 std::string const & get_annotation_opcode();

tests/lean/run/div2.lean

@@ -0,0 +1,120 @@
+import logic data.nat.sub struc.relation data.prod
+import tools.fake_simplifier
+
+open nat relation relation.iff_ops prod
+open fake_simplifier decidable
+open eq_ops
+
+namespace nat
+
+-- A general recursion principle
+-- -----------------------------
+--
+-- Data:
+--
+--   dom, codom : Type
+--   default : codom
+--   measure : dom → ℕ
+--   rec_val : dom → (dom → codom) → codom
+--
+-- and a proof
+--
+--   rec_decreasing : ∀m, m ≥ measure x, rec_val x f = rec_val x (restrict f m)
+--
+-- ... which says that the recursive call only depends on f at values with measure less than x,
+-- in the sense that changing other values to the default value doesn't change the result.
+--
+-- The result is a function f = rec_measure, satisfying
+--
+--   f x = rec_val x f
+
+definition restrict {dom codom : Type} (default : codom) (measure : dom → ℕ) (f : dom → codom)
+    (m : ℕ) (x : dom) :=
+if measure x < m then f x else default
+
+theorem restrict_lt_eq {dom codom : Type} (default : codom) (measure : dom → ℕ) (f : dom → codom)
+    (m : ℕ) (x : dom) (H : measure x < m) :
+  restrict default measure f m x = f x :=
+if_pos H
+
+theorem restrict_not_lt_eq {dom codom : Type} (default : codom) (measure : dom → ℕ)
+    (f : dom → codom) (m : ℕ) (x : dom) (H : ¬ measure x < m) :
+  restrict default measure f m x = default :=
+if_neg H
+
+definition rec_measure_aux {dom codom : Type} (default : codom) (measure : dom → ℕ)
+    (rec_val : dom → (dom → codom) → codom) : ℕ → dom → codom :=
+rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default)
+
+definition rec_measure {dom codom : Type} (default : codom) (measure : dom → ℕ)
+    (rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
+rec_measure_aux default measure rec_val (succ (measure x)) x
+
+theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ)
+    (rec_val : dom → (dom → codom) → codom)
+    (rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) →
+        rec_val x g1 = rec_val x g2)
+    (m : ℕ) :
+  let f' := rec_measure_aux default measure rec_val in
+  let f := rec_measure default measure rec_val in
+  ∀x, f' m x = restrict default measure f m x :=
+let f' := rec_measure_aux default measure rec_val in
+let f  := rec_measure default measure rec_val in
+case_strong_induction_on m
+  (take x,
+    have H1 : f' 0 x = default, from rfl,
+    have H2 : ¬ measure x < 0, from not_lt_zero,
+    have H3 : restrict default measure f 0 x = default, from if_neg H2,
+    show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹)
+  (take m,
+    assume IH: ∀n, n ≤ m → ∀x, f' n x = restrict default measure f n x,
+    take x : dom,
+    show f' (succ m) x = restrict default measure f (succ m) x, from
+      by_cases -- (measure x < succ m)
+        (assume H1 : measure x < succ m,
+          have H2a : ∀z, measure z < measure x → f' m z = f z,
+          proof
+            take z,
+              assume Hzx : measure z < measure x,
+              calc
+                f' m z = restrict default measure f m z : IH m le_refl z
+                  ... = f z : restrict_lt_eq _ _ _ _ _ (lt_le_trans Hzx (lt_succ_imp_le H1))
+          ∎,
+          have H2 : f' (succ m) x = rec_val x f,
+          proof
+            calc
+              f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
+                ... = rec_val x (f' m) : if_pos H1
+                ... = rec_val x f : rec_decreasing (f' m) f x H2a
+          ∎,
+          let m' := measure x in
+          have H3a : ∀z, measure z < m' → f' m' z = f z,
+          proof
+            take z,
+              assume Hzx : measure z < measure x,
+              calc
+                f' m' z = restrict default measure f m' z : IH _ (lt_succ_imp_le H1) _
+                  ... = f z : restrict_lt_eq _ _ _ _ _ Hzx
+          qed,
+          have H3 : restrict default measure f (succ m) x = rec_val x f,
+          proof
+            calc
+              restrict default measure f (succ m) x = f x : if_pos H1
+                ... = f' (succ m') x : eq.refl _
+                ... = if measure x < succ m' then rec_val x (f' m') else default : rfl
+                ... = rec_val x (f' m') : if_pos self_lt_succ
+                ... = rec_val x f : rec_decreasing _ _ _ H3a
+          qed,
+          show f' (succ m) x = restrict default measure f (succ m) x,
+            from H2 ⬝ H3⁻¹)
+        (assume H1 : ¬ measure x < succ m,
+          have H2 : f' (succ m) x = default, from
+            calc
+              f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
+                ... = default : if_neg H1,
+          have H3 : restrict default measure f (succ m) x = default,
+            from if_neg H1,
+          show f' (succ m) x = restrict default measure f (succ m) x,
+            from H2 ⬝ H3⁻¹))
+
+end nat