From 3e5252de92f20466ffe60e797fb9695a84584762 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 08:24:59 +0000 Subject: [PATCH 1/8] towards #2267 --- src/Data/List/Base.agda | 21 +++++++++++++++------ src/Data/List/NonEmpty/Base.agda | 18 ++++++++++++++++++ src/Data/List/NonEmpty/Properties.agda | 7 +++++++ src/Data/List/Properties.agda | 4 ++-- 4 files changed, 42 insertions(+), 8 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 16546110b6..1962a0e868 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -193,12 +193,18 @@ iterate f e zero = [] iterate f e (suc n) = e ∷ iterate f (f e) n inits : List A → List (List A) -inits [] = [] ∷ [] -inits (x ∷ xs) = [] ∷ map (x ∷_) (inits xs) +inits {A = A} xs = [] ∷ go xs + where + go : List A → List (List A) + go [] = [] + go (x ∷ xs) = [ x ] ∷ map (x ∷_) (go xs) tails : List A → List (List A) -tails [] = [] ∷ [] -tails (x ∷ xs) = (x ∷ xs) ∷ tails xs +tails {A = A} xs = xs ∷ go xs + where + go : List A → List (List A) + go [] = [] + go (_ ∷ xs) = xs ∷ go xs insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A insertAt xs zero v = v ∷ xs @@ -217,8 +223,11 @@ scanr f e (x ∷ xs) with scanr f e xs ... | y ∷ ys = f x y ∷ y ∷ ys scanl : (A → B → A) → A → List B → List A -scanl f e [] = e ∷ [] -scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs +scanl {A = A} {B = B} f e xs = e ∷ go e xs + where + go : A → List B → List A + go _ [] = [] + go e (x ∷ xs) = let fex = f e x in fex ∷ go fex xs -- Tabulation diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda index 82f16c270a..d27d1faca6 100644 --- a/src/Data/List/NonEmpty/Base.agda +++ b/src/Data/List/NonEmpty/Base.agda @@ -143,6 +143,24 @@ concatMap f = concat ∘′ map f ap : List⁺ (A → B) → List⁺ A → List⁺ B ap fs as = concatMap (λ f → map f as) fs +-- Inits + +inits⁺ : List A → List⁺ (List A) +inits⁺ {A = A} xs = [] ∷ go xs + where + go : List A → List (List A) + go [] = [] + go (x ∷ xs) = List.[ x ] ∷ List.map (x ∷_) (go xs) + +-- Scanl + +scanl⁺ : (A → B → A) → A → List B → List⁺ A +scanl⁺ {A = A} {B = B} f e xs = e ∷ go e xs + where + go : A → List B → List A + go _ [] = [] + go e (x ∷ xs) = let fex = f e x in fex ∷ go fex xs + -- Reverse reverse : List⁺ A → List⁺ A diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 45b27f46c3..f17556d8d2 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -113,6 +113,13 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs) map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs) +------------------------------------------------------------------------ +-- inits + +toList-inits⁺ : (xs : List A) → toList (inits⁺ xs) ≡ List.inits xs +toList-inits⁺ [] = refl +toList-inits⁺ (x ∷ xs) = cong ([] ∷_) (cong (List.map (x ∷_)) (toList-inits⁺ xs)) + ------------------------------------------------------------------------ -- groupSeqs diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 5bd47dc763..1545ed71bc 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -636,7 +636,7 @@ scanr-defn f e (x ∷ y∷xs@(_ ∷ _)) scanl-defn : ∀ (f : A → B → A) (e : A) → scanl f e ≗ map (foldl f e) ∘ inits scanl-defn f e [] = refl -scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin +scanl-defn f e (x ∷ xs) = cong (e ∷_) $ begin scanl f (f e x) xs ≡⟨ scanl-defn f (f e x) xs ⟩ map (foldl f (f e x)) (inits xs) @@ -644,7 +644,7 @@ scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin map (foldl f e ∘ (x ∷_)) (inits xs) ≡⟨ map-∘ (inits xs) ⟩ map (foldl f e) (map (x ∷_) (inits xs)) - ∎) + ∎ ------------------------------------------------------------------------ -- applyUpTo From f65f9b856aa2a24e33eeda73d8e95a2a0e5c0b6c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 09:07:47 +0000 Subject: [PATCH 2/8] simplifed proof --- src/Data/List/NonEmpty/Properties.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index f17556d8d2..9f18c92428 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -113,12 +113,15 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs) map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs) +toList-map : ∀ (f : A → B) xs → toList (map f xs) ≡ List.map f (toList xs) +toList-map f (x ∷ xs) = refl + ------------------------------------------------------------------------ -- inits toList-inits⁺ : (xs : List A) → toList (inits⁺ xs) ≡ List.inits xs toList-inits⁺ [] = refl -toList-inits⁺ (x ∷ xs) = cong ([] ∷_) (cong (List.map (x ∷_)) (toList-inits⁺ xs)) +toList-inits⁺ (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-inits⁺ xs) ------------------------------------------------------------------------ -- groupSeqs From 6abaa23cd1e2a53b04a2bda20c33150b46723287 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 10:10:06 +0000 Subject: [PATCH 3/8] simplified proof --- src/Data/List/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 1545ed71bc..e24fce875c 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -628,7 +628,7 @@ scanr-defn f e (x ∷ []) = refl scanr-defn f e (x ∷ y∷xs@(_ ∷ _)) with eq ← scanr-defn f e y∷xs with z ∷ zs ← scanr f e y∷xs - = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq + = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) eq ------------------------------------------------------------------------ -- scanl From 452e00a32951b3ebcd29b8693e05ba95ede94c2b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 11:57:45 +0000 Subject: [PATCH 4/8] better proofs for better defns of `scanl`, `inits` --- src/Data/List/NonEmpty/Properties.agda | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 9f18c92428..5b13a8b98f 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -123,6 +123,30 @@ toList-inits⁺ : (xs : List A) → toList (inits⁺ xs) ≡ List.inits xs toList-inits⁺ [] = refl toList-inits⁺ (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-inits⁺ xs) +------------------------------------------------------------------------ +-- scanl + +module _ (f : A → B → A) where + + private + h = List.foldl f + + scanl⁺-defn : (e : A) → scanl⁺ f e ≗ map (h e) ∘ inits⁺ + scanl⁺-defn e [] = refl + scanl⁺-defn e (x ∷ xs) = let eq = scanl⁺-defn (f e x) xs in + cong (e ∷_) $ cong (f e x ∷_) (trans (cong tail eq) (List.map-∘ _)) + + toList-scanl⁺ : (e : A) → + toList ∘ scanl⁺ f e ≗ List.map (List.foldl f e) ∘ List.inits + toList-scanl⁺ e xs = begin + toList (scanl⁺ f e xs) + ≡⟨ cong toList (scanl⁺-defn e xs) ⟩ + toList (map (h e) (inits⁺ xs)) + ≡⟨ toList-map (h e) (inits⁺ xs) ⟩ + List.map (h e) (toList (inits⁺ xs)) + ≡⟨ cong (List.map (h e)) (toList-inits⁺ xs) ⟩ + List.map (h e) (List.inits xs) ∎ + ------------------------------------------------------------------------ -- groupSeqs From d003a63c47175e8dbf6fcedf887e6c7443fdfc80 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 12:02:28 +0000 Subject: [PATCH 5/8] `CHANGELOG` --- CHANGELOG.md | 50 ++++++++++---------------------------------------- 1 file changed, 10 insertions(+), 40 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 97eb05989b..79e621b65e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,10 +9,6 @@ Highlights Bug-fixes --------- -* Fix statement of `Data.Vec.Properties.toList-replicate`, where `replicate` - was mistakenly applied to the level of the type `A` instead of the - variable `x` of type `A`. - Non-backwards compatible changes -------------------------------- @@ -33,52 +29,26 @@ Deprecated names New modules ----------- -* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures - Additions to existing modules ----------------------------- -* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. - -* In `Algebra.Module.Construct.DirectProduct`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - ``` - -* In `Algebra.Module.Construct.TensorUnit`: +* In `Data.Fin.Properties`: ```agda - rawLeftSemimodule : RawLeftSemimodule _ c ℓ - rawLeftModule : RawLeftModule _ c ℓ - rawRightSemimodule : RawRightSemimodule _ c ℓ - rawRightModule : RawRightModule _ c ℓ - rawBisemimodule : RawBisemimodule _ _ c ℓ - rawBimodule : RawBimodule _ _ c ℓ - rawSemimodule : RawSemimodule _ c ℓ - rawModule : RawModule _ c ℓ + nonZeroIndex : Fin n → ℕ.NonZero n ``` -* In `Algebra.Module.Construct.Zero`: +* In `Data.List.NonEmpty.Base`: ```agda - rawLeftSemimodule : RawLeftSemimodule R c ℓ - rawLeftModule : RawLeftModule R c ℓ - rawRightSemimodule : RawRightSemimodule R c ℓ - rawRightModule : RawRightModule R c ℓ - rawBisemimodule : RawBisemimodule R c ℓ - rawBimodule : RawBimodule R c ℓ - rawSemimodule : RawSemimodule R c ℓ - rawModule : RawModule R c ℓ + inits⁺ : List A → List⁺ (List A) + scanl⁺ : (A → B → A) → A → List B → List⁺ A ``` -* In `Data.Fin.Properties`: +* In `Data.List.NonEmpty.Properties`: ```agda - nonZeroIndex : Fin n → ℕ.NonZero n + toList-map : (f : A → B) → toList ∘ map f ≗ List.map f ∘ toList + toList-inits⁺ : toList ∘ inits⁺ ≗ List.inits + scanl⁺-defn : scanl⁺ f e ≗ map (List.foldl f e) ∘ inits⁺ + toList-scanl⁺ : toList ∘ scanl⁺ f e ≗ List.map (List.foldl f e) ∘ List.inits ``` * In `Data.List.Relation.Unary.All.Properties`: From aed8a85340c4ca31cfbac5e2031a9ce7f5b77e23 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 29 Jan 2024 17:45:24 +0000 Subject: [PATCH 6/8] fixed `CHANGELOG`? --- CHANGELOG.md | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 79e621b65e..7192d7c9a3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,10 @@ Highlights Bug-fixes --------- +* Fix statement of `Data.Vec.Properties.toList-replicate`, where `replicate` + was mistakenly applied to the level of the type `A` instead of the + variable `x` of type `A`. + Non-backwards compatible changes -------------------------------- @@ -29,9 +33,49 @@ Deprecated names New modules ----------- +* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures + Additions to existing modules ----------------------------- +* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. + +* In `Algebra.Module.Construct.DirectProduct`: + ```agda + rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′) + ``` + +* In `Algebra.Module.Construct.TensorUnit`: + ```agda + rawLeftSemimodule : RawLeftSemimodule _ c ℓ + rawLeftModule : RawLeftModule _ c ℓ + rawRightSemimodule : RawRightSemimodule _ c ℓ + rawRightModule : RawRightModule _ c ℓ + rawBisemimodule : RawBisemimodule _ _ c ℓ + rawBimodule : RawBimodule _ _ c ℓ + rawSemimodule : RawSemimodule _ c ℓ + rawModule : RawModule _ c ℓ + ``` + +* In `Algebra.Module.Construct.Zero`: + ```agda + rawLeftSemimodule : RawLeftSemimodule R c ℓ + rawLeftModule : RawLeftModule R c ℓ + rawRightSemimodule : RawRightSemimodule R c ℓ + rawRightModule : RawRightModule R c ℓ + rawBisemimodule : RawBisemimodule R c ℓ + rawBimodule : RawBimodule R c ℓ + rawSemimodule : RawSemimodule R c ℓ + rawModule : RawModule R c ℓ + ``` + * In `Data.Fin.Properties`: ```agda nonZeroIndex : Fin n → ℕ.NonZero n From f1a1425d9b592d435a60bae3fb8ff34c506a59e3 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 31 Jan 2024 00:33:38 +0000 Subject: [PATCH 7/8] tidying up --- src/Data/List/NonEmpty/Properties.agda | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 5b13a8b98f..7843f49724 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -131,14 +131,13 @@ module _ (f : A → B → A) where private h = List.foldl f - scanl⁺-defn : (e : A) → scanl⁺ f e ≗ map (h e) ∘ inits⁺ + scanl⁺-defn : ∀ e → scanl⁺ f e ≗ map (h e) ∘ inits⁺ scanl⁺-defn e [] = refl scanl⁺-defn e (x ∷ xs) = let eq = scanl⁺-defn (f e x) xs in - cong (e ∷_) $ cong (f e x ∷_) (trans (cong tail eq) (List.map-∘ _)) + cong (e ∷_) $ cong (f e x ∷_) $ trans (cong tail eq) (List.map-∘ _) - toList-scanl⁺ : (e : A) → - toList ∘ scanl⁺ f e ≗ List.map (List.foldl f e) ∘ List.inits - toList-scanl⁺ e xs = begin + toList-scanl⁺ : ∀ e → toList ∘ scanl⁺ f e ≗ List.map (h e) ∘ List.inits + toList-scanl⁺ e xs = begin toList (scanl⁺ f e xs) ≡⟨ cong toList (scanl⁺-defn e xs) ⟩ toList (map (h e) (inits⁺ xs)) From 24f8b3ed77fcc470c46bca1043bc395c14546da5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 8 Apr 2024 08:38:30 +0100 Subject: [PATCH 8/8] `fix-whitespace` --- src/Data/List/NonEmpty/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 7843f49724..240c401117 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -127,7 +127,7 @@ toList-inits⁺ (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-init -- scanl module _ (f : A → B → A) where - + private h = List.foldl f