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

fix(frontends/lean): consistent behavior for protected declarations

Browse source 
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608

closes #609
This commit is contained in:
Leonardo de Moura 2015-05-18 22:35:18 -07:00
parent d8bd3c21b5
commit e1c2340db2
34 changed files with 229 additions and 210 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
hott/algebra/category/functor.hlean
View file

@ -39,7 +39,7 @@ namespace functor
G (F (g ∘ f)) = G (F g ∘ F f) : by rewrite respect_comp
... = G (F g) ∘ G (F f) : by rewrite respect_comp)
infixr `∘f`:60 := compose
infixr `∘f`:60 := functor.compose
protected definition id [reducible] {C : Precategory} : functor C C :=
mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp)
@ -88,7 +88,7 @@ namespace functor
apply (respect_id F) ),
end
attribute preserve_iso [instance]
attribute functor.preserve_iso [instance]
protected definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b)
[H : is_iso f] [H' : is_iso (F f)] :
@ -107,10 +107,10 @@ namespace functor
H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
!functor_mk_eq_constant (λa b f, idp)
protected definition id_left (F : C ⇒ D) : id ∘f F = F :=
protected definition id_left (F : C ⇒ D) : functor.id ∘f F = F :=
functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp))
protected definition id_right (F : C ⇒ D) : F ∘f id = F :=
protected definition id_right (F : C ⇒ D) : F ∘f functor.id = F :=
functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp))
protected definition comp_id_eq_id_comp (F : C ⇒ D) : F ∘f functor.id = functor.id ∘f F :=
@ -198,7 +198,7 @@ definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun
!ap010_functor_eq
definition ap010_assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) (a : A) :
ap010 to_fun_ob (assoc H G F) a = idp :=
ap010 to_fun_ob (functor.assoc H G F) a = idp :=
by apply ap010_functor_mk_eq_constant
definition compose_pentagon (K : D ⇒ E) (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :

10
hott/algebra/category/nat_trans.hlean
View file

@ -30,13 +30,13 @@ namespace nat_trans
... = η b ∘ (θ b ∘ F f) : by rewrite naturality
... = (η b ∘ θ b) ∘ F f : by rewrite assoc)
infixr `∘n`:60 := compose
infixr `∘n`:60 := nat_trans.compose
protected definition id [reducible] {C D : Precategory} {F : functor C D} : nat_trans F F :=
mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹)
protected definition ID [reducible] {C D : Precategory} (F : functor C D) : nat_trans F F :=
(@id C D F)
(@nat_trans.id C D F)
definition nat_trans_mk_eq {η₁ η₂ : Π (a : C), hom (F a) (G a)}
(nat₁ : Π (a b : C) (f : hom a b), G f ∘ η₁ a = η₁ b ∘ F f)
@ -52,10 +52,10 @@ namespace nat_trans
η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
nat_trans_eq (λa, !assoc)
protected definition id_left (η : F ⟹ G) : id ∘n η = η :=
protected definition id_left (η : F ⟹ G) : nat_trans.id ∘n η = η :=
nat_trans_eq (λa, !id_left)
protected definition id_right (η : F ⟹ G) : η ∘n id = η :=
protected definition id_right (η : F ⟹ G) : η ∘n nat_trans.id = η :=
nat_trans_eq (λa, !id_right)
protected definition sigma_char (F G : C ⇒ D) :
@ -78,7 +78,7 @@ namespace nat_trans
end
definition is_hset_nat_trans [instance] : is_hset (F ⟹ G) :=
by apply is_trunc_is_equiv_closed; apply (equiv.to_is_equiv !sigma_char)
by apply is_trunc_is_equiv_closed; apply (equiv.to_is_equiv !nat_trans.sigma_char)
definition nat_trans_functor_compose [reducible] (η : G ⟹ H) (F : E ⇒ C) : G ∘f F ⟹ H ∘f F :=
nat_trans.mk

60
hott/hit/circle.hlean
View file

