From 0dc91d8c84814b67964d21465e780ff6d4cde297 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 13 Apr 2024 10:30:07 +0100 Subject: [PATCH 01/11] `with`-free definitions plus tests --- src/Data/List/Base.agda | 8 ++++++ src/Data/List/Properties.agda | 52 +++++++++++++++++++++++++---------- 2 files changed, 45 insertions(+), 15 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 8b988c646d..4dfefc6748 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -49,6 +49,14 @@ map : (A → B) → List A → List B map f [] = [] map f (x ∷ xs) = f x ∷ map f xs +catMaybes′ : List (Maybe A) → List A +catMaybes′ [] = [] +catMaybes′ (nothing ∷ xs) = catMaybes′ xs +catMaybes′ (just x ∷ xs) = x ∷ catMaybes′ xs + +mapMaybe′ : (A → Maybe B) → List A → List B +mapMaybe′ p = catMaybes′ ∘ map p + mapMaybe : (A → Maybe B) → List A → List B mapMaybe p [] = [] mapMaybe p (x ∷ xs) with p x diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 2d3c9e20e0..19827268cf 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -62,16 +62,16 @@ private module _ {x y : A} {xs ys : List A} where - ∷-injective : x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys + ∷-injective : x ∷ xs ≡ y ∷ ys → x ≡ y × xs ≡ ys ∷-injective refl = (refl , refl) - ∷-injectiveˡ : x ∷ xs ≡ y List.∷ ys → x ≡ y + ∷-injectiveˡ : x ∷ xs ≡ y ∷ ys → x ≡ y ∷-injectiveˡ refl = refl - ∷-injectiveʳ : x ∷ xs ≡ y List.∷ ys → xs ≡ ys + ∷-injectiveʳ : x ∷ xs ≡ y ∷ ys → xs ≡ ys ∷-injectiveʳ refl = refl - ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x List.∷ xs ≡ y ∷ ys) + ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y ∷ ys) ∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys) ≡-dec : DecidableEquality A → DecidableEquality (List A) @@ -122,28 +122,50 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq = ------------------------------------------------------------------------ -- mapMaybe +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) + +catMaybesTest : catMaybes {A = A} ≗ catMaybes′ +catMaybesTest [] = refl +catMaybesTest (just x ∷ xs) = cong (x ∷_) (catMaybesTest xs) +catMaybesTest (nothing ∷ xs) = catMaybesTest xs + +mapMaybeTest : (p : A → Maybe B) → mapMaybe p ≗ mapMaybe′ p +mapMaybeTest p [] = refl +mapMaybeTest p (x ∷ xs) with ih ← mapMaybeTest p xs | p x +... | nothing = ih +... | just y = cong (y ∷_) ih + mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs mapMaybe-just [] = refl mapMaybe-just (x ∷ xs) = cong (x ∷_) (mapMaybe-just xs) +mapMaybe′-just : (xs : List A) → mapMaybe′ just xs ≡ xs +mapMaybe′-just [] = refl +mapMaybe′-just (x ∷ xs) = cong (x ∷_) (mapMaybe′-just xs) + mapMaybe-nothing : (xs : List A) → - mapMaybe {B = A} (λ _ → nothing) xs ≡ [] + mapMaybe (λ _ → nothing {A = A}) xs ≡ [] mapMaybe-nothing [] = refl mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs +mapMaybe′-nothing : (xs : List A) → + mapMaybe′ (λ _ → nothing {A = A}) xs ≡ [] +mapMaybe′-nothing [] = refl +mapMaybe′-nothing (x ∷ xs) = mapMaybe′-nothing xs + module _ (f : A → Maybe B) where - mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f) - mapMaybe-concatMap [] = refl + mapMaybe-concatMap : mapMaybe′ f ≗ concatMap (fromMaybe ∘ f) + mapMaybe-concatMap [] = refl mapMaybe-concatMap (x ∷ xs) with ih ← mapMaybe-concatMap xs | f x ... | just y = cong (y ∷_) ih ... | nothing = ih - length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs - length-mapMaybe [] = z≤n - length-mapMaybe (x ∷ xs) with ih ← length-mapMaybe xs | f x - ... | just y = s≤s ih - ... | nothing = m≤n⇒m≤1+n ih + length-mapMaybe : ∀ xs → length (mapMaybe′ f xs) ≤ length xs + length-mapMaybe xs = ≤-trans (length-catMaybes (map f xs)) (≤-reflexive (length-map f xs)) ------------------------------------------------------------------------ -- _++_ @@ -175,14 +197,14 @@ module _ {A : Set a} where ++-identityʳ-unique : ∀ (xs : List A) {ys} → xs ≡ xs ++ ys → ys ≡ [] ++-identityʳ-unique [] refl = refl ++-identityʳ-unique (x ∷ xs) eq = - ++-identityʳ-unique xs (proj₂ (∷-injective eq)) + ++-identityʳ-unique xs (∷-injectiveʳ eq) ++-identityˡ-unique : ∀ {xs} (ys : List A) → xs ≡ ys ++ xs → ys ≡ [] ++-identityˡ-unique [] _ = refl ++-identityˡ-unique {xs = x ∷ xs} (y ∷ ys) eq with ++-identityˡ-unique (ys ++ [ x ]) (begin - xs ≡⟨ proj₂ (∷-injective eq) ⟩ - ys ++ x ∷ xs ≡⟨ sym (++-assoc ys [ x ] xs) ⟩ + xs ≡⟨ ∷-injectiveʳ eq ⟩ + ys ++ x ∷ xs ≡⟨ ++-assoc ys [ x ] xs ⟨ (ys ++ [ x ]) ++ xs ∎) ++-identityˡ-unique {xs = x ∷ xs} (y ∷ [] ) eq | () ++-identityˡ-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | () From 80d71f305d005efc8cf9991e23aa6ffb6ee93436 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 13 Apr 2024 10:33:23 +0100 Subject: [PATCH 02/11] `CHANGELOG` --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 469c926af8..e7d776393a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -273,6 +273,7 @@ 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) From 738d893bdec1bfd2bb0b4be82e24e1f824b3bf9a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 13 Apr 2024 16:19:50 +0100 Subject: [PATCH 03/11] use `foldr` on @JacquesCarette 's solution --- src/Data/List/Base.agda | 11 ++++++++--- src/Data/List/Properties.agda | 2 +- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 4dfefc6748..e50657180b 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -50,9 +50,8 @@ map f [] = [] map f (x ∷ xs) = f x ∷ map f xs catMaybes′ : List (Maybe A) → List A -catMaybes′ [] = [] -catMaybes′ (nothing ∷ xs) = catMaybes′ xs -catMaybes′ (just x ∷ xs) = x ∷ catMaybes′ xs +catMaybes′ [] = [] +catMaybes′ (x ∷ xs) = maybe′ _∷_ id x $ catMaybes′ xs mapMaybe′ : (A → Maybe B) → List A → List B mapMaybe′ p = catMaybes′ ∘ map p @@ -182,6 +181,12 @@ product = foldr _*_ 1 length : List A → ℕ length = foldr (const suc) 0 +catMaybes″ : List (Maybe A) → List A +catMaybes″ = foldr (maybe′ _∷_ id) [] + +mapMaybe″ : (A → Maybe B) → List A → List B +mapMaybe″ p = catMaybes″ ∘ map p + ------------------------------------------------------------------------ -- Operations for constructing lists diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 19827268cf..9c9c916ead 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -132,7 +132,7 @@ catMaybesTest [] = refl catMaybesTest (just x ∷ xs) = cong (x ∷_) (catMaybesTest xs) catMaybesTest (nothing ∷ xs) = catMaybesTest xs -mapMaybeTest : (p : A → Maybe B) → mapMaybe p ≗ mapMaybe′ p +mapMaybeTest : (p : A → Maybe B) → mapMaybe p ≗ mapMaybe″ p mapMaybeTest p [] = refl mapMaybeTest p (x ∷ xs) with ih ← mapMaybeTest p xs | p x ... | nothing = ih From 8fd4149dc3237a237da6a0020d894eb0bff4762d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 15 Apr 2024 14:36:39 +0100 Subject: [PATCH 04/11] tidied up unsolved metas --- src/Data/List/Properties.agda | 46 +++++++++++++++++------------------ 1 file changed, 22 insertions(+), 24 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 9c9c916ead..2568d96da4 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -56,23 +56,23 @@ private C : Set c D : Set d E : Set e + x y z w : A + xs ys zs ws : List A ------------------------------------------------------------------------ -- _∷_ -module _ {x y : A} {xs ys : List A} where +∷-injective : x List.∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys +∷-injective refl = (refl , refl) - ∷-injective : x ∷ xs ≡ y ∷ ys → x ≡ y × xs ≡ ys - ∷-injective refl = (refl , refl) +∷-injectiveˡ : x List.∷ xs ≡ y List.∷ ys → x ≡ y +∷-injectiveˡ refl = refl - ∷-injectiveˡ : x ∷ xs ≡ y ∷ ys → x ≡ y - ∷-injectiveˡ refl = refl +∷-injectiveʳ : x List.∷ xs ≡ y List.∷ ys → xs ≡ ys +∷-injectiveʳ refl = refl - ∷-injectiveʳ : x ∷ xs ≡ y ∷ ys → xs ≡ ys - ∷-injectiveʳ refl = refl - - ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y ∷ ys) - ∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys) +∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x List.∷ xs ≡ y List.∷ ys) +∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys) ≡-dec : DecidableEquality A → DecidableEquality (List A) ≡-dec _≟_ [] [] = yes refl @@ -147,7 +147,7 @@ mapMaybe′-just [] = refl mapMaybe′-just (x ∷ xs) = cong (x ∷_) (mapMaybe′-just xs) mapMaybe-nothing : (xs : List A) → - mapMaybe (λ _ → nothing {A = A}) xs ≡ [] + mapMaybe (λ _ → nothing {A = B}) xs ≡ [] mapMaybe-nothing [] = refl mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs @@ -1237,22 +1237,20 @@ reverse-downFrom = reverse-applyDownFrom id ------------------------------------------------------------------------ -- _∷ʳ_ -module _ {x y : A} where - - ∷ʳ-injective : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y - ∷ʳ-injective [] [] refl = (refl , refl) - ∷ʳ-injective (x ∷ xs) (y ∷ ys) eq with refl , eq′ ← ∷-injective eq - = Product.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′) - ∷ʳ-injective [] (_ ∷ _ ∷ _) () - ∷ʳ-injective (_ ∷ _ ∷ _) [] () +∷ʳ-injective : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y +∷ʳ-injective [] [] refl = (refl , refl) +∷ʳ-injective (x ∷ xs) (y ∷ ys) eq with refl , eq′ ← ∷-injective eq + = Product.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′) +∷ʳ-injective [] (_ ∷ _ ∷ _) () +∷ʳ-injective (_ ∷ _ ∷ _) [] () - ∷ʳ-injectiveˡ : ∀ (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys - ∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq) +∷ʳ-injectiveˡ : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys +∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq) - ∷ʳ-injectiveʳ : ∀ (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y - ∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq) +∷ʳ-injectiveʳ : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y +∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq) -∷ʳ-++ : ∀ (xs : List A) (a : A) (ys : List A) → xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys +∷ʳ-++ : ∀ xs (a : A) ys → xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys ∷ʳ-++ xs a ys = ++-assoc xs [ a ] ys From 78d4c7519da3432b5efa2fd8004058075ab1b1fc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 15 Apr 2024 15:21:52 +0100 Subject: [PATCH 05/11] factrored out comparison as removable module `MapMaybeTest` --- src/Data/List/Base.agda | 38 ++++++--------------- src/Data/List/Properties.agda | 64 ++++++++++++++++++++--------------- 2 files changed, 48 insertions(+), 54 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index e50657180b..97352d7697 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -49,22 +49,6 @@ map : (A → B) → List A → List B map f [] = [] map f (x ∷ xs) = f x ∷ map f xs -catMaybes′ : List (Maybe A) → List A -catMaybes′ [] = [] -catMaybes′ (x ∷ xs) = maybe′ _∷_ id x $ catMaybes′ xs - -mapMaybe′ : (A → Maybe B) → List A → List B -mapMaybe′ p = catMaybes′ ∘ map p - -mapMaybe : (A → Maybe B) → List A → List B -mapMaybe p [] = [] -mapMaybe p (x ∷ xs) with p x -... | just y = y ∷ mapMaybe p xs -... | nothing = mapMaybe p xs - -catMaybes : List (Maybe A) → List A -catMaybes = mapMaybe id - infixr 5 _++_ _++_ : List A → List A → List A @@ -130,11 +114,11 @@ partitionSums : List (A ⊎ B) → List A × List B partitionSums = partitionSumsWith id merge : {R : Rel A ℓ} → B.Decidable R → List A → List A → List A -merge R? [] ys = ys -merge R? xs [] = xs -merge R? (x ∷ xs) (y ∷ ys) = if does (R? x y) - then x ∷ merge R? xs (y ∷ ys) - else y ∷ merge R? (x ∷ xs) ys +merge R? [] ys = ys +merge R? xs [] = xs +merge R? xs@(x ∷ xs₁) ys@(y ∷ ys₁) = if does (R? x y) + then x ∷ merge R? xs₁ ys + else y ∷ merge R? xs ys₁ ------------------------------------------------------------------------ -- Operations for reducing lists @@ -156,6 +140,12 @@ concatMap f = concat ∘ map f ap : List (A → B) → List A → List B ap fs as = concatMap (flip map as) fs +catMaybes : List (Maybe A) → List A +catMaybes = foldr (maybe′ _∷_ id) [] + +mapMaybe : (A → Maybe B) → List A → List B +mapMaybe p = catMaybes ∘ map p + null : List A → Bool null [] = true null (x ∷ xs) = false @@ -181,12 +171,6 @@ product = foldr _*_ 1 length : List A → ℕ length = foldr (const suc) 0 -catMaybes″ : List (Maybe A) → List A -catMaybes″ = foldr (maybe′ _∷_ id) [] - -mapMaybe″ : (A → Maybe B) → List A → List B -mapMaybe″ p = catMaybes″ ∘ map p - ------------------------------------------------------------------------ -- Operations for constructing lists diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 2568d96da4..30bcf692aa 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -21,7 +21,7 @@ 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) +open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe) open import Data.Nat.Base open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n) open import Data.Nat.Properties @@ -122,49 +122,56 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq = ------------------------------------------------------------------------ -- mapMaybe -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) - -catMaybesTest : catMaybes {A = A} ≗ catMaybes′ -catMaybesTest [] = refl -catMaybesTest (just x ∷ xs) = cong (x ∷_) (catMaybesTest xs) -catMaybesTest (nothing ∷ xs) = catMaybesTest xs - -mapMaybeTest : (p : A → Maybe B) → mapMaybe p ≗ mapMaybe″ p -mapMaybeTest p [] = refl -mapMaybeTest p (x ∷ xs) with ih ← mapMaybeTest p xs | p x -... | nothing = ih -... | just y = cong (y ∷_) ih +length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs +length-catMaybes [] = ≤-refl +length-catMaybes (x ∷ xs) = let ih = length-catMaybes xs + in maybe {B = λ x → length (catMaybes (x ∷ xs)) ≤ suc (length xs)} + (λ _ → s≤s ih) + (m≤n⇒m≤1+n ih) + x mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs mapMaybe-just [] = refl mapMaybe-just (x ∷ xs) = cong (x ∷_) (mapMaybe-just xs) -mapMaybe′-just : (xs : List A) → mapMaybe′ just xs ≡ xs -mapMaybe′-just [] = refl -mapMaybe′-just (x ∷ xs) = cong (x ∷_) (mapMaybe′-just xs) - mapMaybe-nothing : (xs : List A) → - mapMaybe (λ _ → nothing {A = B}) xs ≡ [] + mapMaybe {B = B} (λ _ → nothing) xs ≡ [] mapMaybe-nothing [] = refl mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs -mapMaybe′-nothing : (xs : List A) → - mapMaybe′ (λ _ → nothing {A = A}) xs ≡ [] -mapMaybe′-nothing [] = refl -mapMaybe′-nothing (x ∷ xs) = mapMaybe′-nothing xs +module MapMaybeTest where + + mapMaybeOld : (A → Maybe B) → List A → List B + mapMaybeOld p [] = [] + mapMaybeOld p (x ∷ xs) with p x + ... | just y = y ∷ mapMaybeOld p xs + ... | nothing = mapMaybeOld p xs + + catMaybesOld : List (Maybe A) → List A + catMaybesOld = mapMaybe id + + catMaybesTest : catMaybes {A = A} ≗ catMaybesOld + catMaybesTest [] = refl + catMaybesTest (x ∷ xs) = let ih = catMaybesTest xs + in maybe {B = λ x → catMaybes (x ∷ xs) ≡ catMaybesOld (x ∷ xs)} + (λ x → cong (x ∷_) ih) ih x + + mapMaybeTest : (p : A → Maybe B) → mapMaybe p ≗ mapMaybeOld p + mapMaybeTest p [] = refl + mapMaybeTest p (x ∷ xs) with ih ← mapMaybeTest p xs | p x + ... | nothing = ih + ... | just y = cong (y ∷_) ih + module _ (f : A → Maybe B) where - mapMaybe-concatMap : mapMaybe′ f ≗ concatMap (fromMaybe ∘ f) + mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f) mapMaybe-concatMap [] = refl mapMaybe-concatMap (x ∷ xs) with ih ← mapMaybe-concatMap xs | f x ... | just y = cong (y ∷_) ih ... | nothing = ih - length-mapMaybe : ∀ xs → length (mapMaybe′ f xs) ≤ length xs + length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs length-mapMaybe xs = ≤-trans (length-catMaybes (map f xs)) (≤-reflexive (length-map f xs)) ------------------------------------------------------------------------ @@ -1351,3 +1358,6 @@ map-─ = map-removeAt "Warning: map-─ was deprecated in v2.0. Please use map-removeAt instead." #-} + +-- Version 2.1 + From 62215bd63b1de198e42c9716061e02175252c1c9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 16 Apr 2024 08:58:15 +0100 Subject: [PATCH 06/11] tidied up; removed `mapMaybeTest` --- src/Data/List/Properties.agda | 36 ++++++----------------------------- 1 file changed, 6 insertions(+), 30 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 30bcf692aa..9d061e1b0c 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -62,16 +62,16 @@ private ------------------------------------------------------------------------ -- _∷_ -∷-injective : x List.∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys -∷-injective refl = (refl , refl) +∷-injective : x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys +∷-injective refl = refl , refl -∷-injectiveˡ : x List.∷ xs ≡ y List.∷ ys → x ≡ y +∷-injectiveˡ : x ∷ xs ≡ y List.∷ ys → x ≡ y ∷-injectiveˡ refl = refl -∷-injectiveʳ : x List.∷ xs ≡ y List.∷ ys → xs ≡ ys +∷-injectiveʳ : x ∷ xs ≡ y List.∷ ys → xs ≡ ys ∷-injectiveʳ refl = refl -∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x List.∷ xs ≡ y List.∷ ys) +∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y List.∷ ys) ∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys) ≡-dec : DecidableEquality A → DecidableEquality (List A) @@ -139,30 +139,6 @@ mapMaybe-nothing : (xs : List A) → mapMaybe-nothing [] = refl mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs -module MapMaybeTest where - - mapMaybeOld : (A → Maybe B) → List A → List B - mapMaybeOld p [] = [] - mapMaybeOld p (x ∷ xs) with p x - ... | just y = y ∷ mapMaybeOld p xs - ... | nothing = mapMaybeOld p xs - - catMaybesOld : List (Maybe A) → List A - catMaybesOld = mapMaybe id - - catMaybesTest : catMaybes {A = A} ≗ catMaybesOld - catMaybesTest [] = refl - catMaybesTest (x ∷ xs) = let ih = catMaybesTest xs - in maybe {B = λ x → catMaybes (x ∷ xs) ≡ catMaybesOld (x ∷ xs)} - (λ x → cong (x ∷_) ih) ih x - - mapMaybeTest : (p : A → Maybe B) → mapMaybe p ≗ mapMaybeOld p - mapMaybeTest p [] = refl - mapMaybeTest p (x ∷ xs) with ih ← mapMaybeTest p xs | p x - ... | nothing = ih - ... | just y = cong (y ∷_) ih - - module _ (f : A → Maybe B) where mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f) @@ -1245,7 +1221,7 @@ reverse-downFrom = reverse-applyDownFrom id -- _∷ʳ_ ∷ʳ-injective : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y -∷ʳ-injective [] [] refl = (refl , refl) +∷ʳ-injective [] [] refl = refl , refl ∷ʳ-injective (x ∷ xs) (y ∷ ys) eq with refl , eq′ ← ∷-injective eq = Product.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′) ∷ʳ-injective [] (_ ∷ _ ∷ _) () From 17d78b5f6d4a8e4145b212896f3599cc084dd0ce Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 16 Apr 2024 08:59:51 +0100 Subject: [PATCH 07/11] tidied up; removed v2.1 deprecation section --- src/Data/List/Properties.agda | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 9d061e1b0c..f4c7ebb25f 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -1334,6 +1334,3 @@ map-─ = map-removeAt "Warning: map-─ was deprecated in v2.0. Please use map-removeAt instead." #-} - --- Version 2.1 - From 7c40295c0c1efab5503e7bf26a1033b2daa53787 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 19 Apr 2024 09:09:32 +0100 Subject: [PATCH 08/11] tidy up long line --- src/Data/List/Properties.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index f4c7ebb25f..c342343eb9 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -148,7 +148,8 @@ module _ (f : A → Maybe B) where ... | nothing = ih length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs - length-mapMaybe xs = ≤-trans (length-catMaybes (map f xs)) (≤-reflexive (length-map f xs)) + length-mapMaybe xs = + ≤-trans (length-catMaybes (map f xs)) (≤-reflexive (length-map f xs)) ------------------------------------------------------------------------ -- _++_ From e894d3448607d3ea5d1d0d70d8fa3325d64c5215 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Fri, 19 Apr 2024 10:16:36 +0100 Subject: [PATCH 09/11] Update src/Data/List/Base.agda Co-authored-by: G. Allais --- src/Data/List/Base.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 97352d7697..4794e7d01b 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -116,9 +116,9 @@ partitionSums = partitionSumsWith id merge : {R : Rel A ℓ} → B.Decidable R → List A → List A → List A merge R? [] ys = ys merge R? xs [] = xs -merge R? xs@(x ∷ xs₁) ys@(y ∷ ys₁) = if does (R? x y) - then x ∷ merge R? xs₁ ys - else y ∷ merge R? xs ys₁ +merge R? x∷xs@(x ∷ xs) y∷ys@(y ∷ ys) = if does (R? x y) + then x ∷ merge R? x∷xs ys + else y ∷ merge R? xs y∷ys ------------------------------------------------------------------------ -- Operations for reducing lists From 714f66c5bada04cafe795383627fa5ab1f7dbf81 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 19 Apr 2024 10:44:05 +0100 Subject: [PATCH 10/11] @gallais 's comments --- src/Data/List/Properties.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index c342343eb9..1dcf0d1a20 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -124,11 +124,8 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq = length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs length-catMaybes [] = ≤-refl -length-catMaybes (x ∷ xs) = let ih = length-catMaybes xs - in maybe {B = λ x → length (catMaybes (x ∷ xs)) ≤ suc (length xs)} - (λ _ → s≤s ih) - (m≤n⇒m≤1+n ih) - x +length-catMaybes (just x ∷ xs) = s≤s (length-catMaybes xs) +length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n (length-catMaybes xs) mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs mapMaybe-just [] = refl @@ -148,8 +145,11 @@ module _ (f : A → Maybe B) where ... | nothing = ih length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs - length-mapMaybe xs = - ≤-trans (length-catMaybes (map f xs)) (≤-reflexive (length-map f xs)) + length-mapMaybe xs = ≤-begin + length (mapMaybe f xs) ≤⟨ length-catMaybes (map f xs) ⟩ + length (map f xs) ≤⟨ ≤-reflexive (length-map f xs) ⟩ + length xs ≤-∎ + where open ≤-Reasoning renaming (begin_ to ≤-begin_; _∎ to _≤-∎) ------------------------------------------------------------------------ -- _++_ From 55be00367691b28fbf50685cf110e909dbff7b7a Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Fri, 19 Apr 2024 10:46:25 +0100 Subject: [PATCH 11/11] Update src/Data/List/Base.agda Oops! Co-authored-by: G. Allais --- src/Data/List/Base.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 4794e7d01b..03e5d4ae9a 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -117,8 +117,8 @@ merge : {R : Rel A ℓ} → B.Decidable R → List A → List A → List A merge R? [] ys = ys merge R? xs [] = xs merge R? x∷xs@(x ∷ xs) y∷ys@(y ∷ ys) = if does (R? x y) - then x ∷ merge R? x∷xs ys - else y ∷ merge R? xs y∷ys + then x ∷ merge R? xs y∷ys + else y ∷ merge R? x∷xs ys ------------------------------------------------------------------------ -- Operations for reducing lists