feat(frontends/lean): rename '[fact]' to '[visible]'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
35e68fea76
commit
b4793df653
19 changed files with 50 additions and 50 deletions
|
|
@ -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)⁻¹}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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")
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
@ -75,10 +75,10 @@ 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_fact = false;
|
||||
bool is_visible = false;
|
||||
optional<expr> 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,21 +195,21 @@ static expr parse_proof(parser & p, expr const & prop) {
|
|||
|
||||
static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> 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;
|
||||
is_visible = true;
|
||||
prop = p.parse_expr();
|
||||
} else if (p.curr_is_token(g_colon)) {
|
||||
p.next();
|
||||
|
|
@ -237,7 +237,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> 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));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -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",
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
});
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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))))))),
|
||||
|
|
|
|||
|
|
@ -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 [fact] (p q : bool) (H1 : p) (H2 : q) : q ∧ p
|
||||
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),
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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,
|
||||
then have H [visible] : a ∧ b, from and_intro a b Ha Hb,
|
||||
Ha
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue