feat(frontends/lean): add 'obtains' expression

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

library/standard/logic.lean

@@ -204,7 +204,8 @@ theorem exists_unique_intro {A : Type} {p : A → Bool} (w : A) (H1 : p w) (H2 :
 := exists_intro w (and_intro H1 H2)
 
 theorem exists_unique_elim {A : Type} {p : A → Bool} {b : Bool} (H2 : ∃! x, p x) (H1 : ∀ x, p x → (∀ y, y ≠ x → ¬ p y) → b) : b
-:= exists_elim H2 (λ w Hw, H1 w (and_elim_left Hw) (and_elim_right Hw))
+:= obtains w Hw, from H2,
+     H1 w (and_elim_left Hw) (and_elim_right Hw)
 
 inductive inhabited (A : Type) : Bool :=
 | inhabited_intro : A → inhabited A
@@ -236,15 +237,15 @@ definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b
 infixl `==`:50 := heq
 
 theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B
-:= exists_elim H (λ H Hw, H)
+:= obtains w Hw, from H, w
 
 theorem eq_to_heq {A : Type} {a b : A} (H : a = b) : a == b
 := exists_intro (refl A) (trans (cast_refl a) H)
 
 theorem heq_to_eq {A : Type} {a b : A} (H : a == b) : a = b
-:= exists_elim H (λ (H : A = A) (Hw : cast H a = b),
+:= obtains (w : A = A) (Hw : cast w a = b), from H,
-    calc a = cast H a : symm (cast_eq H a)
+    calc a = cast w a : symm (cast_eq w a)
-      ...  = b        : Hw)
+      ...  = b        : Hw
 
 theorem heq_refl {A : Type} (a : A) : a == a
 := eq_to_heq (refl a)

src/emacs/lean-mode.el

@@ -26,7 +26,7 @@
   '("--")          ;; comments start with
   '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "including" "class" "instance" "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)
+    ("\\_<\\(calc\\|have\\|obtains\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
     ("\"[^\"]*\"" . 'font-lock-string-face)
     ("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face)
     ("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face)

src/frontends/lean/builtin_exprs.cpp

@@ -278,6 +278,47 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos)
     return mk_let(p, H_show, prop, proof, Var(0), pos, mk_contextual_info(false));
 }
 
+static name g_exists_elim("exists_elim");
+static expr parse_obtains(parser & p, unsigned, expr const *, pos_info const & pos) {
+    if (!p.env().find(g_exists_elim))
+        throw parser_error("invalid use of 'obtains' expression, environment does not contain 'exists_elim' theorem", pos);
+    // exists_elim {A : Type} {P : A → Bool} {B : Bool} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B)
+    buffer<expr> ps;
+    auto b_pos = p.pos();
+    environment env = p.parse_binders(ps);
+    unsigned num_ps = ps.size();
+    if (num_ps < 2)
+        throw parser_error("invalid 'obtains' expression, at least 2 binders expected", b_pos);
+    bool is_fact = false;
+    if (p.curr_is_token(g_fact)) {
+        p.next();
+        is_fact = true;
+    }
+    if (!is_fact) {
+        expr H = ps[num_ps-1];
+        ps[num_ps-1] = update_local(H, mlocal_type(H), local_info(H).update_contextual(false));
+    }
+    p.check_token_next(g_comma, "invalid 'obtains' expression, ',' expected");
+    p.check_token_next(g_from, "invalid 'obtains' expression, 'from' expected");
+    expr H1 = p.parse_expr();
+    p.check_token_next(g_comma, "invalid 'obtains' expression, ',' expected");
+    expr b  = p.parse_scoped_expr(ps, env);
+    expr H  = ps[num_ps-1];
+    unsigned i = num_ps-1;
+    while (i > 1) {
+        --i;
+        expr a      = ps[i];
+        expr H_aux  = mk_local(p.mk_fresh_name(), mk_expr_placeholder(), mk_contextual_info(is_fact));
+        expr  H2    = Fun({a, H}, b);
+        b = mk_constant(g_exists_elim)(H_aux, H2);
+        H = H_aux;
+    }
+    expr a  = ps[0];
+    expr H2 = Fun({a, H}, b);
+    expr r  = mk_constant(g_exists_elim)(H1, H2);
+    return p.rec_save_pos(r, pos);
+}
+
 static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &) {
     return parse_calc(p);
 }
@@ -329,6 +370,7 @@ parse_table init_nud_table() {
     r = r.add({transition("by", mk_ext_action(parse_by))}, x0);
     r = r.add({transition("have", mk_ext_action(parse_have))}, x0);
     r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
+    r = r.add({transition("obtains", mk_ext_action(parse_obtains))}, x0);
     r = r.add({transition("(", Expr), transition(")", Skip)}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);

src/frontends/lean/token_table.cpp

@@ -65,7 +65,7 @@ static char const * g_cup            = "\u2294";
 token_table init_token_table() {
     token_table t;
     std::pair<char const *, unsigned> builtin[] =
-        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, {"then", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtains", 0}, {"by", 0}, {"then", 0},
          {"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}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},

tests/lean/run/elim.lean

@@ -0,0 +1,7 @@
+import standard
+using num
+variable p : num → num → num → Bool
+axiom H1 : ∃ x y z, p x y z
+axiom H2 : ∀ {x y z : num}, p x y z → p x x x
+theorem tst : ∃ x, p x x x
+:= obtains a b c H, from H1, exists_intro a (H2 H)