From 05097c9a9d08fc3eebe28e6463af1bb30ce447ac Mon Sep 17 00:00:00 2001 From: = Date: Fri, 11 Feb 2022 10:22:02 +0000 Subject: [PATCH 1/3] Reimplement `split` and `flatten` in `Data.List.NonEmpty` --- CHANGELOG.md | 12 ++ src/Data/List/NonEmpty.agda | 160 ++---------------- src/Data/List/NonEmpty/Base.agda | 133 ++++++++++++++- src/Data/List/NonEmpty/Properties.agda | 120 ++++++++----- .../List/NonEmpty/Relation/Unary/All.agda | 39 +++++ 5 files changed, 274 insertions(+), 190 deletions(-) create mode 100644 src/Data/List/NonEmpty/Relation/Unary/All.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index c0961022da..9930d9a57b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -418,6 +418,13 @@ Non-backwards compatible changes in order to keep another new definition of `_>>=_`, located in `DiagonalBind` which is also a submodule of `Data.Vec.Base`. +* The functions `split`, `flatten` and `flatten-split` have been removed from + `Data.List.NonEmpty`. In their place `groupSequences` and `ungroupSequences` + have been added to `Data.List.NonEmpty.Base` which morally perform the same + operations but without computing the accompanying proofs. The proofs can be + found in `Data.List.NonEmpty.Properties` under the names `groupSequences-groups` + and `ungroupSequences` and `groupSequences`. + * The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)` directly to use them. @@ -766,6 +773,11 @@ New modules Data.Vec.Reflection ``` +* The `All` predicate over non-empty lists: + ``` + Data.List.NonEmpty.Relation.Unary.All + ``` + * A small library for heterogenous equational reasoning on vectors: ``` Data.Vec.Properties.Heterogeneous diff --git a/src/Data/List/NonEmpty.agda b/src/Data/List/NonEmpty.agda index 2748f69ae2..1bb7d59ab2 100644 --- a/src/Data/List/NonEmpty.agda +++ b/src/Data/List/NonEmpty.agda @@ -27,160 +27,30 @@ open import Function.Equivalence open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl) open import Relation.Nullary.Decidable using (isYes) -private - variable - a b c : Level - A : Set a - B : Set b - C : Set c - ------------------------------------------------------------------------ -- Re-export basic type and operations open import Data.List.NonEmpty.Base public ------------------------------------------------------------------------- --- More operations - --- Groups all contiguous elements for which the predicate returns the --- same result into lists. - -split : (p : A → Bool) → List A → - List (List⁺ (∃ (T ∘ p)) ⊎ List⁺ (∃ (T ∘ not ∘ p))) -split p [] = [] -split p (x ∷ xs) with p x | P.inspect p x | split p xs -... | true | P.[ px≡t ] | inj₁ xs′ ∷ xss = inj₁ ((x , Eq.from T-≡ ⟨$⟩ px≡t) ∷⁺ xs′) ∷ xss -... | true | P.[ px≡t ] | xss = inj₁ [ x , Eq.from T-≡ ⟨$⟩ px≡t ] ∷ xss -... | false | P.[ px≡f ] | inj₂ xs′ ∷ xss = inj₂ ((x , Eq.from T-not-≡ ⟨$⟩ px≡f) ∷⁺ xs′) ∷ xss -... | false | P.[ px≡f ] | xss = inj₂ [ x , Eq.from T-not-≡ ⟨$⟩ px≡f ] ∷ xss - --- If we flatten the list returned by split, then we get the list we --- started with. - -flatten : ∀ {p q} {P : A → Set p} {Q : A → Set q} → - List (List⁺ (∃ P) ⊎ List⁺ (∃ Q)) → List A -flatten = List.concat ∘ - List.map Sum.[ toList ∘ map proj₁ , toList ∘ map proj₁ ] - -flatten-split : (p : A → Bool) (xs : List A) → flatten (split p xs) ≡ xs -flatten-split p [] = refl -flatten-split p (x ∷ xs) - with p x | P.inspect p x | split p xs | flatten-split p xs -... | true | P.[ _ ] | [] | hyp = P.cong (_∷_ x) hyp -... | true | P.[ _ ] | inj₁ _ ∷ _ | hyp = P.cong (_∷_ x) hyp -... | true | P.[ _ ] | inj₂ _ ∷ _ | hyp = P.cong (_∷_ x) hyp -... | false | P.[ _ ] | [] | hyp = P.cong (_∷_ x) hyp -... | false | P.[ _ ] | inj₁ _ ∷ _ | hyp = P.cong (_∷_ x) hyp -... | false | P.[ _ ] | inj₂ _ ∷ _ | hyp = P.cong (_∷_ x) hyp - --- Groups all contiguous elements /not/ satisfying the predicate into --- lists. Elements satisfying the predicate are dropped. - -wordsBy : (A → Bool) → List A → List (List⁺ A) -wordsBy p = - List.mapMaybe Sum.[ const nothing , just ∘′ map proj₁ ] ∘ split p ------------------------------------------------------------------------ --- Examples - --- Note that these examples are simple unit tests, because the type --- checker verifies them. +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. private - module Examples {A B : Set} - (_⊕_ : A → B → B) - (_⊗_ : B → A → B) - (_⊙_ : A → A → A) - (f : A → B) - (a b c : A) - where - - hd : head (a ∷⁺ b ∷⁺ [ c ]) ≡ a - hd = refl - - tl : tail (a ∷⁺ b ∷⁺ [ c ]) ≡ b ∷ c ∷ [] - tl = refl - - mp : map f (a ∷⁺ b ∷⁺ [ c ]) ≡ f a ∷⁺ f b ∷⁺ [ f c ] - mp = refl - - right : foldr _⊕_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊕ (b ⊕ f c)) - right = refl - - right₁ : foldr₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊙ (b ⊙ c)) - right₁ = refl - - left : foldl _⊗_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ ((f a ⊗ b) ⊗ c) - left = refl - - left₁ : foldl₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c) - left₁ = refl - - ⁺app⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺++⁺ (b ∷⁺ [ c ]) ≡ - a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ] - ⁺app⁺ = refl - - ⁺app : (a ∷⁺ b ∷⁺ [ c ]) ⁺++ (b ∷ c ∷ []) ≡ - a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ] - ⁺app = refl - - app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷⁺ [ c ]) ≡ - a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ] - app⁺ = refl - - conc : concat ((a ∷⁺ b ∷⁺ [ c ]) ∷⁺ [ b ∷⁺ [ c ] ]) ≡ - a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ] - conc = refl - - rev : reverse (a ∷⁺ b ∷⁺ [ c ]) ≡ c ∷⁺ b ∷⁺ [ a ] - rev = refl - - snoc : (a ∷ b ∷ c ∷ []) ∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ] - snoc = refl - - snoc⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ] - snoc⁺ = refl - - split-true : split (const true) (a ∷ b ∷ c ∷ []) ≡ - inj₁ ((a , tt) ∷⁺ (b , tt) ∷⁺ [ c , tt ]) ∷ [] - split-true = refl - - split-false : split (const false) (a ∷ b ∷ c ∷ []) ≡ - inj₂ ((a , tt) ∷⁺ (b , tt) ∷⁺ [ c , tt ]) ∷ [] - split-false = refl - - split-≡1 : - split (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡ - inj₁ [ 1 , tt ] ∷ inj₂ ((2 , tt) ∷⁺ [ 3 , tt ]) ∷ - inj₁ ((1 , tt) ∷⁺ [ 1 , tt ]) ∷ inj₂ [ 2 , tt ] ∷ inj₁ [ 1 , tt ] ∷ - [] - split-≡1 = refl - - wordsBy-true : wordsBy (const true) (a ∷ b ∷ c ∷ []) ≡ [] - wordsBy-true = refl - - wordsBy-false : wordsBy (const false) (a ∷ b ∷ c ∷ []) ≡ - (a ∷⁺ b ∷⁺ [ c ]) ∷ [] - wordsBy-false = refl - - wordsBy-≡1 : - wordsBy (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡ - (2 ∷⁺ [ 3 ]) ∷ [ 2 ] ∷ [] - wordsBy-≡1 = refl - - ------------------------------------------------------------------------ - -- DEPRECATED - ------------------------------------------------------------------------ - -- Please use the new names as continuing support for the old names is - -- not guaranteed. + variable + a : Level + A : Set a - -- Version 1.4 +-- Version 1.4 - infixl 5 _∷ʳ'_ +infixl 5 _∷ʳ'_ - _∷ʳ'_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x) - _∷ʳ'_ = SnocView._∷ʳ′_ - {-# WARNING_ON_USAGE _∷ʳ'_ - "Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4. - Please use _∷ʳ′_ (ending in a prime) instead." - #-} +_∷ʳ'_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x) +_∷ʳ'_ = SnocView._∷ʳ′_ +{-# WARNING_ON_USAGE _∷ʳ'_ +"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4. +Please use _∷ʳ′_ (ending in a prime) instead." +#-} diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda index ed49a5ac94..76e4ded548 100644 --- a/src/Data/List/NonEmpty/Base.agda +++ b/src/Data/List/NonEmpty/Base.agda @@ -10,6 +10,7 @@ module Data.List.NonEmpty.Base where open import Level using (Level) open import Data.Bool.Base using (Bool; false; true; not; T) +open import Data.Bool.Properties using (T?) open import Data.List.Base as List using (List; []; _∷_) open import Data.Maybe.Base using (Maybe ; nothing; just) open import Data.Nat.Base as ℕ @@ -18,17 +19,19 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Data.These.Base as These using (These; this; that; these) open import Data.Vec.Base as Vec using (Vec; []; _∷_) open import Function.Base -open import Relation.Binary.PropositionalEquality.Core using (_≢_) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≢_; refl) +open import Relation.Unary using (Pred; Decidable; U; ∅) +open import Relation.Unary.Properties using (U?; ∅?) +open import Relation.Nullary using (does) private variable - a b c : Level - A : Set a - B : Set b - C : Set c + a p : Level + A B C : Set a ------------------------------------------------------------------------ --- Non-empty lists +-- Definition infixr 5 _∷_ @@ -40,6 +43,7 @@ record List⁺ (A : Set a) : Set a where open List⁺ public +------------------------------------------------------------------------ -- Basic combinators uncons : List⁺ A → A × List A @@ -85,7 +89,8 @@ map f (x ∷ xs) = (f x ∷ List.map f xs) replicate : ∀ n → n ≢ 0 → A → List⁺ A replicate n n≢0 a = a ∷ List.replicate (pred n) a --- when dropping more than the size of the length of the list, the last element remains +-- when dropping more than the size of the length of the list, the +-- last element remains drop+ : ℕ → List⁺ A → List⁺ A drop+ zero xs = xs drop+ (suc n) (x ∷ []) = x ∷ [] @@ -199,3 +204,117 @@ snocView (x ∷ .(xs List.∷ʳ y)) | xs List.∷ʳ′ y = (x ∷ xs) ∷ʳ′ y last : List⁺ A → A last xs with snocView xs last .(ys ∷ʳ y) | ys ∷ʳ′ y = y + +-- Groups all contiguous elements for which the predicate returns the +-- same result into lists. The left sums are the ones for which the +-- predicate holds, the right ones are the ones for which it doesn't. +groupSequencesᵇ : (A → Bool) → List A → List (List⁺ A ⊎ List⁺ A) +groupSequencesᵇ p [] = [] +groupSequencesᵇ p (x ∷ xs) with p x | groupSequencesᵇ p xs +... | true | inj₁ xs′ ∷ xss = inj₁ (x ∷⁺ xs′) ∷ xss +... | true | xss = inj₁ [ x ] ∷ xss +... | false | inj₂ xs′ ∷ xss = inj₂ (x ∷⁺ xs′) ∷ xss +... | false | xss = inj₂ [ x ] ∷ xss + +-- Groups all contiguous elements /not/ satisfying the predicate into +-- lists. Elements satisfying the predicate are dropped. +wordsByᵇ : (A → Bool) → List A → List (List⁺ A) +wordsByᵇ p = List.mapMaybe Sum.[ const nothing , just ] ∘ groupSequencesᵇ p + +groupSequences : {P : Pred A p} → Decidable P → List A → List (List⁺ A ⊎ List⁺ A) +groupSequences P? = groupSequencesᵇ (does ∘ P?) + +wordsBy : {P : Pred A p} → Decidable P → List A → List (List⁺ A) +wordsBy P? = wordsByᵇ (does ∘ P?) + +-- Inverse operation for groupSequences. +ungroupSequences : List (List⁺ A ⊎ List⁺ A) → List A +ungroupSequences = List.concat ∘ List.map Sum.[ toList , toList ] + +------------------------------------------------------------------------ +-- Examples + +-- Note that these examples are simple unit tests, because the type +-- checker verifies them. + +private + module Examples {A B : Set} + (_⊕_ : A → B → B) + (_⊗_ : B → A → B) + (_⊙_ : A → A → A) + (f : A → B) + (a b c : A) + where + + hd : head (a ∷⁺ b ∷⁺ [ c ]) ≡ a + hd = refl + + tl : tail (a ∷⁺ b ∷⁺ [ c ]) ≡ b ∷ c ∷ [] + tl = refl + + mp : map f (a ∷⁺ b ∷⁺ [ c ]) ≡ f a ∷⁺ f b ∷⁺ [ f c ] + mp = refl + + right : foldr _⊕_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊕ (b ⊕ f c)) + right = refl + + right₁ : foldr₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊙ (b ⊙ c)) + right₁ = refl + + left : foldl _⊗_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ ((f a ⊗ b) ⊗ c) + left = refl + + left₁ : foldl₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c) + left₁ = refl + + ⁺app⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺++⁺ (b ∷⁺ [ c ]) ≡ + a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ] + ⁺app⁺ = refl + + ⁺app : (a ∷⁺ b ∷⁺ [ c ]) ⁺++ (b ∷ c ∷ []) ≡ + a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ] + ⁺app = refl + + app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷⁺ [ c ]) ≡ + a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ] + app⁺ = refl + + conc : concat ((a ∷⁺ b ∷⁺ [ c ]) ∷⁺ [ b ∷⁺ [ c ] ]) ≡ + a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ] + conc = refl + + rev : reverse (a ∷⁺ b ∷⁺ [ c ]) ≡ c ∷⁺ b ∷⁺ [ a ] + rev = refl + + snoc : (a ∷ b ∷ c ∷ []) ∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ] + snoc = refl + + snoc⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ] + snoc⁺ = refl + + groupSequences-true : groupSequences U? (a ∷ b ∷ c ∷ []) ≡ + inj₁ (a ∷⁺ b ∷⁺ [ c ]) ∷ [] + groupSequences-true = refl + + groupSequences-false : groupSequences ∅? (a ∷ b ∷ c ∷ []) ≡ + inj₂ (a ∷⁺ b ∷⁺ [ c ]) ∷ [] + groupSequences-false = refl + + groupSequences-≡1 : + groupSequences (T? ∘ (ℕ._≡ᵇ 1)) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡ + inj₁ [ 1 ] ∷ inj₂ (2 ∷⁺ [ 3 ]) ∷ + inj₁ (1 ∷⁺ [ 1 ]) ∷ inj₂ [ 2 ] ∷ inj₁ [ 1 ] ∷ + [] + groupSequences-≡1 = refl + + wordsBy-true : wordsByᵇ (const true) (a ∷ b ∷ c ∷ []) ≡ [] + wordsBy-true = refl + + wordsBy-false : wordsByᵇ (const false) (a ∷ b ∷ c ∷ []) ≡ + (a ∷⁺ b ∷⁺ [ c ]) ∷ [] + wordsBy-false = refl + + wordsBy-≡1 : + wordsByᵇ (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡ + (2 ∷⁺ [ 3 ]) ∷ [ 2 ] ∷ [] + wordsBy-≡1 = refl diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 0cb4a8ca59..d484c2f337 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -8,65 +8,73 @@ module Data.List.NonEmpty.Properties where -open import Level using (Level) - open import Category.Monad open import Data.Nat open import Data.Nat.Properties open import Data.Maybe.Properties using (just-injective) +open import Data.Bool using (Bool; true; false) open import Data.List.Base as List using (List; []; _∷_; _++_) open import Data.List.Categorical using () renaming (monad to listMonad) open import Data.List.NonEmpty.Categorical using () renaming (monad to list⁺Monad) -open import Data.List.NonEmpty as List⁺ -import Data.List.Properties as Listₚ -open import Function +open import Data.List.NonEmpty +open import Data.List.NonEmpty.Relation.Unary.All +open import Data.List.Relation.Unary.All using ([]; _∷_) renaming (All to ListAll) +import Data.List.Relation.Unary.All using (All; []; _∷_) +import Data.List.Properties as List +open import Data.Sum.Base using (inj₁; inj₂) +open import Data.Sum.Relation.Unary.All using (inj₁; inj₂) +import Data.Sum.Relation.Unary.All as Sum using (All; inj₁; inj₂) +open import Level using (Level) +open import Function.Base open import Relation.Binary.PropositionalEquality +open import Relation.Unary using (Pred; Decidable; ∁) +open import Relation.Nullary using (¬_; does; yes; no) open ≡-Reasoning -private - open module LMo {a} = - RawMonad {f = a} listMonad - using () renaming (_>>=_ to _⋆>>=_) - open module L⁺Mo {a} = - RawMonad {f = a} list⁺Monad +private variable - a : Level + a p : Level A B C : Set a -η : ∀ {a} {A : Set a} - (xs : List⁺ A) → head xs ∷ tail xs ≡ List⁺.toList xs + open module LMo {a} = RawMonad {f = a} listMonad + using () renaming (_>>=_ to _⋆>>=_) + open module L⁺Mo {a} = RawMonad {f = a} list⁺Monad + +------------------------------------------------------------------------ +-- toList + +η : ∀ (xs : List⁺ A) → head xs ∷ tail xs ≡ toList xs η _ = refl -toList-fromList : ∀ {a} {A : Set a} x (xs : List A) → - x ∷ xs ≡ List⁺.toList (x ∷ xs) +toList-fromList : ∀ x (xs : List A) → x ∷ xs ≡ toList (x ∷ xs) toList-fromList _ _ = refl -toList-⁺++ : ∀ {a} {A : Set a} (xs : List⁺ A) ys → - List⁺.toList xs ++ ys ≡ - List⁺.toList (xs ⁺++ ys) +toList-⁺++ : ∀ (xs : List⁺ A) ys → toList xs ++ ys ≡ toList (xs ⁺++ ys) toList-⁺++ _ _ = refl -toList-⁺++⁺ : ∀ {a} {A : Set a} (xs ys : List⁺ A) → - List⁺.toList xs ++ List⁺.toList ys ≡ - List⁺.toList (xs ⁺++⁺ ys) +toList-⁺++⁺ : ∀ (xs ys : List⁺ A) → + toList xs ++ toList ys ≡ toList (xs ⁺++⁺ ys) toList-⁺++⁺ _ _ = refl -toList->>= : ∀ {ℓ} {A B : Set ℓ} - (f : A → List⁺ B) (xs : List⁺ A) → - (List⁺.toList xs ⋆>>= List⁺.toList ∘ f) ≡ - (List⁺.toList (xs >>= f)) +toList->>= : ∀ (f : A → List⁺ B) (xs : List⁺ A) → + (toList xs ⋆>>= toList ∘ f) ≡ toList (xs >>= f) toList->>= f (x ∷ xs) = begin - List.concat (List.map (List⁺.toList ∘ f) (x ∷ xs)) - ≡⟨ cong List.concat $ Listₚ.map-compose {g = List⁺.toList} (x ∷ xs) ⟩ - List.concat (List.map List⁺.toList (List.map f (x ∷ xs))) + List.concat (List.map (toList ∘ f) (x ∷ xs)) + ≡⟨ cong List.concat $ List.map-compose {g = toList} (x ∷ xs) ⟩ + List.concat (List.map toList (List.map f (x ∷ xs))) ∎ -length-++⁺ : (xs : List A) (ys : List⁺ A) → length (xs ++⁺ ys) ≡ List.length xs + length ys +------------------------------------------------------------------------ +-- _++⁺_ + +length-++⁺ : (xs : List A) (ys : List⁺ A) → + length (xs ++⁺ ys) ≡ List.length xs + length ys length-++⁺ [] ys = refl length-++⁺ (x ∷ xs) ys rewrite length-++⁺ xs ys = refl -length-++⁺-tail : (xs : List A) (ys : List⁺ A) → length (xs ++⁺ ys) ≡ suc (List.length xs + List.length (List⁺.tail ys)) +length-++⁺-tail : (xs : List A) (ys : List⁺ A) → + length (xs ++⁺ ys) ≡ suc (List.length xs + List.length (List⁺.tail ys)) length-++⁺-tail [] ys = refl length-++⁺-tail (x ∷ xs) ys rewrite length-++⁺-tail xs ys = refl @@ -74,10 +82,13 @@ length-++⁺-tail (x ∷ xs) ys rewrite length-++⁺-tail xs ys = refl ++-++⁺ [] = refl ++-++⁺ (x ∷ l) = cong (x ∷_) (cong toList (++-++⁺ l)) -++⁺-cancelˡ′ : ∀ xs ys {zs zs′ : List⁺ A} → xs ++⁺ zs ≡ ys ++⁺ zs′ → List.length xs ≡ List.length ys → zs ≡ zs′ +++⁺-cancelˡ′ : ∀ xs ys {zs zs′ : List⁺ A} → + xs ++⁺ zs ≡ ys ++⁺ zs′ → + List.length xs ≡ List.length ys → zs ≡ zs′ ++⁺-cancelˡ′ [] [] eq eqxs = eq -++⁺-cancelˡ′ (x ∷ xs) (y ∷ ys) eq eql = ++⁺-cancelˡ′ xs ys (just-injective (cong fromList (cong List⁺.tail eq))) - (suc-injective eql) +++⁺-cancelˡ′ (x ∷ xs) (y ∷ ys) eq eql = ++⁺-cancelˡ′ xs ys + (just-injective (cong fromList (cong List⁺.tail eq))) + (suc-injective eql) ++⁺-cancelˡ : ∀ xs {ys zs : List⁺ A} → xs ++⁺ ys ≡ xs ++⁺ zs → ys ≡ zs ++⁺-cancelˡ xs eq = ++⁺-cancelˡ′ xs xs eq refl @@ -87,15 +98,48 @@ drop-+-++⁺ [] ys = refl drop-+-++⁺ (x ∷ xs) ys = drop-+-++⁺ xs ys map-++⁺-commute : ∀ (f : A → B) xs ys → - map f (xs ++⁺ ys) ≡ List.map f xs ++⁺ map f ys + map f (xs ++⁺ ys) ≡ List.map f xs ++⁺ map f ys map-++⁺-commute f [] ys = refl map-++⁺-commute f (x ∷ xs) ys = cong (λ zs → f x ∷ toList zs) (map-++⁺-commute f xs ys) +------------------------------------------------------------------------ +-- map + length-map : ∀ (f : A → B) xs → length (map f xs) ≡ length xs -length-map f (_ ∷ xs) = cong suc (Listₚ.length-map f xs) +length-map f (_ ∷ xs) = cong suc (List.length-map f xs) map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g -map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (Listₚ.map-cong f≗g xs) +map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs) map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f -map-compose (x ∷ xs) = cong (_ ∷_) (Listₚ.map-compose xs) +map-compose (x ∷ xs) = cong (_ ∷_) (List.map-compose xs) + +------------------------------------------------------------------------ +-- groupSequences + +-- Groups all contiguous elements for which the predicate returns the +-- same result into lists. + +module _ {P : Pred A p} (P? : Decidable P) where + + groupSequences-groups : ∀ xs → ListAll (Sum.All (All P) (All (∁ P))) (groupSequences P? xs) + groupSequences-groups [] = [] + groupSequences-groups (x ∷ xs) with P? x | groupSequences P? xs | groupSequences-groups xs + ... | yes px | [] | hyp = inj₁ (px ∷ []) ∷ hyp + ... | yes px | inj₁ xs′ ∷ xss | inj₁ pxs ∷ pxss = inj₁ (px ∷ toListAll pxs) ∷ pxss + ... | yes px | inj₂ xs′ ∷ xss | inj₂ pxs ∷ pxss = inj₁ (px ∷ []) ∷ inj₂ pxs ∷ pxss + ... | no ¬px | [] | hyp = inj₂ (¬px ∷ []) ∷ hyp + ... | no ¬px | inj₂ xs′ ∷ xss | inj₂ pxs ∷ pxss = inj₂ (¬px ∷ toListAll pxs) ∷ pxss + ... | no ¬px | inj₁ xs′ ∷ xss | inj₁ pxs ∷ pxss = inj₂ (¬px ∷ []) ∷ inj₁ pxs ∷ pxss + + ungroupSequences-groupSequences : ∀ xs → ungroupSequences (groupSequences P? xs) ≡ xs + ungroupSequences-groupSequences [] = refl + ungroupSequences-groupSequences (x ∷ xs) + with does (P? x) | groupSequences P? xs | ungroupSequences-groupSequences xs + ... | true | [] | hyp = cong (x ∷_) hyp + ... | true | inj₁ _ ∷ _ | hyp = cong (x ∷_) hyp + ... | true | inj₂ _ ∷ _ | hyp = cong (x ∷_) hyp + ... | false | [] | hyp = cong (x ∷_) hyp + ... | false | inj₁ _ ∷ _ | hyp = cong (x ∷_) hyp + ... | false | inj₂ _ ∷ _ | hyp = cong (x ∷_) hyp + diff --git a/src/Data/List/NonEmpty/Relation/Unary/All.agda b/src/Data/List/NonEmpty/Relation/Unary/All.agda new file mode 100644 index 0000000000..881f0b6ab1 --- /dev/null +++ b/src/Data/List/NonEmpty/Relation/Unary/All.agda @@ -0,0 +1,39 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Non-empty lists where all elements satisfy a given property +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.List.NonEmpty.Relation.Unary.All where + +import Data.List.Relation.Unary.All as List +open import Data.List.Relation.Unary.All using ([]; _∷_) +open import Data.List.Base using ([]; _∷_) +open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList) +open import Level +open import Relation.Unary using (Pred) + +private + variable + a p : Level + A : Set a + P : Pred A p + +------------------------------------------------------------------------ +-- Definition + +-- Given a predicate P, then All P xs means that every element in xs +-- satisfies P. See `Relation.Unary` for an explanation of predicates. + +infixr 5 _∷_ + +data All {A : Set a} (P : Pred A p) : Pred (List⁺ A) (a ⊔ p) where + _∷_ : ∀ {x xs} (px : P x) (pxs : List.All P xs) → All P (x ∷ xs) + +------------------------------------------------------------------------ +-- Functions + +toListAll : ∀ {xs : List⁺ A} → All P xs → List.All P (toList xs) +toListAll (px ∷ pxs) = px ∷ pxs From 13ea4ad9bddeea53242ed110686ccbe6007af0b6 Mon Sep 17 00:00:00 2001 From: = Date: Mon, 7 Mar 2022 22:45:31 +0000 Subject: [PATCH 2/3] Addressed @gallais feedback and shortened sequences to seqs --- src/Data/List/NonEmpty/Base.agda | 45 ++++++++++--------- src/Data/List/NonEmpty/Properties.agda | 20 ++++----- .../List/NonEmpty/Relation/Unary/All.agda | 4 +- 3 files changed, 36 insertions(+), 33 deletions(-) diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda index 76e4ded548..2982958a35 100644 --- a/src/Data/List/NonEmpty/Base.agda +++ b/src/Data/List/NonEmpty/Base.agda @@ -208,9 +208,9 @@ last .(ys ∷ʳ y) | ys ∷ʳ′ y = y -- Groups all contiguous elements for which the predicate returns the -- same result into lists. The left sums are the ones for which the -- predicate holds, the right ones are the ones for which it doesn't. -groupSequencesᵇ : (A → Bool) → List A → List (List⁺ A ⊎ List⁺ A) -groupSequencesᵇ p [] = [] -groupSequencesᵇ p (x ∷ xs) with p x | groupSequencesᵇ p xs +groupSeqsᵇ : (A → Bool) → List A → List (List⁺ A ⊎ List⁺ A) +groupSeqsᵇ p [] = [] +groupSeqsᵇ p (x ∷ xs) with p x | groupSeqsᵇ p xs ... | true | inj₁ xs′ ∷ xss = inj₁ (x ∷⁺ xs′) ∷ xss ... | true | xss = inj₁ [ x ] ∷ xss ... | false | inj₂ xs′ ∷ xss = inj₂ (x ∷⁺ xs′) ∷ xss @@ -219,17 +219,17 @@ groupSequencesᵇ p (x ∷ xs) with p x | groupSequencesᵇ p xs -- Groups all contiguous elements /not/ satisfying the predicate into -- lists. Elements satisfying the predicate are dropped. wordsByᵇ : (A → Bool) → List A → List (List⁺ A) -wordsByᵇ p = List.mapMaybe Sum.[ const nothing , just ] ∘ groupSequencesᵇ p +wordsByᵇ p = List.mapMaybe Sum.[ const nothing , just ] ∘ groupSeqsᵇ p -groupSequences : {P : Pred A p} → Decidable P → List A → List (List⁺ A ⊎ List⁺ A) -groupSequences P? = groupSequencesᵇ (does ∘ P?) +groupSeqs : {P : Pred A p} → Decidable P → List A → List (List⁺ A ⊎ List⁺ A) +groupSeqs P? = groupSeqsᵇ (does ∘ P?) wordsBy : {P : Pred A p} → Decidable P → List A → List (List⁺ A) wordsBy P? = wordsByᵇ (does ∘ P?) -- Inverse operation for groupSequences. -ungroupSequences : List (List⁺ A ⊎ List⁺ A) → List A -ungroupSequences = List.concat ∘ List.map Sum.[ toList , toList ] +ungroupSeqs : List (List⁺ A ⊎ List⁺ A) → List A +ungroupSeqs = List.concat ∘ List.map Sum.[ toList , toList ] ------------------------------------------------------------------------ -- Examples @@ -292,20 +292,22 @@ private snoc⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ] snoc⁺ = refl - groupSequences-true : groupSequences U? (a ∷ b ∷ c ∷ []) ≡ + groupSeqs-true : groupSeqs U? (a ∷ b ∷ c ∷ []) ≡ inj₁ (a ∷⁺ b ∷⁺ [ c ]) ∷ [] - groupSequences-true = refl + groupSeqs-true = refl - groupSequences-false : groupSequences ∅? (a ∷ b ∷ c ∷ []) ≡ + groupSeqs-false : groupSeqs ∅? (a ∷ b ∷ c ∷ []) ≡ inj₂ (a ∷⁺ b ∷⁺ [ c ]) ∷ [] - groupSequences-false = refl + groupSeqs-false = refl - groupSequences-≡1 : - groupSequences (T? ∘ (ℕ._≡ᵇ 1)) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡ - inj₁ [ 1 ] ∷ inj₂ (2 ∷⁺ [ 3 ]) ∷ - inj₁ (1 ∷⁺ [ 1 ]) ∷ inj₂ [ 2 ] ∷ inj₁ [ 1 ] ∷ - [] - groupSequences-≡1 = refl + groupSeqs-≡1 : groupSeqsᵇ (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡ + inj₁ [ 1 ] ∷ + inj₂ (2 ∷⁺ [ 3 ]) ∷ + inj₁ (1 ∷⁺ [ 1 ]) ∷ + inj₂ [ 2 ] ∷ + inj₁ [ 1 ] ∷ + [] + groupSeqs-≡1 = refl wordsBy-true : wordsByᵇ (const true) (a ∷ b ∷ c ∷ []) ≡ [] wordsBy-true = refl @@ -314,7 +316,8 @@ private (a ∷⁺ b ∷⁺ [ c ]) ∷ [] wordsBy-false = refl - wordsBy-≡1 : - wordsByᵇ (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡ - (2 ∷⁺ [ 3 ]) ∷ [ 2 ] ∷ [] + wordsBy-≡1 : wordsByᵇ (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡ + (2 ∷⁺ [ 3 ]) ∷ + [ 2 ] ∷ + [] wordsBy-≡1 = refl diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index d484c2f337..4d8ecd3e37 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -115,27 +115,27 @@ map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f map-compose (x ∷ xs) = cong (_ ∷_) (List.map-compose xs) ------------------------------------------------------------------------ --- groupSequences +-- groupSeqs -- Groups all contiguous elements for which the predicate returns the -- same result into lists. module _ {P : Pred A p} (P? : Decidable P) where - groupSequences-groups : ∀ xs → ListAll (Sum.All (All P) (All (∁ P))) (groupSequences P? xs) - groupSequences-groups [] = [] - groupSequences-groups (x ∷ xs) with P? x | groupSequences P? xs | groupSequences-groups xs + groupSeqs-groups : ∀ xs → ListAll (Sum.All (All P) (All (∁ P))) (groupSeqs P? xs) + groupSeqs-groups [] = [] + groupSeqs-groups (x ∷ xs) with P? x | groupSeqs P? xs | groupSeqs-groups xs ... | yes px | [] | hyp = inj₁ (px ∷ []) ∷ hyp - ... | yes px | inj₁ xs′ ∷ xss | inj₁ pxs ∷ pxss = inj₁ (px ∷ toListAll pxs) ∷ pxss + ... | yes px | inj₁ xs′ ∷ xss | inj₁ pxs ∷ pxss = inj₁ (px ∷ toList⁺ pxs) ∷ pxss ... | yes px | inj₂ xs′ ∷ xss | inj₂ pxs ∷ pxss = inj₁ (px ∷ []) ∷ inj₂ pxs ∷ pxss ... | no ¬px | [] | hyp = inj₂ (¬px ∷ []) ∷ hyp - ... | no ¬px | inj₂ xs′ ∷ xss | inj₂ pxs ∷ pxss = inj₂ (¬px ∷ toListAll pxs) ∷ pxss + ... | no ¬px | inj₂ xs′ ∷ xss | inj₂ pxs ∷ pxss = inj₂ (¬px ∷ toList⁺ pxs) ∷ pxss ... | no ¬px | inj₁ xs′ ∷ xss | inj₁ pxs ∷ pxss = inj₂ (¬px ∷ []) ∷ inj₁ pxs ∷ pxss - ungroupSequences-groupSequences : ∀ xs → ungroupSequences (groupSequences P? xs) ≡ xs - ungroupSequences-groupSequences [] = refl - ungroupSequences-groupSequences (x ∷ xs) - with does (P? x) | groupSequences P? xs | ungroupSequences-groupSequences xs + ungroupSeqs-groupSeqs : ∀ xs → ungroupSeqs (groupSeqs P? xs) ≡ xs + ungroupSeqs-groupSeqs [] = refl + ungroupSeqs-groupSeqs (x ∷ xs) + with does (P? x) | groupSeqs P? xs | ungroupSeqs-groupSeqs xs ... | true | [] | hyp = cong (x ∷_) hyp ... | true | inj₁ _ ∷ _ | hyp = cong (x ∷_) hyp ... | true | inj₂ _ ∷ _ | hyp = cong (x ∷_) hyp diff --git a/src/Data/List/NonEmpty/Relation/Unary/All.agda b/src/Data/List/NonEmpty/Relation/Unary/All.agda index 881f0b6ab1..6d56b9ba67 100644 --- a/src/Data/List/NonEmpty/Relation/Unary/All.agda +++ b/src/Data/List/NonEmpty/Relation/Unary/All.agda @@ -35,5 +35,5 @@ data All {A : Set a} (P : Pred A p) : Pred (List⁺ A) (a ⊔ p) where ------------------------------------------------------------------------ -- Functions -toListAll : ∀ {xs : List⁺ A} → All P xs → List.All P (toList xs) -toListAll (px ∷ pxs) = px ∷ pxs +toList⁺ : ∀ {xs : List⁺ A} → All P xs → List.All P (toList xs) +toList⁺ (px ∷ pxs) = px ∷ pxs From cfb899ec2572e42c9f34b16d6cdc1f119be2ab13 Mon Sep 17 00:00:00 2001 From: = Date: Tue, 8 Mar 2022 09:31:56 +0000 Subject: [PATCH 3/3] Update CHANGELOG --- CHANGELOG.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9930d9a57b..d429239920 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -419,11 +419,11 @@ Non-backwards compatible changes which is also a submodule of `Data.Vec.Base`. * The functions `split`, `flatten` and `flatten-split` have been removed from - `Data.List.NonEmpty`. In their place `groupSequences` and `ungroupSequences` + `Data.List.NonEmpty`. In their place `groupSeqs` and `ungroupSeqs` have been added to `Data.List.NonEmpty.Base` which morally perform the same operations but without computing the accompanying proofs. The proofs can be - found in `Data.List.NonEmpty.Properties` under the names `groupSequences-groups` - and `ungroupSequences` and `groupSequences`. + found in `Data.List.NonEmpty.Properties` under the names `groupSeqs-groups` + and `ungroupSeqs` and `groupSeqs`. * The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)`