@ -99,7 +99,7 @@ namespace circle
protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base)
(Ploop : loop ▸ Pbase = Pbase) : P x :=
rec Pbase Ploop x
circle.rec Pbase Ploop x
theorem rec_loop_helper {A : Type} (P : A → Type)
{x y : A} {p : x = y} {u : P x} {v : P y} (q : u = p⁻¹ ▸ v) :
@ -110,9 +110,9 @@ namespace circle
eq.rec_on p idp
theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▸ Pbase = Pbase) :
apd (rec Pbase Ploop) loop = Ploop :=
apd (circle.rec Pbase Ploop) loop = Ploop :=
begin
rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap], --con_idp should work here
rewrite [↑loop,apd_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap], --con_idp should work here
apply concat, apply (ap (λx, x ⬝ _)), apply con_idp, esimp,
rewrite [rec_loop_helper,inv_con_inv_left],
apply con_inv_cancel_left
@ -120,33 +120,33 @@ namespace circle
protected definition elim {P : Type} (Pbase : P) (Ploop : Pbase = Pbase)
(x : circle) : P :=
rec Pbase (tr_constant loop Pbase ⬝ Ploop) x
circle.rec Pbase (tr_constant loop Pbase ⬝ Ploop) x
protected definition elim_on [reducible] {P : Type} (x : circle) (Pbase : P)
(Ploop : Pbase = Pbase) : P :=
elim Pbase Ploop x
circle.elim Pbase Ploop x
theorem elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) :
ap (elim Pbase Ploop) loop = Ploop :=
ap (circle.elim Pbase Ploop) loop = Ploop :=
begin
apply (@cancel_left _ _ _ _ (tr_constant loop (elim Pbase Ploop base))),
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_loop],
apply (@cancel_left _ _ _ _ (tr_constant loop (circle.elim Pbase Ploop base))),
rewrite [-apd_eq_tr_constant_con_ap,↑circle.elim,rec_loop],
end
protected definition elim_type (Pbase : Type) (Ploop : Pbase ≃ Pbase)
(x : circle) : Type :=
elim Pbase (ua Ploop) x
circle.elim Pbase (ua Ploop) x
protected definition elim_type_on [reducible] (x : circle) (Pbase : Type)
(Ploop : Pbase ≃ Pbase) : Type :=
elim_type Pbase Ploop x
circle.elim_type Pbase Ploop x
theorem elim_type_loop (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
transport (elim_type Pbase Ploop) loop = Ploop :=
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_loop];apply cast_ua_fn
transport (circle.elim_type Pbase Ploop) loop = Ploop :=
by rewrite [tr_eq_cast_ap_fn,↑circle.elim_type,circle.elim_loop];apply cast_ua_fn
theorem elim_type_loop_inv (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
transport (elim_type Pbase Ploop) loop⁻¹ = to_inv Ploop :=
transport (circle.elim_type Pbase Ploop) loop⁻¹ = to_inv Ploop :=
by rewrite [tr_inv_fn,↑to_inv]; apply inv_eq_inv; apply elim_type_loop
end circle
@ -188,17 +188,17 @@ namespace circle
protected definition code (x : circle) : Type₀ :=
circle.elim_type_on x ℤ equiv_succ
definition transport_code_loop (a : ℤ) : transport code loop a = succ a :=
definition transport_code_loop (a : ℤ) : transport circle.code loop a = succ a :=
ap10 !elim_type_loop a
definition transport_code_loop_inv (a : ℤ)
: transport code loop⁻¹ a = pred a :=
: transport circle.code loop⁻¹ a = pred a :=
ap10 !elim_type_loop_inv a
protected definition encode {x : circle} (p : base = x) : code x :=
transport code p (of_num 0) -- why is the explicit coercion needed here?
protected definition encode {x : circle} (p : base = x) : circle.code x :=
transport circle.code p (of_num 0) -- why is the explicit coercion needed here?
protected definition decode {x : circle} : code x → base = x :=
protected definition decode {x : circle} : circle.code x → base = x :=
begin
refine circle.rec_on x _ _,
{ exact power loop},
@ -208,30 +208,30 @@ namespace circle
end
--remove this theorem after #484
theorem encode_decode {x : circle} : Π(a : code x), encode (decode a) = a :=
theorem encode_decode {x : circle} : Π(a : circle.code x), circle.encode (circle.decode a) = a :=
begin
unfold decode, refine circle.rec_on x _ _,
unfold circle.decode, refine circle.rec_on x _ _,
{ intro a, esimp [base,base1], --simplify after #587
apply rec_nat_on a,
{ exact idp},
{ intros n p,
apply transport (λ(y : base = base), transport code y _ = _), apply power_con,
rewrite [▸*,con_tr, transport_code_loop, ↑[encode,code] at p, p]},
apply transport (λ(y : base = base), transport circle.code y _ = _), apply power_con,
rewrite [▸*,con_tr, transport_code_loop, ↑[circle.encode,circle.code] at p, p]},
{ intros n p,
apply transport (λ(y : base = base), transport code y _ = _),
apply transport (λ(y : base = base), transport circle.code y _ = _),
{ exact !power_con_inv ⬝ ap (power loop) !neg_succ⁻¹},
rewrite [▸*,@con_tr _ code,transport_code_loop_inv, ↑[encode] at p, p, -neg_succ]}},
{ apply eq_of_homotopy, intro a, apply @is_hset.elim, esimp [code,base,base1], exact _}
rewrite [▸*,@con_tr _ circle.code,transport_code_loop_inv, ↑[circle.encode] at p, p, -neg_succ]}},
{ apply eq_of_homotopy, intro a, apply @is_hset.elim, esimp [circle.code,base,base1], exact _}
--simplify after #587
end
definition circle_eq_equiv (x : circle) : (base = x) ≃ code x :=
definition circle_eq_equiv (x : circle) : (base = x) ≃ circle.code x :=
begin
fapply equiv.MK,
{ exact encode},
{ exact decode},
{ exact encode_decode},
{ exact circle.encode},
{ exact circle.decode},
{ exact circle.encode_decode},
{ intro p, cases p, exact idp},
end
@ -242,7 +242,7 @@ namespace circle
base_eq_base_equiv⁻¹ a ⬝ base_eq_base_equiv⁻¹ b = base_eq_base_equiv⁻¹ (a + b) :=
!power_con_power
definition encode_con (p q : base = base) : encode (p ⬝ q) = encode p + encode q :=
definition encode_con (p q : base = base) : circle.encode (p ⬝ q) = circle.encode p + circle.encode q :=
preserve_binary_of_inv_preserve base_eq_base_equiv concat add decode_add p q
--the carrier of π₁(S¹) is the set-truncation of base = base.

22
hott/hit/suspension.hlean
View file

@ -37,39 +37,39 @@ namespace suspension
protected definition rec_on [reducible] {P : suspension A → Type} (y : suspension A)
(PN : P !north) (PS : P !south) (Pm : Π(a : A), merid a ▸ PN = PS) : P y :=
rec PN PS Pm y
suspension.rec PN PS Pm y
theorem rec_merid {P : suspension A → Type} (PN : P !north) (PS : P !south)
(Pm : Π(a : A), merid a ▸ PN = PS) (a : A)
: apd (rec PN PS Pm) (merid a) = Pm a :=
: apd (suspension.rec PN PS Pm) (merid a) = Pm a :=
!rec_glue
protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
(x : suspension A) : P :=
rec PN PS (λa, !tr_constant ⬝ Pm a) x
suspension.rec PN PS (λa, !tr_constant ⬝ Pm a) x
protected definition elim_on [reducible] {P : Type} (x : suspension A)
(PN : P) (PS : P) (Pm : A → PN = PS) : P :=
elim PN PS Pm x
suspension.elim PN PS Pm x
theorem elim_merid {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) (a : A)
: ap (elim PN PS Pm) (merid a) = Pm a :=
: ap (suspension.elim PN PS Pm) (merid a) = Pm a :=
begin
apply (@cancel_left _ _ _ _ (tr_constant (merid a) (elim PN PS Pm !north))),
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_merid],
apply (@cancel_left _ _ _ _ (tr_constant (merid a) (suspension.elim PN PS Pm !north))),
rewrite [-apd_eq_tr_constant_con_ap,↑suspension.elim,rec_merid],
end
protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
(x : suspension A) : Type :=
elim PN PS (λa, ua (Pm a)) x
suspension.elim PN PS (λa, ua (Pm a)) x
protected definition elim_type_on [reducible] (x : suspension A)
(PN : Type) (PS : Type) (Pm : A → PN ≃ PS) : Type :=
elim_type PN PS Pm x
suspension.elim_type PN PS Pm x
theorem elim_type_merid (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
(x : suspension A) (a : A) : transport (elim_type PN PS Pm) (merid a) = Pm a :=
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_merid];apply cast_ua_fn
(x : suspension A) (a : A) : transport (suspension.elim_type PN PS Pm) (merid a) = Pm a :=
by rewrite [tr_eq_cast_ap_fn,↑suspension.elim_type,elim_merid];apply cast_ua_fn
end suspension

2
hott/hit/trunc.hlean
View file

@ -24,7 +24,7 @@ namespace trunc
protected definition elim_on {n : trunc_index} {A : Type} {P : Type} (aa : trunc n A)
[Pt : is_trunc n P] (H : A → P) : P :=
elim H aa
trunc.elim H aa
/-
there are no theorems to eliminate to the universe here,

20
hott/hit/type_quotient.hlean
View file

