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

refactor(library/algebra/category/morphism): reduce compilation time using rewrite tactic

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-25 10:14:51 -08:00
parent db1fba3ddc
commit 577a6da119
1 changed files with 26 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

54
library/algebra/category/morphism.lean
View file

@ -97,23 +97,14 @@ namespace morphism
theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g] theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g]
: is_section (g ∘ f) := : is_section (g ∘ f) :=
is_section.mk is_section.mk
(calc (show (retraction_of f ∘ retraction_of g) ∘ g ∘ f = id,
(retraction_of f ∘ retraction_of g) ∘ g ∘ f by rewrite [-assoc, assoc _ g f, retraction_compose, id_left, retraction_compose])
= retraction_of f ∘ retraction_of g ∘ g ∘ f : by rewrite -assoc
... = retraction_of f ∘ (retraction_of g ∘ g) ∘ f : by rewrite (assoc _ g f)
... = retraction_of f ∘ id ∘ f : by rewrite retraction_compose
... = retraction_of f ∘ f : by rewrite id_left
... = id : by rewrite retraction_compose)
theorem composition_is_retraction [instance] [Hf : is_retraction f] [Hg : is_retraction g] theorem composition_is_retraction [instance] [Hf : is_retraction f] [Hg : is_retraction g]
: is_retraction (g ∘ f) := : is_retraction (g ∘ f) :=
is_retraction.mk is_retraction.mk
(calc (show (g ∘ f) ∘ section_of f ∘ section_of g = id,
(g ∘ f) ∘ section_of f ∘ section_of g = g ∘ f ∘ section_of f ∘ section_of g : symm !assoc by rewrite [-assoc, {f ∘ _}assoc, compose_section, id_left, compose_section])
... = g ∘ (f ∘ section_of f) ∘ section_of g : by rewrite -assoc
... = g ∘ id ∘ section_of g : by rewrite compose_section
... = g ∘ section_of g : by rewrite id_left
... = id : by rewrite compose_section)
theorem composition_is_inverse [instance] [Hf : is_iso f] [Hg : is_iso g] : is_iso (g ∘ f) := theorem composition_is_inverse [instance] [Hf : is_iso f] [Hg : is_iso g] : is_iso (g ∘ f) :=
!section_retraction_imp_iso !section_retraction_imp_iso
@ -140,20 +131,23 @@ namespace morphism
inductive is_epi [class] (f : a ⟶ b) : Prop := inductive is_epi [class] (f : a ⟶ b) : Prop :=
mk : (∀c (g h : hom b c), g ∘ f = h ∘ f → g = h) → is_epi f mk : (∀c (g h : hom b c), g ∘ f = h ∘ f → g = h) → is_epi f
theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h :=
:= is_mono.rec (λH3, H3 c g h H2) H match H with
theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h is_mono.mk H3 := H3 c g h H2
:= is_epi.rec (λH3, H3 c g h H2) H end
theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h :=
match H with
is_epi.mk H3 := H3 c g h H2
end
theorem section_is_mono [instance] (f : a ⟶ b) [H : is_section f] : is_mono f := theorem section_is_mono [instance] (f : a ⟶ b) [H : is_section f] : is_mono f :=
is_mono.mk is_mono.mk
(λ c g h H, (λ c g h H,
calc calc
g = id ∘ g : symm (id_left g) g = id ∘ g : by rewrite id_left
... = (retraction_of f ∘ f) ∘ g : by rewrite -retraction_compose ... = (retraction_of f ∘ f) ∘ g : by rewrite -retraction_compose
... = retraction_of f ∘ f ∘ g : by rewrite assoc ... = (retraction_of f ∘ f) ∘ h : by rewrite [-assoc, H, -assoc]
... = retraction_of f ∘ f ∘ h : by rewrite H
... = (retraction_of f ∘ f) ∘ h : by rewrite -assoc
... = id ∘ h : by rewrite retraction_compose ... = id ∘ h : by rewrite retraction_compose
... = h : by rewrite id_left) ... = h : by rewrite id_left)
@ -161,11 +155,9 @@ namespace morphism
is_epi.mk is_epi.mk
(λ c g h H, (λ c g h H,
calc calc
g = g ∘ id : symm (id_right g) g = g ∘ id : by rewrite id_right
... = g ∘ f ∘ section_of f : by rewrite -(compose_section f) ... = g ∘ f ∘ section_of f : by rewrite -compose_section
... = (g ∘ f) ∘ section_of f : by rewrite assoc ... = h ∘ f ∘ section_of f : by rewrite [assoc, H, -assoc]
... = (h ∘ f) ∘ section_of f : by rewrite H
... = h ∘ f ∘ section_of f : by rewrite -assoc
... = h ∘ id : by rewrite compose_section ... = h ∘ id : by rewrite compose_section
... = h : by rewrite id_right) ... = h : by rewrite id_right)
@ -177,13 +169,19 @@ namespace morphism
theorem composition_is_mono [instance] [Hf : is_mono f] [Hg : is_mono g] : is_mono (g ∘ f) := theorem composition_is_mono [instance] [Hf : is_mono f] [Hg : is_mono g] : is_mono (g ∘ f) :=
is_mono.mk is_mono.mk
(λ d h₁ h₂ H, (λ d h₁ h₂ H,
have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂), from symm (assoc g f h₁) ▸ symm (assoc g f h₂) ▸ H, have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂),
begin
rewrite *assoc, exact H
end,
mono_elim (mono_elim H2)) mono_elim (mono_elim H2))
theorem composition_is_epi [instance] [Hf : is_epi f] [Hg : is_epi g] : is_epi (g ∘ f) := theorem composition_is_epi [instance] [Hf : is_epi f] [Hg : is_epi g] : is_epi (g ∘ f) :=
is_epi.mk is_epi.mk
(λ d h₁ h₂ H, (λ d h₁ h₂ H,
have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f, from assoc h₁ g f ▸ assoc h₂ g f ▸ H, have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f,
begin
rewrite -*assoc, exact H
end,
epi_elim (epi_elim H2)) epi_elim (epi_elim H2))
end morphism end morphism
namespace morphism namespace morphism