docs(control/traversable/lemmas): Add module docstring (#9927)

Author: YaelDillies

docs/references.bib

@@ -527,8 +527,7 @@ @InProceedings{   Gallier2011Notes
 
 @Article{         ghys87:groupes,
   author        = {Étienne Ghys},
-  title         = {Groupes d'homéomorphismes du cercle et cohomologie
-                  bornée},
+  title         = {Groupes d'homéomorphismes du cercle et cohomologie bornée},
   journal       = {Contemporary Mathematics},
   year          = 1987,
   volume        = 58,
@@ -538,6 +537,23 @@ @Article{         ghys87:groupes
   language      = {french}
 }
 
+@Article{         gibbons2009,
+  title         = {The essence of the Iterator pattern},
+  volume        = {19},
+  issn          = {0956-7968, 1469-7653},
+  url           = {https://www.cambridge.org/core/product/identifier/S0956796809007291/type/journal_article},
+  doi           = {10.1017/S0956796809007291},
+  language      = {en},
+  number        = {3-4},
+  urldate       = {2021-10-24},
+  journal       = {Journal of Functional Programming},
+  author        = {Gibbons, Jeremy and Oliveira, BRUNO C. d. S.},
+  month         = jul,
+  year          = {2009},
+  pages         = {377--402},
+}
+
+
 @Book{            GierzEtAl1980,
   author        = {Gierz, Gerhard and Hofmann, Karl Heinrich and Keimel,
                   Klaus and Lawson, Jimmie D. and Mislove, Michael W. and

src/control/traversable/lemmas.lean

@@ -2,18 +2,20 @@
 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
 
-Lemmas about traversing collections.
+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`.
 
-Inspired by:
+## References
 
-    The Essence of the Iterator Pattern
-    Jeremy Gibbons and Bruno César dos Santos Oliveira
-    In Journal of Functional Programming. Vol. 19. No. 3&4. Pages 377−402. 2009.
-    <http://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf>
+Inspired by [The Essence of the Iterator Pattern][gibbons2009].
 -/
-import control.traversable.basic
-import control.applicative
 
 universes u
 
@@ -42,19 +44,16 @@ 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; refl }
-
-@[simp] theorem pure_transformation_apply {α} (x : id α) :
-  (pure_transformation F) x = 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 :=
+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 _,
@@ -69,14 +68,12 @@ begin
   congr, apply comp.applicative_id_comp
 end
 
-lemma pure_traverse (x : t α) :
-  traverse pure x = (pure x : F (t α)) :=
+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 :=
+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 α))) :
@@ -88,34 +85,29 @@ lemma naturality' (η : applicative_transformation F G) (x : t (F α)) :
 by simp [sequence, naturality, traverse_map]
 
 @[functor_norm]
-lemma traverse_id :
-  traverse id.mk = (id.mk : t α → id (t α)) :=
-by ext; simp [id_traverse]; refl
+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; simp [comp_traverse]
+by { ext, exact comp_traverse _ _ _ }
 
-lemma traverse_eq_map_id' (f : β → γ) :
-  traverse (id.mk ∘ f) =
-  id.mk ∘ (map f : t β → t γ) :=
-by ext;rw traverse_eq_map_id
+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; simp [traverse_map]
+  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; simp [map_traverse]
+  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; simp [naturality]
+by { ext, rw [comp_app, naturality] }
 
 end traversable