@ -22,34 +22,32 @@ namespace type_quotient
protected definition elim_on [reducible] {P : Type} (x : type_quotient R)
(Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=
elim Pc Pp x
type_quotient.elim Pc Pp x
theorem elim_eq_of_rel {P : Type} (Pc : A → P)
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a')
: ap (elim Pc Pp) (eq_of_rel R H) = Pp H :=
: ap (type_quotient.elim Pc Pp) (eq_of_rel R H) = Pp H :=
begin
apply (@cancel_left _ _ _ _ (tr_constant (eq_of_rel R H) (elim Pc Pp (class_of R a)))),
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_eq_of_rel],
apply (@cancel_left _ _ _ _ (tr_constant (eq_of_rel R H) (type_quotient.elim Pc Pp (class_of R a)))),
rewrite [-apd_eq_tr_constant_con_ap,↑type_quotient.elim,rec_eq_of_rel],
end
protected definition elim_type (Pc : A → Type)
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : type_quotient R → Type :=
elim Pc (λa a' H, ua (Pp H))
type_quotient.elim Pc (λa a' H, ua (Pp H))
protected definition elim_type_on [reducible] (x : type_quotient R) (Pc : A → Type)
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : Type :=
elim_type Pc Pp x
type_quotient.elim_type Pc Pp x
theorem elim_type_eq_of_rel (Pc : A → Type)
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a')
: transport (elim_type Pc Pp) (eq_of_rel R H) = to_fun (Pp H) :=
by rewrite [tr_eq_cast_ap_fn, ↑elim_type, elim_eq_of_rel];apply cast_ua_fn
: transport (type_quotient.elim_type Pc Pp) (eq_of_rel R H) = to_fun (Pp H) :=
by rewrite [tr_eq_cast_ap_fn, ↑type_quotient.elim_type, elim_eq_of_rel];apply cast_ua_fn
definition elim_type_uncurried (H : Σ(Pc : A → Type), Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a')
: type_quotient R → Type :=
elim_type H.1 H.2
type_quotient.elim_type H.1 H.2
end type_quotient
attribute type_quotient.elim [unfold-c 6]

2
hott/init/hit.hlean
View file

@ -62,7 +62,7 @@ namespace type_quotient
protected definition rec_on [reducible] {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
(x : type_quotient R) (Pc : Π(a : A), P (class_of R a))
(Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a') : P x :=
rec Pc Pp x
type_quotient.rec Pc Pp x
end type_quotient

6
hott/init/logic.hlean
View file

@ -200,13 +200,13 @@ protected definition destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A
inhabited.rec H2 H1
definition inhabited_fun [instance] (A : Type) {B : Type} [H : inhabited B] : inhabited (A → B) :=
destruct H (λb, mk (λa, b))
inhabited.destruct H (λb, mk (λa, b))
definition inhabited_Pi [instance] (A : Type) {B : A → Type} [H : Πx, inhabited (B x)] :
inhabited (Πx, B x) :=
mk (λa, destruct (H a) (λb, b))
mk (λa, inhabited.destruct (H a) (λb, b))
definition default (A : Type) [H : inhabited A] : A := destruct H (take a, a)
definition default (A : Type) [H : inhabited A] : A := inhabited.destruct H (take a, a)
end inhabited

8
hott/types/W.hlean
View file

@ -24,7 +24,7 @@ namespace Wtype
protected definition pr1 [unfold-c 3] (w : W(a : A), B a) : A :=
by cases w with a f; exact a
protected definition pr2 [unfold-c 3] (w : W(a : A), B a) : B (pr1 w) → W(a : A), B a :=
protected definition pr2 [unfold-c 3] (w : W(a : A), B a) : B (Wtype.pr1 w) → W(a : A), B a :=
by cases w with a f; exact f
namespace ops
@ -40,13 +40,13 @@ namespace Wtype
definition sup_eq_sup (p : a = a') (q : p ▸ f = f') : ⟨a, f⟩ = ⟨a', f'⟩ :=
by cases p; cases q; exact idp
protected definition Wtype_eq (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2) : w = w' :=
definition Wtype_eq (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2) : w = w' :=
by cases w; cases w';exact (sup_eq_sup p q)
protected definition Wtype_eq_pr1 (p : w = w') : w.1 = w'.1 :=
definition Wtype_eq_pr1 (p : w = w') : w.1 = w'.1 :=
by cases p;exact idp
protected definition Wtype_eq_pr2 (p : w = w') : Wtype_eq_pr1 p ▸ w.2 = w'.2 :=
definition Wtype_eq_pr2 (p : w = w') : Wtype_eq_pr1 p ▸ w.2 = w'.2 :=
by cases p;exact idp
namespace ops

2
hott/types/equiv.hlean
View file

@ -76,7 +76,7 @@ namespace is_equiv
local attribute is_contr_right_coherence [instance] [priority 1600]
theorem is_hprop_is_equiv [instance] : is_hprop (is_equiv f) :=
is_hprop_of_imp_is_contr (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !sigma_char'))
is_hprop_of_imp_is_contr (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !is_equiv.sigma_char'))
definition inv_eq_inv {A B : Type} {f f' : A → B} {Hf : is_equiv f} {Hf' : is_equiv f'}
(p : f = f') : f⁻¹ = f'⁻¹ :=

6
hott/types/int/basic.hlean
View file

@ -171,10 +171,10 @@ have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from
... = pr2 p + pr1 r + pr2 q : by exact sorry,
show pr1 p + pr2 r = pr2 p + pr1 r, from add.cancel_right H3
protected definition int_equiv_int_equiv : is_equivalence int_equiv :=
definition int_equiv_int_equiv : is_equivalence int_equiv :=
is_equivalence.mk @int_equiv.refl @int_equiv.symm @int_equiv.trans
protected definition int_equiv_cases {p q : ℕ × ℕ} (H : int_equiv p q) :
definition int_equiv_cases {p q : ℕ × ℕ} (H : int_equiv p q) :
(pr1 p ≥ pr2 p × pr1 q ≥ pr2 q) ⊎ (pr1 p < pr2 p × pr1 q < pr2 q) :=
sum.rec_on (@le_or_gt (pr2 p) (pr1 p))
(assume H1: pr1 p ≥ pr2 p,
@ -184,7 +184,7 @@ sum.rec_on (@le_or_gt (pr2 p) (pr1 p))
have H2 : pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right H1 (pr2 q),
sum.inr (pair H1 (lt_of_add_lt_add_left H2)))
protected definition int_equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ int_equiv.refl
definition int_equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ int_equiv.refl
/- the representation and abstraction functions -/

4
hott/types/nat/order.hlean
View file

@ -328,8 +328,8 @@ H1 !lt_succ_self
protected theorem case_strong_induction_on {P : nat → Type} (a : nat) (H0 : P 0)
(Hind : Π(n : nat), (Πm, m ≤ n → P m) → P (succ n)) : P a :=
strong_induction_on a (
take n,
nat.strong_induction_on a
(take n,
show (Π m, m < n → P m) → P n, from
nat.cases_on n
(assume H : (Πm, m < 0 → P m), show P 0, from H0)

4
hott/types/prod.hlean
View file

@ -27,8 +27,8 @@ namespace prod
begin
cases u with a₁ b₁,
cases v with a₂ b₂,
apply transport _ (eta (a₁, b₁)),
apply transport _ (eta (a₂, b₂)),
apply transport _ (prod.eta (a₁, b₁)),
apply transport _ (prod.eta (a₂, b₂)),
apply pair_eq H₁ H₂,
end

10
hott/types/sigma.hlean
View file

@ -273,7 +273,7 @@ namespace sigma
definition sigma_assoc_equiv (C : (Σa, B a) → Type) : (Σa b, C ⟨a, b⟩) ≃ (Σu, C u) :=
equiv.mk _ (adjointify
(λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩)
(λuc, ⟨uc.1.1, uc.1.2, !eta⁻¹ ▸ uc.2⟩)
(λuc, ⟨uc.1.1, uc.1.2, !sigma.eta⁻¹ ▸ uc.2⟩)
begin intro uc, cases uc with u c, cases u, reflexivity end
begin intro av, cases av with a v, cases v, reflexivity end)
@ -331,18 +331,18 @@ namespace sigma
⟨fg.1 a, fg.2 a⟩
protected definition coind (f : Π a, B a) (g : Π a, C a (f a)) (a : A) : Σ(b : B a), C a b :=
coind_uncurried ⟨f, g⟩ a
sigma.coind_uncurried ⟨f, g⟩ a
--is the instance below dangerous?
--in Coq this can be done without function extensionality
definition is_equiv_coind [instance] (C : Πa, B a → Type)
: is_equiv (@coind_uncurried _ _ C) :=
: is_equiv (@sigma.coind_uncurried _ _ C) :=
adjointify _ (λ h, ⟨λa, (h a).1, λa, (h a).2⟩)
(λ h, proof eq_of_homotopy (λu, !eta) qed)
(λ h, proof eq_of_homotopy (λu, !sigma.eta) qed)
(λfg, destruct fg (λ(f : Π (a : A), B a) (g : Π (x : A), C x (f x)), proof idp qed))
definition sigma_pi_equiv_pi_sigma : (Σ(f : Πa, B a), Πa, C a (f a)) ≃ (Πa, Σb, C a b) :=
equiv.mk coind_uncurried _
equiv.mk sigma.coind_uncurried _
end
/- ** Subtypes (sigma types whose second components are hprops) -/

16
hott/types/trunc.hlean
View file

@ -148,27 +148,27 @@ namespace trunc
protected definition code (n : trunc_index) (aa aa' : trunc n.+1 A) : n-Type :=
trunc.rec_on aa (λa, trunc.rec_on aa' (λa', trunctype.mk' n (trunc n (a = a'))))
protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → code n aa aa' :=
protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → trunc.code n aa aa' :=
begin
intro p, cases p, apply (trunc.rec_on aa),
intro a, esimp [code,trunc.rec_on], exact (tr idp)
intro a, esimp [trunc.code,trunc.rec_on], exact (tr idp)
end
protected definition decode (n : trunc_index) (aa aa' : trunc n.+1 A) : code n aa aa' → aa = aa' :=
protected definition decode (n : trunc_index) (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' :=
begin
eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa),
intro a a' x, esimp [code, trunc.rec_on] at x,
intro a a' x, esimp [trunc.code, trunc.rec_on] at x,
apply (trunc.rec_on x), intro p, exact (ap tr p)
end
definition trunc_eq_equiv (n : trunc_index) (aa aa' : trunc n.+1 A)
: aa = aa' ≃ code n aa aa' :=
: aa = aa' ≃ trunc.code n aa aa' :=
begin
fapply equiv.MK,
{ apply encode},
{ apply decode},
{ apply trunc.encode},
{ apply trunc.decode},
{ eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa),
intro a a' x, esimp [code, trunc.rec_on] at x,
intro a a' x, esimp [trunc.code, trunc.rec_on] at x,
apply (trunc.rec_on x), intro p, cases p, exact idp},
{ intro p, cases p, apply (trunc.rec_on aa), intro a, exact idp},
end

80
library/algebra/category/constructions.lean
View file

@ -176,32 +176,32 @@ namespace category
open sigma function
variables {ob : Type} {C : category ob} {c : ob}
protected definition slice_obs (C : category ob) (c : ob) := Σ(b : ob), hom b c
variables {a b : slice_obs C c}
protected definition to_ob (a : slice_obs C c) : ob := sigma.pr1 a
protected definition to_ob_def (a : slice_obs C c) : to_ob a = sigma.pr1 a := rfl
protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := sigma.pr2 a
variables {a b : slice.slice_obs C c}
protected definition to_ob (a : slice.slice_obs C c) : ob := sigma.pr1 a
protected definition to_ob_def (a : slice.slice_obs C c) : slice.to_ob a = sigma.pr1 a := rfl
protected definition ob_hom (a : slice.slice_obs C c) : hom (slice.to_ob a) c := sigma.pr2 a
-- protected theorem slice_obs_equal (H₁ : to_ob a = to_ob b)
-- (H₂ : eq.drec_on H₁ (ob_hom a) = ob_hom b) : a = b :=
-- sigma.equal H₁ H₂
protected definition slice_hom (a b : slice_obs C c) : Type :=
Σ(g : hom (to_ob a) (to_ob b)), ob_hom b ∘ g = ob_hom a
protected definition slice_hom (a b : slice.slice_obs C c) : Type :=
Σ(g : hom (slice.to_ob a) (slice.to_ob b)), slice.ob_hom b ∘ g = slice.ob_hom a
protected definition hom_hom (f : slice_hom a b) : hom (to_ob a) (to_ob b) := sigma.pr1 f
protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := sigma.pr2 f
protected definition hom_hom (f : slice.slice_hom a b) : hom (slice.to_ob a) (slice.to_ob b) := sigma.pr1 f
protected definition commute (f : slice.slice_hom a b) : slice.ob_hom b ∘ (slice.hom_hom f) = slice.ob_hom a := sigma.pr2 f
-- protected theorem slice_hom_equal (f g : slice_hom a b) (H : hom_hom f = hom_hom g) : f = g :=
-- sigma.equal H !proof_irrel
definition slice_category (C : category ob) (c : ob) : category (slice_obs C c) :=
mk (λa b, slice_hom a b)
(λ a b c g f, sigma.mk (hom_hom g ∘ hom_hom f)
(show ob_hom c ∘ (hom_hom g ∘ hom_hom f) = ob_hom a,
definition slice_category (C : category ob) (c : ob) : category (slice.slice_obs C c) :=
mk (λa b, slice.slice_hom a b)
(λ a b c g f, sigma.mk (slice.hom_hom g ∘ slice.hom_hom f)
(show slice.ob_hom c ∘ (slice.hom_hom g ∘ slice.hom_hom f) = slice.ob_hom a,
proof
calc
ob_hom c ∘ (hom_hom g ∘ hom_hom f) = (ob_hom c ∘ hom_hom g) ∘ hom_hom f : !assoc
... = ob_hom b ∘ hom_hom f : {commute g}
... = ob_hom a : {commute f}
slice.ob_hom c ∘ (slice.hom_hom g ∘ slice.hom_hom f) = (slice.ob_hom c ∘ slice.hom_hom g) ∘ slice.hom_hom f : !assoc
... = slice.ob_hom b ∘ slice.hom_hom f : {slice.commute g}
... = slice.ob_hom a : {slice.commute f}
qed))
(λ a, sigma.mk id !id_right)
(λ a b c d h g f, dpair_eq !assoc !proof_irrel)
@ -231,20 +231,20 @@ namespace category
attribute slice_category [instance]
variables {D : Category}
definition forgetful (x : D) : (Slice_category D x) ⇒ D :=
functor.mk (λ a, to_ob a)
(λ a b f, hom_hom f)
functor.mk (λ a, slice.to_ob a)
(λ a b f, slice.hom_hom f)
(λ a, rfl)
(λ a b c g f, rfl)
definition postcomposition_functor {x y : D} (h : x ⟶ y)
: Slice_category D x ⇒ Slice_category D y :=
functor.mk
(λ a, sigma.mk (to_ob a) (h ∘ ob_hom a))
(λ a, sigma.mk (slice.to_ob a) (h ∘ slice.ob_hom a))
(λ a b f,
⟨hom_hom f,
⟨slice.hom_hom f,
calc
(h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : by rewrite assoc
... = h ∘ ob_hom a : by rewrite commute⟩)
(h ∘ slice.ob_hom b) ∘ slice.hom_hom f = h ∘ (slice.ob_hom b ∘ slice.hom_hom f) : by rewrite assoc
... = h ∘ slice.ob_hom a : by rewrite slice.commute⟩)
(λ a, rfl)
(λ a b c g f, dpair_eq rfl !proof_irrel)
@ -330,30 +330,32 @@ namespace category
-- make these definitions private?
variables {ob : Type} {C : category ob}
protected definition arrow_obs (ob : Type) (C : category ob) := Σ(a b : ob), hom a b
variables {a b : arrow_obs ob C}
protected definition src (a : arrow_obs ob C) : ob := sigma.pr1 a
protected definition dst (a : arrow_obs ob C) : ob := sigma.pr2' a
protected definition to_hom (a : arrow_obs ob C) : hom (src a) (dst a) := sigma.pr3 a
variables {a b : category.arrow_obs ob C}
protected definition src (a : category.arrow_obs ob C) : ob := sigma.pr1 a
protected definition dst (a : category.arrow_obs ob C) : ob := sigma.pr2' a
protected definition to_hom (a : category.arrow_obs ob C) : hom (category.src a) (category.dst a) := sigma.pr3 a
protected definition arrow_hom (a b : arrow_obs ob C) : Type :=
Σ (g : hom (src a) (src b)) (h : hom (dst a) (dst b)), to_hom b ∘ g = h ∘ to_hom a
protected definition arrow_hom (a b : category.arrow_obs ob C) : Type :=
Σ (g : hom (category.src a) (category.src b)) (h : hom (category.dst a) (category.dst b)),
category.to_hom b ∘ g = h ∘ category.to_hom a
protected definition hom_src (m : arrow_hom a b) : hom (src a) (src b) := sigma.pr1 m
protected definition hom_dst (m : arrow_hom a b) : hom (dst a) (dst b) := sigma.pr2' m
protected definition commute (m : arrow_hom a b) : to_hom b ∘ (hom_src m) = (hom_dst m) ∘ to_hom a
protected definition hom_src (m : category.arrow_hom a b) : hom (category.src a) (category.src b) := sigma.pr1 m
protected definition hom_dst (m : category.arrow_hom a b) : hom (category.dst a) (category.dst b) := sigma.pr2' m
protected definition commute (m : category.arrow_hom a b) :
category.to_hom b ∘ (category.hom_src m) = (category.hom_dst m) ∘ category.to_hom a
:= sigma.pr3 m
definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) :=
mk (λa b, arrow_hom a b)
(λ a b c g f, sigma.mk (hom_src g ∘ hom_src f) (sigma.mk (hom_dst g ∘ hom_dst f)
(show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a,
definition arrow (ob : Type) (C : category ob) : category (category.arrow_obs ob C) :=
mk (λa b, category.arrow_hom a b)
(λ a b c g f, sigma.mk (category.hom_src g ∘ category.hom_src f) (sigma.mk (category.hom_dst g ∘ category.hom_dst f)
(show category.to_hom c ∘ (category.hom_src g ∘ category.hom_src f) = (category.hom_dst g ∘ category.hom_dst f) ∘ category.to_hom a,
proof
calc
to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : by rewrite assoc
... = (hom_dst g ∘ to_hom b) ∘ hom_src f : by rewrite commute
... = hom_dst g ∘ (to_hom b ∘ hom_src f) : by rewrite assoc
... = hom_dst g ∘ (hom_dst f ∘ to_hom a) : by rewrite commute
... = (hom_dst g ∘ hom_dst f) ∘ to_hom a : by rewrite assoc
category.to_hom c ∘ (category.hom_src g ∘ category.hom_src f) = (category.to_hom c ∘ category.hom_src g) ∘ category.hom_src f : by rewrite assoc
... = (category.hom_dst g ∘ category.to_hom b) ∘ category.hom_src f : by rewrite category.commute
... = category.hom_dst g ∘ (category.to_hom b ∘ category.hom_src f) : by rewrite assoc
... = category.hom_dst g ∘ (category.hom_dst f ∘ category.to_hom a) : by rewrite category.commute
... = (category.hom_dst g ∘ category.hom_dst f) ∘ category.to_hom a : by rewrite assoc
qed)
))
(λ a, sigma.mk id (sigma.mk id (!id_right ⬝ (symm !id_left))))

8
library/algebra/category/functor.lean
View file

@ -39,7 +39,7 @@ namespace functor
G (F (g ∘ f)) = G (F g ∘ F f) : respect_comp F g f
... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f) qed)
infixr `∘f`:60 := compose
infixr `∘f`:60 := functor.compose
protected theorem assoc (H : functor C D) (G : functor B C) (F : functor A B) :
H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
@ -47,11 +47,11 @@ namespace functor
protected definition id [reducible] {C : Category} : functor C C :=
mk (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl)
protected definition ID [reducible] (C : Category) : functor C C := @id C
protected definition ID [reducible] (C : Category) : functor C C := @functor.id C
protected theorem id_left (F : functor C D) : (@id D) ∘f F = F :=
protected theorem id_left (F : functor C D) : (@functor.id D) ∘f F = F :=
functor.rec (λ obF homF idF compF, dcongr_arg4 mk rfl rfl !proof_irrel !proof_irrel) F
protected theorem id_right (F : functor C D) : F ∘f (@id C) = F :=
protected theorem id_right (F : functor C D) : F ∘f (@functor.id C) = F :=
functor.rec (λ obF homF idF compF, dcongr_arg4 mk rfl rfl !proof_irrel !proof_irrel) F
end functor

2
library/algebra/category/natural_transformation.lean
View file

@ -36,7 +36,7 @@ namespace natural_transformation
... = (η b ∘ θ b) ∘ F f : assoc)
--congr_arg (λx, η b ∘ x) (naturality θ f) -- this needed to be explicit for some reason (on Oct 24)
infixr `∘n`:60 := compose
infixr `∘n`:60 := natural_transformation.compose
protected theorem assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) :
η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
dcongr_arg2 mk (funext (take x, !assoc)) !proof_irrel

2
library/data/empty.lean
View file

@ -12,7 +12,7 @@ namespace empty
empty.rec (λe, A) H
protected theorem subsingleton [instance] : subsingleton empty :=
subsingleton.intro (λ a b, !elim a)
subsingleton.intro (λ a b, !empty.elim a)
end empty
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=

2
library/data/finset/basic.lean
View file

@ -223,7 +223,7 @@ protected theorem induction_on {P : finset A → Prop} (s : finset A)
(H1 : P empty)
(H2 : ∀⦃s : finset A⦄, ∀{a : A}, a ∉ s → P s → P (insert a s)) :
P s :=
induction H1 H2 s
finset.induction H1 H2 s
end insert
/- erase -/

16
library/data/int/basic.lean
View file

@ -181,10 +181,10 @@ have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from
... = pr2 p + pr1 r + pr2 q : by simp,
show pr1 p + pr2 r = pr2 p + pr1 r, from add.cancel_right H3
protected theorem equiv_equiv : is_equivalence equiv :=
protected theorem equiv_equiv : is_equivalence int.equiv :=
is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans
protected theorem equiv_cases {p q : ℕ × ℕ} (H : equiv p q) :
protected theorem equiv_cases {p q : ℕ × ℕ} (H : int.equiv p q) :
(pr1 p ≥ pr2 p ∧ pr1 q ≥ pr2 q) ∨ (pr1 p < pr2 p ∧ pr1 q < pr2 q) :=
or.elim (@le_or_gt (pr2 p) (pr1 p))
(assume H1: pr1 p ≥ pr2 p,
@ -232,7 +232,7 @@ theorem repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p :=
!prod.eta ▸ !repr_sub_nat_nat
theorem abstr_eq {p q : ℕ × ℕ} (Hequiv : p ≡ q) : abstr p = abstr q :=
or.elim (equiv_cases Hequiv)
or.elim (int.equiv_cases Hequiv)
(assume H2,
have H3 : pr1 p ≥ pr2 p, from and.elim_left H2,
have H4 : pr1 q ≥ pr2 q, from and.elim_right H2,
@ -264,9 +264,9 @@ or.elim (equiv_cases Hequiv)
theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ ((p ≡ p) ∧ (q ≡ q) ∧ (abstr p = abstr q)) :=
iff.intro
(assume H : equiv p q,
(assume H : int.equiv p q,
and.intro !equiv.refl (and.intro !equiv.refl (abstr_eq H)))
(assume H : equiv p p ∧ equiv q q ∧ abstr p = abstr q,
(assume H : int.equiv p p ∧ int.equiv q q ∧ abstr p = abstr q,
have H1 : abstr p = abstr q, from and.elim_right (and.elim_right H),
equiv.trans (H1 ▸ equiv.symm (repr_abstr p)) (repr_abstr q))
@ -335,7 +335,7 @@ int.cases_on a
int.cases_on b
(take n, !equiv.refl)
(take n',
have H1 : equiv (repr (add (of_nat m) (neg_succ_of_nat n'))) (m, succ n'),
have H1 : int.equiv (repr (add (of_nat m) (neg_succ_of_nat n'))) (m, succ n'),
from !repr_sub_nat_nat,
have H2 : padd (repr (of_nat m)) (repr (neg_succ_of_nat n')) = (m, 0 + succ n'),
from rfl,
@ -343,7 +343,7 @@ int.cases_on a
(take m',
int.cases_on b
(take n,
have H1 : equiv (repr (add (neg_succ_of_nat m') (of_nat n))) (n, succ m'),
have H1 : int.equiv (repr (add (neg_succ_of_nat m') (of_nat n))) (n, succ m'),
from !repr_sub_nat_nat,
have H2 : padd (repr (neg_succ_of_nat m')) (repr (of_nat n)) = (0 + n, succ m'),
from rfl,
@ -566,7 +566,7 @@ eq_of_repr_equiv_repr
... = repr (a * (b * c)) : repr_mul) ▸ !equiv.refl)
theorem mul_one (a : ℤ) : a * 1 = a :=
eq_of_repr_equiv_repr (equiv_of_eq
eq_of_repr_equiv_repr (int.equiv_of_eq
((calc
repr (a * 1) = pmul (repr a) (repr 1) : repr_mul
... = (pr1 (repr a), pr2 (repr a)) : by simp

2
library/data/nat/basic.lean
View file

@ -307,7 +307,7 @@ section migrate_algebra
mul_zero := mul_zero,
mul_comm := mul.comm⦄
local attribute comm_semiring [instance]
local attribute nat.comm_semiring [instance]
definition dvd (a b : ℕ) : Prop := algebra.dvd a b
notation a ∣ b := dvd a b

2
library/data/nat/choose.lean
View file

@ -104,6 +104,6 @@ end find_x
protected definition choose {p : nat → Prop} [d : decidable_pred p] : (∃ x, p x) → nat :=
assume h, elt_of (find_x h)
protected theorem choose_spec {p : nat → Prop} [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex) :=
protected theorem choose_spec {p : nat → Prop} [d : decidable_pred p] (ex : ∃ x, p x) : p (nat.choose ex) :=
has_property (find_x ex)
end nat

4
library/data/nat/order.lean
View file

@ -326,8 +326,8 @@ H1 !lt_succ_self
protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
(Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a :=
strong_induction_on a (
take n,
nat.strong_induction_on a
(take n,
show (∀ m, m < n → P m) → P n, from
nat.cases_on n
(assume H : (∀m, m < 0 → P m), show P 0, from H0)

6
library/data/set/classical_inverse.lean
View file

@ -71,15 +71,15 @@ protected definition inverse (f : map a b) {dflt : X} (dflta : dflt ∈ a) :=
map.mk (inv_fun f a dflt) (@maps_to_inv_fun _ _ _ _ b _ dflta)
theorem left_inverse_inverse {f : map a b} {dflt : X} (dflta : dflt ∈ a) (H : map.injective f) :
map.left_inverse (inverse f dflta) f :=
map.left_inverse (map.inverse f dflta) f :=
left_inv_on_inv_fun_of_inj_on dflt H
theorem right_inverse_inverse {f : map a b} {dflt : X} (dflta : dflt ∈ a) (H : map.surjective f) :
map.right_inverse (inverse f dflta) f :=
map.right_inverse (map.inverse f dflta) f :=
right_inv_on_inv_fun_of_surj_on dflt H
theorem is_inverse_inverse {f : map a b} {dflt : X} (dflta : dflt ∈ a) (H : map.bijective f) :
map.is_inverse (inverse f dflta) f :=
map.is_inverse (map.inverse f dflta) f :=
and.intro
(left_inverse_inverse dflta (and.left H))
(right_inverse_inverse dflta (and.right H))

70
library/data/set/map.lean
View file

@ -38,57 +38,57 @@ assume H₁ : f₁ ~ f₂, assume H₂ : f₂ ~ f₃,
take x, assume Ha : x ∈ a, eq.trans (H₁ Ha) (H₂ Ha)
protected theorem equiv.is_equivalence {X Y : Type} (a : set X) (b : set Y) :
equivalence (@equiv X Y a b) :=
mk_equivalence (@equiv X Y a b) (@equiv.refl X Y a b) (@equiv.symm X Y a b) (@equiv.trans X Y a b)
equivalence (@map.equiv X Y a b) :=
mk_equivalence (@map.equiv X Y a b) (@equiv.refl X Y a b) (@equiv.symm X Y a b) (@equiv.trans X Y a b)
/- compose -/
protected definition compose (g : map b c) (f : map a b) : map a c :=
map.mk (#function g ∘ f) (maps_to_compose (mapsto g) (mapsto f))
notation g ∘ f := compose g f
notation g ∘ f := map.compose g f
/- range -/
protected definition range (f : map a b) : set Y := image f a
theorem range_eq_range_of_equiv {f1 f2 : map a b} (H : f1 ~ f2) : range f1 = range f2 :=
theorem range_eq_range_of_equiv {f1 f2 : map a b} (H : f1 ~ f2) : map.range f1 = map.range f2 :=
image_eq_image_of_eq_on H
/- injective -/
protected definition injective (f : map a b) : Prop := inj_on f a
theorem injective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : injective f1) :
injective f2 :=
theorem injective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.injective f1) :
map.injective f2 :=
inj_on_of_eq_on H1 H2
theorem injective_compose {g : map b c} {f : map a b} (Hg : injective g) (Hf: injective f) :
injective (g ∘ f) :=
theorem injective_compose {g : map b c} {f : map a b} (Hg : map.injective g) (Hf: map.injective f) :
map.injective (g ∘ f) :=
inj_on_compose (mapsto f) Hg Hf
/- surjective -/
protected definition surjective (f : map a b) : Prop := surj_on f a b
theorem surjective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : surjective f1) :
surjective f2 :=
theorem surjective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.surjective f1) :
map.surjective f2 :=
surj_on_of_eq_on H1 H2
theorem surjective_compose {g : map b c} {f : map a b} (Hg : surjective g) (Hf: surjective f) :
surjective (g ∘ f) :=
theorem surjective_compose {g : map b c} {f : map a b} (Hg : map.surjective g) (Hf: map.surjective f) :
map.surjective (g ∘ f) :=
surj_on_compose Hg Hf
/- bijective -/
protected definition bijective (f : map a b) : Prop := injective f ∧ surjective f
protected definition bijective (f : map a b) : Prop := map.injective f ∧ map.surjective f
theorem bijective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : bijective f1) :
bijective f2 :=
theorem bijective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.bijective f1) :
map.bijective f2 :=
and.intro (injective_of_equiv H1 (and.left H2)) (surjective_of_equiv H1 (and.right H2))
theorem bijective_compose {g : map b c} {f : map a b} (Hg : bijective g) (Hf: bijective f) :
bijective (g ∘ f) :=
theorem bijective_compose {g : map b c} {f : map a b} (Hg : map.bijective g) (Hf: map.bijective f) :
map.bijective (g ∘ f) :=
obtain Hg₁ Hg₂, from Hg,
obtain Hf₁ Hf₂, from Hf,
and.intro (injective_compose Hg₁ Hf₁) (surjective_compose Hg₂ Hf₂)
@ -99,53 +99,53 @@ and.intro (injective_compose Hg₁ Hf₁) (surjective_compose Hg₂ Hf₂)
protected definition left_inverse (g : map b a) (f : map a b) : Prop := left_inv_on g f a
theorem left_inverse_of_equiv_left {g1 g2 : map b a} {f : map a b} (eqg : g1 ~ g2)
(H : left_inverse g1 f) : left_inverse g2 f :=
(H : map.left_inverse g1 f) : map.left_inverse g2 f :=
left_inv_on_of_eq_on_left (mapsto f) eqg H
theorem left_inverse_of_equiv_right {g : map b a} {f1 f2 : map a b} (eqf : f1 ~ f2)
(H : left_inverse g f1) : left_inverse g f2 :=
(H : map.left_inverse g f1) : map.left_inverse g f2 :=
left_inv_on_of_eq_on_right eqf H
theorem injective_of_left_inverse {g : map b a} {f : map a b} (H : left_inverse g f) :
injective f :=
theorem injective_of_left_inverse {g : map b a} {f : map a b} (H : map.left_inverse g f) :
map.injective f :=
inj_on_of_left_inv_on H
theorem left_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
(Hf : left_inverse f' f) (Hg : left_inverse g' g) : left_inverse (f' ∘ g') (g ∘ f) :=
(Hf : map.left_inverse f' f) (Hg : map.left_inverse g' g) : map.left_inverse (f' ∘ g') (g ∘ f) :=
left_inv_on_compose (mapsto f) Hf Hg
/- right inverse -/
-- g is a right inverse to f
protected definition right_inverse (g : map b a) (f : map a b) : Prop := left_inverse f g
protected definition right_inverse (g : map b a) (f : map a b) : Prop := map.left_inverse f g
theorem right_inverse_of_equiv_left {g1 g2 : map b a} {f : map a b} (eqg : g1 ~ g2)
(H : right_inverse g1 f) : right_inverse g2 f :=
left_inverse_of_equiv_right eqg H
(H : map.right_inverse g1 f) : map.right_inverse g2 f :=
map.left_inverse_of_equiv_right eqg H
theorem right_inverse_of_equiv_right {g : map b a} {f1 f2 : map a b} (eqf : f1 ~ f2)
(H : right_inverse g f1) : right_inverse g f2 :=
left_inverse_of_equiv_left eqf H
(H : map.right_inverse g f1) : map.right_inverse g f2 :=
map.left_inverse_of_equiv_left eqf H
theorem surjective_of_right_inverse {g : map b a} {f : map a b} (H : right_inverse g f) :
surjective f :=
theorem surjective_of_right_inverse {g : map b a} {f : map a b} (H : map.right_inverse g f) :
map.surjective f :=
surj_on_of_right_inv_on (mapsto g) H
theorem right_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
(Hf : right_inverse f' f) (Hg : right_inverse g' g) : right_inverse (f' ∘ g') (g ∘ f) :=
left_inverse_compose Hg Hf
(Hf : map.right_inverse f' f) (Hg : map.right_inverse g' g) : map.right_inverse (f' ∘ g') (g ∘ f) :=
map.left_inverse_compose Hg Hf
theorem equiv_of_left_inverse_of_right_inverse {g1 g2 : map b a} {f : map a b}
(H1 : left_inverse g1 f) (H2 : right_inverse g2 f) : g1 ~ g2 :=
theorem equiv_of_map.left_inverse_of_right_inverse {g1 g2 : map b a} {f : map a b}
(H1 : map.left_inverse g1 f) (H2 : map.right_inverse g2 f) : g1 ~ g2 :=
eq_on_of_left_inv_of_right_inv (mapsto g2) H1 H2
/- inverse -/
-- g is an inverse to f
protected definition is_inverse (g : map b a) (f : map a b) : Prop :=
left_inverse g f ∧ right_inverse g f
map.left_inverse g f ∧ map.right_inverse g f
theorem bijective_of_is_inverse {g : map b a} {f : map a b} (H : is_inverse g f) : bijective f :=
theorem bijective_of_is_inverse {g : map b a} {f : map a b} (H : map.is_inverse g f) : map.bijective f :=
and.intro
(injective_of_left_inverse (and.left H))
(surjective_of_right_inverse (and.right H))

4
library/data/unit.lean
View file

@ -17,11 +17,11 @@ namespace unit
unit.equal a star
protected theorem subsingleton [instance] : subsingleton unit :=
subsingleton.intro (λ a b, equal a b)
subsingleton.intro (λ a b, unit.equal a b)
protected definition is_inhabited [instance] : inhabited unit :=
inhabited.mk unit.star
protected definition has_decidable_eq [instance] : decidable_eq unit :=
take (a b : unit), decidable.inl (equal a b)
take (a b : unit), decidable.inl (unit.equal a b)
end unit

4
library/init/funext.lean
View file

@ -28,8 +28,8 @@ namespace function
protected theorem equiv.trans {f₁ f₂ f₃ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
λH₁ H₂ x, eq.trans (H₁ x) (H₂ x)
protected theorem equiv.is_equivalence (A : Type) (B : A → Type) : equivalence (@equiv A B) :=
mk_equivalence (@equiv A B) (@equiv.refl A B) (@equiv.symm A B) (@equiv.trans A B)
protected theorem equiv.is_equivalence (A : Type) (B : A → Type) : equivalence (@function.equiv A B) :=
mk_equivalence (@function.equiv A B) (@equiv.refl A B) (@equiv.symm A B) (@equiv.trans A B)
end function
section

12
library/init/quot.lean
View file

@ -49,19 +49,19 @@ namespace quot
protected lemma indep_coherent (f : Π a, B ⟦a⟧)
(H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
: ∀ a b, a ≈ b → indep f a = indep f b :=
: ∀ a b, a ≈ b → quot.indep f a = quot.indep f b :=
λa b e, sigma.equal (sound e) (H a b e)
protected lemma lift_indep_pr1
(f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
(q : quot s) : (lift (indep f) (indep_coherent f H) q).1 = q :=
(q : quot s) : (lift (quot.indep f) (quot.indep_coherent f H) q).1 = q :=
quot.ind (λ a, by esimp) q
protected definition rec [reducible]
(f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
(q : quot s) : B q :=
let p := lift (indep f) (indep_coherent f H) q in
eq.rec_on (lift_indep_pr1 f H q) (p.2)
let p := lift (quot.indep f) (quot.indep_coherent f H) q in
eq.rec_on (quot.lift_indep_pr1 f H q) (p.2)
protected definition rec_on [reducible]
(q : quot s) (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b) : B q :=
@ -126,8 +126,8 @@ namespace quot
protected definition hrec_on₂ [reducible]
{C : quot s₁ → quot s₂ → Type₁} (q₁ : quot s₁) (q₂ : quot s₂)
(f : Π a b, C ⟦a⟧ ⟦b⟧) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ == f b₁ b₂) : C q₁ q₂:=
hrec_on q₁
(λ a, hrec_on q₂ (λ b, f a b) (λ b₁ b₂ p, c _ _ _ _ !setoid.refl p))
quot.hrec_on q₁
(λ a, quot.hrec_on q₂ (λ b, f a b) (λ b₁ b₂ p, c _ _ _ _ !setoid.refl p))
(λ a₁ a₂ p, quot.induction_on q₂
(λ b,
have aux : f a₁ b == f a₂ b, from c _ _ _ _ p !setoid.refl,

12
src/frontends/lean/decl_cmds.cpp
View file

@ -152,8 +152,12 @@ static environment declare_var(parser & p, environment env,
env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type)));
p.add_decl_index(full_n, pos, get_variable_tk(), new_type);
}
if (!ns.is_anonymous())
if (!ns.is_anonymous()) {
if (is_protected)
env = add_expr_alias(env, get_protected_shortest_name(full_n), full_n);
else
env = add_expr_alias(env, n, full_n);
}
if (is_protected)
env = add_protected(env, full_n);
return env;
@ -1101,8 +1105,12 @@ class definition_cmd_fn {
m_p.add_decl_index(real_n, m_pos, m_p.get_cmd_token(), type);
if (m_is_protected)
m_env = add_protected(m_env, real_n);
if (n != real_n)
if (n != real_n) {
if (m_is_protected)
m_env = add_expr_alias_rec(m_env, get_protected_shortest_name(real_n), real_n);
else
m_env = add_expr_alias_rec(m_env, n, real_n);
}
if (m_kind == Abbreviation || m_kind == LocalAbbreviation) {
bool persistent = m_kind == Abbreviation;
m_env = add_abbreviation(m_env, real_n, m_attributes.m_is_parsing_only, persistent);

9
src/library/protected.cpp
View file

@ -53,6 +53,15 @@ bool is_protected(environment const & env, name const & n) {
return get_extension(env).m_protected.contains(n);
}
name get_protected_shortest_name(name const & n) {
if (n.is_atomic() || n.get_prefix().is_atomic()) {
return n;
} else {
name new_prefix = n.get_prefix().replace_prefix(n.get_prefix().get_prefix(), name());
return n.replace_prefix(n.get_prefix(), new_prefix);
}
}
void initialize_protected() {
g_ext = new protected_ext_reg();
g_prt_key = new std::string("prt");

2
src/library/protected.h
View file

@ -12,6 +12,8 @@ namespace lean {
environment add_protected(environment const & env, name const & n);
/** \brief Return true iff \c n was marked as protected in the environment \c n. */
bool is_protected(environment const & env, name const & n);
/** \brief Return the shortest name that can be used to reference the given name */
name get_protected_shortest_name(name const & n);
void initialize_protected();
void finalize_protected();

2
tests/lean/hott/433.hlean
View file

@ -95,7 +95,7 @@ namespace pi
definition transport_V [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
p⁻¹ ▸ u
protected definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
/- Equivalences -/
definition isequiv_functor_pi [instance] (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')
[H0 : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')]

4
tests/lean/protected_consts.lean
View file

@ -1,10 +1,10 @@
namespace foo
protected axiom A : Prop
axiom B : Prop
protected constant a : A
protected constant a : foo.A
constant b : B
protected axioms (A₁ A₂ : Prop)
protected constants (a₁ a₂ : A)
protected constants (a₁ a₂ : foo.A)
axioms (B₁ B₂ : Prop)
constants (b₁ b₂ : B)
end foo