From b4793df653d545d30475bb85c7733812a1df187b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Sep 2014 07:47:42 -0700 Subject: [PATCH] feat(frontends/lean): rename '[fact]' to '[visible]' Signed-off-by: Leonardo de Moura --- library/data/quotient/basic.lean | 2 +- library/logic/axioms/piext.lean | 4 +-- library/logic/core/if.lean | 2 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_exprs.cpp | 38 ++++++++++++++-------------- src/frontends/lean/pp.cpp | 4 +-- src/frontends/lean/token_table.cpp | 2 +- src/library/tactic/tactic.cpp | 2 +- tests/lean/have1.lean | 4 +-- tests/lean/have1.lean.expected.out | 4 +-- tests/lean/let1.lean | 4 +-- tests/lean/run/elim2.lean | 2 +- tests/lean/run/have2.lean | 4 +-- tests/lean/run/have6.lean | 10 ++++---- tests/lean/run/tactic11.lean | 2 +- tests/lean/run/univ_bug2.lean | 4 +-- tests/lean/run/uuu.lean | 2 +- tests/lean/show1.lean | 4 +-- tests/lean/show1.lean.expected.out | 4 +-- 19 files changed, 50 insertions(+), 50 deletions(-) diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean index 28559bf87..32947889c 100644 --- a/library/data/quotient/basic.lean +++ b/library/data/quotient/basic.lean @@ -121,7 +121,7 @@ theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {C : B → Type} {f : forall (a : A), C (abs a)} (H : forall (r s : A) (H' : R r s), eq.rec_on (eq_abs Q H') (f r) = f s) {a : A} (Ha : R a a) : rec Q f (abs a) = f a := -have H2 [fact] : R a (rep (abs a)), from R_rep_abs Q Ha, +have H2 [visible] : R a (rep (abs a)), from R_rep_abs Q Ha, calc rec Q f (abs a) = eq.rec_on _ (f (rep (abs a))) : rfl ... = eq.rec_on _ (eq.rec_on _ (f a)) : {(H _ _ H2)⁻¹} diff --git a/library/logic/axioms/piext.lean b/library/logic/axioms/piext.lean index 69f982f47..6d64306d1 100644 --- a/library/logic/axioms/piext.lean +++ b/library/logic/axioms/piext.lean @@ -14,13 +14,13 @@ axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} : theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x) (a : A) : cast H f a == f a := -have Hi [fact] : inhabited (Π x, B x), from inhabited.mk f, +have Hi [visible] : inhabited (Π x, B x), from inhabited.mk f, have Hb : B = B', from piext H, cast_app' Hb f a theorem hcongr_fun {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H : f == f') : f a == f' a := -have Hi [fact] : inhabited (Π x, B x), from inhabited.mk f, +have Hi [visible] : inhabited (Π x, B x), from inhabited.mk f, have Hb : B = B', from piext (type_eq H), hcongr_fun' a H Hb diff --git a/library/logic/core/if.lean b/library/logic/core/if.lean index ce104db86..246842c59 100644 --- a/library/logic/core/if.lean +++ b/library/logic/core/if.lean @@ -53,5 +53,5 @@ Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁) theorem if_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : (if c₁ then t₁ else e₁) = (@ite c₂ (decidable_iff_equiv H₁ Hc) A t₂ e₂) := -have H2 [fact] : decidable c₂, from (decidable_iff_equiv H₁ Hc), +have H2 [visible] : decidable c₂, from (decidable_iff_equiv H₁ Hc), if_congr_aux Hc Ht He diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 5979fbc78..a5ce50a58 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -70,7 +70,7 @@ ;; place holder (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) ;; modifiers - (,(rx (or "\[notation\]" "\[protected\]" "\[private\]" "\[instance\]" "\[class\]" "\[coercion\]" "\[inline\]")) . 'font-lock-doc-face) + (,(rx (or "\[notation\]" "\[visible\]" "\[protected\]" "\[private\]" "\[instance\]" "\[class\]" "\[coercion\]" "\[inline\]")) . 'font-lock-doc-face) ;; tactics (,(rx symbol-start (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat") diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index a34dff6ec..88cb4f74f 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -25,7 +25,7 @@ Author: Leonardo de Moura namespace lean { namespace notation { static name g_llevel_curly(".{"), g_rcurly("}"), g_in("in"), g_colon(":"), g_assign(":="); -static name g_comma(","), g_fact("[fact]"), g_from("from"), g_using("using"); +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_take("take"), g_assume("assume"), g_show("show"), g_fun("fun"); @@ -57,10 +57,10 @@ static expr parse_let_body(parser & p, pos_info const & pos) { } } -static void parse_let_modifiers(parser & p, bool & is_fact) { +static void parse_let_modifiers(parser & p, bool & is_visible) { while (true) { - if (p.curr_is_token(g_fact)) { - is_fact = true; + if (p.curr_is_token(g_visible)) { + is_visible = true; p.next(); } else { break; @@ -73,12 +73,12 @@ static expr parse_let(parser & p, pos_info const & pos) { if (p.parse_local_notation_decl()) { return parse_let_body(p, pos); } else { - auto id_pos = p.pos(); - name id = p.check_atomic_id_next("invalid let declaration, identifier expected"); - bool is_fact = false; + 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_fact); + parse_let_modifiers(p, is_visible); if (p.curr_is_token(g_assign)) { p.next(); value = p.parse_expr(); @@ -195,22 +195,22 @@ static expr parse_proof(parser & p, expr const & prop) { static expr parse_have_core(parser & p, pos_info const & pos, optional const & prev_local) { auto id_pos = p.pos(); - bool is_fact = false; + bool is_visible = false; name id; expr prop; - if (p.curr_is_token(g_fact)) { + if (p.curr_is_token(g_visible)) { p.next(); - is_fact = true; + is_visible = true; id = p.mk_fresh_name(); prop = p.parse_expr(); } else if (p.curr_is_identifier()) { id = p.get_name_val(); p.next(); - if (p.curr_is_token(g_fact)) { + if (p.curr_is_token(g_visible)) { p.next(); p.check_token_next(g_colon, "invalid 'have' declaration, ':' expected"); - is_fact = true; - prop = p.parse_expr(); + is_visible = true; + prop = p.parse_expr(); } else if (p.curr_is_token(g_colon)) { p.next(); prop = p.parse_expr(); @@ -237,7 +237,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con } p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected"); parser::local_scope scope(p); - binder_info bi = mk_contextual_info(is_fact); + binder_info bi = mk_contextual_info(is_visible); expr l = p.save_pos(mk_local(id, prop, bi), pos); p.add_local(l); expr body; @@ -280,12 +280,12 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po unsigned num_ps = ps.size(); if (num_ps < 2) throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos); - bool is_fact = false; - if (p.curr_is_token(g_fact)) { + bool is_visible = false; + if (p.curr_is_token(g_visible)) { p.next(); - is_fact = true; + is_visible = true; } - if (!is_fact) { + if (!is_visible) { expr H = ps[num_ps-1]; ps[num_ps-1] = update_local(H, mlocal_type(H), local_info(H).update_contextual(false)); } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 94117c8de..006c8af39 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -43,7 +43,7 @@ static format g_in_fmt = highlight_keyword(format("in")); static format g_assign_fmt = highlight_keyword(format(":=")); static format g_have_fmt = highlight_keyword(format("have")); static format g_from_fmt = highlight_keyword(format("from")); -static format g_fact_fmt = highlight_keyword(format("[fact]")); +static format g_visible_fmt = highlight_keyword(format("[visible]")); static format g_show_fmt = highlight_keyword(format("show")); static format g_explicit_fmt = highlight_keyword(format("@")); @@ -362,7 +362,7 @@ auto pretty_fn::pp_have(expr const & e) -> result { format body_fmt = pp_child(body, 0).first; format r = g_have_fmt + space() + format(n) + space(); if (binding_info(binding).is_contextual()) - r += compose(g_fact_fmt, space()); + r += compose(g_visible_fmt, space()); r += colon() + nest(m_indent, line() + type_fmt + comma() + space() + g_from_fmt); r = group(r); r += nest(m_indent, line() + proof_fmt + comma()); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index dc849c2f3..930c2865d 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -77,7 +77,7 @@ token_table init_token_table() { {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion", - "variables", "[private]", "[protected]", "[inline]", "[fact]", "[instance]", + "variables", "[private]", "[protected]", "[inline]", "[visible]", "[instance]", "[class]", "[module]", "[coercion]", "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe", diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 43e94b515..78dadf092 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -28,7 +28,7 @@ void check_has_no_local(expr const & v, expr const & e, char const * tac_name) { if (is_local(l)) throw tactic_exception(e, sstream() << "tactic '" << tac_name << "' contains reference to local '" << local_pp_name(l) << "' which is not visible by this tactic " - << "possible causes: it was not marked as [fact]; it was destructued"); + << "possible causes: it was not marked as [visible]; it was destructued"); return has_local(l); }); } diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean index 858989c3f..8a7f4c6b6 100644 --- a/tests/lean/have1.lean +++ b/tests/lean/have1.lean @@ -5,10 +5,10 @@ variables a b c : bool axiom H1 : a = b axiom H2 : b = c -check have e1 [fact] : a = b, from H1, +check have e1 [visible] : a = b, from H1, have e2 : a = c, by apply trans; apply e1; apply H2, have e3 : c = a, from e2⁻¹, - have e4 [fact] : b = a, from e1⁻¹, + have e4 [visible] : b = a, from e1⁻¹, have e5 : b = c, from e4 ⬝ e2, have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹, e3 ⬝ e2 diff --git a/tests/lean/have1.lean.expected.out b/tests/lean/have1.lean.expected.out index e2604264f..4bb73aac7 100644 --- a/tests/lean/have1.lean.expected.out +++ b/tests/lean/have1.lean.expected.out @@ -1,7 +1,7 @@ -have e1 [fact] : eq a b, from H1, +have e1 [visible] : eq a b, from H1, have e2 : eq a c, from trans e1 H2, have e3 : eq c a, from symm e2, -have e4 [fact] : eq b a, from symm e1, +have e4 [visible] : eq b a, from symm e1, have e5 : eq b c, from trans e4 e2, have e6 : eq a a, from trans H1 (trans H2 (trans (symm H2) (trans (symm H1) (trans H1 (trans H2 (trans (symm H2) (symm H1))))))), diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean index bcad91633..93b717bf3 100644 --- a/tests/lean/let1.lean +++ b/tests/lean/let1.lean @@ -14,8 +14,8 @@ 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 [fact] (p q : bool) (H1 : p) (H2 : q) : q ∧ p + infixl `∧`:25 := and, + and_intro [visible] (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/elim2.lean b/tests/lean/run/elim2.lean index c7a33fa81..c1a2e677c 100644 --- a/tests/lean/run/elim2.lean +++ b/tests/lean/run/elim2.lean @@ -4,5 +4,5 @@ variable p : num → num → num → Prop 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 -:= obtain a b c H [fact], from H1, +:= obtain a b c H [visible], from H1, by (apply exists_intro; apply H2; eassumption) diff --git a/tests/lean/run/have2.lean b/tests/lean/run/have2.lean index 71ca1ed2d..ef0cb5a18 100644 --- a/tests/lean/run/have2.lean +++ b/tests/lean/run/have2.lean @@ -3,6 +3,6 @@ variables a b c : Prop axiom Ha : a axiom Hb : b axiom Hc : c -check have H1 [fact] : a, from Ha, +check have H1 [visible] : a, from Ha, have H2 : a, from H1, - H2 \ No newline at end of file + H2 diff --git a/tests/lean/run/have6.lean b/tests/lean/run/have6.lean index 758bf68fd..df5face1f 100644 --- a/tests/lean/run/have6.lean +++ b/tests/lean/run/have6.lean @@ -8,11 +8,11 @@ axiom Hb : b axiom Hc : c check have a ∧ b, from and_intro a b Ha Hb, - have [fact] b ∧ a, from and_intro b a Hb Ha, + have [visible] b ∧ a, from and_intro b a Hb Ha, have H : a ∧ b, from and_intro a b Ha Hb, - have H [fact] : a ∧ b, from and_intro a b Ha Hb, + have H [visible] : a ∧ b, from and_intro a b Ha Hb, then have a ∧ b, from and_intro a b Ha Hb, - then have [fact] b ∧ a, from and_intro b a Hb Ha, + then have [visible] b ∧ a, from and_intro b a Hb Ha, then have H : a ∧ b, from and_intro a b Ha Hb, - then have H [fact] : a ∧ b, from and_intro a b Ha Hb, - Ha \ No newline at end of file + then have H [visible] : a ∧ b, from and_intro a b Ha Hb, + Ha diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean index 8b41c6e41..32eaabea2 100644 --- a/tests/lean/run/tactic11.lean +++ b/tests/lean/run/tactic11.lean @@ -2,7 +2,7 @@ import logic open tactic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a -:= have H1 [fact] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics +:= have H1 [visible] : 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; apply (assume Hb, iff.elim_right H Hb); diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean index 5c58b2ee5..219f85180 100644 --- a/tests/lean/run/univ_bug2.lean +++ b/tests/lean/run/univ_bug2.lean @@ -25,8 +25,8 @@ mk (congr (get_eq C1) (get_eq C2)) theorem test1 (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S) (Hf : f1 = f2) (Hs : s1 = s2) : f1 s1 = f2 s2 := -have Rs [fact] : simplifies_to f1 f2, from mk Hf, -have Cs [fact] : simplifies_to s1 s2, from mk Hs, +have Rs [visible] : simplifies_to f1 f2, from mk Hf, +have Cs [visible] : simplifies_to s1 s2, from mk Hs, infer_eq _ _ end simplifies_to diff --git a/tests/lean/run/uuu.lean b/tests/lean/run/uuu.lean index 8b8a09936..a0b8422e5 100644 --- a/tests/lean/run/uuu.lean +++ b/tests/lean/run/uuu.lean @@ -68,7 +68,7 @@ definition dirprodf {X : Type} {Y : Type} {X' : Type} {Y' : Type} (f : X → Y) := dirprodpair (f (pr1 xx')) (f' (pr2 xx')) definition ddualand {X : Type} {Y : Type} {P : Type} (xp : (X → P) → P) (yp : (Y → P) → P) : (dirprod X Y → P) → P := λ X0, - let int1 [fact] := λ (ypp : (Y → P) → P) (x : X), yp (λ y : Y, X0 (dirprodpair x y)) in + let int1 := λ (ypp : (Y → P) → P) (x : X), yp (λ y : Y, X0 (dirprodpair x y)) in xp (int1 yp) definition neg (X : Type) : Type := X → empty diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean index e0688bcf8..27479a3ed 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 [fact] : a = b, from H1, +check have e1 [visible] : a = b, from H1, have e2 : a = c, by apply eq.trans; apply e1; apply H2, have e3 : c = a, from e2⁻¹, - have e4 [fact] : b = a, from e1⁻¹, + have e4 [visible] : b = a, from e1⁻¹, show b = c, from e1⁻¹ ⬝ e2 diff --git a/tests/lean/show1.lean.expected.out b/tests/lean/show1.lean.expected.out index d136ca271..415259862 100644 --- a/tests/lean/show1.lean.expected.out +++ b/tests/lean/show1.lean.expected.out @@ -1,8 +1,8 @@ show eq a c, from eq.trans H1 H2 : eq a c ------------ -have e1 [fact] : eq a b, from H1, +have e1 [visible] : eq a b, from H1, have e2 : eq a c, from eq.trans e1 H2, have e3 : eq c a, from eq.symm e2, -have e4 [fact] : eq b a, from eq.symm e1, +have e4 [visible] : eq b a, from eq.symm e1, show eq b c, from eq.trans (eq.symm e1) e2 : eq b c