chore(frontends/lean): rename 'obtains' to 'obtain'

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

library/standard/logic.lean

@@ -204,7 +204,7 @@ 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
-:= obtains w Hw, from H2,
+:= obtain w Hw, from H2,
      H1 w (and_elim_left Hw) (and_elim_right Hw)
 
 inductive inhabited (A : Type) : Bool :=
@@ -237,13 +237,13 @@ 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
-:= obtains w Hw, from H, w
+:= obtain 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
-:= obtains (w : A = A) (Hw : cast w a = b), from H,
+:= obtain (w : A = A) (Hw : cast w a = b), from H,
     calc a = cast w a : symm (cast_eq w a)
       ...  = b        : Hw
 
@@ -258,7 +258,7 @@ opaque_hint (hiding cast)
 theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Bool} (H1 : a == b) (H2 : P A a) : P B b
 := have Haux1 : ∀ H : A = A, P A (cast H a), from
      assume H : A = A, subst (symm (cast_eq H a)) H2,
-   obtains (Heq : A = B) (Hw : cast Heq a = b), from H1,
+   obtain (Heq : A = B) (Hw : cast Heq a = b), from H1,
    have Haux2 : P B (cast Heq a), from subst Heq Haux1 Heq,
      subst Hw Haux2
 

src/frontends/lean/builtin_exprs.cpp

@@ -279,16 +279,16 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos)
 }
 
 static name g_exists_elim("exists_elim");
-static expr parse_obtains(parser & p, unsigned, expr const *, pos_info const & pos) {
+static expr parse_obtain(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);
+        throw parser_error("invalid use of 'obtain' 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);
+        throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos);
     bool is_fact = false;
     if (p.curr_is_token(g_fact)) {
         p.next();
@@ -298,10 +298,10 @@ static expr parse_obtains(parser & p, unsigned, expr const *, pos_info const & p
         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_comma, "invalid 'obtain' expression, ',' expected");
-    p.check_token_next(g_from, "invalid 'obtains' expression, 'from' expected");
+    p.check_token_next(g_from, "invalid 'obtain' expression, 'from' expected");
     expr H1 = p.parse_expr();
-    p.check_token_next(g_comma, "invalid 'obtains' expression, ',' expected");
+    p.check_token_next(g_comma, "invalid 'obtain' expression, ',' expected");
     expr b  = p.parse_scoped_expr(ps, env);
     expr H  = ps[num_ps-1];
     name H_name = local_pp_name(H);
@@ -371,7 +371,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("obtain", mk_ext_action(parse_obtain))}, 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}, {"obtains", 0}, {"by", 0}, {"then", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 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

@@ -4,4 +4,4 @@ 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)
+:= obtain a b c H, from H1, exists_intro a (H2 H)

tests/lean/run/elim2.lean

@@ -4,5 +4,5 @@ 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 [fact], from H1,
+:= obtain a b c H [fact], from H1,
      by (apply exists_intro; apply H2; eassumption)