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

feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'

Browse source 
see issue #693
This commit is contained in:
Leonardo de Moura 2015-07-07 16:37:06 -07:00
parent 991ff67b45
commit 4b1b3e277f
57 changed files with 336 additions and 317 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
hott/algebra/category/constructions/comma.hlean
View file

@ -17,9 +17,9 @@ namespace category
(a : A) (a : A)
(b : B) (b : B)
(f : S a ⟶ T b) (f : S a ⟶ T b)
abbreviation ob1 [unfold-c 6] := @comma_object.a abbreviation ob1 [unfold 6] := @comma_object.a
abbreviation ob2 [unfold-c 6] := @comma_object.b abbreviation ob2 [unfold 6] := @comma_object.b
abbreviation mor [unfold-c 6] := @comma_object.f abbreviation mor [unfold 6] := @comma_object.f
variables {A B C : Precategory} (S : A ⇒ C) (T : B ⇒ C) variables {A B C : Precategory} (S : A ⇒ C) (T : B ⇒ C)

22
hott/algebra/category/iso.hlean
View file

@ -24,13 +24,13 @@ namespace iso
attribute is_iso [multiple-instances] attribute is_iso [multiple-instances]
open split_mono split_epi is_iso open split_mono split_epi is_iso
abbreviation retraction_of [unfold-c 6] := @split_mono.retraction_of abbreviation retraction_of [unfold 6] := @split_mono.retraction_of
abbreviation retraction_comp [unfold-c 6] := @split_mono.retraction_comp abbreviation retraction_comp [unfold 6] := @split_mono.retraction_comp
abbreviation section_of [unfold-c 6] := @split_epi.section_of abbreviation section_of [unfold 6] := @split_epi.section_of
abbreviation comp_section [unfold-c 6] := @split_epi.comp_section abbreviation comp_section [unfold 6] := @split_epi.comp_section
abbreviation inverse [unfold-c 6] := @is_iso.inverse abbreviation inverse [unfold 6] := @is_iso.inverse
abbreviation left_inverse [unfold-c 6] := @is_iso.left_inverse abbreviation left_inverse [unfold 6] := @is_iso.left_inverse
abbreviation right_inverse [unfold-c 6] := @is_iso.right_inverse abbreviation right_inverse [unfold 6] := @is_iso.right_inverse
postfix `⁻¹` := inverse postfix `⁻¹` := inverse
--a second notation for the inverse, which is not overloaded --a second notation for the inverse, which is not overloaded
postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h
@ -145,7 +145,7 @@ namespace iso
(H1 : g ∘ f = id) (H2 : f ∘ g = id) := (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
@mk _ _ _ _ f (is_iso.mk H1 H2) @mk _ _ _ _ f (is_iso.mk H1 H2)
definition to_inv [unfold-c 5] (f : a ≅ b) : b ⟶ a := definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a :=
(to_hom f)⁻¹ (to_hom f)⁻¹
protected definition refl [constructor] (a : ob) : a ≅ a := protected definition refl [constructor] (a : ob) : a ≅ a :=
@ -182,13 +182,13 @@ namespace iso
apply equiv.to_is_equiv (!iso.sigma_char), apply equiv.to_is_equiv (!iso.sigma_char),
end end
definition iso_of_eq [unfold-c 5] (p : a = b) : a ≅ b := definition iso_of_eq [unfold 5] (p : a = b) : a ≅ b :=
eq.rec_on p (iso.refl a) eq.rec_on p (iso.refl a)
definition hom_of_eq [reducible] [unfold-c 5] (p : a = b) : a ⟶ b := definition hom_of_eq [reducible] [unfold 5] (p : a = b) : a ⟶ b :=
iso.to_hom (iso_of_eq p) iso.to_hom (iso_of_eq p)
definition inv_of_eq [reducible] [unfold-c 5] (p : a = b) : b ⟶ a := definition inv_of_eq [reducible] [unfold 5] (p : a = b) : b ⟶ a :=
iso.to_inv (iso_of_eq p) iso.to_inv (iso_of_eq p)
definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) := definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) :=

4
hott/arity.hlean
View file

@ -121,10 +121,10 @@ namespace eq
-- : f a b c d e ff g h = f a' b' c' d' e' f' g' h' := -- : f a b c d e ff g h = f a' b' c' d' e' f' g' h' :=
-- by cases Ha; cases Hb; cases Hc; cases Hd; cases He; cases Hf; cases Hg; cases Hh; reflexivity -- by cases Ha; cases Hb; cases Hc; cases Hd; cases He; cases Hf; cases Hg; cases Hh; reflexivity
definition apd100 [unfold-c 6] {f g : Πa b, C a b} (p : f = g) : f ~2 g := definition apd100 [unfold 6] {f g : Πa b, C a b} (p : f = g) : f ~2 g :=
λa b, apd10 (apd10 p a) b λa b, apd10 (apd10 p a) b
definition apd1000 [unfold-c 7] {f g : Πa b c, D a b c} (p : f = g) : f ~3 g := definition apd1000 [unfold 7] {f g : Πa b c, D a b c} (p : f = g) : f ~3 g :=
λa b c, apd100 (apd10 p a) b c λa b c, apd100 (apd10 p a) b c
/- some properties of these variants of ap -/ /- some properties of these variants of ap -/

16
hott/hit/circle.hlean
View file

@ -148,14 +148,14 @@ namespace circle
end circle end circle
attribute circle.base1 circle.base2 circle.base [constructor] attribute circle.base1 circle.base2 circle.base [constructor]
attribute circle.rec2 circle.elim2 [unfold-c 6] [recursor 6] attribute circle.rec2 circle.elim2 [unfold 6] [recursor 6]
attribute circle.elim2_type [unfold-c 5] attribute circle.elim2_type [unfold 5]
attribute circle.rec2_on circle.elim2_on [unfold-c 2] attribute circle.rec2_on circle.elim2_on [unfold 2]
attribute circle.elim2_type [unfold-c 1] attribute circle.elim2_type [unfold 1]
attribute circle.elim circle.rec [unfold-c 4] [recursor 4] attribute circle.elim circle.rec [unfold 4] [recursor 4]
attribute circle.elim_type [unfold-c 3] attribute circle.elim_type [unfold 3]
attribute circle.rec_on circle.elim_on [unfold-c 2] attribute circle.rec_on circle.elim_on [unfold 2]
attribute circle.elim_type_on [unfold-c 1] attribute circle.elim_type_on [unfold 1]
namespace circle namespace circle
definition pointed_circle [instance] [constructor] : pointed circle := definition pointed_circle [instance] [constructor] : pointed circle :=

8
hott/hit/coeq.hlean
View file

@ -79,7 +79,7 @@ end
end coeq end coeq
attribute coeq.coeq_i [constructor] attribute coeq.coeq_i [constructor]
attribute coeq.rec coeq.elim [unfold-c 8] [recursor 8] attribute coeq.rec coeq.elim [unfold 8] [recursor 8]
attribute coeq.elim_type [unfold-c 7] attribute coeq.elim_type [unfold 7]
attribute coeq.rec_on coeq.elim_on [unfold-c 6] attribute coeq.rec_on coeq.elim_on [unfold 6]
attribute coeq.elim_type_on [unfold-c 5] attribute coeq.elim_type_on [unfold 5]

16
hott/hit/colimit.hlean
View file

@ -171,11 +171,11 @@ end
end seq_colim end seq_colim
attribute colimit.incl seq_colim.inclusion [constructor] attribute colimit.incl seq_colim.inclusion [constructor]
attribute colimit.rec colimit.elim [unfold-c 10] [recursor 10] attribute colimit.rec colimit.elim [unfold 10] [recursor 10]
attribute colimit.elim_type [unfold-c 9] attribute colimit.elim_type [unfold 9]
attribute colimit.rec_on colimit.elim_on [unfold-c 8] attribute colimit.rec_on colimit.elim_on [unfold 8]
attribute colimit.elim_type_on [unfold-c 7] attribute colimit.elim_type_on [unfold 7]
attribute seq_colim.rec seq_colim.elim [unfold-c 6] [recursor 6] attribute seq_colim.rec seq_colim.elim [unfold 6] [recursor 6]
attribute seq_colim.elim_type [unfold-c 5] attribute seq_colim.elim_type [unfold 5]
attribute seq_colim.rec_on seq_colim.elim_on [unfold-c 4] attribute seq_colim.rec_on seq_colim.elim_on [unfold 4]
attribute seq_colim.elim_type_on [unfold-c 3] attribute seq_colim.elim_type_on [unfold 3]

8
hott/hit/cylinder.hlean
View file

@ -89,7 +89,7 @@ end
end cylinder end cylinder
attribute cylinder.base cylinder.top [constructor] attribute cylinder.base cylinder.top [constructor]
attribute cylinder.rec cylinder.elim [unfold-c 8] [recursor 8] attribute cylinder.rec cylinder.elim [unfold 8] [recursor 8]
attribute cylinder.elim_type [unfold-c 7] attribute cylinder.elim_type [unfold 7]
attribute cylinder.rec_on cylinder.elim_on [unfold-c 5] attribute cylinder.rec_on cylinder.elim_on [unfold 5]
attribute cylinder.elim_type_on [unfold-c 4] attribute cylinder.elim_type_on [unfold 4]

8
hott/hit/pushout.hlean
View file

@ -86,7 +86,7 @@ end
end pushout end pushout
attribute pushout.inl pushout.inr [constructor] attribute pushout.inl pushout.inr [constructor]
attribute pushout.rec pushout.elim [unfold-c 10] [recursor 10] attribute pushout.rec pushout.elim [unfold 10] [recursor 10]
attribute pushout.elim_type [unfold-c 9] attribute pushout.elim_type [unfold 9]
attribute pushout.rec_on pushout.elim_on [unfold-c 7] attribute pushout.rec_on pushout.elim_on [unfold 7]
attribute pushout.elim_type_on [unfold-c 6] attribute pushout.elim_type_on [unfold 6]

8
hott/hit/quotient.hlean
View file

@ -55,7 +55,7 @@ namespace quotient
end quotient end quotient
attribute quotient.rec [recursor] attribute quotient.rec [recursor]
attribute quotient.elim [unfold-c 6] [recursor 6] attribute quotient.elim [unfold 6] [recursor 6]
attribute quotient.elim_type [unfold-c 5] attribute quotient.elim_type [unfold 5]
attribute quotient.elim_on [unfold-c 4] attribute quotient.elim_on [unfold 4]
attribute quotient.elim_type_on [unfold-c 3] attribute quotient.elim_type_on [unfold 3]

8
hott/hit/red_susp.hlean
View file

@ -81,7 +81,7 @@ end
end red_susp end red_susp
attribute red_susp.base [constructor] attribute red_susp.base [constructor]
attribute /-red_susp.rec-/ red_susp.elim [unfold-c 6] [recursor 6] attribute /-red_susp.rec-/ red_susp.elim [unfold 6] [recursor 6]
--attribute red_susp.elim_type [unfold-c 9] --attribute red_susp.elim_type [unfold 9]
attribute /-red_susp.rec_on-/ red_susp.elim_on [unfold-c 3] attribute /-red_susp.rec_on-/ red_susp.elim_on [unfold 3]
--attribute red_susp.elim_type_on [unfold-c 6] --attribute red_susp.elim_type_on [unfold 6]

8
hott/hit/refl_quotient.hlean
View file

@ -84,7 +84,7 @@ end
end refl_quotient end refl_quotient
attribute refl_quotient.rclass_of [constructor] attribute refl_quotient.rclass_of [constructor]
attribute /-refl_quotient.rec-/ refl_quotient.elim [unfold-c 8] [recursor 8] attribute /-refl_quotient.rec-/ refl_quotient.elim [unfold 8] [recursor 8]
--attribute refl_quotient.elim_type [unfold-c 9] --attribute refl_quotient.elim_type [unfold 9]
attribute /-refl_quotient.rec_on-/ refl_quotient.elim_on [unfold-c 5] attribute /-refl_quotient.rec_on-/ refl_quotient.elim_on [unfold 5]
--attribute refl_quotient.elim_type_on [unfold-c 6] --attribute refl_quotient.elim_type_on [unfold 6]

4
hott/hit/set_quotient.hlean
View file

@ -71,5 +71,5 @@ end
end set_quotient end set_quotient
attribute set_quotient.class_of [constructor] attribute set_quotient.class_of [constructor]
attribute set_quotient.rec set_quotient.elim [unfold-c 7] [recursor 7] attribute set_quotient.rec set_quotient.elim [unfold 7] [recursor 7]
attribute set_quotient.rec_on set_quotient.elim_on [unfold-c 4] attribute set_quotient.rec_on set_quotient.elim_on [unfold 4]

