feat: port Control.Bitraversable.Instances (#5225)

Mathlib.lean

@@ -1185,6 +1185,7 @@ import Mathlib.Control.Applicative
 import Mathlib.Control.Basic
 import Mathlib.Control.Bifunctor
 import Mathlib.Control.Bitraversable.Basic
+import Mathlib.Control.Bitraversable.Instances
 import Mathlib.Control.Bitraversable.Lemmas
 import Mathlib.Control.EquivFunctor
 import Mathlib.Control.EquivFunctor.Instances

Mathlib/Control/Bitraversable/Basic.lean

@@ -29,7 +29,7 @@ and value respectively with `Bitraverse f g : AList key val → IO (AList key' v
 ## Main definitions
 
 * `Bitraversable`: Bare typeclass to hold the `Bitraverse` function.
-* `IsLawfulBitraversable`: Typeclass for the laws of the `Bitraverse` function. Similar to
+* `LawfulBitraversable`: Typeclass for the laws of the `Bitraverse` function. Similar to
   `IsLawfulTraversable`.
 
 ## References
@@ -62,7 +62,7 @@ def bisequence {t m} [Bitraversable t] [Applicative m] {α β} : t (m α) (m β)
 open Functor
 
 /-- Bifunctor. This typeclass asserts that a lawless bitraversable bifunctor is lawful. -/
-class IsLawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t] extends
+class LawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t] extends
   LawfulBifunctor t where
   -- Porting note: need to specify `m := Id` because `id` no longer has a `Monad` instance
   id_bitraverse : ∀ {α β} (x : t α β), bitraverse (m := Id) pure pure x = pure x
@@ -78,16 +78,16 @@ class IsLawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t]
     ∀ {F G} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G]
       (η : ApplicativeTransformation F G) {α α' β β'} (f : α → F β) (f' : α' → F β') (x : t α α'),
       η (bitraverse f f' x) = bitraverse (@η _ ∘ f) (@η _ ∘ f') x
-#align is_lawful_bitraversable IsLawfulBitraversable
+#align is_lawful_bitraversable LawfulBitraversable
 
-export IsLawfulBitraversable (id_bitraverse comp_bitraverse bitraverse_eq_bimap_id)
+export LawfulBitraversable (id_bitraverse comp_bitraverse bitraverse_eq_bimap_id)
 
-open IsLawfulBitraversable
+open LawfulBitraversable
 
 attribute [higher_order bitraverse_id_id] id_bitraverse
 
 attribute [higher_order bitraverse_comp] comp_bitraverse
 
 attribute [higher_order] binaturality bitraverse_eq_bimap_id
 
-export IsLawfulBitraversable (bitraverse_id_id bitraverse_comp)
+export LawfulBitraversable (bitraverse_id_id bitraverse_comp)

Mathlib/Control/Bitraversable/Instances.lean

@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon
+
+! This file was ported from Lean 3 source module control.bitraversable.instances
+! leanprover-community/mathlib commit 1e7f6b9a746d445350890f3ad5236f3fc686c103
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Control.Bitraversable.Lemmas
+import Mathlib.Control.Traversable.Lemmas
+
+/-!
+# Bitraversable instances
+
+This file provides `Bitraversable` instances for concrete bifunctors:
+* `Prod`
+* `Sum`
+* `Functor.Const`
+* `flip`
+* `Function.bicompl`
+* `Function.bicompr`
+
+## References
+
+* Hackage: <https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html>
+
+## Tags
+
+traversable bitraversable functor bifunctor applicative
+-/
+
+
+universe u v w
+
+variable {t : Type u → Type u → Type u} [Bitraversable t]
+
+section
+
+variable {F : Type u → Type u} [Applicative F]
+
+/-- The bitraverse function for `α × β`. -/
+def Prod.bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') : α × β → F (α' × β')
+  | (x, y) => Prod.mk <$> f x <*> f' y
+#align prod.bitraverse Prod.bitraverse
+
+instance : Bitraversable Prod where bitraverse := @Prod.bitraverse
+
+instance : LawfulBitraversable Prod := by
+  constructor <;> intros <;> casesm _ × _ <;>
+    simp [bitraverse, Prod.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe] <;> rfl
+
+open Functor
+
+/-- The bitraverse function for `α ⊕ β`. -/
+def Sum.bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') : Sum α β → F (Sum α' β')
+  | Sum.inl x => Sum.inl <$> f x
+  | Sum.inr x => Sum.inr <$> f' x
+#align sum.bitraverse Sum.bitraverse
+
+instance : Bitraversable Sum where bitraverse := @Sum.bitraverse
+
+instance : LawfulBitraversable Sum := by
+  constructor <;> intros <;> casesm _ ⊕ _ <;>
+    simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe] <;> rfl
+
+
+set_option linter.unusedVariables false in
+/-- The bitraverse function for `Const`. It throws away the second map. -/
+@[nolint unusedArguments]
+def Const.bitraverse {F : Type u → Type u} [Applicative F] {α α' β β'} (f : α → F α')
+    (f' : β → F β') : Const α β → F (Const α' β') :=
+  f
+#align const.bitraverse Const.bitraverse
+
+instance Bitraversable.const : Bitraversable Const where bitraverse := @Const.bitraverse
+#align bitraversable.const Bitraversable.const
+
+instance LawfulBitraversable.const : LawfulBitraversable Const := by
+  constructor <;> intros <;> simp [bitraverse, Const.bitraverse, functor_norm] <;> rfl
+#align is_lawful_bitraversable.const LawfulBitraversable.const
+
+/-- The bitraverse function for `flip`. -/
+nonrec def flip.bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') :
+    flip t α β → F (flip t α' β') :=
+  (bitraverse f' f : t β α → F (t β' α'))
+#align flip.bitraverse flip.bitraverse
+
+instance Bitraversable.flip : Bitraversable (flip t) where bitraverse := @flip.bitraverse t _
+#align bitraversable.flip Bitraversable.flip
+
+open LawfulBitraversable
+
+instance LawfulBitraversable.flip [LawfulBitraversable t] : LawfulBitraversable (flip t) := by
+  constructor <;> intros <;> casesm LawfulBitraversable t <;> apply_assumption only [*]
+#align is_lawful_bitraversable.flip LawfulBitraversable.flip
+
+open Bitraversable Functor
+
+instance (priority := 10) Bitraversable.traversable {α} : Traversable (t α) where
+  traverse := @tsnd t _ _
+#align bitraversable.traversable Bitraversable.traversable
+
+instance (priority := 10) Bitraversable.isLawfulTraversable [LawfulBitraversable t] {α} :
+    IsLawfulTraversable (t α) := by
+  constructor <;> intros <;>
+    simp [traverse, comp_tsnd, functor_norm, -ApplicativeTransformation.app_eq_coe]
+  · simp [tsnd_eq_snd_id]; rfl
+  · simp [tsnd, binaturality, Function.comp, functor_norm, -ApplicativeTransformation.app_eq_coe]
+#align bitraversable.is_lawful_traversable Bitraversable.isLawfulTraversable
+
+end
+
+open Bifunctor Traversable IsLawfulTraversable LawfulBitraversable
+
+open Function (bicompl bicompr)
+
+section Bicompl
+
+variable (F G : Type u → Type u) [Traversable F] [Traversable G]
+
+/-- The bitraverse function for `bicompl`. -/
+nonrec def Bicompl.bitraverse {m} [Applicative m] {α β α' β'} (f : α → m β) (f' : α' → m β') :
+    bicompl t F G α α' → m (bicompl t F G β β') :=
+  (bitraverse (traverse f) (traverse f') : t (F α) (G α') → m _)
+#align bicompl.bitraverse Bicompl.bitraverse
+
+instance : Bitraversable (bicompl t F G) where bitraverse := @Bicompl.bitraverse t _ F G _ _
+
+instance [IsLawfulTraversable F] [IsLawfulTraversable G] [LawfulBitraversable t] :
+    LawfulBitraversable (bicompl t F G) := by
+  constructor <;> intros <;>
+    simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
+      functor_norm, -ApplicativeTransformation.app_eq_coe]
+  · simp [traverse_eq_map_id', bitraverse_eq_bimap_id]
+  · dsimp only [bicompl]
+    simp [binaturality, naturality_pf]
+
+end Bicompl
+
+section Bicompr
+
+variable (F : Type u → Type u) [Traversable F]
+
+/-- The bitraverse function for `bicompr`. -/
+nonrec def Bicompr.bitraverse {m} [Applicative m] {α β α' β'} (f : α → m β) (f' : α' → m β') :
+    bicompr F t α α' → m (bicompr F t β β') :=
+  (traverse (bitraverse f f') : F (t α α') → m _)
+#align bicompr.bitraverse Bicompr.bitraverse
+
+instance : Bitraversable (bicompr F t) where bitraverse := @Bicompr.bitraverse t _ F _
+
+instance [IsLawfulTraversable F] [LawfulBitraversable t] : LawfulBitraversable (bicompr F t) := by
+  constructor <;> intros <;>
+    simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm,
+      -ApplicativeTransformation.app_eq_coe]
+  · simp [bitraverse_eq_bimap_id', traverse_eq_map_id']; rfl
+  · dsimp only [bicompr]
+    simp [naturality, binaturality']
+
+end Bicompr

Mathlib/Control/Bitraversable/Lemmas.lean

@@ -62,7 +62,7 @@ def tsnd {α α'} (f : α → F α') : t β α → F (t β α') :=
   bitraverse pure f
 #align bitraversable.tsnd Bitraversable.tsnd
 
-variable [IsLawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G]
+variable [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G]
 
 @[higher_order tfst_id]
 theorem id_tfst : ∀ {α β} (x : t α β), tfst (F := Id) pure x = pure x :=