From 1d273fcfddc9a0429f378d60aa50eabc225616fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Jul 2014 06:35:24 +0100 Subject: [PATCH] chore(frontends/lean): rename 'obtains' to 'obtain' Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 8 ++++---- src/frontends/lean/builtin_exprs.cpp | 14 +++++++------- src/frontends/lean/token_table.cpp | 2 +- tests/lean/run/elim.lean | 2 +- tests/lean/run/elim2.lean | 2 +- 5 files changed, 14 insertions(+), 14 deletions(-) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index 8c43a156a..cfdf6857c 100644 --- a/library/standard/logic.lean +++ b/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 diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 8f9f97ef9..f07c0cbc8 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/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 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_from, "invalid 'obtains' expression, 'from' expected"); + p.check_token_next(g_comma, "invalid 'obtain' expression, ',' 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); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index d7c59dea6..d00c50b3e 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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 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}, diff --git a/tests/lean/run/elim.lean b/tests/lean/run/elim.lean index a3bb4ba72..51786842e 100644 --- a/tests/lean/run/elim.lean +++ b/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) diff --git a/tests/lean/run/elim2.lean b/tests/lean/run/elim2.lean index a6036e011..6ed301e5a 100644 --- a/tests/lean/run/elim2.lean +++ b/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)