8
hott/hit/susp.hlean
View file

@ -72,10 +72,10 @@ namespace susp
end susp end susp
attribute susp.north susp.south [constructor] attribute susp.north susp.south [constructor]
attribute susp.rec susp.elim [unfold-c 6] [recursor 6] attribute susp.rec susp.elim [unfold 6] [recursor 6]
attribute susp.elim_type [unfold-c 5] attribute susp.elim_type [unfold 5]
attribute susp.rec_on susp.elim_on [unfold-c 3] attribute susp.rec_on susp.elim_on [unfold 3]
attribute susp.elim_type_on [unfold-c 2] attribute susp.elim_type_on [unfold 2]
namespace susp namespace susp
open pointed open pointed

8
hott/hit/torus.hlean
View file

@ -87,7 +87,7 @@ namespace torus
end torus end torus
attribute torus.base [constructor] attribute torus.base [constructor]
attribute /-torus.rec-/ torus.elim [unfold-c 6] [recursor 6] attribute /-torus.rec-/ torus.elim [unfold 6] [recursor 6]
--attribute torus.elim_type [unfold-c 9] --attribute torus.elim_type [unfold 9]
attribute /-torus.rec_on-/ torus.elim_on [unfold-c 2] attribute /-torus.rec_on-/ torus.elim_on [unfold 2]
--attribute torus.elim_type_on [unfold-c 6] --attribute torus.elim_type_on [unfold 6]

6
hott/hit/trunc.hlean
View file

@ -51,7 +51,7 @@ namespace trunc
tr⁻¹ tr⁻¹
/- Functoriality -/ /- Functoriality -/
definition trunc_functor [unfold-c 5] (f : X → Y) : trunc n X → trunc n Y := definition trunc_functor [unfold 5] (f : X → Y) : trunc n X → trunc n Y :=
λxx, trunc.rec_on xx (λx, tr (f x)) λxx, trunc.rec_on xx (λx, tr (f x))
definition trunc_functor_compose (f : X → Y) (g : Y → Z) definition trunc_functor_compose (f : X → Y) (g : Y → Z)
@ -130,6 +130,6 @@ namespace trunc
end trunc end trunc
attribute trunc.elim_on [unfold-c 4] attribute trunc.elim_on [unfold 4]
attribute trunc.rec [recursor] attribute trunc.rec [recursor]
attribute trunc.elim [recursor 6] [unfold-c 6] attribute trunc.elim [recursor 6] [unfold 6]

28
hott/hit/two_quotient.hlean
View file

