refactor(library/*): rename 'compose' to 'comp'
This commit is contained in:
Jeremy Avigad
parent
ebb3e60096
commit
4050892889
22 changed files with 83 additions and 83 deletions
|
|
@ -76,11 +76,11 @@ namespace binary
|
|||
... = a*((b*c)*d) : H_assoc
|
||||
end
|
||||
|
||||
definition right_commutative_compose_right [reducible]
|
||||
{A B : Type} (f : A → A → A) (g : B → A) (rcomm : right_commutative f) : right_commutative (compose_right f g) :=
|
||||
definition right_commutative_comp_right [reducible]
|
||||
{A B : Type} (f : A → A → A) (g : B → A) (rcomm : right_commutative f) : right_commutative (comp_right f g) :=
|
||||
λ a b₁ b₂, !rcomm
|
||||
|
||||
definition left_commutative_compose_left [reducible]
|
||||
{A B : Type} (f : A → A → A) (g : B → A) (lcomm : left_commutative f) : left_commutative (compose_left f g) :=
|
||||
{A B : Type} (f : A → A → A) (g : B → A) (lcomm : left_commutative f) : left_commutative (comp_left f g) :=
|
||||
λ a b₁ b₂, !lcomm
|
||||
end binary
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ namespace category
|
|||
-- (λ a b f, !id_right)
|
||||
-- (λ a b f, !id_left)
|
||||
|
||||
infixr `∘op`:60 := @compose _ (opposite _) _ _ _
|
||||
infixr `∘op`:60 := @comp _ (opposite _) _ _ _
|
||||
|
||||
variables {C : Category} {a b c : C}
|
||||
|
||||
|
|
@ -47,11 +47,11 @@ namespace category
|
|||
|
||||
definition type_category [reducible] : category Type :=
|
||||
mk (λa b, a → b)
|
||||
(λ a b c, function.compose)
|
||||
(λ a b c, function.comp)
|
||||
(λ a, _root_.id)
|
||||
(λ a b c d h g f, symm (function.compose.assoc h g f))
|
||||
(λ a b f, function.compose.left_id f)
|
||||
(λ a b f, function.compose.right_id f)
|
||||
(λ a b c d h g f, symm (function.comp.assoc h g f))
|
||||
(λ a b f, function.comp.left_id f)
|
||||
(λ a b f, function.comp.right_id f)
|
||||
|
||||
definition Type_category [reducible] : Category := Mk type_category
|
||||
|
||||
|
|
|
|||
|
|
@ -203,7 +203,7 @@ namespace finset
|
|||
variable [comm_semigroup B]
|
||||
|
||||
theorem mulf_rcomm (f : A → B) : right_commutative (mulf f) :=
|
||||
right_commutative_compose_right (@has_mul.mul B _) f (@mul.right_comm B _)
|
||||
right_commutative_comp_right (@has_mul.mul B _) f (@mul.right_comm B _)
|
||||
|
||||
namespace Prod_semigroup
|
||||
open Prodl_semigroup
|
||||
|
|
|
|||
|
|
@ -63,7 +63,7 @@ open equiv.ops
|
|||
lemma id_apply {A : Type} (x : A) : id ∙ x = x :=
|
||||
rfl
|
||||
|
||||
lemma compose_apply {A B C : Type} (g : B ≃ C) (f : A ≃ B) (x : A) : (g ∘ f) ∙ x = g ∙ f ∙ x :=
|
||||
lemma comp_apply {A B C : Type} (g : B ≃ C) (f : A ≃ B) (x : A) : (g ∘ f) ∙ x = g ∙ f ∙ x :=
|
||||
begin cases g, cases f, esimp end
|
||||
|
||||
lemma inverse_apply_apply {A B : Type} : ∀ (e : A ≃ B) (x : A), e⁻¹ ∙ e ∙ x = x
|
||||
|
|
@ -379,7 +379,7 @@ assume h₁ h₂, by rewrite [swap_apply_def, if_neg h₁, if_neg h₂]
|
|||
lemma swap_swap (a b : A) : swap a b ∘ swap a b = id :=
|
||||
eq_of_to_fun_eq (funext (λ x, begin unfold [swap, fn, equiv.trans, equiv.refl], rewrite swap_core_swap_core end))
|
||||
|
||||
lemma swap_compose_apply (a b : A) (π : perm A) (x : A) : (swap a b ∘ π) ∙ x = if π ∙ x = a then b else if π ∙ x = b then a else π ∙ x :=
|
||||
lemma swap_comp_apply (a b : A) (π : perm A) (x : A) : (swap a b ∘ π) ∙ x = if π ∙ x = a then b else if π ∙ x = b then a else π ∙ x :=
|
||||
begin cases π, reflexivity end
|
||||
|
||||
end swap
|
||||
|
|
|
|||
|
|
@ -455,7 +455,7 @@ theorem powerset_insert {a : hf} {s : hf} : a ∉ s → 𝒫 (insert a s) = 𝒫
|
|||
begin unfold [mem, powerset, insert, union, image], rewrite [*to_finset_of_finset], intro h,
|
||||
have (λ (x : finset hf), of_finset (finset.insert a x)) = (λ (x : finset hf), of_finset (finset.insert a (to_finset (of_finset x)))), from
|
||||
funext (λ x, by rewrite to_finset_of_finset),
|
||||
rewrite [finset.powerset_insert h, finset.image_union, -*finset.image_comp, ↑compose, this]
|
||||
rewrite [finset.powerset_insert h, finset.image_union, -*finset.image_comp, ↑comp, this]
|
||||
end
|
||||
|
||||
theorem mem_powerset_iff_subset (s : hf) : ∀ x : hf, x ∈ 𝒫 s ↔ x ⊆ s :=
|
||||
|
|
|
|||
|
|
@ -118,7 +118,7 @@ assume xa : x ∈ a,
|
|||
have H : f1 x ∈ b, from maps_to_f1 xa,
|
||||
show f2 x ∈ b, from eq_on_a xa ▸ H
|
||||
|
||||
theorem maps_to_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
|
||||
theorem maps_to_comp {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
|
||||
(H1 : maps_to g b c) (H2 : maps_to f a b) : maps_to (g ∘ f) a c :=
|
||||
take x, assume H : x ∈ a, H1 (H2 H)
|
||||
|
||||
|
|
@ -157,7 +157,7 @@ assume H : f2 x1 = f2 x2,
|
|||
have H' : f1 x1 = f1 x2, from eq_f1_f2 ax1 ⬝ H ⬝ (eq_f1_f2 ax2)⁻¹,
|
||||
show x1 = x2, from inj_f1 ax1 ax2 H'
|
||||
|
||||
theorem inj_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y}
|
||||
theorem inj_on_comp {g : Y → Z} {f : X → Y} {a : set X} {b : set Y}
|
||||
(fab : maps_to f a b) (Hg : inj_on g b) (Hf: inj_on f a) :
|
||||
inj_on (g ∘ f) a :=
|
||||
take x1 x2 : X,
|
||||
|
|
@ -195,7 +195,7 @@ have H2 : x ∈ a, from and.left H1,
|
|||
have H3 : f2 x = y, from (eq_f1_f2 H2)⁻¹ ⬝ and.right H1,
|
||||
exists.intro x (and.intro H2 H3)
|
||||
|
||||
theorem surj_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
|
||||
theorem surj_on_comp {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
|
||||
(Hg : surj_on g b c) (Hf: surj_on f a b) :
|
||||
surj_on (g ∘ f) a c :=
|
||||
take z,
|
||||
|
|
@ -260,16 +260,16 @@ lemma image_eq_of_bij_on {f : X → Y} {a : set X} {b : set Y} (bfab : bij_on f
|
|||
f ' a = b :=
|
||||
image_eq_of_maps_to_of_surj_on (and.left bfab) (and.right (and.right bfab))
|
||||
|
||||
theorem bij_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
|
||||
theorem bij_on_comp {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
|
||||
(Hg : bij_on g b c) (Hf: bij_on f a b) :
|
||||
bij_on (g ∘ f) a c :=
|
||||
match Hg with and.intro Hgmap (and.intro Hginj Hgsurj) :=
|
||||
match Hf with and.intro Hfmap (and.intro Hfinj Hfsurj) :=
|
||||
and.intro
|
||||
(maps_to_compose Hgmap Hfmap)
|
||||
(maps_to_comp Hgmap Hfmap)
|
||||
(and.intro
|
||||
(inj_on_compose Hfmap Hginj Hfinj)
|
||||
(surj_on_compose Hgsurj Hfsurj))
|
||||
(inj_on_comp Hfmap Hginj Hfinj)
|
||||
(surj_on_comp Hgsurj Hfsurj))
|
||||
end
|
||||
end
|
||||
|
||||
|
|
@ -320,7 +320,7 @@ calc
|
|||
... = g (f x2) : H1
|
||||
... = x2 : H x2a
|
||||
|
||||
theorem left_inv_on_compose {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
|
||||
theorem left_inv_on_comp {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
|
||||
{a : set X} {b : set Y} (fab : maps_to f a b)
|
||||
(Hf : left_inv_on f' f a) (Hg : left_inv_on g' g b) : left_inv_on (f' ∘ g') (g ∘ f) a :=
|
||||
take x : X,
|
||||
|
|
@ -353,10 +353,10 @@ have gya : g y ∈ a, from gba yb,
|
|||
have H1 : f (g y) = y, from H yb,
|
||||
exists.intro (g y) (and.intro gya H1)
|
||||
|
||||
theorem right_inv_on_compose {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
|
||||
theorem right_inv_on_comp {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
|
||||
{c : set Z} {b : set Y} (g'cb : maps_to g' c b)
|
||||
(Hf : right_inv_on f' f b) (Hg : right_inv_on g' g c) : right_inv_on (f' ∘ g') (g ∘ f) c :=
|
||||
left_inv_on_compose g'cb Hg Hf
|
||||
left_inv_on_comp g'cb Hg Hf
|
||||
|
||||
theorem right_inv_on_of_inj_on_of_left_inv_on {f : X → Y} {g : Y → X} {a : set X} {b : set Y}
|
||||
(fab : maps_to f a b) (gba : maps_to g b a) (injf : inj_on f a) (lfg : left_inv_on f g b) :
|
||||
|
|
|
|||
|
|
@ -44,10 +44,10 @@ mk_equivalence (@map.equiv X Y a b) (@equiv.refl X Y a b) (@equiv.symm X Y a b)
|
|||
|
||||
/- compose -/
|
||||
|
||||
protected definition compose (g : map b c) (f : map a b) : map a c :=
|
||||
map.mk (#function g ∘ f) (maps_to_compose (mapsto g) (mapsto f))
|
||||
protected definition comp (g : map b c) (f : map a b) : map a c :=
|
||||
map.mk (#function g ∘ f) (maps_to_comp (mapsto g) (mapsto f))
|
||||
|
||||
notation g ∘ f := map.compose g f
|
||||
notation g ∘ f := map.comp g f
|
||||
|
||||
/- range -/
|
||||
|
||||
|
|
@ -64,9 +64,9 @@ theorem injective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.injective
|
|||
map.injective f2 :=
|
||||
inj_on_of_eq_on H1 H2
|
||||
|
||||
theorem injective_compose {g : map b c} {f : map a b} (Hg : map.injective g) (Hf: map.injective f) :
|
||||
theorem injective_comp {g : map b c} {f : map a b} (Hg : map.injective g) (Hf: map.injective f) :
|
||||
map.injective (g ∘ f) :=
|
||||
inj_on_compose (mapsto f) Hg Hf
|
||||
inj_on_comp (mapsto f) Hg Hf
|
||||
|
||||
/- surjective -/
|
||||
|
||||
|
|
@ -76,10 +76,10 @@ theorem surjective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.surjectiv
|
|||
map.surjective f2 :=
|
||||
surj_on_of_eq_on H1 H2
|
||||
|
||||
theorem surjective_compose {g : map b c} {f : map a b} (Hg : map.surjective g)
|
||||
theorem surjective_comp {g : map b c} {f : map a b} (Hg : map.surjective g)
|
||||
(Hf: map.surjective f) :
|
||||
map.surjective (g ∘ f) :=
|
||||
surj_on_compose Hg Hf
|
||||
surj_on_comp Hg Hf
|
||||
|
||||
theorem image_eq_of_surjective {f : map a b} (H : map.surjective f) : f ' a = b :=
|
||||
image_eq_of_maps_to_of_surj_on (map.mapsto f) H
|
||||
|
|
@ -92,11 +92,11 @@ theorem bijective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.bijective
|
|||
map.bijective f2 :=
|
||||
and.intro (injective_of_equiv H1 (and.left H2)) (surjective_of_equiv H1 (and.right H2))
|
||||
|
||||
theorem bijective_compose {g : map b c} {f : map a b} (Hg : map.bijective g) (Hf: map.bijective f) :
|
||||
theorem bijective_comp {g : map b c} {f : map a b} (Hg : map.bijective g) (Hf: map.bijective f) :
|
||||
map.bijective (g ∘ f) :=
|
||||
obtain Hg₁ Hg₂, from Hg,
|
||||
obtain Hf₁ Hf₂, from Hf,
|
||||
and.intro (injective_compose Hg₁ Hf₁) (surjective_compose Hg₂ Hf₂)
|
||||
and.intro (injective_comp Hg₁ Hf₁) (surjective_comp Hg₂ Hf₂)
|
||||
|
||||
theorem image_eq_of_bijective {f : map a b} (H : map.bijective f) : f ' a = b :=
|
||||
image_eq_of_surjective (proof and.right H qed)
|
||||
|
|
@ -118,10 +118,10 @@ theorem injective_of_left_inverse {g : map b a} {f : map a b} (H : map.left_inve
|
|||
map.injective f :=
|
||||
inj_on_of_left_inv_on H
|
||||
|
||||
theorem left_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
|
||||
theorem left_inverse_comp {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
|
||||
(Hf : map.left_inverse f' f) (Hg : map.left_inverse g' g) :
|
||||
map.left_inverse (f' ∘ g') (g ∘ f) :=
|
||||
left_inv_on_compose (mapsto f) Hf Hg
|
||||
left_inv_on_comp (mapsto f) Hf Hg
|
||||
|
||||
/- right inverse -/
|
||||
|
||||
|
|
@ -150,10 +150,10 @@ theorem left_inverse_of_surjective_of_right_inverse {f : map a b} {g : map b a}
|
|||
map.left_inverse f g :=
|
||||
left_inv_on_of_surj_on_right_inv_on surjf rfg
|
||||
|
||||
theorem right_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
|
||||
theorem right_inverse_comp {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
|
||||
(Hf : map.right_inverse f' f) (Hg : map.right_inverse g' g) :
|
||||
map.right_inverse (f' ∘ g') (g ∘ f) :=
|
||||
map.left_inverse_compose Hg Hf
|
||||
map.left_inverse_comp Hg Hf
|
||||
|
||||
theorem equiv_of_map.left_inverse_of_right_inverse {g1 g2 : map b a} {f : map a b}
|
||||
(H1 : map.left_inverse g1 f) (H2 : map.right_inverse g2 f) : g1 ~ g2 :=
|
||||
|
|
|
|||
|
|
@ -595,7 +595,7 @@ infix `⊛`:75 := apply -- input as \o*
|
|||
|
||||
theorem identity (s : stream A) : pure id ⊛ s = s :=
|
||||
rfl
|
||||
theorem composition (g : stream (B → C)) (f : stream (A → B)) (s : stream A) : pure compose ⊛ g ⊛ f ⊛ s = g ⊛ (f ⊛ s) :=
|
||||
theorem composition (g : stream (B → C)) (f : stream (A → B)) (s : stream A) : pure comp ⊛ g ⊛ f ⊛ s = g ⊛ (f ⊛ s) :=
|
||||
rfl
|
||||
theorem homomorphism (f : A → B) (a : A) : pure f ⊛ pure a = pure (f a) :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -12,13 +12,13 @@ namespace function
|
|||
|
||||
variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
|
||||
|
||||
definition compose [reducible] [unfold_full] (f : B → C) (g : A → B) : A → C :=
|
||||
definition comp [reducible] [unfold_full] (f : B → C) (g : A → B) : A → C :=
|
||||
λx, f (g x)
|
||||
|
||||
definition compose_right [reducible] [unfold_full] (f : B → B → B) (g : A → B) : B → A → B :=
|
||||
definition comp_right [reducible] [unfold_full] (f : B → B → B) (g : A → B) : B → A → B :=
|
||||
λ b a, f b (g a)
|
||||
|
||||
definition compose_left [reducible] [unfold_full] (f : B → B → B) (g : A → B) : A → B → B :=
|
||||
definition comp_left [reducible] [unfold_full] (f : B → B → B) (g : A → B) : A → B → B :=
|
||||
λ a b, f (g a) b
|
||||
|
||||
definition on_fun [reducible] [unfold_full] (f : B → B → C) (g : A → B) : A → A → C :=
|
||||
|
|
@ -31,7 +31,7 @@ definition combine [reducible] [unfold_full] (f : A → B → C) (op : C → D
|
|||
definition const [reducible] [unfold_full] (B : Type) (a : A) : B → A :=
|
||||
λx, a
|
||||
|
||||
definition dcompose [reducible] [unfold_full] {B : A → Type} {C : Π {x : A}, B x → Type}
|
||||
definition dcomp [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) :=
|
||||
λx, f (g x)
|
||||
|
||||
|
|
@ -53,8 +53,8 @@ rfl
|
|||
theorem uncurry_curry (f : A × B → C) : uncurry (curry f) = f :=
|
||||
funext (λ p, match p with (a, b) := rfl end)
|
||||
|
||||
infixr ` ∘ ` := compose
|
||||
infixr ` ∘' `:60 := dcompose
|
||||
infixr ` ∘ ` := comp
|
||||
infixr ` ∘' `:60 := dcomp
|
||||
infixl ` on `:1 := on_fun
|
||||
infixr ` $ `:1 := app
|
||||
notation f ` -[` op `]- ` g := combine f op g
|
||||
|
|
@ -63,23 +63,23 @@ lemma left_id (f : A → B) : id ∘ f = f := rfl
|
|||
|
||||
lemma right_id (f : A → B) : f ∘ id = f := rfl
|
||||
|
||||
theorem compose.assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
|
||||
theorem comp.assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
|
||||
|
||||
theorem compose.left_id (f : A → B) : id ∘ f = f := rfl
|
||||
theorem comp.left_id (f : A → B) : id ∘ f = f := rfl
|
||||
|
||||
theorem compose.right_id (f : A → B) : f ∘ id = f := rfl
|
||||
theorem comp.right_id (f : A → B) : f ∘ id = f := rfl
|
||||
|
||||
theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := rfl
|
||||
theorem comp_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := rfl
|
||||
|
||||
definition injective [reducible] (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
|
||||
|
||||
theorem injective_compose {g : B → C} {f : A → B} (Hg : injective g) (Hf : injective f) :
|
||||
theorem injective_comp {g : B → C} {f : A → B} (Hg : injective g) (Hf : injective f) :
|
||||
injective (g ∘ f) :=
|
||||
take a₁ a₂, assume Heq, Hf (Hg Heq)
|
||||
|
||||
definition surjective [reducible] (f : A → B) : Prop := ∀ b, ∃ a, f a = b
|
||||
|
||||
theorem surjective_compose {g : B → C} {f : A → B} (Hg : surjective g) (Hf : surjective f) :
|
||||
theorem surjective_comp {g : B → C} {f : A → B} (Hg : surjective g) (Hf : surjective f) :
|
||||
surjective (g ∘ f) :=
|
||||
take c,
|
||||
obtain b (Hb : g b = c), from Hg c,
|
||||
|
|
@ -88,11 +88,11 @@ take c,
|
|||
|
||||
definition bijective (f : A → B) := injective f ∧ surjective f
|
||||
|
||||
theorem bijective_compose {g : B → C} {f : A → B} (Hg : bijective g) (Hf : bijective f) :
|
||||
theorem bijective_comp {g : B → C} {f : A → B} (Hg : bijective g) (Hf : bijective f) :
|
||||
bijective (g ∘ f) :=
|
||||
obtain Hginj Hgsurj, from Hg,
|
||||
obtain Hfinj Hfsurj, from Hf,
|
||||
and.intro (injective_compose Hginj Hfinj) (surjective_compose Hgsurj Hfsurj)
|
||||
and.intro (injective_comp Hginj Hfinj) (surjective_comp Hgsurj Hfsurj)
|
||||
|
||||
-- g is a left inverse to f
|
||||
definition left_inverse (g : B → A) (f : A → B) : Prop := ∀x, g (f x) = x
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ section
|
|||
theorem hproof_irrel {a b : Prop} (H : a = b) (H₁ : a) (H₂ : b) : H₁ == H₂ :=
|
||||
eq_rec_to_heq (proof_irrel (cast H H₁) H₂)
|
||||
|
||||
--TODO: generalize to eq.rec. This is a special case of rec_on_compose in eq.lean
|
||||
--TODO: generalize to eq.rec. This is a special case of rec_on_comp in eq.lean
|
||||
theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) :
|
||||
cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
|
||||
by subst Hab
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ namespace eq
|
|||
eq.drec_on H b = eq.drec_on H' b :=
|
||||
proof_irrel H H' ▸ rfl
|
||||
|
||||
theorem rec_on_compose {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
|
||||
theorem rec_on_comp {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
|
||||
(u : P a) : eq.rec_on H₂ (eq.rec_on H₁ u) = eq.rec_on (trans H₁ H₂) u :=
|
||||
(show ∀ H₂ : b = c, eq.rec_on H₂ (eq.rec_on H₁ u) = eq.rec_on (trans H₁ H₂) u,
|
||||
from eq.drec_on H₂ (take (H₂ : b = b), rec_on_id H₂ _))
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ have linv : left_inverse finv f, from
|
|||
have ex : ∃ a₁ : A, f a₁ = f a, from exists.intro a rfl,
|
||||
have h₁ : f (some ex) = f a, from !some_spec,
|
||||
begin
|
||||
esimp [mk_left_inv, compose, id],
|
||||
esimp [mk_left_inv, comp, id],
|
||||
rewrite [dif_pos ex],
|
||||
exact (!inj h₁)
|
||||
end,
|
||||
|
|
|
|||
|
|
@ -114,7 +114,7 @@ assume Pgstab,
|
|||
have hom g a = a, from of_mem_sep Pgstab, calc
|
||||
hom (f*g) a = perm.f ((hom f) * (hom g)) a : is_hom hom
|
||||
... = ((hom f) ∘ (hom g)) a : by rewrite perm_f_mul
|
||||
... = (hom f) a : by unfold compose; rewrite this
|
||||
... = (hom f) a : by unfold comp; rewrite this
|
||||
|
||||
lemma stab_subset : stab hom H a ⊆ H :=
|
||||
begin
|
||||
|
|
@ -126,7 +126,7 @@ assume Pg,
|
|||
have hom g a = hom h a, from of_mem_sep Pg, calc
|
||||
hom (h⁻¹*g) a = perm.f ((hom h⁻¹) * (hom g)) a : by rewrite (is_hom hom)
|
||||
... = ((hom h⁻¹) ∘ hom g) a : by rewrite perm_f_mul
|
||||
... = perm.f ((hom h)⁻¹ * hom h) a : by unfold compose; rewrite [this, perm_f_mul, hom_map_inv hom h]
|
||||
... = perm.f ((hom h)⁻¹ * hom h) a : by unfold comp; rewrite [this, perm_f_mul, hom_map_inv hom h]
|
||||
... = perm.f (1 : perm S) a : by rewrite (mul.left_inv (hom h))
|
||||
... = a : by esimp
|
||||
|
||||
|
|
@ -486,7 +486,7 @@ definition lower_perm (p : perm (fin (succ n))) (P : p maxi = maxi) : perm (fin
|
|||
perm.mk (lower_inj p (perm.inj p) P)
|
||||
(take i j, begin
|
||||
rewrite [-eq_iff_veq, *lower_inj_apply, eq_iff_veq],
|
||||
apply injective_compose (perm.inj p) lift_succ_inj
|
||||
apply injective_comp (perm.inj p) lift_succ_inj
|
||||
end)
|
||||
|
||||
lemma lift_lower_eq : ∀ {p : perm (fin (succ n))} (P : p maxi = maxi),
|
||||
|
|
|
|||
|
|
@ -292,7 +292,7 @@ lemma rotl_rotr : ∀ {n : nat} (m : nat), (@rotl n m) ∘ (rotr m) = id
|
|||
| (nat.succ n) := take m, funext take i, calc (mk_mod n (n*m)) + (-(mk_mod n (n*m)) + i) = i : add_neg_cancel_left
|
||||
|
||||
lemma rotl_succ {n : nat} : (rotl 1) ∘ (@succ n) = lift_succ :=
|
||||
funext (take i, eq_of_veq (begin rewrite [↑compose, ↑rotl, ↑madd, mul_one n, ↑mk_mod, mod_add_mod, ↑lift_succ, val_succ, -succ_add_eq_succ_add, add_mod_self_left, mod_eq_of_lt (lt.trans (is_lt i) !lt_succ_self), -val_lift] end))
|
||||
funext (take i, eq_of_veq (begin rewrite [↑comp, ↑rotl, ↑madd, mul_one n, ↑mk_mod, mod_add_mod, ↑lift_succ, val_succ, -succ_add_eq_succ_add, add_mod_self_left, mod_eq_of_lt (lt.trans (is_lt i) !lt_succ_self), -val_lift] end))
|
||||
|
||||
definition list.rotl {A : Type} : ∀ l : list A, list A
|
||||
| [] := []
|
||||
|
|
@ -336,7 +336,7 @@ lemma rotl_seq_ne_id : ∀ {n : nat}, (∃ a b : A, a ≠ b) → ∀ i, i < n
|
|||
assume Peq, absurd (congr_fun Peq f) P
|
||||
|
||||
lemma rotr_rotl_fun {n : nat} (m : nat) (f : seq A n) : rotr_fun m (rotl_fun m f) = f :=
|
||||
calc f ∘ (rotl m) ∘ (rotr m) = f ∘ ((rotl m) ∘ (rotr m)) : by rewrite -compose.assoc
|
||||
calc f ∘ (rotl m) ∘ (rotr m) = f ∘ ((rotl m) ∘ (rotr m)) : by rewrite -comp.assoc
|
||||
... = f ∘ id : by rewrite (rotl_rotr m)
|
||||
|
||||
lemma rotl_fun_inj {n : nat} {m : nat} : @injective (seq A n) (seq A n) (rotl_fun m) :=
|
||||
|
|
@ -365,7 +365,7 @@ include finA deceqA
|
|||
|
||||
lemma rotl_perm_mul {i j : nat} : (rotl_perm A n i) * (rotl_perm A n j) = rotl_perm A n (j+i) :=
|
||||
eq_of_feq (funext take f, calc
|
||||
f ∘ (rotl j) ∘ (rotl i) = f ∘ ((rotl j) ∘ (rotl i)) : by rewrite -compose.assoc
|
||||
f ∘ (rotl j) ∘ (rotl i) = f ∘ ((rotl j) ∘ (rotl i)) : by rewrite -comp.assoc
|
||||
... = f ∘ (rotl (j+i)) : by rewrite rotl_compose)
|
||||
|
||||
lemma rotl_perm_pow_eq : ∀ {i : nat}, (rotl_perm A n 1) ^ i = rotl_perm A n i
|
||||
|
|
|
|||
|
|
@ -137,7 +137,7 @@ begin
|
|||
esimp [fin_inv, fin_lcoset, fin_rcoset],
|
||||
rewrite [-image_comp],
|
||||
apply ext, intro b,
|
||||
rewrite [*mem_image_iff, ↑compose, ↑lmul_by, ↑rmul_by],
|
||||
rewrite [*mem_image_iff, ↑comp, ↑lmul_by, ↑rmul_by],
|
||||
apply iff.intro,
|
||||
intro Pl, cases Pl with h Ph, cases Ph with Pin Peq,
|
||||
existsi h⁻¹, apply and.intro,
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ definition perm_is_fintype [instance] : fintype (perm A) :=
|
|||
fintype.mk all_perms nodup_all_perms all_perms_complete
|
||||
|
||||
definition perm.mul (f g : perm A) :=
|
||||
perm.mk (f∘g) (injective_compose (perm.inj f) (perm.inj g))
|
||||
perm.mk (f∘g) (injective_comp (perm.inj f) (perm.inj g))
|
||||
definition perm.one [reducible] : perm A := perm.mk id injective_id
|
||||
definition perm.inv (f : perm A) := let inj := perm.inj f in
|
||||
perm.mk (perm_inv inj) (perm_inv_inj inj)
|
||||
|
|
|
|||
|
|
@ -200,7 +200,7 @@ lemma rotl_perm_peo_of_peo {n : nat} : ∀ {m} {s : seq A n}, peo s → peo (rot
|
|||
| (succ m) := take s,
|
||||
have Pmul : rotl_perm A n (m + 1) s = rotl_fun 1 (rotl_perm A n m s), from
|
||||
calc s ∘ (rotl (m + 1)) = s ∘ ((rotl m) ∘ (rotl 1)) : rotl_compose
|
||||
... = s ∘ (rotl m) ∘ (rotl 1) : compose.assoc,
|
||||
... = s ∘ (rotl m) ∘ (rotl 1) : comp.assoc,
|
||||
begin
|
||||
rewrite [-add_one, Pmul], intro P,
|
||||
exact rotl1_peo_of_peo (rotl_perm_peo_of_peo P)
|
||||
|
|
@ -257,7 +257,7 @@ funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, -rotl_perm_pow_eq, rot
|
|||
|
||||
lemma rotl_peo_seq_compose {n i j : nat} :
|
||||
(rotl_peo_seq A n i) ∘ (rotl_peo_seq A n j) = rotl_peo_seq A n (j + i) :=
|
||||
funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, ↑rotl_perm, ↑rotl_fun, compose.assoc, rotl_compose] end
|
||||
funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, ↑rotl_perm, ↑rotl_fun, comp.assoc, rotl_compose] end
|
||||
|
||||
lemma rotl_peo_seq_mod {n i : nat} : rotl_peo_seq A n i = rotl_peo_seq A n (i % succ n) :=
|
||||
funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, rotl_perm_mod] end
|
||||
|
|
|
|||
|
|
@ -22,11 +22,11 @@ definition r a (S : set A) := (rmul a) ' S
|
|||
lemma lmul_compose : ∀ (a b : A), (lmul a) ∘ (lmul b) = lmul (a*b) :=
|
||||
take a, take b,
|
||||
funext (assume x, by
|
||||
rewrite [↑function.compose, ↑lmul, mul.assoc])
|
||||
rewrite [↑function.comp, ↑lmul, mul.assoc])
|
||||
lemma rmul_compose : ∀ (a b : A), (rmul a) ∘ (rmul b) = rmul (b*a) :=
|
||||
take a, take b,
|
||||
funext (assume x, by
|
||||
rewrite [↑function.compose, ↑rmul, mul.assoc])
|
||||
rewrite [↑function.comp, ↑rmul, mul.assoc])
|
||||
lemma lcompose a b (S : set A) : l a (l b S) = l (a*b) S :=
|
||||
calc (lmul a) ' ((lmul b) ' S) = ((lmul a) ∘ (lmul b)) ' S : image_comp
|
||||
... = lmul (a*b) ' S : lmul_compose
|
||||
|
|
|
|||
|
|
@ -12,19 +12,19 @@ attribute bijection.func [coercion]
|
|||
namespace bijection
|
||||
variable {A : Type}
|
||||
|
||||
definition compose (f g : bijection A) : bijection A :=
|
||||
definition comp (f g : bijection A) : bijection A :=
|
||||
bijection.mk
|
||||
(f ∘ g)
|
||||
(finv g ∘ finv f)
|
||||
(by rewrite [compose.assoc, -{finv f ∘ _}compose.assoc, linv f, compose.left_id, linv g])
|
||||
(by rewrite [-compose.assoc, {_ ∘ finv g}compose.assoc, rinv g, compose.right_id, rinv f])
|
||||
(by rewrite [comp.assoc, -{finv f ∘ _}comp.assoc, linv f, comp.left_id, linv g])
|
||||
(by rewrite [-comp.assoc, {_ ∘ finv g}comp.assoc, rinv g, comp.right_id, rinv f])
|
||||
|
||||
infixr ` ∘b `:100 := compose
|
||||
infixr ` ∘b `:100 := comp
|
||||
|
||||
lemma compose.assoc (f g h : bijection A) : (f ∘b g) ∘b h = f ∘b (g ∘b h) := rfl
|
||||
|
||||
definition id : bijection A :=
|
||||
bijection.mk id id (compose.left_id id) (compose.left_id id)
|
||||
bijection.mk id id (comp.left_id id) (comp.left_id id)
|
||||
|
||||
lemma id.left_id (f : bijection A) : id ∘b f = f :=
|
||||
bijection.rec_on f (λx x x x, rfl)
|
||||
|
|
@ -40,5 +40,5 @@ namespace bijection
|
|||
(linv f)
|
||||
|
||||
lemma inv.linv (f : bijection A) : inv f ∘b f = id :=
|
||||
bijection.rec_on f (λfunc finv linv rinv, by rewrite [↑inv, ↑compose, linv])
|
||||
bijection.rec_on f (λfunc finv linv rinv, by rewrite [↑inv, ↑comp, linv])
|
||||
end bijection
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
550.lean:43:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application
|
||||
550.lean:43:69: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application
|
||||
eq.symm linv
|
||||
term
|
||||
linv
|
||||
|
|
@ -16,13 +16,13 @@ linv : finv ∘ func = id,
|
|||
rinv : func ∘ finv = id
|
||||
⊢ mk (finv ∘ func) (finv ∘ func)
|
||||
(eq.rec
|
||||
(eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (compose.left_id func))) (eq.symm rinv))
|
||||
(function.compose.assoc func finv func))
|
||||
(eq.symm (function.compose.assoc finv func (finv ∘ func))))
|
||||
(eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (comp.left_id func))) (eq.symm rinv))
|
||||
(comp.assoc func finv func))
|
||||
(eq.symm (comp.assoc finv func (finv ∘ func))))
|
||||
(eq.rec
|
||||
(eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (compose.right_id finv))) (eq.symm rinv))
|
||||
(eq.symm (function.compose.assoc finv func finv)))
|
||||
(function.compose.assoc (finv ∘ func) finv func)) = id
|
||||
(eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (comp.right_id finv))) (eq.symm rinv))
|
||||
(eq.symm (comp.assoc finv func finv)))
|
||||
(comp.assoc (finv ∘ func) finv func)) = id
|
||||
550.lean:43:44: error: don't know how to synthesize placeholder
|
||||
A : Type,
|
||||
f : bijection A,
|
||||
|
|
|
|||
|
|
@ -44,15 +44,15 @@ example : m = n → xs == ys → nil ++ xs == ys := by inst_simp
|
|||
example : (xs ++ ys) ++ zs == xs ++ (ys ++ zs) := by inst_simp
|
||||
example : p = m + n → zs == xs ++ ys → zs ++ ws == (xs ++ ys) ++ ws := by inst_simp
|
||||
example : m + n = p → xs ++ ys == zs → zs ++ ws == xs ++ (ys ++ ws) := by inst_simp
|
||||
|
||||
|
||||
example : m = n → p = q → m + n = p → xs == ys → zs == ws → xs ++ ys == zs → ws ++ ws == (ys ++ xs) ++ (xs ++ ys) := by inst_simp
|
||||
|
||||
example : m = n → n = p → xs == reverse ys → ys == reverse zs → xs == zs := by inst_simp
|
||||
|
||||
example : m = n → xs == ys → f = g → a = b → map f (cons a xs) == cons (g b) (map g ys) := by
|
||||
example : m = n → xs == ys → f = g → a = b → map f (cons a xs) == cons (g b) (map g ys) := by
|
||||
inst_simp
|
||||
|
||||
attribute function.compose [semireducible]
|
||||
attribute function.comp [semireducible]
|
||||
example : m = n → xs == ys → h1 = h2 → k1 = k2 → map k1 (map h1 xs) == map (k2 ∘ h2) ys := by inst_simp
|
||||
|
||||
example : ∀ (xs : tuple A (nat.succ m)) (ys : tuple A (nat.succ n))
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ open set function eq.ops
|
|||
|
||||
variables {X Y Z : Type}
|
||||
|
||||
lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
|
||||
lemma image_comp (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
|
||||
ext (take z,
|
||||
iff.intro
|
||||
(assume Hz,
|
||||
|
|
@ -11,4 +11,4 @@ ext (take z,
|
|||
by repeat (apply mem_image | assumption | reflexivity))
|
||||
(assume Hz,
|
||||
obtain y [x Hz₁ Hz₂] Hy₂, from Hz,
|
||||
by repeat (apply mem_image | assumption | esimp [compose] | rewrite Hz₂)))
|
||||
by repeat (apply mem_image | assumption | esimp [comp] | rewrite Hz₂)))
|
||||
|
|
|
|||
Loading…
Reference in a new issue