From 98c34d9e6440835f09908394d11f1814c591c635 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pol=27tta=20/=20Miyahara=20K=C5=8D?= Date: Wed, 21 Jun 2023 05:19:21 +0000 Subject: [PATCH] feat: port Control.Bitraversable.Instances (#5225) --- Mathlib.lean | 1 + Mathlib/Control/Bitraversable/Basic.lean | 12 +- Mathlib/Control/Bitraversable/Instances.lean | 162 +++++++++++++++++++ Mathlib/Control/Bitraversable/Lemmas.lean | 2 +- 4 files changed, 170 insertions(+), 7 deletions(-) create mode 100644 Mathlib/Control/Bitraversable/Instances.lean diff --git a/Mathlib.lean b/Mathlib.lean index 20100ee1004b7..ec09d435b2af0 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Control/Bitraversable/Basic.lean b/Mathlib/Control/Bitraversable/Basic.lean index d0a0d81f86fc6..9a76de55334b7 100644 --- a/Mathlib/Control/Bitraversable/Basic.lean +++ b/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,11 +78,11 @@ 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 @@ -90,4 +90,4 @@ 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) diff --git a/Mathlib/Control/Bitraversable/Instances.lean b/Mathlib/Control/Bitraversable/Instances.lean new file mode 100644 index 0000000000000..711e2b7266c86 --- /dev/null +++ b/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: + +## 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 diff --git a/Mathlib/Control/Bitraversable/Lemmas.lean b/Mathlib/Control/Bitraversable/Lemmas.lean index 8adcc26d56729..8008a5710f379 100644 --- a/Mathlib/Control/Bitraversable/Lemmas.lean +++ b/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 :=