Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - refactor(control/fold): don't use is_monoid_hom #13350

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - refactor(control/fold): don't use is_monoid_hom #13350

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e8bebca
refactor(control/fold): don't use is_monoid_hom
semorrison Apr 11, 2022
40e5d5b
lint
semorrison Apr 11, 2022
55e224f
Merge remote-tracking branch 'origin/master' into semorrison/control_…
semorrison Apr 11, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
120 changes: 52 additions & 68 deletions src/control/fold.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ import control.traversable.lemmas
import category_theory.endomorphism
import category_theory.types
import category_theory.category.Kleisli
import deprecated.group
/-!

# List folds generalized to `traversable`
Expand All @@ -26,7 +25,7 @@ primitive and `fold_map_hom` as a defining property.
def fold_map {α ω} [has_one ω] [has_mul ω] (f : α → ω) : t α → ω := ...

lemma fold_map_hom (α β)
[monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
[monoid α] [monoid β] (f : α →* β)
(g : γ → α) (x : t γ) :
f (fold_map g x) = fold_map (f ∘ g) x :=
...
Expand Down Expand Up @@ -104,28 +103,45 @@ how the monoid of endofunctions define `foldl`.
@[reducible] def foldl (α : Type u) : Type u := (End α)ᵐᵒᵖ
def foldl.mk (f : α → α) : foldl α := op f
def foldl.get (x : foldl α) : α → α := unop x
def foldl.of_free_monoid (f : β → α → β) (xs : free_monoid α) : monoid.foldl β :=
op $ flip (list.foldl f) xs
@[simps] def foldl.of_free_monoid (f : β → α → β) : free_monoid α →* monoid.foldl β :=
{ to_fun := λ xs, op $ flip (list.foldl f) xs,
map_one' := rfl,
map_mul' := by intros; simp only [free_monoid.mul_def, flip, unop_op,
list.foldl_append, op_inj]; refl }

@[reducible] def foldr (α : Type u) : Type u := End α
def foldr.mk (f : α → α) : foldr α := f
def foldr.get (x : foldr α) : α → α := x
def foldr.of_free_monoid (f : α → β → β) (xs : free_monoid α) : monoid.foldr β :=
flip (list.foldr f) xs
@[simps] def foldr.of_free_monoid (f : α → β → β) : free_monoid α →* monoid.foldr β :=
{ to_fun := λ xs, flip (list.foldr f) xs,
map_one' := rfl,
map_mul' :=
begin
intros,
simp only [free_monoid.mul_def, list.foldr_append, flip],
refl
end }


