From e5fdf1caa4a0308ecfa6d8ac06a7988bb5b1da43 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Thu, 23 May 2024 10:17:11 +0100 Subject: [PATCH 1/2] More list properties about `catMaybes/mapMaybe` - Follow-up to PR #2361 - Ported from my [formal-prelude](https://github.com/omelkonian/formal-prelude/tree/c10fe94876a7378088f2e4cf68d9b18858dcc256) --- CHANGELOG.md | 100 ++++++++++------- src/Data/List/Properties.agda | 104 ++++++++++++------ .../Permutation/Propositional/Properties.agda | 25 ++++- .../Binary/Permutation/Setoid/Properties.agda | 2 +- .../Permutation/Setoid/Properties/Maybe.agda | 72 ++++++++++++ 5 files changed, 225 insertions(+), 78 deletions(-) create mode 100644 src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 30dc56b3d0..014c1b4056 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -343,47 +343,55 @@ Additions to existing modules * In `Data.List.Properties`: ```agda - length-catMaybes : length (catMaybes xs) ≤ length xs - applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n) - applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n) - upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n) - downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n) - reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse - reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n - reverse-upTo : reverse (upTo n) ≡ downFrom n - reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n - reverse-downFrom : reverse (downFrom n) ≡ upTo n - mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g) - map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f) - align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys) - zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys) - unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g) - map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f) - unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip - splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n - uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons - last-map : last ∘ map f ≗ map f ∘ last - tail-map : tail ∘ map f ≗ map (map f) ∘ tail - mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g - zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as - unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g - foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x - alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs - alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs - align-flip : align xs ys ≡ map swap (align ys xs) - zip-flip : zip xs ys ≡ map swap (zip ys xs) - unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f - unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip - take-take : take n (take m xs) ≡ take (n ⊓ m) xs - take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs) - zip-unzip : uncurry′ zip ∘ unzip ≗ id - unzipWith-zipWith : f ∘ uncurry′ g ≗ id → length xs ≡ length ys → unzipWith f (zipWith g xs ys) ≡ (xs , ys) - unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys) - mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys - unzipWith-++ : unzipWith f (xs ++ ys) ≡ zip _++_ _++_ (unzipWith f xs) (unzipWith f ys) - catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe - catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys - map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) + length-catMaybes : length (catMaybes xs) ≤ length xs + applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n) + applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n) + upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n) + downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n) + reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse + reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n + reverse-upTo : reverse (upTo n) ≡ downFrom n + reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n + reverse-downFrom : reverse (downFrom n) ≡ upTo n + mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g) + map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f) + align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys) + zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys) + unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g) + map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f) + unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip + splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n + uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons + last-map : last ∘ map f ≗ map f ∘ last + tail-map : tail ∘ map f ≗ map (map f) ∘ tail + mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g + zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as + unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g + foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x + alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs + alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs + align-flip : align xs ys ≡ map swap (align ys xs) + zip-flip : zip xs ys ≡ map swap (zip ys xs) + unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f + unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip + take-take : take n (take m xs) ≡ take (n ⊓ m) xs + take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs) + zip-unzip : uncurry′ zip ∘ unzip ≗ id + unzipWith-zipWith : f ∘ uncurry′ g ≗ id → + length xs ≡ length ys → + unzipWith f (zipWith g xs ys) ≡ (xs , ys) + unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys) + mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys + unzipWith-++ : unzipWith f (xs ++ ys) ≡ + zip _++_ _++_ (unzipWith f xs) (unzipWith f ys) + catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe + catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys + map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) + Any-catMaybes⁺ : Any (M.Any P) xs → Any P (catMaybes xs) + mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs + mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ [] + mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs + mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ [] ``` * In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: @@ -496,7 +504,15 @@ Additions to existing modules * Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`: ```agda - product-↭ : product Preserves _↭_ ⟶ _≡_ + product-↭ : product Preserves _↭_ ⟶ _≡_ + catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys + mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys + ``` + +* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`: + ```agda + catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys + mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys ``` * Added new functions in `Data.String.Base`: diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index ab9b0241e1..393ef3832e 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -23,14 +23,15 @@ open import Data.List.Base as List open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.Any using (Any; here; there) -open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe) +open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) +open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny) open import Data.Nat.Base open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n) open import Data.Nat.Properties open import Data.Product.Base as Product using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>) import Data.Product.Relation.Unary.All as Product using (All) -open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Data.Sum using (_⊎_; inj₁; inj₂; isInj₁; isInj₂) open import Data.These.Base as These using (These; this; that; these) open import Data.Fin.Properties using (toℕ-cast) open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip) @@ -48,12 +49,11 @@ open import Relation.Unary using (Pred; Decidable; ∁) open import Relation.Unary.Properties using (∁?) import Data.Nat.GeneralisedArithmetic as ℕ - open ≡-Reasoning private variable - a b c d e p : Level + a b c d e p ℓ : Level A : Set a B : Set b C : Set c @@ -122,32 +122,6 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq = let fx≡fy , fxs≡fys = ∷-injective eq in cong₂ _∷_ (finj fx≡fy) (map-injective finj fxs≡fys) ------------------------------------------------------------------------- --- catMaybes - -catMaybes-concatMap : catMaybes {A = A} ≗ concatMap fromMaybe -catMaybes-concatMap [] = refl -catMaybes-concatMap (just x ∷ xs) = cong (x ∷_) (catMaybes-concatMap xs) -catMaybes-concatMap (nothing ∷ xs) = catMaybes-concatMap xs - -length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs -length-catMaybes [] = ≤-refl -length-catMaybes (just x ∷ xs) = s≤s (length-catMaybes xs) -length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n (length-catMaybes xs) - -catMaybes-++ : (xs ys : List (Maybe A)) → - catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys -catMaybes-++ [] ys = refl -catMaybes-++ (just x ∷ xs) ys = cong (x ∷_) (catMaybes-++ xs ys) -catMaybes-++ (nothing ∷ xs) ys = catMaybes-++ xs ys - -module _ (f : A → B) where - - map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) - map-catMaybes [] = refl - map-catMaybes (just x ∷ xs) = cong (f x ∷_) (map-catMaybes xs) - map-catMaybes (nothing ∷ xs) = map-catMaybes xs - ------------------------------------------------------------------------ -- _++_ @@ -741,12 +715,44 @@ map-concatMap f g xs = begin ∎ ------------------------------------------------------------------------ --- mapMaybe +-- catMaybes -module _ {f g : A → Maybe B} where +catMaybes-concatMap : catMaybes {A = A} ≗ concatMap fromMaybe +catMaybes-concatMap [] = refl +catMaybes-concatMap (mx ∷ xs) with ih ← catMaybes-concatMap xs | mx +... | just x = cong (x ∷_) ih +... | nothing = ih - mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g - mapMaybe-cong f≗g = cong catMaybes ∘ map-cong f≗g +length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs +length-catMaybes [] = ≤-refl +length-catMaybes (mx ∷ xs) with ih ← length-catMaybes xs | mx +... | just _ = s≤s ih +... | nothing = m≤n⇒m≤1+n ih + +catMaybes-++ : (xs ys : List (Maybe A)) → + catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys +catMaybes-++ [] _ = refl +catMaybes-++ (mx ∷ xs) ys with ih ← catMaybes-++ xs ys | mx +... | just x = cong (x ∷_) ih +... | nothing = ih + +map-catMaybes : (f : A → B) → map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) +map-catMaybes _ [] = refl +map-catMaybes f (mx ∷ xs) with ih ← map-catMaybes f xs | mx +... | just x = cong (f x ∷_) ih +... | nothing = ih + +Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)} → + Any (MAny P) xs → Any P (catMaybes xs) +Any-catMaybes⁺ {xs = nothing ∷ xs} (there x∈) = Any-catMaybes⁺ x∈ +Any-catMaybes⁺ {xs = just x ∷ xs} (here (just px)) = here px +Any-catMaybes⁺ {xs = just x ∷ xs} (there x∈) = there $ Any-catMaybes⁺ x∈ + +------------------------------------------------------------------------ +-- mapMaybe + +mapMaybe-cong : {f g : A → Maybe B} → f ≗ g → mapMaybe f ≗ mapMaybe g +mapMaybe-cong f≗g = cong catMaybes ∘ map-cong f≗g mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs mapMaybe-just [] = refl @@ -792,6 +798,36 @@ module _ (g : B → C) (f : A → Maybe B) where mapMaybe (Maybe.map g) (map f xs) ≡⟨ mapMaybe-map _ f xs ⟩ mapMaybe (Maybe.map g ∘ f) xs ∎ +-- embedding-projection pairs +module _ {proj : B → Maybe A} {emb : A → B} where + mapMaybe-map-retract : proj ∘ emb ≗ just → mapMaybe proj ∘ map emb ≗ id + mapMaybe-map-retract retract xs = begin + mapMaybe proj (map emb xs) ≡⟨ mapMaybe-map _ _ xs ⟩ + mapMaybe (proj ∘ emb) xs ≡⟨ mapMaybe-cong retract xs ⟩ + mapMaybe just xs ≡⟨ mapMaybe-just _ ⟩ + xs ∎ + +module _ {proj : C → Maybe B} {emb : A → C} where + mapMaybe-map-none : proj ∘ emb ≗ const nothing → mapMaybe proj ∘ map emb ≗ const [] + mapMaybe-map-none retract xs = begin + mapMaybe proj (map emb xs) ≡⟨ mapMaybe-map _ _ xs ⟩ + mapMaybe (proj ∘ emb) xs ≡⟨ mapMaybe-cong retract xs ⟩ + mapMaybe (const nothing) xs ≡⟨ mapMaybe-nothing xs ⟩ + [] ∎ + +-- embedding-projection pairs on sums +mapMaybeIsInj₁∘mapInj₁ : (xs : List A) → mapMaybe (isInj₁ {B = B}) (map inj₁ xs) ≡ xs +mapMaybeIsInj₁∘mapInj₁ = mapMaybe-map-retract λ _ → refl + +mapMaybeIsInj₁∘mapInj₂ : (xs : List B) → mapMaybe (isInj₁ {A = A}) (map inj₂ xs) ≡ [] +mapMaybeIsInj₁∘mapInj₂ = mapMaybe-map-none λ _ → refl + +mapMaybeIsInj₂∘mapInj₂ : (xs : List B) → mapMaybe (isInj₂ {A = A}) (map inj₂ xs) ≡ xs +mapMaybeIsInj₂∘mapInj₂ = mapMaybe-map-retract λ _ → refl + +mapMaybeIsInj₂∘mapInj₁ : (xs : List A) → mapMaybe (isInj₂ {B = B}) (map inj₁ xs) ≡ [] +mapMaybeIsInj₂∘mapInj₁ = mapMaybe-map-none λ _ → refl + ------------------------------------------------------------------------ -- sum diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index d56bdb7fb3..ee767780e6 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -23,7 +23,8 @@ open import Data.List.Membership.Propositional open import Data.List.Membership.Propositional.Properties import Data.List.Properties as Lₚ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂) -open import Function.Base using (_∘_; _⟨_⟩_) +open import Data.Maybe.Base using (Maybe; just; nothing) +open import Function.Base using (_∘_; _⟨_⟩_; _$_) open import Level using (Level) open import Relation.Unary using (Pred) open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_) @@ -38,6 +39,7 @@ private a b p : Level A : Set a B : Set b + xs ys : List A ------------------------------------------------------------------------ -- Permutations of empty and singleton lists @@ -373,3 +375,24 @@ product-↭ (swap {xs} {ys} x y r) = begin (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩ y * (x * product ys) ∎ where open ≡-Reasoning + +------------------------------------------------------------------------ +-- catMaybes + +catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys +catMaybes-↭ refl = refl +catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys) +catMaybes-↭ (prep mx xs↭) with ih ← catMaybes-↭ xs↭ | mx +... | nothing = ih +... | just x = prep x ih +catMaybes-↭ (swap mx my xs↭) with ih ← catMaybes-↭ xs↭ | mx | my +... | nothing | nothing = ih +... | nothing | just y = prep y ih +... | just x | nothing = prep x ih +... | just x | just y = swap x y ih + +------------------------------------------------------------------------ +-- mapMaybe + +mapMaybe-↭ : (f : A → Maybe B) → xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys +mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 57c9100e02..0440e3a3b6 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -144,7 +144,7 @@ steps-respʳ ys≋xs (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_) ------------------------------------------------------------------------ -- map -module _ (T : Setoid b ℓ) where +module _ {ℓ} (T : Setoid b ℓ) where open Setoid T using () renaming (_≈_ to _≈′_) open Permutation T using () renaming (_↭_ to _↭′_) diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda new file mode 100644 index 0000000000..655f13af67 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda @@ -0,0 +1,72 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of permutations using setoid equality (on Maybe elements) +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe where + +open import Relation.Binary.Core using (_Preserves_⟶_) +open import Relation.Binary.Bundles using (Setoid) + +open import Level using (Level) +open import Function.Base using (_∘_) + +open import Data.List.Base using (catMaybes; mapMaybe) +open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_) +import Data.List.Relation.Binary.Permutation.Setoid as Permutation +open import Data.List.Relation.Binary.Permutation.Setoid.Properties + +open import Data.Maybe using (Maybe; nothing; just) +open import Data.Maybe.Relation.Binary.Pointwise using (nothing; just) + renaming (setoid to setoidᴹ) + +private + variable + a b ℓ ℓ′ : Level + +------------------------------------------------------------------------ +-- catMaybes + +module _ (sᴬ : Setoid a ℓ) where + open Setoid sᴬ using (_≈_) + open Permutation sᴬ + + private sᴹ = setoidᴹ sᴬ + open Setoid sᴹ using () renaming (_≈_ to _≈ᴹ_) + open Permutation sᴹ using () renaming (_↭_ to _↭ᴹ_) + + catMaybes-↭ : ∀ {xs ys} → xs ↭ᴹ ys → catMaybes xs ↭ catMaybes ys + catMaybes-↭ (refl p) = refl (pointwise p) + where + pointwise : ∀ {xs ys} → Pointwise _≈ᴹ_ xs ys → + Pointwise _≈_ (catMaybes xs) (catMaybes ys) + pointwise [] = [] + pointwise (just p ∷ ps) = p ∷ pointwise ps + pointwise (nothing ∷ ps) = pointwise ps + catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys) + catMaybes-↭ (prep p xs↭) with ih ← catMaybes-↭ xs↭ | p + ... | nothing = ih + ... | just x~y = prep x~y ih + catMaybes-↭ (swap p q xs↭) with ih ← catMaybes-↭ xs↭ | p | q + ... | nothing | nothing = ih + ... | nothing | just y = prep y ih + ... | just x | nothing = prep x ih + ... | just x | just y = swap x y ih + +------------------------------------------------------------------------ +-- mapMaybe + +module _ (sᴬ : Setoid a ℓ) (sᴮ : Setoid b ℓ′) where + open Setoid sᴬ using () renaming (_≈_ to _≈ᴬ_) + open Permutation sᴬ using () renaming (_↭_ to _↭ᴬ_) + open Permutation sᴮ using () renaming (_↭_ to _↭ᴮ_) + + private sᴹᴮ = setoidᴹ sᴮ + open Setoid sᴹᴮ using () renaming (_≈_ to _≈ᴹᴮ_) + + mapMaybe-↭ : ∀ {f} → f Preserves _≈ᴬ_ ⟶ _≈ᴹᴮ_ → + ∀ {xs ys} → xs ↭ᴬ ys → mapMaybe f xs ↭ᴮ mapMaybe f ys + mapMaybe-↭ pres = catMaybes-↭ sᴮ ∘ map⁺ sᴬ sᴹᴮ pres From 6cf7716167eee025dc2c43dc905792cbec20ee31 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Mon, 3 Jun 2024 13:15:25 +0100 Subject: [PATCH 2/2] Revert irrefutable `with`s for inductive hypotheses. --- src/Data/List/Properties.agda | 28 ++++++++----------- .../Permutation/Propositional/Properties.agda | 18 ++++++------ .../Permutation/Setoid/Properties/Maybe.agda | 18 ++++++------ 3 files changed, 28 insertions(+), 36 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 393ef3832e..82d3f4f6b6 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -718,29 +718,25 @@ map-concatMap f g xs = begin -- catMaybes catMaybes-concatMap : catMaybes {A = A} ≗ concatMap fromMaybe -catMaybes-concatMap [] = refl -catMaybes-concatMap (mx ∷ xs) with ih ← catMaybes-concatMap xs | mx -... | just x = cong (x ∷_) ih -... | nothing = ih +catMaybes-concatMap [] = refl +catMaybes-concatMap (just x ∷ xs) = cong (x ∷_) $ catMaybes-concatMap xs +catMaybes-concatMap (nothing ∷ xs) = catMaybes-concatMap xs length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs -length-catMaybes [] = ≤-refl -length-catMaybes (mx ∷ xs) with ih ← length-catMaybes xs | mx -... | just _ = s≤s ih -... | nothing = m≤n⇒m≤1+n ih +length-catMaybes [] = ≤-refl +length-catMaybes (just _ ∷ xs) = s≤s $ length-catMaybes xs +length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n $ length-catMaybes xs catMaybes-++ : (xs ys : List (Maybe A)) → catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys -catMaybes-++ [] _ = refl -catMaybes-++ (mx ∷ xs) ys with ih ← catMaybes-++ xs ys | mx -... | just x = cong (x ∷_) ih -... | nothing = ih +catMaybes-++ [] _ = refl +catMaybes-++ (just x ∷ xs) ys = cong (x ∷_) $ catMaybes-++ xs ys +catMaybes-++ (nothing ∷ xs) ys = catMaybes-++ xs ys map-catMaybes : (f : A → B) → map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) -map-catMaybes _ [] = refl -map-catMaybes f (mx ∷ xs) with ih ← map-catMaybes f xs | mx -... | just x = cong (f x ∷_) ih -... | nothing = ih +map-catMaybes _ [] = refl +map-catMaybes f (just x ∷ xs) = cong (f x ∷_) $ map-catMaybes f xs +map-catMaybes f (nothing ∷ xs) = map-catMaybes f xs Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)} → Any (MAny P) xs → Any P (catMaybes xs) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index ee767780e6..6fe439ed03 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -380,16 +380,14 @@ product-↭ (swap {xs} {ys} x y r) = begin -- catMaybes catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys -catMaybes-↭ refl = refl -catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys) -catMaybes-↭ (prep mx xs↭) with ih ← catMaybes-↭ xs↭ | mx -... | nothing = ih -... | just x = prep x ih -catMaybes-↭ (swap mx my xs↭) with ih ← catMaybes-↭ xs↭ | mx | my -... | nothing | nothing = ih -... | nothing | just y = prep y ih -... | just x | nothing = prep x ih -... | just x | just y = swap x y ih +catMaybes-↭ refl = refl +catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys) +catMaybes-↭ (prep nothing xs↭) = catMaybes-↭ xs↭ +catMaybes-↭ (prep (just x) xs↭) = prep x $ catMaybes-↭ xs↭ +catMaybes-↭ (swap nothing nothing xs↭) = catMaybes-↭ xs↭ +catMaybes-↭ (swap nothing (just y) xs↭) = prep y $ catMaybes-↭ xs↭ +catMaybes-↭ (swap (just x) nothing xs↭) = prep x $ catMaybes-↭ xs↭ +catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭ ------------------------------------------------------------------------ -- mapMaybe diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda index 655f13af67..e453a599bb 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda @@ -12,7 +12,7 @@ open import Relation.Binary.Core using (_Preserves_⟶_) open import Relation.Binary.Bundles using (Setoid) open import Level using (Level) -open import Function.Base using (_∘_) +open import Function.Base using (_∘_; _$_) open import Data.List.Base using (catMaybes; mapMaybe) open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_) @@ -46,15 +46,13 @@ module _ (sᴬ : Setoid a ℓ) where pointwise [] = [] pointwise (just p ∷ ps) = p ∷ pointwise ps pointwise (nothing ∷ ps) = pointwise ps - catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys) - catMaybes-↭ (prep p xs↭) with ih ← catMaybes-↭ xs↭ | p - ... | nothing = ih - ... | just x~y = prep x~y ih - catMaybes-↭ (swap p q xs↭) with ih ← catMaybes-↭ xs↭ | p | q - ... | nothing | nothing = ih - ... | nothing | just y = prep y ih - ... | just x | nothing = prep x ih - ... | just x | just y = swap x y ih + catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys) + catMaybes-↭ (prep nothing xs↭) = catMaybes-↭ xs↭ + catMaybes-↭ (prep (just x~y) xs↭) = prep x~y $ catMaybes-↭ xs↭ + catMaybes-↭ (swap nothing nothing xs↭) = catMaybes-↭ xs↭ + catMaybes-↭ (swap nothing (just y) xs↭) = prep y $ catMaybes-↭ xs↭ + catMaybes-↭ (swap (just x) nothing xs↭) = prep x $ catMaybes-↭ xs↭ + catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭ ------------------------------------------------------------------------ -- mapMaybe