/-

Copyright (c) 2018 Simon Hudon. All rights reserved.

Released under Apache 2.0 license as described in the file LICENSE.

Authors: Simon Hudon

-/

import control.applicative

import control.traversable.basic

/-!

# Traversing collections

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.

> Any changes to this file require a corresponding PR to mathlib4.

This file proves basic properties of traversable and applicative functors and defines

`pure_transformation F`, the natural applicative transformation from the identity functor to `F`.

## References

Inspired by [The Essence of the Iterator Pattern][gibbons2009].

-/

universes u

open is_lawful_traversable

open function (hiding comp)

open functor

attribute [functor_norm] is_lawful_traversable.naturality

attribute [simp] is_lawful_traversable.id_traverse

namespace traversable

variable {t : Type u → Type u}

variables [traversable t] [is_lawful_traversable t]

variables F G : Type u → Type u

variables [applicative F] [is_lawful_applicative F]

variables [applicative G] [is_lawful_applicative G]

variables {α β γ : Type u}

variables g : α → F β

variables h : β → G γ

variables f : β → γ

/-- The natural applicative transformation from the identity functor

to `F`, defined by `pure : Π {α}, α → F α`. -/

def pure_transformation : applicative_transformation id F :=

{ app := @pure F _,

preserves_pure' := λ α x, rfl,

preserves_seq' := λ α β f x, by { simp only [map_pure, seq_pure], refl } }

@[simp] theorem pure_transformation_apply {α} (x : id α) : pure_transformation F x = pure x := rfl

variables {F G} (x : t β)

lemma map_eq_traverse_id : map f = @traverse t _ _ _ _ _ (id.mk ∘ f) :=

funext $ λ y, (traverse_eq_map_id f y).symm

theorem map_traverse (x : t α) : map f <$> traverse g x = traverse (map f ∘ g) x :=

begin

rw @map_eq_traverse_id t _ _ _ _ f,

refine (comp_traverse (id.mk ∘ f) g x).symm.trans _,

congr, apply comp.applicative_comp_id

end

theorem traverse_map (f : β → F γ) (g : α → β) (x : t α) :

traverse f (g <$> x) = traverse (f ∘ g) x :=

begin

rw @map_eq_traverse_id t _ _ _ _ g,

refine (comp_traverse f (id.mk ∘ g) x).symm.trans _,

congr, apply comp.applicative_id_comp

end

lemma pure_traverse (x : t α) : traverse pure x = (pure x : F (t α)) :=

by have : traverse pure x = pure (traverse id.mk x) :=

(naturality (pure_transformation F) id.mk x).symm;

rwa id_traverse at this

lemma id_sequence (x : t α) : sequence (id.mk <$> x) = id.mk x :=

by simp [sequence, traverse_map, id_traverse]; refl

lemma comp_sequence (x : t (F (G α))) :

sequence (comp.mk <$> x) = comp.mk (sequence <$> sequence x) :=

by simp [sequence, traverse_map]; rw ← comp_traverse; simp [map_id]

lemma naturality' (η : applicative_transformation F G) (x : t (F α)) :

η (sequence x) = sequence (@η _ <$> x) :=

by simp [sequence, naturality, traverse_map]

@[functor_norm]

lemma traverse_id : traverse id.mk = (id.mk : t α → id (t α)) :=

by { ext, exact id_traverse _ }

@[functor_norm]

lemma traverse_comp (g : α → F β) (h : β → G γ) :

traverse (comp.mk ∘ map h ∘ g) =

(comp.mk ∘ map (traverse h) ∘ traverse g : t α → comp F G (t γ)) :=

by { ext, exact comp_traverse _ _ _ }

lemma traverse_eq_map_id' (f : β → γ) : traverse (id.mk ∘ f) = id.mk ∘ (map f : t β → t γ) :=

by { ext, exact traverse_eq_map_id _ _ }

-- @[functor_norm]

lemma traverse_map' (g : α → β) (h : β → G γ) :

traverse (h ∘ g) = (traverse h ∘ map g : t α → G (t γ)) :=

by { ext, rw [comp_app, traverse_map] }

lemma map_traverse' (g : α → G β) (h : β → γ) :

traverse (map h ∘ g) = (map (map h) ∘ traverse g : t α → G (t γ)) :=

by { ext, rw [comp_app, map_traverse] }

lemma naturality_pf (η : applicative_transformation F G) (f : α → F β) :

traverse (@η _ ∘ f) = @η _ ∘ (traverse f : t α → F (t β)) :=

by { ext, rw [comp_app, naturality] }

end traversable