From b41c65f549156d66cd8340fc909c28886de4af36 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Feb 2016 12:31:23 -0800 Subject: [PATCH] feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking --- hott/init/equiv.hlean | 4 +- hott/init/trunc.hlean | 2 +- library/algebra/ordered_field.lean | 2 +- library/data/pnat.lean | 2 +- library/theories/analysis/metric_space.lean | 10 ++-- library/theories/analysis/real_limit.lean | 4 +- src/frontends/lean/builtin_exprs.cpp | 66 ++++++--------------- src/frontends/lean/tokens.cpp | 4 -- src/frontends/lean/tokens.h | 1 - src/frontends/lean/tokens.txt | 1 - tests/lean/let1.lean | 2 +- tests/lean/run/class8.lean | 4 +- tests/lean/run/have2.lean | 2 +- tests/lean/run/tactic11.lean | 4 +- tests/lean/show1.lean | 4 +- 15 files changed, 37 insertions(+), 75 deletions(-) diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 70113618b..98edc28d3 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -132,11 +132,11 @@ namespace is_equiv adjointify f⁻¹ f (left_inv f) (right_inv f) definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) := - have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f, + have Hfinv : is_equiv f⁻¹, from is_equiv_inv f, @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@right_inv _ _ f _ b)) definition cancel_left (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) := - have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f, + have Hfinv : is_equiv f⁻¹, from is_equiv_inv f, @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, left_inv f (g a)) definition eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : x = y := diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 2630de5e1..527e0eab4 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -201,7 +201,7 @@ namespace is_trunc theorem is_prop_of_imp_is_contr {A : Type} (H : A → is_contr A) : is_prop A := @is_trunc_succ_intro A -2 (λx y, - have H2 [visible] : is_contr A, from H x, + have H2 : is_contr A, from H x, !is_contr_eq) theorem is_prop.mk {A : Type} (H : ∀x y : A, x = y) : is_prop A := diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index 396359c3b..5bde93627 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -539,7 +539,7 @@ section discrete_linear_ordered_field !eq_div_of_mul_eq this !eq_sign_mul_abs⁻¹) theorem add_quarters (a : A) : a / 4 + a / 4 = a / 2 := - have H4 [visible] : (4 : A) = 2 * 2, by norm_num, + have H4 : (4 : A) = 2 * 2, by norm_num, calc a / 4 + a / 4 = (a + a) / (2 * 2) : by rewrite [-H4, div_add_div_same] ... = (a * 1 + a * 1) / (2 * 2) : by rewrite mul_one diff --git a/library/data/pnat.lean b/library/data/pnat.lean index 4b4bf6f8d..fbf68b547 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -228,7 +228,7 @@ end theorem add_halves_double (m n : ℕ+) : m⁻¹ + n⁻¹ = ((2 * m)⁻¹ + (2 * n)⁻¹) + ((2 * m)⁻¹ + (2 * n)⁻¹) := -have hsimp [visible] : ∀ a b : ℚ, (a + a) + (b + b) = (a + b) + (a + b), +have hsimp : ∀ a b : ℚ, (a + a) + (b + b) = (a + b) + (a + b), by intros; rewrite [rat.add_assoc, -(rat.add_assoc a b b), {_+b}rat.add_comm, -*rat.add_assoc], by rewrite [-pnat.add_halves m, -pnat.add_halves n, hsimp] diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index fd3f01242..978e7eb80 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -46,7 +46,7 @@ lt_of_le_of_ne !dist_nonneg (suppose 0 = dist x y, H (iff.mp !dist_eq_zero_iff t proposition ne_of_dist_pos {x y : M} (H : dist x y > 0) : x ≠ y := suppose x = y, -have H1 [visible] : dist x x > 0, by rewrite this at {2}; exact H, +have H1 : dist x x > 0, by rewrite this at {2}; exact H, by rewrite dist_self at H1; apply not_lt_self _ H1 proposition eq_of_forall_dist_le {x y : M} (H : ∀ ε, ε > 0 → dist x y ≤ ε) : x = y := @@ -351,7 +351,7 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) obtain ε Hε, from exists_not_of_not_forall Hnot, let Hε' := and_not_of_not_implies Hε in obtain (H1 : ε > 0) H2, from Hε', - have H3 [visible] : ∀ δ : ℝ, (δ > 0 → ∃ x' : M, x' ≠ c ∧ dist x' c < δ ∧ dist (f x') l ≥ ε), begin -- tedious!! + have H3 : ∀ δ : ℝ, (δ > 0 → ∃ x' : M, x' ≠ c ∧ dist x' c < δ ∧ dist (f x') l ≥ ε), begin -- tedious!! intros δ Hδ, note Hε'' := forall_not_of_not_exists H2, note H4 := forall_not_of_not_exists H2 δ, @@ -371,7 +371,7 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) assumption end, let S : ℕ → M → Prop := λ n x, 0 < dist x c ∧ dist x c < 1 / (of_nat n + 1) ∧ dist (f x) l ≥ ε in - have HS [visible] : ∀ n : ℕ, ∃ m : M, S n m, begin + have HS : ∀ n : ℕ, ∃ m : M, S n m, begin intro k, have Hpos : 0 < of_nat k + 1, from of_nat_succ_pos k, cases H3 (1 / (k + 1)) (one_div_pos_of_pos Hpos) with x' Hx', @@ -386,7 +386,7 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) repeat assumption end, let X : ℕ → M := λ n, some (HS n) in - have H4 [visible] : ∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c in ℕ), from + have H4 : ∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c in ℕ), from (take n, and.intro (begin note Hspec := some_spec (HS n), @@ -404,7 +404,7 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) cases Hspec2, assumption end)), - have H5 [visible] : (λ n : ℕ, f (X n)) ⟶ l in ℕ, from Hseq X H4, + have H5 : (λ n : ℕ, f (X n)) ⟶ l in ℕ, from Hseq X H4, begin note H6 := H5 H1, cases H6 with Q HQ, diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index c8bf2b606..084e4db7a 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -343,7 +343,7 @@ proposition mul_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : assumption end, obtain K HK, from Hbd, - have Habsle [visible] : ∀ n, abs (X n * Y n - x * y) ≤ K * abs (Y n - y) + abs y * abs (X n - x), begin + have Habsle : ∀ n, abs (X n * Y n - x * y) ≤ K * abs (Y n - y) + abs y * abs (X n - x), begin intro, have Heq : X n * Y n - x * y = (X n * Y n - X n * y) + (X n * y - x * y), by rewrite [-sub_add_cancel (X n * Y n) (X n * y) at {1}, sub_eq_add_neg, *add.assoc], @@ -358,7 +358,7 @@ proposition mul_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : rewrite [-mul_sub_right_distrib, abs_mul, mul.comm], apply le.refl end, - have Hdifflim [visible] : (λ n, abs (X n * Y n - x * y)) ⟶ 0 in ℕ, begin + have Hdifflim : (λ n, abs (X n * Y n - x * y)) ⟶ 0 in ℕ, begin apply converges_to_seq_squeeze, rotate 2, intro, apply abs_nonneg, diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index b47bc9d5c..5617a9cf5 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -73,17 +73,6 @@ static expr parse_let_body(parser & p, pos_info const & pos) { } } -static void parse_let_modifiers(parser & p, bool & is_visible) { - while (true) { - if (p.curr_is_token(get_visible_tk())) { - is_visible = true; - p.next(); - } else { - break; - } - } -} - // Distribute mk_typed_expr over choice expression. // see issue #768 static expr mk_typed_expr_distrib_choice(parser & p, expr const & type, expr const & value, pos_info const & pos) { @@ -105,10 +94,8 @@ static expr parse_let(parser & p, pos_info const & pos) { } else { auto id_pos = p.pos(); name id = p.check_atomic_id_next("invalid let declaration, identifier expected"); - bool is_visible = false; optional type; expr value; - parse_let_modifiers(p, is_visible); if (p.curr_is_token(get_assign_tk())) { p.next(); value = p.parse_expr(); @@ -342,9 +329,9 @@ static expr parse_proof_qed_core(parser & p, pos_info const & pos) { return r; } -static expr parse_proof(parser & p, expr const & prop); +static expr parse_proof(parser & p); -static expr parse_using_expr(parser & p, expr const & prop, pos_info const & using_pos) { +static expr parse_using_expr(parser & p, pos_info const & using_pos) { parser::local_scope scope(p); buffer locals; buffer new_locals; @@ -366,7 +353,7 @@ static expr parse_using_expr(parser & p, expr const & prop, pos_info const & usi new_locals.push_back(new_l); } p.next(); // consume ',' - expr pr = parse_proof(p, prop); + expr pr = parse_proof(p); unsigned i = locals.size(); while (i > 0) { --i; @@ -379,11 +366,10 @@ static expr parse_using_expr(parser & p, expr const & prop, pos_info const & usi } static expr parse_using(parser & p, unsigned, expr const *, pos_info const & pos) { - expr prop = p.save_pos(mk_expr_placeholder(), pos); - return parse_using_expr(p, prop, pos); + return parse_using_expr(p, pos); } -static expr parse_proof(parser & p, expr const & prop) { +static expr parse_proof(parser & p) { if (p.curr_is_token(get_from_tk())) { // parse: 'from' expr p.next(); @@ -409,24 +395,14 @@ static expr parse_proof(parser & p, expr const & prop) { } } -static expr parse_have_core(parser & p, pos_info const & pos, optional const & prev_local, bool is_visible) { +static expr parse_have_core(parser & p, pos_info const & pos, optional const & prev_local) { auto id_pos = p.pos(); name id; expr prop; - if (p.curr_is_token(get_visible_tk())) { - p.next(); - is_visible = true; - id = get_this_tk(); - prop = p.parse_expr(); - } else if (p.curr_is_identifier()) { + if (p.curr_is_identifier()) { id = p.get_name_val(); p.next(); - if (p.curr_is_token(get_visible_tk())) { - p.next(); - p.check_token_next(get_colon_tk(), "invalid 'have/assert' declaration, ':' expected"); - is_visible = true; - prop = p.parse_expr(); - } else if (p.curr_is_token(get_colon_tk())) { + if (p.curr_is_token(get_colon_tk())) { p.next(); prop = p.parse_expr(); } else { @@ -452,18 +428,16 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con parser::local_scope scope(p); p.add_local(*prev_local); auto proof_pos = p.pos(); - proof = parse_proof(p, prop); + proof = parse_proof(p); proof = p.save_pos(Fun(*prev_local, proof), proof_pos); proof = p.save_pos(mk_app(proof, *prev_local), proof_pos); } else { - proof = parse_proof(p, prop); + proof = parse_proof(p); } } p.check_token_next(get_comma_tk(), "invalid 'have/assert' declaration, ',' expected"); parser::local_scope scope(p); - is_visible = true; - binder_info bi = mk_contextual_info(is_visible); - expr l = p.save_pos(mk_local(id, prop, bi), pos); + expr l = p.save_pos(mk_local(id, prop), pos); p.add_local(l); expr body; if (p.curr_is_token(get_then_tk())) { @@ -471,12 +445,10 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con p.next(); if (p.curr_is_token(get_assert_tk())) { p.next(); - is_visible = true; } else { p.check_token_next(get_have_tk(), "invalid 'then' declaration, 'have' or 'assert' expected"); - is_visible = true; } - body = parse_have_core(p, then_pos, some_expr(l), is_visible); + body = parse_have_core(p, then_pos, some_expr(l)); } else { body = p.parse_expr(); } @@ -484,16 +456,12 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con body = abstract(body, l); if (get_parser_checkpoint_have(p.get_options())) body = mk_checkpoint_annotation(body); - expr r = p.save_pos(mk_have_annotation(p.save_pos(mk_lambda(id, prop, body, bi), pos)), pos); + expr r = p.save_pos(mk_have_annotation(p.save_pos(mk_lambda(id, prop, body), pos)), pos); return p.mk_app(r, proof, pos); } static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) { - return parse_have_core(p, pos, none_expr(), false); -} - -static expr parse_assert(parser & p, unsigned, expr const *, pos_info const & pos) { - return parse_have_core(p, pos, none_expr(), true); + return parse_have_core(p, pos, none_expr()); } static expr parse_suppose(parser & p, unsigned, expr const *, pos_info const & pos) { @@ -534,7 +502,7 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) return parse_local_equations(p, fn); } else { p.check_token_next(get_comma_tk(), "invalid 'show' declaration, ',' expected"); - expr proof = parse_proof(p, prop); + expr proof = parse_proof(p); expr b = p.save_pos(mk_lambda(get_this_tk(), prop, Var(0)), pos); expr r = p.mk_app(b, proof, pos); return p.save_pos(mk_show_annotation(r), pos); @@ -572,7 +540,7 @@ static expr parse_suffices_to_show(parser & p, unsigned, expr const *, pos_info { parser::local_scope scope(p); p.add_local(local); - body = parse_proof(p, prop); + body = parse_proof(p); } expr proof = p.save_pos(Fun(local, body), pos); p.check_token_next(get_comma_tk(), "invalid 'suffices' declaration, ',' expected"); @@ -765,7 +733,7 @@ parse_table init_nud_table() { r = r.add({transition("by", mk_ext_action_core(parse_by))}, x0); r = r.add({transition("by+", mk_ext_action_core(parse_by_plus))}, x0); r = r.add({transition("have", mk_ext_action(parse_have))}, x0); - r = r.add({transition("assert", mk_ext_action(parse_assert))}, x0); + r = r.add({transition("assert", mk_ext_action(parse_have))}, x0); r = r.add({transition("suppose", mk_ext_action(parse_suppose))}, x0); r = r.add({transition("show", mk_ext_action(parse_show))}, x0); r = r.add({transition("suffices", mk_ext_action(parse_suffices_to_show))}, x0); diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 2f708a826..26c2b2a9d 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -77,7 +77,6 @@ static name const * g_wf_tk = nullptr; static name const * g_in_tk = nullptr; static name const * g_at_tk = nullptr; static name const * g_assign_tk = nullptr; -static name const * g_visible_tk = nullptr; static name const * g_from_tk = nullptr; static name const * g_using_tk = nullptr; static name const * g_then_tk = nullptr; @@ -227,7 +226,6 @@ void initialize_tokens() { g_in_tk = new name{"in"}; g_at_tk = new name{"at"}; g_assign_tk = new name{":="}; - g_visible_tk = new name{"[visible]"}; g_from_tk = new name{"from"}; g_using_tk = new name{"using"}; g_then_tk = new name{"then"}; @@ -378,7 +376,6 @@ void finalize_tokens() { delete g_in_tk; delete g_at_tk; delete g_assign_tk; - delete g_visible_tk; delete g_from_tk; delete g_using_tk; delete g_then_tk; @@ -528,7 +525,6 @@ name const & get_wf_tk() { return *g_wf_tk; } name const & get_in_tk() { return *g_in_tk; } name const & get_at_tk() { return *g_at_tk; } name const & get_assign_tk() { return *g_assign_tk; } -name const & get_visible_tk() { return *g_visible_tk; } name const & get_from_tk() { return *g_from_tk; } name const & get_using_tk() { return *g_using_tk; } name const & get_then_tk() { return *g_then_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 4288c8adb..468c49525 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -79,7 +79,6 @@ name const & get_wf_tk(); name const & get_in_tk(); name const & get_at_tk(); name const & get_assign_tk(); -name const & get_visible_tk(); name const & get_from_tk(); name const & get_using_tk(); name const & get_then_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index 13d4eedd4..d42d63532 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -72,7 +72,6 @@ wf [wf] in in at at assign := -visible [visible] from from using using then then diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean index 5741efe45..b762e8110 100644 --- a/tests/lean/let1.lean +++ b/tests/lean/let1.lean @@ -15,7 +15,7 @@ check let bool := Type.{0}, check let bool := Type.{0}, and (p q : bool) := ∀ c : bool, (p → q → c) → c, infixl `∧`:25 := and, - and_intro [visible] (p q : bool) (H1 : p) (H2 : q) : q ∧ p + and_intro (p q : bool) (H1 : p) (H2 : q) : q ∧ p := λ (c : bool) (H : p → q → c), H H1 H2, and_elim_left (p q : bool) (H : p ∧ q) : p := H p (λ (H1 : p) (H2 : q), H1), diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean index 31d445358..dd8fd8268 100644 --- a/tests/lean/run/class8.lean +++ b/tests/lean/run/class8.lean @@ -28,8 +28,8 @@ theorem tst {A B : Type} (H : inh B) : inh (A → B → B) set_option trace.class_instances true theorem T1 {A B C D : Type} {P : C → Prop} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Prop) := -have h1 [visible] : inh A, from inh.intro a, -have h2 [visible] : inh C, from inh_exists H2, +have h1 : inh A, from inh.intro a, +have h2 : inh C, from inh_exists H2, by exact _ reveal T1 diff --git a/tests/lean/run/have2.lean b/tests/lean/run/have2.lean index bc40d4bc2..aae47af58 100644 --- a/tests/lean/run/have2.lean +++ b/tests/lean/run/have2.lean @@ -4,6 +4,6 @@ constants a b c : Prop axiom Ha : a axiom Hb : b axiom Hc : c -check have H1 [visible] : a, from Ha, +check have H1 : a, from Ha, have H2 : a, from H1, H2 diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean index f5c0df598..9aa53a80b 100644 --- a/tests/lean/run/tactic11.lean +++ b/tests/lean/run/tactic11.lean @@ -1,7 +1,7 @@ import logic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a -:= have H1 [visible] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics +:= have H1 : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics from iff.elim_left H, by apply iff.intro; intro Hb; @@ -10,7 +10,7 @@ theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a apply (H1 Ha) theorem tst2 (a b : Prop) (H : a ↔ b) : b ↔ a -:= have H1 [visible] : a → b, +:= have H1 : a → b, from iff.elim_left H, begin apply iff.intro, diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean index 4efbb3d37..b57e62dc3 100644 --- a/tests/lean/show1.lean +++ b/tests/lean/show1.lean @@ -7,8 +7,8 @@ axiom H2 : b = c check show a = c, from H1 ⬝ H2 print "------------" -check have e1 [visible] : a = b, from H1, +check have e1 : a = b, from H1, have e2 : a = c, by apply eq.trans; apply e1; apply H2, have e3 : c = a, from e2⁻¹, - have e4 [visible] : b = a, from e1⁻¹, + have e4 : b = a, from e1⁻¹, show b = c, from e1⁻¹ ⬝ e2