@ -34,10 +34,10 @@ namespace simple_two_quotient
class_of pre_simple_two_quotient_rel (inr ⟨a, r, q⟩) class_of pre_simple_two_quotient_rel (inr ⟨a, r, q⟩)
protected definition e (s : R a a') : j a = j a' := eq_of_rel _ (pre_Rmk s) protected definition e (s : R a a') : j a = j a' := eq_of_rel _ (pre_Rmk s)
protected definition et (t : T a a') : j a = j a' := e_closure.elim e t protected definition et (t : T a a') : j a = j a' := e_closure.elim e t
protected definition f [unfold-c 7] (q : Q r) : S¹ → C := protected definition f [unfold 7] (q : Q r) : S¹ → C :=
circle.elim (j a) (et r) circle.elim (j a) (et r)
protected definition pre_rec [unfold-c 8] {P : C → Type} protected definition pre_rec [unfold 8] {P : C → Type}
(Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q)) (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q))
(Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') (x : C) : P x := (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') (x : C) : P x :=
begin begin
@ -48,7 +48,7 @@ namespace simple_two_quotient
{ induction H, esimp, apply Pe}, { induction H, esimp, apply Pe},
end end
protected definition pre_elim [unfold-c 8] {P : Type} (Pj : A → P) protected definition pre_elim [unfold 8] {P : Type} (Pj : A → P)
(Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P) (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') (x : C) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P) (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') (x : C)
: P := : P :=
pre_rec Pj Pa (λa a' s, pathover_of_eq (Pe s)) x pre_rec Pj Pa (λa a' s, pathover_of_eq (Pe s)) x
@ -124,7 +124,7 @@ namespace simple_two_quotient
!ap_constant⁻¹ end !ap_constant⁻¹ end
} end end}, } end end},
end end
local attribute elim [unfold-c 8] local attribute elim [unfold 8]
protected definition elim_on {P : Type} (x : D) (P0 : A → P) protected definition elim_on {P : Type} (x : D) (P0 : A → P)
(P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
@ -237,10 +237,10 @@ end
end simple_two_quotient end simple_two_quotient
--attribute simple_two_quotient.j [constructor] --TODO --attribute simple_two_quotient.j [constructor] --TODO
attribute /-simple_two_quotient.rec-/ simple_two_quotient.elim [unfold-c 8] [recursor 8] attribute /-simple_two_quotient.rec-/ simple_two_quotient.elim [unfold 8] [recursor 8]
--attribute simple_two_quotient.elim_type [unfold-c 9] --attribute simple_two_quotient.elim_type [unfold 9]
attribute /-simple_two_quotient.rec_on-/ simple_two_quotient.elim_on [unfold-c 5] attribute /-simple_two_quotient.rec_on-/ simple_two_quotient.elim_on [unfold 5]
--attribute simple_two_quotient.elim_type_on [unfold-c 6] --attribute simple_two_quotient.elim_type_on [unfold 6]
namespace two_quotient namespace two_quotient
open e_closure simple_two_quotient open e_closure simple_two_quotient
@ -272,11 +272,11 @@ namespace two_quotient
induction x, induction x,
{ exact P0 a}, { exact P0 a},
{ exact P1 s}, { exact P1 s},
{ exact abstract [unfold-c 10] begin induction q with a a' t t' q, { exact abstract [unfold 10] begin induction q with a a' t t' q,
rewrite [↑e_closure.elim,↓e_closure.elim P1 t,↓e_closure.elim P1 t'], rewrite [↑e_closure.elim,↓e_closure.elim P1 t,↓e_closure.elim P1 t'],
apply con_inv_eq_idp, exact P2 q end end}, apply con_inv_eq_idp, exact P2 q end end},
end end
local attribute elim [unfold-c 8] local attribute elim [unfold 8]
protected definition elim_on {P : Type} (x : two_quotient) (P0 : A → P) protected definition elim_on {P : Type} (x : two_quotient) (P0 : A → P)
(P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
@ -314,7 +314,7 @@ end
end two_quotient end two_quotient
--attribute two_quotient.j [constructor] --TODO --attribute two_quotient.j [constructor] --TODO
attribute /-two_quotient.rec-/ two_quotient.elim [unfold-c 8] [recursor 8] attribute /-two_quotient.rec-/ two_quotient.elim [unfold 8] [recursor 8]
--attribute two_quotient.elim_type [unfold-c 9] --attribute two_quotient.elim_type [unfold 9]
attribute /-two_quotient.rec_on-/ two_quotient.elim_on [unfold-c 5] attribute /-two_quotient.rec_on-/ two_quotient.elim_on [unfold 5]
--attribute two_quotient.elim_type_on [unfold-c 6] --attribute two_quotient.elim_type_on [unfold 6]

8
hott/init/datatypes.hlean
View file

@ -31,10 +31,10 @@ up :: (down : A)
inductive prod (A B : Type) := inductive prod (A B : Type) :=
mk : A → B → prod A B mk : A → B → prod A B
definition prod.pr1 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : A := definition prod.pr1 [reducible] [unfold 3] {A B : Type} (p : prod A B) : A :=
prod.rec (λ a b, a) p prod.rec (λ a b, a) p
definition prod.pr2 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : B := definition prod.pr2 [reducible] [unfold 3] {A B : Type} (p : prod A B) : B :=
prod.rec (λ a b, b) p prod.rec (λ a b, b) p
definition prod.destruct [reducible] := @prod.cases_on definition prod.destruct [reducible] := @prod.cases_on
@ -52,10 +52,10 @@ sum.inr b
inductive sigma {A : Type} (B : A → Type) := inductive sigma {A : Type} (B : A → Type) :=
mk : Π (a : A), B a → sigma B mk : Π (a : A), B a → sigma B
definition sigma.pr1 [reducible] [unfold-c 3] {A : Type} {B : A → Type} (p : sigma B) : A := definition sigma.pr1 [reducible] [unfold 3] {A : Type} {B : A → Type} (p : sigma B) : A :=
sigma.rec (λ a b, a) p sigma.rec (λ a b, a) p
definition sigma.pr2 [reducible] [unfold-c 3] {A : Type} {B : A → Type} (p : sigma B) : B (sigma.pr1 p) := definition sigma.pr2 [reducible] [unfold 3] {A : Type} {B : A → Type} (p : sigma B) : B (sigma.pr1 p) :=
sigma.rec (λ a b, b) p sigma.rec (λ a b, b) p
-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.

8
hott/init/equiv.hlean
View file

@ -232,14 +232,14 @@ namespace equiv
(right_inv : f ∘ g ~ id) (left_inv : g ∘ f ~ id) : A ≃ B := (right_inv : f ∘ g ~ id) (left_inv : g ∘ f ~ id) : A ≃ B :=
equiv.mk f (adjointify f g right_inv left_inv) equiv.mk f (adjointify f g right_inv left_inv)
definition to_inv [reducible] [unfold-c 3] (f : A ≃ B) : B → A := f⁻¹ definition to_inv [reducible] [unfold 3] (f : A ≃ B) : B → A := f⁻¹
definition to_right_inv [reducible] [unfold-c 3] (f : A ≃ B) : f ∘ f⁻¹ ~ id := right_inv f definition to_right_inv [reducible] [unfold 3] (f : A ≃ B) : f ∘ f⁻¹ ~ id := right_inv f
definition to_left_inv [reducible] [unfold-c 3] (f : A ≃ B) : f⁻¹ ∘ f ~ id := left_inv f definition to_left_inv [reducible] [unfold 3] (f : A ≃ B) : f⁻¹ ∘ f ~ id := left_inv f
protected definition refl [refl] [constructor] : A ≃ A := protected definition refl [refl] [constructor] : A ≃ A :=
equiv.mk id !is_equiv_id equiv.mk id !is_equiv_id
protected definition symm [symm] [unfold-c 3] (f : A ≃ B) : B ≃ A := protected definition symm [symm] [unfold 3] (f : A ≃ B) : B ≃ A :=
equiv.mk f⁻¹ !is_equiv_inv equiv.mk f⁻¹ !is_equiv_inv
protected definition trans [trans] (f : A ≃ B) (g: B ≃ C) : A ≃ C := protected definition trans [trans] (f : A ≃ B) (g: B ≃ C) : A ≃ C :=

24
hott/init/function.hlean
View file

@ -15,42 +15,42 @@ namespace function
variables {A B C D E : Type} variables {A B C D E : Type}
definition compose [reducible] [unfold-f] (f : B → C) (g : A → B) : A → C := definition compose [reducible] [unfold-full] (f : B → C) (g : A → B) : A → C :=
λx, f (g x) λx, f (g x)
definition compose_right [reducible] [unfold-f] (f : B → B → B) (g : A → B) : B → A → B := definition compose_right [reducible] [unfold-full] (f : B → B → B) (g : A → B) : B → A → B :=
λ b a, f b (g a) λ b a, f b (g a)
definition compose_left [reducible] [unfold-f] (f : B → B → B) (g : A → B) : A → B → B := definition compose_left [reducible] [unfold-full] (f : B → B → B) (g : A → B) : A → B → B :=
λ a b, f (g a) b λ a b, f (g a) b
definition id [reducible] [unfold-f] (a : A) : A := definition id [reducible] [unfold-full] (a : A) : A :=
a a
definition on_fun [reducible] [unfold-f] (f : B → B → C) (g : A → B) : A → A → C := definition on_fun [reducible] [unfold-full] (f : B → B → C) (g : A → B) : A → A → C :=
λx y, f (g x) (g y) λx y, f (g x) (g y)
definition combine [reducible] [unfold-f] (f : A → B → C) (op : C → D → E) (g : A → B → D) definition combine [reducible] [unfold-full] (f : A → B → C) (op : C → D → E) (g : A → B → D)
: A → B → E := : A → B → E :=
λx y, op (f x y) (g x y) λx y, op (f x y) (g x y)
definition const [reducible] [unfold-f] (B : Type) (a : A) : B → A := definition const [reducible] [unfold-full] (B : Type) (a : A) : B → A :=
λx, a λx, a
definition dcompose [reducible] [unfold-f] {B : A → Type} {C : Π {x : A}, B x → Type} definition dcompose [reducible] [unfold-full] {B : A → Type} {C : Π {x : A}, B x → Type}
(f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) := (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
λx, f (g x) λx, f (g x)
definition flip [reducible] [unfold-f] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := definition flip [reducible] [unfold-full] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
λy x, f x y λy x, f x y
definition app [reducible] [unfold-f] {B : A → Type} (f : Πx, B x) (x : A) : B x := definition app [reducible] [unfold-full] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
f x f x
definition curry [reducible] [unfold-f] : (A × B → C) → A → B → C := definition curry [reducible] [unfold-full] : (A × B → C) → A → B → C :=
λ f a b, f (a, b) λ f a b, f (a, b)
definition uncurry [reducible] [unfold-c 5] : (A → B → C) → (A × B → C) := definition uncurry [reducible] [unfold 5] : (A → B → C) → (A × B → C) :=
λ f p, match p with (a, b) := f a b end λ f p, match p with (a, b) := f a b end
precedence `∘'`:60 precedence `∘'`:60

4
hott/init/hit.hlean
View file

@ -85,5 +85,5 @@ namespace quotient
end quotient end quotient
attribute quotient.class_of trunc.tr [constructor] attribute quotient.class_of trunc.tr [constructor]
attribute quotient.rec trunc.rec [unfold-c 6] attribute quotient.rec trunc.rec [unfold 6]
attribute quotient.rec_on trunc.rec_on [unfold-c 4] attribute quotient.rec_on trunc.rec_on [unfold 4]

6
hott/init/logic.hlean
View file

@ -42,13 +42,13 @@ definition rfl {A : Type} {a : A} := eq.refl a
namespace eq namespace eq
variables {A : Type} {a b c : A} variables {A : Type} {a b c : A}
definition subst [unfold-c 5] {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b := definition subst [unfold 5] {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b :=
eq.rec H₂ H₁ eq.rec H₂ H₁
definition trans [unfold-c 5] (H₁ : a = b) (H₂ : b = c) : a = c := definition trans [unfold 5] (H₁ : a = b) (H₂ : b = c) : a = c :=
subst H₂ H₁ subst H₂ H₁
definition symm [unfold-c 4] (H : a = b) : b = a := definition symm [unfold 4] (H : a = b) : b = a :=
subst H (refl a) subst H (refl a)
namespace ops namespace ops

10
hott/init/nat.hlean
View file

@ -26,7 +26,7 @@ namespace nat
infix `≥` := ge infix `≥` := ge
infix `>` := gt infix `>` := gt
definition pred [unfold-c 1] (a : nat) : nat := definition pred [unfold 1] (a : nat) : nat :=
nat.cases_on a zero (λ a₁, a₁) nat.cases_on a zero (λ a₁, a₁)
-- add is defined in init.num -- add is defined in init.num
@ -73,16 +73,16 @@ namespace nat
definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
definition succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := definition succ_le_succ [unfold 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
by induction H;reflexivity;exact le.step v_0 by induction H;reflexivity;exact le.step v_0
definition pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := definition pred_le_pred [unfold 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
by induction H;reflexivity;cases b;exact v_0;exact le.step v_0 by induction H;reflexivity;cases b;exact v_0;exact le.step v_0
definition le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := definition le_of_succ_le_succ [unfold 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
pred_le_pred H pred_le_pred H
definition le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m := definition le_succ_of_pred_le [unfold 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
by cases n;exact le.step H;exact succ_le_succ H by cases n;exact le.step H;exact succ_le_succ H
definition not_succ_le_self {n : ℕ} : ¬succ n ≤ n := definition not_succ_le_self {n : ℕ} : ¬succ n ≤ n :=

62
hott/init/path.hlean
View file

@ -22,20 +22,20 @@ namespace eq
definition idpath [reducible] [constructor] (a : A) := refl a definition idpath [reducible] [constructor] (a : A) := refl a
-- unbased path induction -- unbased path induction
definition rec' [reducible] [unfold-c 6] {P : Π (a b : A), (a = b) → Type} definition rec' [reducible] [unfold 6] {P : Π (a b : A), (a = b) → Type}
(H : Π (a : A), P a a idp) {a b : A} (p : a = b) : P a b p := (H : Π (a : A), P a a idp) {a b : A} (p : a = b) : P a b p :=
eq.rec (H a) p eq.rec (H a) p
definition rec_on' [reducible] [unfold-c 5] {P : Π (a b : A), (a = b) → Type} definition rec_on' [reducible] [unfold 5] {P : Π (a b : A), (a = b) → Type}
{a b : A} (p : a = b) (H : Π (a : A), P a a idp) : P a b p := {a b : A} (p : a = b) (H : Π (a : A), P a a idp) : P a b p :=
eq.rec (H a) p eq.rec (H a) p
/- Concatenation and inverse -/ /- Concatenation and inverse -/
definition concat [trans] [unfold-c 6] (p : x = y) (q : y = z) : x = z := definition concat [trans] [unfold 6] (p : x = y) (q : y = z) : x = z :=
eq.rec (λp', p') q p eq.rec (λp', p') q p
definition inverse [symm] [unfold-c 4] (p : x = y) : y = x := definition inverse [symm] [unfold 4] (p : x = y) : y = x :=
eq.rec (refl x) p eq.rec (refl x) p
infix ⬝ := concat infix ⬝ := concat
@ -46,11 +46,11 @@ namespace eq
/- The 1-dimensional groupoid structure -/ /- The 1-dimensional groupoid structure -/
-- The identity path is a right unit. -- The identity path is a right unit.
definition con_idp [unfold-f] (p : x = y) : p ⬝ idp = p := definition con_idp [unfold-full] (p : x = y) : p ⬝ idp = p :=
idp idp
-- The identity path is a right unit. -- The identity path is a right unit.
definition idp_con [unfold-c 4] (p : x = y) : idp ⬝ p = p := definition idp_con [unfold 4] (p : x = y) : idp ⬝ p = p :=
eq.rec_on p idp eq.rec_on p idp
-- Concatenation is associative. -- Concatenation is associative.
@ -63,11 +63,11 @@ namespace eq
eq.rec_on r (eq.rec_on q idp) eq.rec_on r (eq.rec_on q idp)
-- The left inverse law. -- The left inverse law.
definition con.right_inv [unfold-c 4] (p : x = y) : p ⬝ p⁻¹ = idp := definition con.right_inv [unfold 4] (p : x = y) : p ⬝ p⁻¹ = idp :=
eq.rec_on p idp eq.rec_on p idp
-- The right inverse law. -- The right inverse law.
definition con.left_inv [unfold-c 4] (p : x = y) : p⁻¹ ⬝ p = idp := definition con.left_inv [unfold 4] (p : x = y) : p⁻¹ ⬝ p = idp :=
eq.rec_on p idp eq.rec_on p idp
/- Several auxiliary theorems about canceling inverses across associativity. These are somewhat /- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
@ -113,7 +113,7 @@ namespace eq
p = r⁻¹ ⬝ q → r ⬝ p = q := p = r⁻¹ ⬝ q → r ⬝ p = q :=
eq.rec_on r (take p h, !idp_con ⬝ h ⬝ !idp_con) p eq.rec_on r (take p h, !idp_con ⬝ h ⬝ !idp_con) p
definition con_eq_of_eq_con_inv [unfold-c 5] {p : x = z} {q : y = z} {r : y = x} : definition con_eq_of_eq_con_inv [unfold 5] {p : x = z} {q : y = z} {r : y = x} :
r = q ⬝ p⁻¹ → r ⬝ p = q := r = q ⬝ p⁻¹ → r ⬝ p = q :=
eq.rec_on p (take q h, h) q eq.rec_on p (take q h, h) q
@ -121,7 +121,7 @@ namespace eq
p = r ⬝ q → r⁻¹ ⬝ p = q := p = r ⬝ q → r⁻¹ ⬝ p = q :=
eq.rec_on r (take q h, !idp_con ⬝ h ⬝ !idp_con) q eq.rec_on r (take q h, !idp_con ⬝ h ⬝ !idp_con) q
definition con_inv_eq_of_eq_con [unfold-c 5] {p : z = x} {q : y = z} {r : y = x} : definition con_inv_eq_of_eq_con [unfold 5] {p : z = x} {q : y = z} {r : y = x} :
r = q ⬝ p → r ⬝ p⁻¹ = q := r = q ⬝ p → r ⬝ p⁻¹ = q :=
eq.rec_on p (take r h, h) r eq.rec_on p (take r h, h) r
@ -129,7 +129,7 @@ namespace eq
r⁻¹ ⬝ q = p → q = r ⬝ p := r⁻¹ ⬝ q = p → q = r ⬝ p :=
eq.rec_on r (take p h, !idp_con⁻¹ ⬝ h ⬝ !idp_con⁻¹) p eq.rec_on r (take p h, !idp_con⁻¹ ⬝ h ⬝ !idp_con⁻¹) p
definition eq_con_of_con_inv_eq [unfold-c 5] {p : x = z} {q : y = z} {r : y = x} : definition eq_con_of_con_inv_eq [unfold 5] {p : x = z} {q : y = z} {r : y = x} :
q ⬝ p⁻¹ = r → q = r ⬝ p := q ⬝ p⁻¹ = r → q = r ⬝ p :=
eq.rec_on p (take q h, h) q eq.rec_on p (take q h, h) q
@ -137,17 +137,17 @@ namespace eq
r ⬝ q = p → q = r⁻¹ ⬝ p := r ⬝ q = p → q = r⁻¹ ⬝ p :=
eq.rec_on r (take q h, !idp_con⁻¹ ⬝ h ⬝ !idp_con⁻¹) q eq.rec_on r (take q h, !idp_con⁻¹ ⬝ h ⬝ !idp_con⁻¹) q
definition eq_con_inv_of_con_eq [unfold-c 5] {p : z = x} {q : y = z} {r : y = x} : definition eq_con_inv_of_con_eq [unfold 5] {p : z = x} {q : y = z} {r : y = x} :
q ⬝ p = r → q = r ⬝ p⁻¹ := q ⬝ p = r → q = r ⬝ p⁻¹ :=
eq.rec_on p (take r h, h) r eq.rec_on p (take r h, h) r
definition eq_of_con_inv_eq_idp [unfold-c 5] {p q : x = y} : p ⬝ q⁻¹ = idp → p = q := definition eq_of_con_inv_eq_idp [unfold 5] {p q : x = y} : p ⬝ q⁻¹ = idp → p = q :=
eq.rec_on q (take p h, h) p eq.rec_on q (take p h, h) p
definition eq_of_inv_con_eq_idp {p q : x = y} : q⁻¹ ⬝ p = idp → p = q := definition eq_of_inv_con_eq_idp {p q : x = y} : q⁻¹ ⬝ p = idp → p = q :=
eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p
definition eq_inv_of_con_eq_idp' [unfold-c 5] {p : x = y} {q : y = x} : p ⬝ q = idp → p = q⁻¹ := definition eq_inv_of_con_eq_idp' [unfold 5] {p : x = y} {q : y = x} : p ⬝ q = idp → p = q⁻¹ :=
eq.rec_on q (take p h, h) p eq.rec_on q (take p h, h) p
definition eq_inv_of_con_eq_idp {p : x = y} {q : y = x} : q ⬝ p = idp → p = q⁻¹ := definition eq_inv_of_con_eq_idp {p : x = y} {q : y = x} : q ⬝ p = idp → p = q⁻¹ :=
@ -156,10 +156,10 @@ namespace eq
definition eq_of_idp_eq_inv_con {p q : x = y} : idp = p⁻¹ ⬝ q → p = q := definition eq_of_idp_eq_inv_con {p q : x = y} : idp = p⁻¹ ⬝ q → p = q :=
eq.rec_on p (take q h, h ⬝ !idp_con) q eq.rec_on p (take q h, h ⬝ !idp_con) q
definition eq_of_idp_eq_con_inv [unfold-c 4] {p q : x = y} : idp = q ⬝ p⁻¹ → p = q := definition eq_of_idp_eq_con_inv [unfold 4] {p q : x = y} : idp = q ⬝ p⁻¹ → p = q :=
eq.rec_on p (take q h, h) q eq.rec_on p (take q h, h) q
definition inv_eq_of_idp_eq_con [unfold-c 4] {p : x = y} {q : y = x} : idp = q ⬝ p → p⁻¹ = q := definition inv_eq_of_idp_eq_con [unfold 4] {p : x = y} {q : y = x} : idp = q ⬝ p → p⁻¹ = q :=
eq.rec_on p (take q h, h) q eq.rec_on p (take q h, h) q
definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} : idp = p ⬝ q → p⁻¹ = q := definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} : idp = p ⬝ q → p⁻¹ = q :=
@ -185,20 +185,20 @@ namespace eq
/- Transport -/ /- Transport -/
definition transport [subst] [reducible] [unfold-c 5] (P : A → Type) {x y : A} (p : x = y) definition transport [subst] [reducible] [unfold 5] (P : A → Type) {x y : A} (p : x = y)
(u : P x) : P y := (u : P x) : P y :=
eq.rec_on p u eq.rec_on p u
-- This idiom makes the operation right associative. -- This idiom makes the operation right associative.
notation p `▸` x := transport _ p x notation p `▸` x := transport _ p x
definition cast [reducible] [unfold-c 3] {A B : Type} (p : A = B) (a : A) : B := definition cast [reducible] [unfold 3] {A B : Type} (p : A = B) (a : A) : B :=
p ▸ a p ▸ a
definition tr_rev [reducible] [unfold-c 6] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x := definition tr_rev [reducible] [unfold 6] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
p⁻¹ ▸ u p⁻¹ ▸ u
definition ap [unfold-c 6] ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y := definition ap [unfold 6] ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y :=
eq.rec_on p idp eq.rec_on p idp
abbreviation ap01 [parsing-only] := ap abbreviation ap01 [parsing-only] := ap
@ -218,19 +218,19 @@ namespace eq
(H1 : f ~ g) (H2 : g ~ h) : f ~ h := (H1 : f ~ g) (H2 : g ~ h) : f ~ h :=
λ x, H1 x ⬝ H2 x λ x, H1 x ⬝ H2 x
definition apd10 [unfold-c 5] {f g : Πx, P x} (H : f = g) : f ~ g := definition apd10 [unfold 5] {f g : Πx, P x} (H : f = g) : f ~ g :=
λx, eq.rec_on H idp λx, eq.rec_on H idp
--the next theorem is useful if you want to write "apply (apd10' a)" --the next theorem is useful if you want to write "apply (apd10' a)"
definition apd10' [unfold-c 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a := definition apd10' [unfold 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a :=
eq.rec_on H idp eq.rec_on H idp
definition ap10 [reducible] [unfold-c 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H definition ap10 [reducible] [unfold 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H
definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y := definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y :=
eq.rec_on H (eq.rec_on p idp) eq.rec_on H (eq.rec_on p idp)
definition apd [unfold-c 6] (f : Πa, P a) {x y : A} (p : x = y) : p ▸ f x = f y := definition apd [unfold 6] (f : Πa, P a) {x y : A} (p : x = y) : p ▸ f x = f y :=
eq.rec_on p idp eq.rec_on p idp
/- More theorems for moving things around in equations -/ /- More theorems for moving things around in equations -/
@ -294,7 +294,7 @@ namespace eq
eq.rec_on p idp eq.rec_on p idp
-- The action of constant maps. -- The action of constant maps.
definition ap_constant [unfold-c 5] (p : x = y) (z : B) : ap (λu, z) p = idp := definition ap_constant [unfold 5] (p : x = y) (z : B) : ap (λu, z) p = idp :=
eq.rec_on p idp eq.rec_on p idp
-- Naturality of [ap]. -- Naturality of [ap].
@ -443,7 +443,7 @@ namespace eq
-- Dependent transport in a doubly dependent type. -- Dependent transport in a doubly dependent type.
definition transportD [unfold-c 6] {P : A → Type} (Q : Πa, P a → Type) definition transportD [unfold 6] {P : A → Type} (Q : Πa, P a → Type)
{a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▸ b) := {a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▸ b) :=
eq.rec_on p z eq.rec_on p z
@ -452,7 +452,7 @@ namespace eq
notation p `▸D`:65 x:64 := transportD _ p _ x notation p `▸D`:65 x:64 := transportD _ p _ x
-- Transporting along higher-dimensional paths -- Transporting along higher-dimensional paths
definition transport2 [unfold-c 7] (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) : definition transport2 [unfold 7] (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) :
p ▸ z = q ▸ z := p ▸ z = q ▸ z :=
ap (λp', p' ▸ z) r ap (λp', p' ▸ z) r
@ -473,7 +473,7 @@ namespace eq
transport2 Q r⁻¹ z = (transport2 Q r z)⁻¹ := transport2 Q r⁻¹ z = (transport2 Q r z)⁻¹ :=
eq.rec_on r idp eq.rec_on r idp
definition transportD2 [unfold-c 7] (B C : A → Type) (D : Π(a:A), B a → C a → Type) definition transportD2 [unfold 7] (B C : A → Type) (D : Π(a:A), B a → C a → Type)
{x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▸ y) (p ▸ z) := {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▸ y) (p ▸ z) :=
eq.rec_on p w eq.rec_on p w
@ -549,7 +549,7 @@ namespace eq
eq.rec_on h (eq.rec_on h' idp) eq.rec_on h (eq.rec_on h' idp)
-- 2-dimensional path inversion -- 2-dimensional path inversion
definition inverse2 [unfold-c 6] {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ := definition inverse2 [unfold 6] {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ :=
eq.rec_on h idp eq.rec_on h idp
infixl `◾`:75 := concat2 infixl `◾`:75 := concat2
@ -631,7 +631,7 @@ namespace eq
⬝ (!whisker_left_idp_left ◾ !whisker_right_idp_right) ⬝ (!whisker_left_idp_left ◾ !whisker_right_idp_right)
-- The action of functions on 2-dimensional paths -- The action of functions on 2-dimensional paths
definition ap02 [unfold-c 8] [reducible] (f : A → B) {x y : A} {p q : x = y} (r : p = q) definition ap02 [unfold 8] [reducible] (f : A → B) {x y : A} {p q : x = y} (r : p = q)
: ap f p = ap f q := : ap f p = ap f q :=
ap (ap f) r ap (ap f) r
@ -646,7 +646,7 @@ namespace eq
⬝ (ap_con f p' q')⁻¹ := ⬝ (ap_con f p' q')⁻¹ :=
eq.rec_on r (eq.rec_on s (eq.rec_on q (eq.rec_on p idp))) eq.rec_on r (eq.rec_on s (eq.rec_on q (eq.rec_on p idp)))
definition apd02 [unfold-c 8] {p q : x = y} (f : Π x, P x) (r : p = q) : definition apd02 [unfold 8] {p q : x = y} (f : Π x, P x) (r : p = q) :
apd f p = transport2 P r (f x) ⬝ apd f q := apd f p = transport2 P r (f x) ⬝ apd f q :=
eq.rec_on r !idp_con⁻¹ eq.rec_on r !idp_con⁻¹

26
hott/init/pathover.hlean
View file

@ -32,10 +32,10 @@ namespace eq
definition pathover_of_eq_tr (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ := definition pathover_of_eq_tr (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ :=
by cases p; cases r; exact idpo by cases p; cases r; exact idpo
definition tr_eq_of_pathover [unfold-c 8] (r : b =[p] b₂) : p ▸ b = b₂ := definition tr_eq_of_pathover [unfold 8] (r : b =[p] b₂) : p ▸ b = b₂ :=
by cases r; exact idp by cases r; exact idp
definition eq_tr_of_pathover [unfold-c 8] (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ := definition eq_tr_of_pathover [unfold 8] (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ :=
by cases r; exact idp by cases r; exact idp
definition pathover_equiv_tr_eq [constructor] (p : a = a₂) (b : B a) (b₂ : B a₂) definition pathover_equiv_tr_eq [constructor] (p : a = a₂) (b : B a) (b₂ : B a₂)
@ -58,28 +58,28 @@ namespace eq
{ intro r, cases r, apply idp}, { intro r, cases r, apply idp},
end end
definition pathover_tr [unfold-c 5] (p : a = a₂) (b : B a) : b =[p] p ▸ b := definition pathover_tr [unfold 5] (p : a = a₂) (b : B a) : b =[p] p ▸ b :=
by cases p;exact idpo by cases p;exact idpo
definition tr_pathover [unfold-c 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b := definition tr_pathover [unfold 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b :=
pathover_of_eq_tr idp pathover_of_eq_tr idp
definition concato [unfold-c 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ := definition concato [unfold 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ :=
pathover.rec_on r₂ r pathover.rec_on r₂ r
definition inverseo [unfold-c 8] (r : b =[p] b₂) : b₂ =[p⁻¹] b := definition inverseo [unfold 8] (r : b =[p] b₂) : b₂ =[p⁻¹] b :=
pathover.rec_on r idpo pathover.rec_on r idpo
definition apdo [unfold-c 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ := definition apdo [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ :=
eq.rec_on p idpo eq.rec_on p idpo
definition oap [unfold-c 6] {C : A → Type} (f : Πa, B a → C a) (p : a = a₂) : f a =[p] f a₂ := definition oap [unfold 6] {C : A → Type} (f : Πa, B a → C a) (p : a = a₂) : f a =[p] f a₂ :=
eq.rec_on p idpo eq.rec_on p idpo
definition concato_eq [unfold-c 10] (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' := definition concato_eq [unfold 10] (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' :=
eq.rec_on q r eq.rec_on q r
definition eq_concato [unfold-c 9] (q : b = b') (r : b' =[p] b₂) : b =[p] b₂ := definition eq_concato [unfold 9] (q : b = b') (r : b' =[p] b₂) : b =[p] b₂ :=
by induction q;exact r by induction q;exact r
-- infix `⬝` := concato -- infix `⬝` := concato
@ -126,11 +126,11 @@ namespace eq
{ intro r, cases r, exact idp}, { intro r, cases r, exact idp},
end end
definition eq_of_pathover_idp [unfold-c 6] {b' : B a} (q : b =[idpath a] b') : b = b' := definition eq_of_pathover_idp [unfold 6] {b' : B a} (q : b =[idpath a] b') : b = b' :=
tr_eq_of_pathover q tr_eq_of_pathover q
--should B be explicit in the next two definitions? --should B be explicit in the next two definitions?
definition pathover_idp_of_eq [unfold-c 6] {b' : B a} (q : b = b') : b =[idpath a] b' := definition pathover_idp_of_eq [unfold 6] {b' : B a} (q : b = b') : b =[idpath a] b' :=
eq.rec_on q idpo eq.rec_on q idpo
definition pathover_idp [constructor] (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' := definition pathover_idp [constructor] (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' :=
@ -164,7 +164,7 @@ namespace eq
by cases r; exact H by cases r; exact H
--pathover with fibration B' ∘ f --pathover with fibration B' ∘ f
definition pathover_ap [unfold-c 10] (B' : A' → Type) (f : A → A') {p : a = a₂} definition pathover_ap [unfold 10] (B' : A' → Type) (f : A → A') {p : a = a₂}
{b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[p] b₂) : b =[ap f p] b₂ := {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[p] b₂) : b =[ap f p] b₂ :=
by cases q; exact idpo by cases q; exact idpo

2
hott/init/trunc.hlean
View file

@ -261,7 +261,7 @@ namespace is_trunc
(f : A → B) (g : B → A) : A ≃ B := (f : A → B) (g : B → A) : A ≃ B :=
equiv.mk f (is_equiv_of_is_hprop f g) equiv.mk f (is_equiv_of_is_hprop f g)
definition equiv_of_iff_of_is_hprop [unfold-c 5] [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B := definition equiv_of_iff_of_is_hprop [unfold 5] [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B :=
equiv_of_is_hprop (iff.elim_left H) (iff.elim_right H) equiv_of_is_hprop (iff.elim_left H) (iff.elim_right H)
end end

4
hott/types/W.hlean
View file

@ -19,10 +19,10 @@ namespace Wtype
variables {A A' : Type.{u}} {B B' : A → Type.{v}} {C : Π(a : A), B a → Type} variables {A A' : Type.{u}} {B B' : A → Type.{v}} {C : Π(a : A), B a → Type}
{a a' : A} {f : B a → W a, B a} {f' : B a' → W a, B a} {w w' : W(a : A), B a} {a a' : A} {f : B a → W a, B a} {f' : B a' → W a, B a} {w w' : W(a : A), B a}
protected definition pr1 [unfold-c 3] (w : W(a : A), B a) : A := protected definition pr1 [unfold 3] (w : W(a : A), B a) : A :=
by cases w with a f; exact a by cases w with a f; exact a
protected definition pr2 [unfold-c 3] (w : W(a : A), B a) : B (Wtype.pr1 w) → W(a : A), B a := protected definition pr2 [unfold 3] (w : W(a : A), B a) : B (Wtype.pr1 w) → W(a : A), B a :=
by cases w with a f; exact f by cases w with a f; exact f
namespace ops namespace ops

48
hott/types/cubical/square.hlean
View file

@ -29,50 +29,50 @@ namespace eq
definition ids [reducible] [constructor] := @square.ids definition ids [reducible] [constructor] := @square.ids
definition idsquare [reducible] [constructor] (a : A) := @square.ids A a definition idsquare [reducible] [constructor] (a : A) := @square.ids A a
definition hrefl [unfold-c 4] (p : a = a') : square idp idp p p := definition hrefl [unfold 4] (p : a = a') : square idp idp p p :=
by induction p; exact ids by induction p; exact ids
definition vrefl [unfold-c 4] (p : a = a') : square p p idp idp := definition vrefl [unfold 4] (p : a = a') : square p p idp idp :=
by induction p; exact ids by induction p; exact ids
definition hrfl [unfold-c 4] {p : a = a'} : square idp idp p p := definition hrfl [unfold 4] {p : a = a'} : square idp idp p p :=
!hrefl !hrefl
definition vrfl [unfold-c 4] {p : a = a'} : square p p idp idp := definition vrfl [unfold 4] {p : a = a'} : square p p idp idp :=
!vrefl !vrefl
definition hdeg_square [unfold-c 6] {p q : a = a'} (r : p = q) : square idp idp p q := definition hdeg_square [unfold 6] {p q : a = a'} (r : p = q) : square idp idp p q :=
by induction r;apply hrefl by induction r;apply hrefl
definition vdeg_square [unfold-c 6] {p q : a = a'} (r : p = q) : square p q idp idp := definition vdeg_square [unfold 6] {p q : a = a'} (r : p = q) : square p q idp idp :=
by induction r;apply vrefl by induction r;apply vrefl
definition hconcat [unfold-c 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁) definition hconcat [unfold 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁)
: square (p₁₀ ⬝ p₃₀) (p₁₂ ⬝ p₃₂) p₀₁ p₄₁ := : square (p₁₀ ⬝ p₃₀) (p₁₂ ⬝ p₃₂) p₀₁ p₄₁ :=
by induction s₃₁; exact s₁₁ by induction s₃₁; exact s₁₁
definition vconcat [unfold-c 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃) definition vconcat [unfold 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃)
: square p₁₀ p₁₄ (p₀₁ ⬝ p₀₃) (p₂₁ ⬝ p₂₃) := : square p₁₀ p₁₄ (p₀₁ ⬝ p₀₃) (p₂₁ ⬝ p₂₃) :=
by induction s₁₃; exact s₁₁ by induction s₁₃; exact s₁₁
definition hinverse [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₁₂⁻¹ p₂₁ p₀₁ := definition hinverse [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₁₂⁻¹ p₂₁ p₀₁ :=
by induction s₁₁;exact ids by induction s₁₁;exact ids
definition vinverse [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₂ p₁₀ p₀₁⁻¹ p₂₁⁻¹ := definition vinverse [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₂ p₁₀ p₀₁⁻¹ p₂₁⁻¹ :=
by induction s₁₁;exact ids by induction s₁₁;exact ids
definition eq_vconcat [unfold-c 11] {p : a₀₀ = a₂₀} (r : p = p₁₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : definition eq_vconcat [unfold 11] {p : a₀₀ = a₂₀} (r : p = p₁₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) :
square p p₁₂ p₀₁ p₂₁ := square p p₁₂ p₀₁ p₂₁ :=
by induction r; exact s₁₁ by induction r; exact s₁₁
definition vconcat_eq [unfold-c 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) : definition vconcat_eq [unfold 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) :
square p₁₀ p p₀₁ p₂₁ := square p₁₀ p p₀₁ p₂₁ :=
by induction r; exact s₁₁ by induction r; exact s₁₁
definition eq_hconcat [unfold-c 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : definition eq_hconcat [unfold 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) :
square p₁₀ p₁₂ p p₂₁ := square p₁₀ p₁₂ p p₂₁ :=
by induction r; exact s₁₁ by induction r; exact s₁₁
definition hconcat_eq [unfold-c 11] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) : definition hconcat_eq [unfold 11] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) :
square p₁₀ p₁₂ p₀₁ p := square p₁₀ p₁₂ p₀₁ p :=
by induction r; exact s₁₁ by induction r; exact s₁₁
@ -86,18 +86,18 @@ namespace eq
postfix `⁻¹ʰ`:(max+1) := hinverse postfix `⁻¹ʰ`:(max+1) := hinverse
postfix `⁻¹ᵛ`:(max+1) := vinverse postfix `⁻¹ᵛ`:(max+1) := vinverse
definition transpose [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ := definition transpose [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ :=
by induction s₁₁;exact ids by induction s₁₁;exact ids
definition aps {B : Type} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) definition aps {B : Type} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
: square (ap f p₁₀) (ap f p₁₂) (ap f p₀₁) (ap f p₂₁) := : square (ap f p₁₀) (ap f p₁₂) (ap f p₀₁) (ap f p₂₁) :=
by induction s₁₁;exact ids by induction s₁₁;exact ids
definition natural_square [unfold-c 8] {f g : A → B} (p : f ~ g) (q : a = a') : definition natural_square [unfold 8] {f g : A → B} (p : f ~ g) (q : a = a') :
square (ap f q) (ap g q) (p a) (p a') := square (ap f q) (ap g q) (p a) (p a') :=
eq.rec_on q hrfl eq.rec_on q hrfl
definition natural_square_tr [unfold-c 8] {f g : A → B} (p : f ~ g) (q : a = a') : definition natural_square_tr [unfold 8] {f g : A → B} (p : f ~ g) (q : a = a') :
square (p a) (p a') (ap f q) (ap g q) := square (p a) (p a') (ap f q) (ap g q) :=
eq.rec_on q vrfl eq.rec_on q vrfl
@ -121,13 +121,13 @@ namespace eq
/- equivalences -/ /- equivalences -/
definition eq_of_square [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂ := definition eq_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂ :=
by induction s₁₁; apply idp by induction s₁₁; apply idp
definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ := definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ :=
by induction p₁₂; esimp [concat] at r; induction r; induction p₂₁; induction p₁₀; exact ids by induction p₁₂; esimp [concat] at r; induction r; induction p₂₁; induction p₁₀; exact ids
definition eq_top_of_square [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) definition eq_top_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
: p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹ := : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹ :=
by induction s₁₁; apply idp by induction s₁₁; apply idp
@ -186,11 +186,11 @@ namespace eq
-- example (p q : a = a') : to_inv (hdeg_square_equiv' p q) = hdeg_square := idp -- this fails -- example (p q : a = a') : to_inv (hdeg_square_equiv' p q) = hdeg_square := idp -- this fails
example (p q : a = a') : to_inv (hdeg_square_equiv p q) = hdeg_square := idp example (p q : a = a') : to_inv (hdeg_square_equiv p q) = hdeg_square := idp
definition pathover_eq [unfold-c 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} definition pathover_eq [unfold 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'}
(s : square q r (ap f p) (ap g p)) : q =[p] r := (s : square q r (ap f p) (ap g p)) : q =[p] r :=
by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s
definition square_of_pathover [unfold-c 7] definition square_of_pathover [unfold 7]
{f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'}
(s : q =[p] r) : square q r (ap f p) (ap g p) := (s : q =[p] r) : square q r (ap f p) (ap g p) :=
by induction p;apply vdeg_square;exact eq_of_pathover_idp s by induction p;apply vdeg_square;exact eq_of_pathover_idp s
@ -253,15 +253,15 @@ namespace eq
by induction s₁₁; induction r;reflexivity by induction s₁₁; induction r;reflexivity
-- definition vconcat_eq [unfold-c 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) : -- definition vconcat_eq [unfold 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) :
-- square p₁₀ p p₀₁ p₂₁ := -- square p₁₀ p p₀₁ p₂₁ :=
-- by induction r; exact s₁₁ -- by induction r; exact s₁₁
-- definition eq_hconcat [unfold-c 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) -- definition eq_hconcat [unfold 11] {p : a₀₀ = a₀₂} (r : p = p₀₁)
-- (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀ p₁₂ p p₂₁ := -- (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀ p₁₂ p p₂₁ :=
-- by induction r; exact s₁₁ -- by induction r; exact s₁₁
-- definition hconcat_eq [unfold-c 11] {p : a₂₀ = a₂₂} -- definition hconcat_eq [unfold 11] {p : a₂₀ = a₂₂}
-- (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) : square p₁₀ p₁₂ p₀₁ p := -- (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) : square p₁₀ p₁₂ p₀₁ p :=
-- by induction r; exact s₁₁ -- by induction r; exact s₁₁

2
hott/types/eq.hlean
View file

@ -90,7 +90,7 @@ namespace eq
theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q := theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q :=
by cases q;reflexivity by cases q;reflexivity
definition ap_weakly_constant [unfold-c 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b) definition ap_weakly_constant [unfold 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b)
{x y : A} (q : x = y) : ap f q = p x ⬝ (p y)⁻¹ := {x y : A} (q : x = y) : ap f q = p x ⬝ (p y)⁻¹ :=
by induction q;exact !con.right_inv⁻¹ by induction q;exact !con.right_inv⁻¹

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

@ -797,7 +797,7 @@ definition pred_nat_succ (n : ℕ) : pred (nat.succ n) = n := pred_succ n
definition neg_nat_succ (n : ℕ) : -nat.succ n = pred (-n) := !neg_succ definition neg_nat_succ (n : ℕ) : -nat.succ n = pred (-n) := !neg_succ
definition succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ definition succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ
definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) definition rec_nat_on [unfold 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0)
(Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z := (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z :=
begin begin
induction z with n n, induction z with n n,

8
hott/types/pointed.hlean
View file

@ -22,7 +22,7 @@ namespace pointed
attribute Pointed.carrier [coercion] attribute Pointed.carrier [coercion]
variables {A B : Type} variables {A B : Type}
definition pt [unfold-c 2] [H : pointed A] := point A definition pt [unfold 2] [H : pointed A] := point A
protected abbreviation Mk [constructor] := @Pointed.mk protected abbreviation Mk [constructor] := @Pointed.mk
protected definition mk' [constructor] (A : Type) [H : pointed A] : Pointed := protected definition mk' [constructor] (A : Type) [H : pointed A] : Pointed :=
Pointed.mk (point A) Pointed.mk (point A)
@ -100,7 +100,7 @@ open pmap
namespace pointed namespace pointed
abbreviation respect_pt [unfold-c 3] := @pmap.resp_pt abbreviation respect_pt [unfold 3] := @pmap.resp_pt
notation `map₊` := pmap notation `map₊` := pmap
infix `→*`:30 := pmap infix `→*`:30 := pmap
attribute pmap.map [coercion] attribute pmap.map [coercion]
@ -129,8 +129,8 @@ namespace pointed
(homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f) (homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f)
infix `~*`:50 := phomotopy infix `~*`:50 := phomotopy
abbreviation to_homotopy_pt [unfold-c 5] := @phomotopy.homotopy_pt abbreviation to_homotopy_pt [unfold 5] := @phomotopy.homotopy_pt
abbreviation to_homotopy [coercion] [unfold-c 5] (p : f ~* g) : Πa, f a = g a := abbreviation to_homotopy [coercion] [unfold 5] (p : f ~* g) : Πa, f a = g a :=
phomotopy.homotopy p phomotopy.homotopy p
definition passoc (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) := definition passoc (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) :=

2
hott/types/sigma.hlean
View file

@ -196,7 +196,7 @@ namespace sigma
/- Functorial action -/ /- Functorial action -/
variables (f : A → A') (g : Πa, B a → B' (f a)) variables (f : A → A') (g : Πa, B a → B' (f a))
definition sigma_functor [unfold-c 7] (u : Σa, B a) : Σa', B' a' := definition sigma_functor [unfold 7] (u : Σa, B a) : Σa', B' a' :=
⟨f u.1, g u.1 u.2⟩ ⟨f u.1, g u.1 u.2⟩
/- Equivalences -/ /- Equivalences -/

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

@ -664,7 +664,7 @@ theorem pred_nat_succ (n : ℕ) : pred (nat.succ n) = n := pred_succ n
theorem neg_nat_succ (n : ℕ) : -nat.succ n = pred (-n) := !neg_succ theorem neg_nat_succ (n : ℕ) : -nat.succ n = pred (-n) := !neg_succ
theorem succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ theorem succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ
definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) definition rec_nat_on [unfold 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0)
(Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z := (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z :=
begin begin
induction z with n n, induction z with n n,

2
library/data/stream.lean
View file

@ -282,7 +282,7 @@ definition unfolds (g : A → B) (f : A → A) (a : A) : stream B :=
corec g f a corec g f a
theorem unfolds_eq (g : A → B) (f : A → A) (a : A) : unfolds g f a = g a :: unfolds g f (f a) := theorem unfolds_eq (g : A → B) (f : A → A) (a : A) : unfolds g f a = g a :: unfolds g f (f a) :=
by esimp [unfolds]; rewrite [corec_eq] by esimp [ unfolds ]; rewrite [corec_eq]
theorem nth_unfolds_head_tail : ∀ (n : nat) (s : stream A), nth n (unfolds head tail s) = nth n s := theorem nth_unfolds_head_tail : ∀ (n : nat) (s : stream A), nth n (unfolds head tail s) = nth n s :=
begin begin

4
library/init/datatypes.lean
View file

@ -38,10 +38,10 @@ refl : heq a a
inductive prod (A B : Type) := inductive prod (A B : Type) :=
mk : A → B → prod A B mk : A → B → prod A B
definition prod.pr1 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : A := definition prod.pr1 [reducible] [unfold 3] {A B : Type} (p : prod A B) : A :=
prod.rec (λ a b, a) p prod.rec (λ a b, a) p
definition prod.pr2 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : B := definition prod.pr2 [reducible] [unfold 3] {A B : Type} (p : prod A B) : B :=
prod.rec (λ a b, b) p prod.rec (λ a b, b) p
inductive and (a b : Prop) : Prop := inductive and (a b : Prop) : Prop :=

22
library/init/function.lean
View file

@ -12,42 +12,42 @@ namespace function
variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type} variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
definition compose [reducible] [unfold-f] (f : B → C) (g : A → B) : A → C := definition compose [reducible] [unfold-full] (f : B → C) (g : A → B) : A → C :=
λx, f (g x) λx, f (g x)
definition compose_right [reducible] [unfold-f] (f : B → B → B) (g : A → B) : B → A → B := definition compose_right [reducible] [unfold-full] (f : B → B → B) (g : A → B) : B → A → B :=
λ b a, f b (g a) λ b a, f b (g a)
definition compose_left [reducible] [unfold-f] (f : B → B → B) (g : A → B) : A → B → B := definition compose_left [reducible] [unfold-full] (f : B → B → B) (g : A → B) : A → B → B :=
λ a b, f (g a) b λ a b, f (g a) b
definition id [reducible] [unfold-f] (a : A) : A := definition id [reducible] [unfold-full] (a : A) : A :=
a a
definition on_fun [reducible] [unfold-f] (f : B → B → C) (g : A → B) : A → A → C := definition on_fun [reducible] [unfold-full] (f : B → B → C) (g : A → B) : A → A → C :=
λx y, f (g x) (g y) λx y, f (g x) (g y)
definition combine [reducible] [unfold-f] (f : A → B → C) (op : C → D → E) (g : A → B → D) definition combine [reducible] [unfold-full] (f : A → B → C) (op : C → D → E) (g : A → B → D)
: A → B → E := : A → B → E :=
λx y, op (f x y) (g x y) λx y, op (f x y) (g x y)
definition const [reducible] [unfold-f] (B : Type) (a : A) : B → A := definition const [reducible] [unfold-full] (B : Type) (a : A) : B → A :=
λx, a λx, a
definition dcompose [reducible] [unfold-f] {B : A → Type} {C : Π {x : A}, B x → Type} definition dcompose [reducible] [unfold-full] {B : A → Type} {C : Π {x : A}, B x → Type}
(f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) := (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
λx, f (g x) λx, f (g x)
definition swap [reducible] [unfold-f] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := definition swap [reducible] [unfold-full] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
λy x, f x y λy x, f x y
definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x := definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
f x f x
definition curry [reducible] [unfold-f] : (A × B → C) → A → B → C := definition curry [reducible] [unfold-full] : (A × B → C) → A → B → C :=
λ f a b, f (a, b) λ f a b, f (a, b)
definition uncurry [reducible] [unfold-c 5] : (A → B → C) → (A × B → C) := definition uncurry [reducible] [unfold 5] : (A → B → C) → (A × B → C) :=
λ f p, match p with (a, b) := f a b end λ f p, match p with (a, b) := f a b end
theorem curry_uncurry (f : A → B → C) : curry (uncurry f) = f := theorem curry_uncurry (f : A → B → C) : curry (uncurry f) = f :=

2
library/init/nat.lean
View file

@ -25,7 +25,7 @@ namespace nat
infix `≥` := ge infix `≥` := ge
infix `>` := gt infix `>` := gt
definition pred [unfold-c 1] (a : nat) : nat := definition pred [unfold 1] (a : nat) : nat :=
nat.cases_on a zero (λ a₁, a₁) nat.cases_on a zero (λ a₁, a₁)
-- add is defined in init.num -- add is defined in init.num

18
library/init/quot.lean
View file

@ -164,15 +164,15 @@ namespace quot
end quot end quot
attribute quot.mk [constructor] attribute quot.mk [constructor]
attribute quot.lift_on [unfold-c 4] attribute quot.lift_on [unfold 4]
attribute quot.rec [unfold-c 6] attribute quot.rec [unfold 6]
attribute quot.rec_on [unfold-c 4] attribute quot.rec_on [unfold 4]
attribute quot.hrec_on [unfold-c 4] attribute quot.hrec_on [unfold 4]
attribute quot.rec_on_subsingleton [unfold-c 5] attribute quot.rec_on_subsingleton [unfold 5]
attribute quot.lift₂ [unfold-c 8] attribute quot.lift₂ [unfold 8]
attribute quot.lift_on₂ [unfold-c 6] attribute quot.lift_on₂ [unfold 6]
attribute quot.hrec_on₂ [unfold-c 6] attribute quot.hrec_on₂ [unfold 6]
attribute quot.rec_on_subsingleton₂ [unfold-c 7] attribute quot.rec_on_subsingleton₂ [unfold 7]
open decidable open decidable
definition quot.has_decidable_eq [instance] {A : Type} {s : setoid A} [decR : ∀ a b : A, decidable (a ≈ b)] : decidable_eq (quot s) := definition quot.has_decidable_eq [instance] {A : Type} {s : setoid A} [decR : ∀ a b : A, decidable (a ≈ b)] : decidable_eq (quot s) :=

4
src/emacs/lean-syntax.el
View file

@ -119,7 +119,7 @@
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; modifiers ;; modifiers
(,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[trans-instance\]" "\[class\]" "\[parsing-only\]" (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[trans-instance\]" "\[class\]" "\[parsing-only\]"
"\[coercion\]" "\[unfold-f\]" "\[constructor\]" "\[reducible\]" "\[coercion\]" "\[unfold-full\]" "\[constructor\]" "\[reducible\]"
"\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]" "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]"
"\[whnf\]" "\[multiple-instances\]" "\[none\]" "\[whnf\]" "\[multiple-instances\]" "\[none\]"
"\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]" "\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]"
@ -129,7 +129,7 @@
. 'font-lock-doc-face) . 'font-lock-doc-face)
(,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
(,(rx "\[recursor" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) (,(rx "\[recursor" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
(,(rx "\[unfold-c" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) (,(rx "\[unfold" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
;; tactics ;; tactics
("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face)) ("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face))
(,(rx (not (any "\.")) word-start (,(rx (not (any "\.")) word-start

13
src/frontends/lean/builtin_cmds.cpp
View file

@ -670,6 +670,10 @@ environment set_option_cmd(parser & p) {
return update_fingerprint(env, p.get_options().hash()); return update_fingerprint(env, p.get_options().hash());
} }
static bool is_next_metaclass_tk(parser const & p) {
return p.curr_is_token(get_lbracket_tk()) || p.curr_is_token(get_unfold_hints_bracket_tk());
}
static name parse_metaclass(parser & p) { static name parse_metaclass(parser & p) {
if (p.curr_is_token(get_lbracket_tk())) { if (p.curr_is_token(get_lbracket_tk())) {
p.next(); p.next();
@ -690,6 +694,9 @@ static name parse_metaclass(parser & p) {
if (!is_metaclass(n) && n != get_decls_tk() && n != get_declarations_tk()) if (!is_metaclass(n) && n != get_decls_tk() && n != get_declarations_tk())
throw parser_error(sstream() << "invalid metaclass name '[" << n << "]'", pos); throw parser_error(sstream() << "invalid metaclass name '[" << n << "]'", pos);
return n; return n;
} else if (p.curr_is_token(get_unfold_hints_bracket_tk())) {
p.next();
return get_unfold_hints_tk();
} else { } else {
return name(); return name();
} }
@ -701,7 +708,7 @@ static void parse_metaclasses(parser & p, buffer<name> & r) {
buffer<name> tmp; buffer<name> tmp;
get_metaclasses(tmp); get_metaclasses(tmp);
tmp.push_back(get_decls_tk()); tmp.push_back(get_decls_tk());
while (p.curr_is_token(get_lbracket_tk())) { while (is_next_metaclass_tk(p)) {
name m = parse_metaclass(p); name m = parse_metaclass(p);
tmp.erase_elem(m); tmp.erase_elem(m);
if (m == get_declarations_tk()) if (m == get_declarations_tk())
@ -709,7 +716,7 @@ static void parse_metaclasses(parser & p, buffer<name> & r) {
} }
r.append(tmp); r.append(tmp);
} else { } else {
while (p.curr_is_token(get_lbracket_tk())) { while (is_next_metaclass_tk(p)) {
r.push_back(parse_metaclass(p)); r.push_back(parse_metaclass(p));
} }
} }
@ -837,7 +844,7 @@ environment open_export_cmd(parser & p, bool open) {
} }
} }
} }
if (!p.curr_is_token(get_lbracket_tk()) && !p.curr_is_identifier()) if (!is_next_metaclass_tk(p) && !p.curr_is_identifier())
break; break;
} }
return update_fingerprint(env, fingerprint); return update_fingerprint(env, fingerprint);

30
src/frontends/lean/decl_attributes.cpp
View file

@ -32,7 +32,7 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
m_is_class = false; m_is_class = false;
m_is_parsing_only = false; m_is_parsing_only = false;
m_has_multiple_instances = false; m_has_multiple_instances = false;
m_unfold_f_hint = false; m_unfold_full_hint = false;
m_constructor_hint = false; m_constructor_hint = false;
m_symm = false; m_symm = false;
m_trans = false; m_trans = false;
@ -104,19 +104,19 @@ void decl_attributes::parse(buffer<name> const & ns, parser & p) {
"marked as '[parsing-only]'", pos); "marked as '[parsing-only]'", pos);
m_is_parsing_only = true; m_is_parsing_only = true;
p.next(); p.next();
} else if (p.curr_is_token(get_unfold_f_tk())) { } else if (p.curr_is_token(get_unfold_full_tk())) {
p.next(); p.next();
m_unfold_f_hint = true; m_unfold_full_hint = true;
} else if (p.curr_is_token(get_constructor_tk())) { } else if (p.curr_is_token(get_constructor_tk())) {
p.next(); p.next();
m_constructor_hint = true; m_constructor_hint = true;
} else if (p.curr_is_token(get_unfold_c_tk())) { } else if (p.curr_is_token(get_unfold_tk())) {
p.next(); p.next();
unsigned r = p.parse_small_nat(); unsigned r = p.parse_small_nat();
if (r == 0) if (r == 0)
throw parser_error("invalid '[unfold-c]' attribute, value must be greater than 0", pos); throw parser_error("invalid '[unfold]' attribute, value must be greater than 0", pos);
m_unfold_c_hint = r - 1; m_unfold_hint = r - 1;
p.check_token_next(get_rbracket_tk(), "invalid 'unfold-c', ']' expected"); p.check_token_next(get_rbracket_tk(), "invalid 'unfold', ']' expected");
} else if (p.curr_is_token(get_symm_tk())) { } else if (p.curr_is_token(get_symm_tk())) {
p.next(); p.next();
m_symm = true; m_symm = true;
@ -192,10 +192,10 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
env = set_reducible(env, d, reducible_status::Semireducible, m_persistent); env = set_reducible(env, d, reducible_status::Semireducible, m_persistent);
if (m_is_quasireducible) if (m_is_quasireducible)
env = set_reducible(env, d, reducible_status::Quasireducible, m_persistent); env = set_reducible(env, d, reducible_status::Quasireducible, m_persistent);
if (m_unfold_c_hint) if (m_unfold_hint)
env = add_unfold_c_hint(env, d, *m_unfold_c_hint, m_persistent); env = add_unfold_hint(env, d, *m_unfold_hint, m_persistent);
if (m_unfold_f_hint) if (m_unfold_full_hint)
env = add_unfold_f_hint(env, d, m_persistent); env = add_unfold_full_hint(env, d, m_persistent);
} }
if (m_constructor_hint) if (m_constructor_hint)
env = add_constructor_hint(env, d, m_persistent); env = add_constructor_hint(env, d, m_persistent);
@ -221,16 +221,16 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
void decl_attributes::write(serializer & s) const { void decl_attributes::write(serializer & s) const {
s << m_is_abbrev << m_persistent << m_is_instance << m_is_trans_instance << m_is_coercion s << m_is_abbrev << m_persistent << m_is_instance << m_is_trans_instance << m_is_coercion
<< m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible << m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible
<< m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_f_hint << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_full_hint
<< m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor << m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor
<< m_rewrite << m_recursor_major_pos << m_priority << m_unfold_c_hint; << m_rewrite << m_recursor_major_pos << m_priority << m_unfold_hint;
} }
void decl_attributes::read(deserializer & d) { void decl_attributes::read(deserializer & d) {
d >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_trans_instance >> m_is_coercion d >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_trans_instance >> m_is_coercion
>> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible >> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible
>> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_f_hint >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_full_hint
>> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor >> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor
>> m_rewrite >> m_recursor_major_pos >> m_priority >> m_unfold_c_hint; >> m_rewrite >> m_recursor_major_pos >> m_priority >> m_unfold_hint;
} }
} }

4
src/frontends/lean/decl_attributes.h
View file

@ -22,7 +22,7 @@ class decl_attributes {
bool m_is_class; bool m_is_class;
bool m_is_parsing_only; bool m_is_parsing_only;
bool m_has_multiple_instances; bool m_has_multiple_instances;
bool m_unfold_f_hint; bool m_unfold_full_hint;
bool m_constructor_hint; bool m_constructor_hint;
bool m_symm; bool m_symm;
bool m_trans; bool m_trans;
@ -32,7 +32,7 @@ class decl_attributes {
bool m_rewrite; bool m_rewrite;
optional<unsigned> m_recursor_major_pos; optional<unsigned> m_recursor_major_pos;
optional<unsigned> m_priority; optional<unsigned> m_priority;
optional<unsigned> m_unfold_c_hint; optional<unsigned> m_unfold_hint;
void parse(name const & n, parser & p); void parse(name const & n, parser & p);
public: public:

4
src/frontends/lean/structure_cmd.cpp
View file

@ -724,8 +724,8 @@ struct structure_cmd_fn {
rec_on_decl.get_type(), rec_on_decl.get_value()); rec_on_decl.get_type(), rec_on_decl.get_value());
m_env = module::add(m_env, check(m_env, new_decl)); m_env = module::add(m_env, check(m_env, new_decl));
m_env = set_reducible(m_env, n, reducible_status::Reducible); m_env = set_reducible(m_env, n, reducible_status::Reducible);
if (optional<unsigned> idx = has_unfold_c_hint(m_env, rec_on_name)) if (optional<unsigned> idx = has_unfold_hint(m_env, rec_on_name))
m_env = add_unfold_c_hint(m_env, n, *idx); m_env = add_unfold_hint(m_env, n, *idx);
save_def_info(n); save_def_info(n);
add_alias(n); add_alias(n);
} }

4
src/frontends/lean/token_table.cpp
View file

@ -109,8 +109,8 @@ void init_token_table(token_table & t) {
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[trans-instance]", "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[trans-instance]",
"[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
"[rewrite]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor", "[rewrite]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-f]", "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-full]", "[unfold-hints]",
"[constructor]", "[unfold-c", "print", "[constructor]", "[unfold", "print",
"end", "namespace", "section", "prelude", "help", "end", "namespace", "section", "prelude", "help",
"import", "inductive", "record", "structure", "module", "universe", "universes", "local", "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",

24
src/frontends/lean/tokens.cpp
View file

@ -99,8 +99,10 @@ static name const * g_variables_tk = nullptr;
static name const * g_instance_tk = nullptr; static name const * g_instance_tk = nullptr;
static name const * g_trans_inst_tk = nullptr; static name const * g_trans_inst_tk = nullptr;
static name const * g_priority_tk = nullptr; static name const * g_priority_tk = nullptr;
static name const * g_unfold_c_tk = nullptr; static name const * g_unfold_tk = nullptr;
static name const * g_unfold_f_tk = nullptr; static name const * g_unfold_full_tk = nullptr;
static name const * g_unfold_hints_bracket_tk = nullptr;
static name const * g_unfold_hints_tk = nullptr;
static name const * g_constructor_tk = nullptr; static name const * g_constructor_tk = nullptr;
static name const * g_coercion_tk = nullptr; static name const * g_coercion_tk = nullptr;
static name const * g_reducible_tk = nullptr; static name const * g_reducible_tk = nullptr;
@ -236,8 +238,10 @@ void initialize_tokens() {
g_instance_tk = new name{"[instance]"}; g_instance_tk = new name{"[instance]"};
g_trans_inst_tk = new name{"[trans-instance]"}; g_trans_inst_tk = new name{"[trans-instance]"};
g_priority_tk = new name{"[priority"}; g_priority_tk = new name{"[priority"};
g_unfold_c_tk = new name{"[unfold-c"}; g_unfold_tk = new name{"[unfold"};
g_unfold_f_tk = new name{"[unfold-f]"}; g_unfold_full_tk = new name{"[unfold-full]"};
g_unfold_hints_bracket_tk = new name{"[unfold-hints]"};
g_unfold_hints_tk = new name{"unfold-hints"};
g_constructor_tk = new name{"[constructor]"}; g_constructor_tk = new name{"[constructor]"};
g_coercion_tk = new name{"[coercion]"}; g_coercion_tk = new name{"[coercion]"};
g_reducible_tk = new name{"[reducible]"}; g_reducible_tk = new name{"[reducible]"};
@ -374,8 +378,10 @@ void finalize_tokens() {
delete g_instance_tk; delete g_instance_tk;
delete g_trans_inst_tk; delete g_trans_inst_tk;
delete g_priority_tk; delete g_priority_tk;
delete g_unfold_c_tk; delete g_unfold_tk;
delete g_unfold_f_tk; delete g_unfold_full_tk;
delete g_unfold_hints_bracket_tk;
delete g_unfold_hints_tk;
delete g_constructor_tk; delete g_constructor_tk;
delete g_coercion_tk; delete g_coercion_tk;
delete g_reducible_tk; delete g_reducible_tk;
@ -511,8 +517,10 @@ name const & get_variables_tk() { return *g_variables_tk; }
name const & get_instance_tk() { return *g_instance_tk; } name const & get_instance_tk() { return *g_instance_tk; }
name const & get_trans_inst_tk() { return *g_trans_inst_tk; } name const & get_trans_inst_tk() { return *g_trans_inst_tk; }
name const & get_priority_tk() { return *g_priority_tk; } name const & get_priority_tk() { return *g_priority_tk; }
name const & get_unfold_c_tk() { return *g_unfold_c_tk; } name const & get_unfold_tk() { return *g_unfold_tk; }
name const & get_unfold_f_tk() { return *g_unfold_f_tk; } name const & get_unfold_full_tk() { return *g_unfold_full_tk; }
name const & get_unfold_hints_bracket_tk() { return *g_unfold_hints_bracket_tk; }
name const & get_unfold_hints_tk() { return *g_unfold_hints_tk; }
name const & get_constructor_tk() { return *g_constructor_tk; } name const & get_constructor_tk() { return *g_constructor_tk; }
name const & get_coercion_tk() { return *g_coercion_tk; } name const & get_coercion_tk() { return *g_coercion_tk; }
name const & get_reducible_tk() { return *g_reducible_tk; } name const & get_reducible_tk() { return *g_reducible_tk; }

6
src/frontends/lean/tokens.h
View file

@ -101,8 +101,10 @@ name const & get_variables_tk();
name const & get_instance_tk(); name const & get_instance_tk();
name const & get_trans_inst_tk(); name const & get_trans_inst_tk();
name const & get_priority_tk(); name const & get_priority_tk();
name const & get_unfold_c_tk(); name const & get_unfold_tk();
name const & get_unfold_f_tk(); name const & get_unfold_full_tk();
name const & get_unfold_hints_bracket_tk();
name const & get_unfold_hints_tk();
name const & get_constructor_tk(); name const & get_constructor_tk();
name const & get_coercion_tk(); name const & get_coercion_tk();
name const & get_reducible_tk(); name const & get_reducible_tk();

6
src/frontends/lean/tokens.txt
View file

@ -94,8 +94,10 @@ variables variables
instance [instance] instance [instance]
trans_inst [trans-instance] trans_inst [trans-instance]
priority [priority priority [priority
unfold_c [unfold-c unfold [unfold
unfold_f [unfold-f] unfold_full [unfold-full]
unfold_hints_bracket [unfold-hints]
unfold_hints unfold-hints
constructor [constructor] constructor [constructor]
coercion [coercion] coercion [coercion]
reducible [reducible] reducible [reducible]

4
src/library/definitional/brec_on.cpp
View file

@ -147,7 +147,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
environment new_env = module::add(env, check(env, new_d)); environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, below_name, reducible_status::Reducible); new_env = set_reducible(new_env, below_name, reducible_status::Reducible);
if (!ibelow) if (!ibelow)
new_env = add_unfold_c_hint(new_env, below_name, nparams + nindices + ntypeformers); new_env = add_unfold_hint(new_env, below_name, nparams + nindices + ntypeformers);
return add_protected(new_env, below_name); return add_protected(new_env, below_name);
} }
@ -333,7 +333,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
environment new_env = module::add(env, check(env, new_d)); environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible); new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible);
if (!ind) if (!ind)
new_env = add_unfold_c_hint(new_env, brec_on_name, nparams + nindices + ntypeformers); new_env = add_unfold_hint(new_env, brec_on_name, nparams + nindices + ntypeformers);
return add_protected(new_env, brec_on_name); return add_protected(new_env, brec_on_name);
} }

2
src/library/definitional/cases_on.cpp
View file

@ -182,7 +182,7 @@ environment mk_cases_on(environment const & env, name const & n) {
use_conv_opt); use_conv_opt);
environment new_env = module::add(env, check(env, new_d)); environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible); new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, cases_on_name, cases_on_major_idx); new_env = add_unfold_hint(new_env, cases_on_name, cases_on_major_idx);
return add_protected(new_env, cases_on_name); return add_protected(new_env, cases_on_name);
} }
} }

2
src/library/definitional/projection.cpp
View file

@ -258,7 +258,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
use_conv_opt); use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d)); new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, proj_name, reducible_status::Reducible); new_env = set_reducible(new_env, proj_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, proj_name, nparams); new_env = add_unfold_hint(new_env, proj_name, nparams);
new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit); new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit);
expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
intro_type = instantiate(binding_body(intro_type), proj); intro_type = instantiate(binding_body(intro_type), proj);

2
src/library/definitional/rec_on.cpp
View file

@ -58,7 +58,7 @@ environment mk_rec_on(environment const & env, name const & n) {
check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(), check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(),
rec_on_type, rec_on_val, use_conv_opt))); rec_on_type, rec_on_val, use_conv_opt)));
new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible); new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, rec_on_name, rec_on_major_idx); new_env = add_unfold_hint(new_env, rec_on_name, rec_on_major_idx);
return add_protected(new_env, rec_on_name); return add_protected(new_env, rec_on_name);
} }
} }

78
src/library/normalize.cpp
View file

@ -23,35 +23,35 @@ namespace lean {
/** /**
\brief unfold hints instruct the normalizer (and simplifier) that \brief unfold hints instruct the normalizer (and simplifier) that
a function application. We have two kinds of hints: a function application. We have two kinds of hints:
- unfold_c (f a_1 ... a_i ... a_n) should be unfolded - [unfold] (f a_1 ... a_i ... a_n) should be unfolded
when argument a_i is a constructor. when argument a_i is a constructor.
- unfold_f (f a_1 ... a_i ... a_n) should be unfolded when it is fully applied. - [unfold-full] (f a_1 ... a_i ... a_n) should be unfolded when it is fully applied.
- constructor (f ...) should be unfolded when it is the major premise of a recursor-like operator - constructor (f ...) should be unfolded when it is the major premise of a recursor-like operator
*/ */
struct unfold_hint_entry { struct unfold_hint_entry {
enum kind {UnfoldC, UnfoldF, UnfoldM}; enum kind {Unfold, UnfoldFull, Constructor};
kind m_kind; //!< true if it is an unfold_c hint kind m_kind; //!< true if it is an unfold_c hint
bool m_add; //!< add/remove hint bool m_add; //!< add/remove hint
name m_decl_name; name m_decl_name;
unsigned m_arg_idx; unsigned m_arg_idx;
unfold_hint_entry():m_kind(UnfoldC), m_add(false), m_arg_idx(0) {} unfold_hint_entry():m_kind(Unfold), m_add(false), m_arg_idx(0) {}
unfold_hint_entry(kind k, bool add, name const & n, unsigned idx): unfold_hint_entry(kind k, bool add, name const & n, unsigned idx):
m_kind(k), m_add(add), m_decl_name(n), m_arg_idx(idx) {} m_kind(k), m_add(add), m_decl_name(n), m_arg_idx(idx) {}
}; };
unfold_hint_entry mk_add_unfold_c_entry(name const & n, unsigned idx) { return unfold_hint_entry(unfold_hint_entry::UnfoldC, true, n, idx); } unfold_hint_entry mk_add_unfold_entry(name const & n, unsigned idx) { return unfold_hint_entry(unfold_hint_entry::Unfold, true, n, idx); }
unfold_hint_entry mk_erase_unfold_c_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldC, false, n, 0); } unfold_hint_entry mk_erase_unfold_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::Unfold, false, n, 0); }
unfold_hint_entry mk_add_unfold_f_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldF, true, n, 0); } unfold_hint_entry mk_add_unfold_full_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldFull, true, n, 0); }
unfold_hint_entry mk_erase_unfold_f_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldF, false, n, 0); } unfold_hint_entry mk_erase_unfold_full_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldFull, false, n, 0); }
unfold_hint_entry mk_add_constructor_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldM, true, n, 0); } unfold_hint_entry mk_add_constructor_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::Constructor, true, n, 0); }
unfold_hint_entry mk_erase_constructor_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldM, false, n, 0); } unfold_hint_entry mk_erase_constructor_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::Constructor, false, n, 0); }
static name * g_unfold_hint_name = nullptr; static name * g_unfold_hint_name = nullptr;
static std::string * g_key = nullptr; static std::string * g_key = nullptr;
struct unfold_hint_state { struct unfold_hint_state {
name_map<unsigned> m_unfold_c; name_map<unsigned> m_unfold;
name_set m_unfold_f; name_set m_unfold_full;
name_set m_constructor; name_set m_constructor;
}; };
@ -61,19 +61,19 @@ struct unfold_hint_config {
static void add_entry(environment const &, io_state const &, state & s, entry const & e) { static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
switch (e.m_kind) { switch (e.m_kind) {
case unfold_hint_entry::UnfoldC: case unfold_hint_entry::Unfold:
if (e.m_add) if (e.m_add)
s.m_unfold_c.insert(e.m_decl_name, e.m_arg_idx); s.m_unfold.insert(e.m_decl_name, e.m_arg_idx);
else else
s.m_unfold_c.erase(e.m_decl_name); s.m_unfold.erase(e.m_decl_name);
break; break;
case unfold_hint_entry::UnfoldF: case unfold_hint_entry::UnfoldFull:
if (e.m_add) if (e.m_add)
s.m_unfold_f.insert(e.m_decl_name); s.m_unfold_full.insert(e.m_decl_name);
else else
s.m_unfold_f.erase(e.m_decl_name); s.m_unfold_full.erase(e.m_decl_name);
break; break;
case unfold_hint_entry::UnfoldM: case unfold_hint_entry::Constructor:
if (e.m_add) if (e.m_add)
s.m_constructor.insert(e.m_decl_name); s.m_constructor.insert(e.m_decl_name);
else else
@ -105,39 +105,39 @@ struct unfold_hint_config {
template class scoped_ext<unfold_hint_config>; template class scoped_ext<unfold_hint_config>;
typedef scoped_ext<unfold_hint_config> unfold_hint_ext; typedef scoped_ext<unfold_hint_config> unfold_hint_ext;
environment add_unfold_c_hint(environment const & env, name const & n, unsigned idx, bool persistent) { environment add_unfold_hint(environment const & env, name const & n, unsigned idx, bool persistent) {
declaration const & d = env.get(n); declaration const & d = env.get(n);
if (!d.is_definition()) if (!d.is_definition())
throw exception("invalid unfold-c hint, declaration must be a non-opaque definition"); throw exception("invalid [unfold] hint, declaration must be a non-opaque definition");
return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_c_entry(n, idx), persistent); return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_entry(n, idx), persistent);
} }
optional<unsigned> has_unfold_c_hint(environment const & env, name const & d) { optional<unsigned> has_unfold_hint(environment const & env, name const & d) {
unfold_hint_state const & s = unfold_hint_ext::get_state(env); unfold_hint_state const & s = unfold_hint_ext::get_state(env);
if (auto it = s.m_unfold_c.find(d)) if (auto it = s.m_unfold.find(d))
return optional<unsigned>(*it); return optional<unsigned>(*it);
else else
return optional<unsigned>(); return optional<unsigned>();
} }
environment erase_unfold_c_hint(environment const & env, name const & n, bool persistent) { environment erase_unfold_hint(environment const & env, name const & n, bool persistent) {
return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_c_entry(n), persistent); return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_entry(n), persistent);
} }
environment add_unfold_f_hint(environment const & env, name const & n, bool persistent) { environment add_unfold_full_hint(environment const & env, name const & n, bool persistent) {
declaration const & d = env.get(n); declaration const & d = env.get(n);
if (!d.is_definition()) if (!d.is_definition())
throw exception("invalid unfold-f hint, declaration must be a non-opaque definition"); throw exception("invalid [unfold-full] hint, declaration must be a non-opaque definition");
return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_f_entry(n), persistent); return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_full_entry(n), persistent);
} }
bool has_unfold_f_hint(environment const & env, name const & d) { bool has_unfold_full_hint(environment const & env, name const & d) {
unfold_hint_state const & s = unfold_hint_ext::get_state(env); unfold_hint_state const & s = unfold_hint_ext::get_state(env);
return s.m_unfold_f.contains(d); return s.m_unfold_full.contains(d);
} }
environment erase_unfold_f_hint(environment const & env, name const & n, bool persistent) { environment erase_unfold_full_hint(environment const & env, name const & n, bool persistent) {
return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_f_entry(n), persistent); return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_full_entry(n), persistent);
} }
environment add_constructor_hint(environment const & env, name const & n, bool persistent) { environment add_constructor_hint(environment const & env, name const & n, bool persistent) {
@ -246,14 +246,14 @@ class normalize_fn {
return update_binding(e, d, b); return update_binding(e, d, b);
} }
optional<unsigned> has_unfold_c_hint(expr const & f) { optional<unsigned> has_unfold_hint(expr const & f) {
if (!is_constant(f)) if (!is_constant(f))
return optional<unsigned>(); return optional<unsigned>();
return ::lean::has_unfold_c_hint(env(), const_name(f)); return ::lean::has_unfold_hint(env(), const_name(f));
} }
bool has_unfold_f_hint(expr const & f) { bool has_unfold_full_hint(expr const & f) {
return is_constant(f) && ::lean::has_unfold_f_hint(env(), const_name(f)); return is_constant(f) && ::lean::has_unfold_full_hint(env(), const_name(f));
} }
optional<expr> is_constructor_like(expr const & e) { optional<expr> is_constructor_like(expr const & e) {
@ -305,13 +305,13 @@ class normalize_fn {
modified = true; modified = true;
a = new_a; a = new_a;
} }
if (has_unfold_f_hint(f)) { if (has_unfold_full_hint(f)) {
if (!is_pi(m_tc.whnf(m_tc.infer(e).first).first)) { if (!is_pi(m_tc.whnf(m_tc.infer(e).first).first)) {
if (optional<expr> r = unfold_app(env(), mk_rev_app(f, args))) if (optional<expr> r = unfold_app(env(), mk_rev_app(f, args)))
return normalize(*r); return normalize(*r);
} }
} }
if (auto idx = has_unfold_c_hint(f)) { if (auto idx = has_unfold_hint(f)) {
if (auto r = unfold_recursor_like(f, *idx, args)) if (auto r = unfold_recursor_like(f, *idx, args))
return *r; return *r;
} }

20
src/library/normalize.h
View file

@ -32,7 +32,7 @@ expr normalize(type_checker & tc, expr const & e, constraint_seq & cs, bool eta
expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const&)> const & pred, // NOLINT expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const&)> const & pred, // NOLINT
constraint_seq & cs, bool eta = false); constraint_seq & cs, bool eta = false);
/** \brief unfold-c hint instructs the normalizer (and simplifier) that /** \brief [unfold] hint instructs the normalizer (and simplifier) that
a function application (f a_1 ... a_i ... a_n) should be unfolded a function application (f a_1 ... a_i ... a_n) should be unfolded
when argument a_i is a constructor. when argument a_i is a constructor.
@ -40,17 +40,17 @@ expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const&
Of course, kernel opaque constants are not unfolded. Of course, kernel opaque constants are not unfolded.
*/ */
environment add_unfold_c_hint(environment const & env, name const & n, unsigned idx, bool persistent = true); environment add_unfold_hint(environment const & env, name const & n, unsigned idx, bool persistent = true);
environment erase_unfold_c_hint(environment const & env, name const & n, bool persistent = true); environment erase_unfold_hint(environment const & env, name const & n, bool persistent = true);
/** \brief Retrieve the hint added with the procedure add_unfold_c_hint. */ /** \brief Retrieve the hint added with the procedure add_unfold_hint. */
optional<unsigned> has_unfold_c_hint(environment const & env, name const & d); optional<unsigned> has_unfold_hint(environment const & env, name const & d);
/** \brief unfold-f hint instructs normalizer (and simplifier) that function application /** \brief [unfold-full] hint instructs normalizer (and simplifier) that function application
(f a_1 ... a_n) should be unfolded when it is fully applied */ (f a_1 ... a_n) should be unfolded when it is fully applied */
environment add_unfold_f_hint(environment const & env, name const & n, bool persistent = true); environment add_unfold_full_hint(environment const & env, name const & n, bool persistent = true);
environment erase_unfold_f_hint(environment const & env, name const & n, bool persistent = true); environment erase_unfold_full_hint(environment const & env, name const & n, bool persistent = true);
/** \brief Retrieve the hint added with the procedure add_unfold_f_hint. */ /** \brief Retrieve the hint added with the procedure add_unfold_full_hint. */
optional<unsigned> has_unfold_f_hint(environment const & env, name const & d); optional<unsigned> has_unfold_full_hint(environment const & env, name const & d);
/** \brief unfold-m hint instructs normalizer (and simplifier) that function application /** \brief unfold-m hint instructs normalizer (and simplifier) that function application

2
tests/lean/640.hlean
View file

@ -6,7 +6,7 @@ open quotient eq sum
local abbreviation C := quotient R local abbreviation C := quotient R
definition f [unfold-c 2] (a : A) (x : unit) : C := definition f [unfold 2] (a : A) (x : unit) : C :=
!class_of a !class_of a
inductive S : C → C → Type := inductive S : C → C → Type :=

4
tests/lean/run/all_goals.lean
View file

@ -1,8 +1,8 @@
import data.nat import data.nat
open nat open nat
attribute nat.add [unfold-c 2] attribute nat.add [unfold 2]
attribute nat.rec_on [unfold-c 2] attribute nat.rec_on [unfold 2]
example (a b c : nat) : a + 0 = 0 + a ∧ b + 0 = 0 + b := example (a b c : nat) : a + 0 = 0 + a ∧ b + 0 = 0 + b :=
begin begin

4
tests/lean/run/all_goals2.lean
View file

@ -1,8 +1,8 @@
import data.nat import data.nat
open nat open nat
attribute nat.add [unfold-c 2] attribute nat.add [unfold 2]
attribute nat.rec_on [unfold-c 2] attribute nat.rec_on [unfold 2]
infixl `;`:15 := tactic.and_then infixl `;`:15 := tactic.and_then

4
tests/lean/run/rewriter14.lean
View file

@ -1,10 +1,10 @@
import data.nat import data.nat
open nat open nat
definition f [unfold-c 2] (x y z : nat) : nat := definition f [unfold 2] (x y z : nat) : nat :=
x + y + z x + y + z
attribute of_num [unfold-c 1] attribute of_num [unfold 1]
example (x y : nat) (H1 : f x 0 0 = 0) : x = 0 := example (x y : nat) (H1 : f x 0 0 = 0) : x = 0 :=
begin begin

4
tests/lean/unfoldf.lean
View file

@ -1,6 +1,6 @@
open nat open nat
definition id [unfold-f] {A : Type} (a : A) := a definition id [unfold-full] {A : Type} (a : A) := a
definition compose {A B C : Type} (g : B → C) (f : A → B) (a : A) := g (f a) definition compose {A B C : Type} (g : B → C) (f : A → B) (a : A) := g (f a)
notation g ∘ f := compose g f notation g ∘ f := compose g f
@ -18,7 +18,7 @@ begin
exact H exact H
end end
attribute compose [unfold-f] attribute compose [unfold-full]
example (a b : nat) (H : a = b) : (id ∘ id) a = b := example (a b : nat) (H : a = b) : (id ∘ id) a = b :=
begin begin