michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean): import explicit versions when using the command 'using'

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-06 17:33:58 -08:00
parent ea06bb2885
commit 4b4b5e3345
2 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/builtin/sum.lean
View file

@ -15,17 +15,17 @@ definition sum (A B : (Type U)) := subtype ((optional A) # (optional B)) (sum_pr
namespace sum
theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none)
:= not_intro
(assume N : (some a = none) = (none = (optional::@none B)),
(assume N : (some a = none) = (none = (@none B)),
have eq : some a = none,
from (symm N) ◂ (refl (optional::@none B)),
from (symm N) ◂ (refl (@none B)),
show false,
from absurd eq (distinct a))
theorem inr_pred (A : (Type U)) {B : (Type U)} (b : B) : sum_pred A B (pair none (some b))
:= not_intro
(assume N : (none = (optional::@none A)) = (some b = none),
(assume N : (none = (@none A)) = (some b = none),
have eq : some b = none,
from N ◂ (refl (optional::@none A)),
from N ◂ (refl (@none A)),
show false,
from absurd eq (distinct b))
@ -53,8 +53,8 @@ theorem inl_inj {A B : (Type U)} {a1 a2 : A} : inl a1 B = inl a2 B → a1 = a2
from abst_inj (inhabl (inhabited_intro a1) B) (inl_pred a1 B) (inl_pred a2 B) (trans (trans (symm eq1) Heq) eq2),
show a1 = a2,
from optional::injectivity
(calc some a1 = proj1 (pair (some a1) (optional::@none B)) : refl (some a1)
... = proj1 (pair (some a2) (optional::@none B)) : pair_inj1 rep_eq
(calc some a1 = proj1 (pair (some a1) (@none B)) : refl (some a1)
... = proj1 (pair (some a2) (@none B)) : pair_inj1 rep_eq
... = some a2 : refl (some a2))
theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
@ -67,9 +67,9 @@ theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
from abst_inj (inhabr A (inhabited_intro b1)) (inr_pred A b1) (inr_pred A b2) (trans (trans (symm eq1) Heq) eq2),
show b1 = b2,
from optional::injectivity
(calc some b1 = proj2 (pair (optional::@none A) (some b1)) : refl (some b1)
... = proj2 (pair (optional::@none A) (some b2)) : pair_inj2 rep_eq
... = some b2 : refl (some b2))
(calc some b1 = proj2 (pair (@none A) (some b1)) : refl (some b1)
... = proj2 (pair (@none A) (some b2)) : pair_inj2 rep_eq
... = some b2 : refl (some b2))
theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
:= assume N : inl a B = inr A b,
@ -86,7 +86,7 @@ theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃
:= let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n
in or_elim (em (proj1 (rep n) = none))
(assume Heq : proj1 (rep n) = none,
have neq_none : ¬ proj2 (rep n) = (optional::@none B),
have neq_none : ¬ proj2 (rep n) = (@none B),
from (symm (not_iff_elim (ne_symm pred))) ◂ Heq,
have ex_some : ∃ b, proj2 (rep n) = some b,
from resolve1 (optional::dichotomy (proj2 (rep n))) neq_none,
@ -103,7 +103,7 @@ theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃
show (∃ b, n = inr A b),
from exists_intro b n_eq_inr))
(assume Hne : ¬ proj1 (rep n) = none,
have eq_none : proj2 (rep n) = (optional::@none B),
have eq_none : proj2 (rep n) = (@none B),
from (not_iff_elim pred) ◂ Hne,
have ex_some : ∃ a, proj1 (rep n) = some a,
from resolve1 (optional::dichotomy (proj1 (rep n))) Hne,

2
src/frontends/lean/parser_cmds.cpp
View file

@ -809,7 +809,7 @@ void parser_imp::parse_using() {
}
buffer<std::pair<name, name>> to_add;
for (auto it = m_env->begin_objects(); it != m_env->end_objects(); ++it) {
if (it->has_type() && it->has_name() && !is_hidden_object(*it) && is_prefix_of(prefix, it->get_name())) {
if (it->has_type() && it->has_name() && supported_by_pp(*it) && is_prefix_of(prefix, it->get_name())) {
auto n = replace_prefix(it->get_name(), prefix, new_prefix);
if (!n.is_anonymous())
to_add.emplace_back(n, it->get_name());