@[reducible] def mfoldl (m : Type u → Type u) [monad m] (α : Type u) : Type u :=
mul_opposite $ End $ Kleisli.mk m α
def mfoldl.mk (f : α → m α) : mfoldl m α := op f
def mfoldl.get (x : mfoldl m α) : α → m α := unop x
def mfoldl.of_free_monoid (f : β → α → m β) (xs : free_monoid α) : monoid.mfoldl m β :=
op $ flip (list.mfoldl f) xs
@[simps] def mfoldl.of_free_monoid [is_lawful_monad m] (f : β → α → m β) :
free_monoid α →* monoid.mfoldl m β :=
{ to_fun := λ xs, op $ flip (list.mfoldl f) xs,
map_one' := rfl,
map_mul' := by intros; apply unop_injective; ext; apply list.mfoldl_append }

@[reducible] def mfoldr (m : Type u → Type u) [monad m] (α : Type u) : Type u :=
End $ Kleisli.mk m α
def mfoldr.mk (f : α → m α) : mfoldr m α := f
def mfoldr.get (x : mfoldr m α) : α → m α := x
def mfoldr.of_free_monoid (f : α → β → m β) (xs : free_monoid α) : monoid.mfoldr m β :=
flip (list.mfoldr f) xs
@[simps] def mfoldr.of_free_monoid [is_lawful_monad m] (f : α → β → m β) :
free_monoid α →* monoid.mfoldr m β :=
{ to_fun := λ xs, flip (list.mfoldr f) xs,
map_one' := rfl,
map_mul' := by intros; ext; apply list.mfoldr_append }

end monoid

Expand Down Expand Up @@ -180,78 +196,48 @@ end defs
section applicative_transformation
variables {α β γ : Type u}

open function (hiding const) is_monoid_hom
open function (hiding const)

def map_fold [monoid α] [monoid β] {f : α → β} (hf : is_monoid_hom f) :
def map_fold [monoid α] [monoid β] (f : α →* β) :
applicative_transformation (const α) (const β) :=
{ app := λ x, f,
preserves_seq' := by { intros, simp only [hf.map_mul, (<*>)], },
preserves_pure' := by { intros, simp only [hf.map_one, pure] } }
preserves_seq' := by { intros, simp only [f.map_mul, (<*>)], },
preserves_pure' := by { intros, simp only [f.map_one, pure] } }

def free.mk : α → free_monoid α := list.ret

def free.map (f : α → β) : free_monoid α → free_monoid β := list.map f
def free.map (f : α → β) : free_monoid α →* free_monoid β :=
{ to_fun := list.map f,
map_mul' := λ x y,
by simp only [free_monoid.mul_def, list.map_append, free_add_monoid.add_def],
map_one' := by simp only [free_monoid.one_def, list.map, free_add_monoid.zero_def] }

lemma free.map_eq_map (f : α → β) (xs : list α) :
f <$> xs = free.map f xs := rfl

lemma free.map.is_monoid_hom (f : α → β) : is_monoid_hom (free.map f) :=
{ map_mul := λ x y,
by simp only [free.map, free_monoid.mul_def, list.map_append, free_add_monoid.add_def],
map_one := by simp only [free.map, free_monoid.one_def, list.map, free_add_monoid.zero_def] }

lemma fold_foldl (f : β → α → β) :
is_monoid_hom (foldl.of_free_monoid f) :=
{ map_one := rfl,
map_mul := by intros; simp only [free_monoid.mul_def, foldl.of_free_monoid, flip, unop_op,
list.foldl_append, op_inj]; refl }

lemma foldl.unop_of_free_monoid (f : β → α → β) (xs : free_monoid α) (a : β) :
unop (foldl.of_free_monoid f xs) a = list.foldl f a xs := rfl

lemma fold_foldr (f : α → β → β) :
is_monoid_hom (foldr.of_free_monoid f) :=
{ map_one := rfl,
map_mul :=
begin
intros,
simp only [free_monoid.mul_def, foldr.of_free_monoid, list.foldr_append, flip],
refl
end }

variables (m : Type u → Type u) [monad m] [is_lawful_monad m]

@[simp]
lemma mfoldl.unop_of_free_monoid (f : β → α → m β) (xs : free_monoid α) (a : β) :
unop (mfoldl.of_free_monoid f xs) a = list.mfoldl f a xs := rfl

lemma fold_mfoldl (f : β → α → m β) :
is_monoid_hom (mfoldl.of_free_monoid f) :=
{ map_one := rfl,
map_mul := by intros; apply unop_injective; ext; apply list.mfoldl_append }

lemma fold_mfoldr (f : α → β → m β) :
is_monoid_hom (mfoldr.of_free_monoid f) :=
{ map_one := rfl,
map_mul := by intros; ext; apply list.mfoldr_append }

variables {t : Type u → Type u} [traversable t] [is_lawful_traversable t]
open is_lawful_traversable

lemma fold_map_hom
[monoid α] [monoid β] {f : α → β} (hf : is_monoid_hom f)
[monoid α] [monoid β] (f : α →* β)
(g : γ → α) (x : t γ) :
f (fold_map g x) = fold_map (f ∘ g) x :=
calc f (fold_map g x)
= f (traverse (const.mk' ∘ g) x) : rfl
... = (map_fold hf).app _ (traverse (const.mk' ∘ g) x) : rfl
... = traverse ((map_fold hf).app _ ∘ (const.mk' ∘ g)) x : naturality (map_fold hf) _ _
= f (traverse (const.mk' ∘ g) x) : rfl
... = (map_fold f).app _ (traverse (const.mk' ∘ g) x) : rfl
... = traverse ((map_fold f).app _ ∘ (const.mk' ∘ g)) x :
naturality (map_fold f) _ _
... = fold_map (f ∘ g) x : rfl

lemma fold_map_hom_free
[monoid β] {f : free_monoid α → β} (hf : is_monoid_hom f) (x : t α) :
[monoid β] (f : free_monoid α →* β) (x : t α) :
f (fold_map free.mk x) = fold_map (f ∘ free.mk) x :=
fold_map_hom hf _ x
fold_map_hom f _ x

variable {m}

Expand Down Expand Up @@ -281,12 +267,12 @@ lemma foldr.of_free_monoid_comp_free_mk (f : β → α → α) :
@[simp]
lemma mfoldl.of_free_monoid_comp_free_mk {m} [monad m] [is_lawful_monad m] (f : α → β → m α) :
mfoldl.of_free_monoid f ∘ free.mk = mfoldl.mk ∘ flip f :=
by ext; simp only [(∘), mfoldl.of_free_monoid, mfoldl.mk, flip, fold_mfoldl_cons]; refl
by ext; simp [(∘), mfoldl.of_free_monoid, mfoldl.mk, flip, fold_mfoldl_cons]; refl

@[simp]
lemma mfoldr.of_free_monoid_comp_free_mk {m} [monad m] [is_lawful_monad m] (f : β → α → m α) :
mfoldr.of_free_monoid f ∘ free.mk = mfoldr.mk ∘ f :=
by { ext, simp only [(∘), mfoldr.of_free_monoid, mfoldr.mk, flip, fold_mfoldr_cons] }
by { ext, simp [(∘), mfoldr.of_free_monoid, mfoldr.mk, flip, fold_mfoldr_cons] }

lemma to_list_spec (xs : t α) :
to_list xs = (fold_map free.mk xs : free_monoid _) :=
Expand All @@ -296,11 +282,9 @@ calc fold_map free.mk xs
... = (list.foldr cons [] (fold_map free.mk xs).reverse).reverse
: by simp only [list.foldr_eta]
... = (unop (foldl.of_free_monoid (flip cons) (fold_map free.mk xs)) []).reverse
: by simp only [flip,list.foldr_reverse,foldl.of_free_monoid, unop_op]
: by simp [flip,list.foldr_reverse,foldl.of_free_monoid, unop_op]
... = to_list xs : begin
have : is_monoid_hom (foldl.of_free_monoid (flip $ @cons α)),
{ apply fold_foldl },
rw fold_map_hom_free this,
rw fold_map_hom_free (foldl.of_free_monoid (flip $ @cons α)),
simp only [to_list, foldl, list.reverse_inj, foldl.get,
foldl.of_free_monoid_comp_free_mk],
all_goals { apply_instance }
Expand All @@ -314,21 +298,21 @@ lemma foldl_to_list (f : α → β → α) (xs : t β) (x : α) :
foldl f x xs = list.foldl f x (to_list xs) :=
begin
rw ← foldl.unop_of_free_monoid,
simp only [foldl, to_list_spec, fold_map_hom_free (fold_foldl f),
simp only [foldl, to_list_spec, fold_map_hom_free,
foldl.of_free_monoid_comp_free_mk, foldl.get]
end

lemma foldr_to_list (f : α → β → β) (xs : t α) (x : β) :
foldr f x xs = list.foldr f x (to_list xs) :=
begin
change _ = foldr.of_free_monoid _ _ _,
simp only [foldr, to_list_spec, fold_map_hom_free (fold_foldr f),
simp only [foldr, to_list_spec, fold_map_hom_free,
foldr.of_free_monoid_comp_free_mk, foldr.get]
end

lemma to_list_map (f : α → β) (xs : t α) :
to_list (f <$> xs) = f <$> to_list xs := by
{ simp only [to_list_spec,free.map_eq_map,fold_map_hom (free.map.is_monoid_hom f), fold_map_map];
{ simp only [to_list_spec,free.map_eq_map,fold_map_hom (free.map f), fold_map_map];
refl }

@[simp] theorem foldl_map (g : β → γ) (f : α → γ → α) (a : α) (l : t β) :
Expand Down Expand Up @@ -370,15 +354,15 @@ variables {m : Type u → Type u} [monad m] [is_lawful_monad m]
lemma mfoldl_to_list {f : α → β → m α} {x : α} {xs : t β} :
mfoldl f x xs = list.mfoldl f x (to_list xs) :=
calc mfoldl f x xs = unop (mfoldl.of_free_monoid f (to_list xs)) x :
by simp only [mfoldl, to_list_spec, fold_map_hom_free (fold_mfoldl (λ (β : Type u), m β) f),
by simp only [mfoldl, to_list_spec, fold_map_hom_free (mfoldl.of_free_monoid f),
mfoldl.of_free_monoid_comp_free_mk, mfoldl.get]
... = list.mfoldl f x (to_list xs) : by simp only [mfoldl.of_free_monoid, unop_op, flip]
... = list.mfoldl f x (to_list xs) : by simp [mfoldl.of_free_monoid, unop_op, flip]

lemma mfoldr_to_list (f : α → β → m β) (x : β) (xs : t α) :
mfoldr f x xs = list.mfoldr f x (to_list xs) :=
begin
change _ = mfoldr.of_free_monoid f (to_list xs) x,
simp only [mfoldr, to_list_spec, fold_map_hom_free (fold_mfoldr (λ (β : Type u), m β) f),
simp only [mfoldr, to_list_spec, fold_map_hom_free (mfoldr.of_free_monoid f),
mfoldr.of_free_monoid_comp_free_mk, mfoldr.get]
end

Expand Down