From 9b10e00a5ad0b7861903704d6cc9e5edc1d346a1 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 5 Oct 2023 05:27:45 +0530 Subject: [PATCH] Sync `iterate` and `replicate` for `List` and `Vec` (#2051) --- CHANGELOG.md | 30 +++++++++++-- src/Codata/Guarded/Stream/Properties.agda | 2 +- src/Data/List/Base.agda | 4 ++ src/Data/List/Properties.agda | 54 ++++++++++++++++++----- src/Data/Vec/Base.agda | 6 +-- src/Data/Vec/Properties.agda | 24 ++++++++++ 6 files changed, 102 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 612e45673e..7bfefd20e9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1058,17 +1058,20 @@ Non-backwards compatible changes Tactic.RingSolver Tactic.RingSolver.Core.NatSet ``` + * Moved & renamed from `Data.Vec.Relation.Unary.All` to `Data.Vec.Relation.Unary.All.Properties`: ``` lookup ↦ lookup⁺ tabulate ↦ lookup⁻ ``` + * Renamed in `Data.Vec.Relation.Unary.Linked.Properties` and `Codata.Guarded.Stream.Relation.Binary.Pointwise`: ``` lookup ↦ lookup⁺ ``` + * Added the following new definitions to `Data.Vec.Relation.Unary.All`: ``` lookupAny : All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i) @@ -1076,9 +1079,16 @@ Non-backwards compatible changes lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x) lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) ``` + * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to `¬¬-excluded-middle`. + * `iterate` in `Data.Vec.Base` now takes `n` (the length of `Vec`) as an + explicit argument. + ```agda + iterate : (A → A) → A → ∀ n → Vec A n + ``` + Major improvements ------------------ @@ -2441,7 +2451,7 @@ Additions to existing modules gcd-zero : Zero 1ℤ gcd ``` -* Added new functions in `Data.List.Base`: +* Added new functions and definitions to `Data.List.Base`: ```agda takeWhileᵇ : (A → Bool) → List A → List A dropWhileᵇ : (A → Bool) → List A → List A @@ -2466,6 +2476,7 @@ Additions to existing modules ++-rawMagma : Set a → RawMagma a _ ++-[]-rawMonoid : Set a → RawMonoid a _ + iterate : (A → A) → A → ℕ → List A insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A ``` @@ -2527,14 +2538,21 @@ Additions to existing modules drop-take-suc-tabulate : drop m (take (suc m) (tabulate f)) ≡ [ f i ] take-all : n ≥ length xs → take n xs ≡ xs + drop-all : n ≥ length xs → drop n xs ≡ [] take-[] : take m [] ≡ [] drop-[] : drop m [] ≡ [] - map-replicate : map f (replicate n x) ≡ replicate n (f x) - drop-drop : drop n (drop m xs) ≡ drop (m + n) xs + lookup-replicate : lookup (replicate n x) i ≡ x + map-replicate : map f (replicate n x) ≡ replicate n (f x) + zipWith-replicate : zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y) + + length-iterate : length (iterate f x n) ≡ n + iterate-id : iterate id x n ≡ replicate n x + lookup-iterate : lookup (iterate f x n) (cast (sym (length-iterate f x n)) i) ≡ ℕ.iterate f x (toℕ i) + length-insertAt : length (insertAt xs i v) ≡ suc (length xs) length-removeAt′ : length xs ≡ suc (length (removeAt xs k)) removeAt-insertAt : removeAt (insertAt xs i v) ((cast (sym (length-insertAt xs i v)) i)) ≡ xs @@ -2964,6 +2982,12 @@ Additions to existing modules lookup-cast₂ : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq + iterate-id : iterate id x n ≡ replicate x + take-iterate : take n (iterate f x (n + m)) ≡ iterate f x n + drop-iterate : drop n (iterate f x n) ≡ [] + lookup-iterate : lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i) + toList-iterate : toList (iterate f x n) ≡ List.iterate f x n + zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys' ++-assoc : cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs) diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda index a07a614b59..41b19ec947 100644 --- a/src/Codata/Guarded/Stream/Properties.agda +++ b/src/Codata/Guarded/Stream/Properties.agda @@ -255,7 +255,7 @@ lookup-interleave-odd (suc n) as bs = lookup-interleave-odd n (as .tail) (bs .ta ------------------------------------------------------------------------ -- Properties of take -take-iterate : ∀ n f (x : A) → take n (iterate f x) ≡ Vec.iterate f x +take-iterate : ∀ n f (x : A) → take n (iterate f x) ≡ Vec.iterate f x n take-iterate zero f x = P.refl take-iterate (suc n) f x = cong (x ∷_) (take-iterate n f (f x)) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index b96a0451cc..58b51e4893 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -188,6 +188,10 @@ replicate : ℕ → A → List A replicate zero x = [] replicate (suc n) x = x ∷ replicate n x +iterate : (A → A) → A → ℕ → List A +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) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 48f533f08d..5afce0cd54 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -43,6 +43,7 @@ open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradi open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_) open import Relation.Unary using (Pred; Decidable; ∁) open import Relation.Unary.Properties using (∁?) +import Data.Nat.GeneralisedArithmetic as ℕ open ≡-Reasoning @@ -118,10 +119,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) -map-replicate : ∀ (f : A → B) n x → map f (replicate n x) ≡ replicate n (f x) -map-replicate f zero x = refl -map-replicate f (suc n) x = cong (_ ∷_) (map-replicate f n x) - ------------------------------------------------------------------------ -- mapMaybe @@ -621,13 +618,6 @@ sum-++ (x ∷ xs) ys = begin ∈⇒∣product {n} {n ∷ ns} (here refl) = divides (product ns) (*-comm n (product ns)) ∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns) ------------------------------------------------------------------------- --- replicate - -length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n -length-replicate zero = refl -length-replicate (suc n) = cong suc (length-replicate n) - ------------------------------------------------------------------------ -- scanr @@ -858,6 +848,48 @@ drop-drop zero n xs = refl drop-drop (suc m) n [] = drop-[] n drop-drop (suc m) n (x ∷ xs) = drop-drop m n xs +drop-all : (n : ℕ) (xs : List A) → n ≥ length xs → drop n xs ≡ [] +drop-all n [] _ = drop-[] n +drop-all (suc n) (x ∷ xs) p = drop-all n xs (≤-pred p) + +------------------------------------------------------------------------ +-- replicate + +length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n +length-replicate zero = refl +length-replicate (suc n) = cong suc (length-replicate n) + +lookup-replicate : ∀ n (x : A) (i : Fin n) → + lookup (replicate n x) (cast (sym (length-replicate n)) i) ≡ x +lookup-replicate (suc n) x zero = refl +lookup-replicate (suc n) x (suc i) = lookup-replicate n x i + +map-replicate : ∀ (f : A → B) n (x : A) → + map f (replicate n x) ≡ replicate n (f x) +map-replicate f zero x = refl +map-replicate f (suc n) x = cong (_ ∷_) (map-replicate f n x) + +zipWith-replicate : ∀ n (_⊕_ : A → B → C) (x : A) (y : B) → + zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y) +zipWith-replicate zero _⊕_ x y = refl +zipWith-replicate (suc n) _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate n _⊕_ x y) + +------------------------------------------------------------------------ +-- iterate + +length-iterate : ∀ f (x : A) n → length (iterate f x n) ≡ n +length-iterate f x zero = refl +length-iterate f x (suc n) = cong suc (length-iterate f (f x) n) + +iterate-id : ∀ (x : A) n → iterate id x n ≡ replicate n x +iterate-id x zero = refl +iterate-id x (suc n) = cong (_ ∷_) (iterate-id x n) + +lookup-iterate : ∀ f (x : A) n (i : Fin n) → + lookup (iterate f x n) (cast (sym (length-iterate f x n)) i) ≡ ℕ.iterate f x (toℕ i) +lookup-iterate f x (suc n) zero = refl +lookup-iterate f x (suc n) (suc i) = lookup-iterate f (f x) n i + ------------------------------------------------------------------------ -- splitAt diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 469549e1ed..e142db9d00 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -60,9 +60,9 @@ lookup : Vec A n → Fin n → A lookup (x ∷ xs) zero = x lookup (x ∷ xs) (suc i) = lookup xs i -iterate : (A → A) → A → ∀ {n} → Vec A n -iterate s z {zero} = [] -iterate s z {suc n} = z ∷ iterate s (s z) +iterate : (A → A) → A → ∀ n → Vec A n +iterate s z zero = [] +iterate s z (suc n) = z ∷ iterate s (s z) n insertAt : Vec A n → Fin (suc n) → A → Vec A (suc n) insertAt xs zero v = v ∷ xs diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 3d0e3bf590..1357e4e441 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -31,6 +31,7 @@ open import Relation.Binary.PropositionalEquality open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; _×-dec_; map′) open import Relation.Nullary.Negation.Core using (contradiction) +import Data.Nat.GeneralisedArithmetic as ℕ open ≡-Reasoning @@ -1098,6 +1099,29 @@ toList-replicate : ∀ (n : ℕ) (x : A) → toList-replicate zero x = refl toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x) +------------------------------------------------------------------------ +-- iterate + +iterate-id : ∀ (x : A) n → iterate id x n ≡ replicate x +iterate-id x zero = refl +iterate-id x (suc n) = cong (_ ∷_) (iterate-id (id x) n) + +take-iterate : ∀ n f (x : A) → take n (iterate f x (n + m)) ≡ iterate f x n +take-iterate zero f x = refl +take-iterate (suc n) f x = cong (_ ∷_) (take-iterate n f (f x)) + +drop-iterate : ∀ n f (x : A) → drop n (iterate f x (n + zero)) ≡ [] +drop-iterate zero f x = refl +drop-iterate (suc n) f x = drop-iterate n f (f x) + +lookup-iterate : ∀ f (x : A) (i : Fin n) → lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i) +lookup-iterate f x zero = refl +lookup-iterate f x (suc i) = lookup-iterate f (f x) i + +toList-iterate : ∀ f (x : A) n → toList (iterate f x n) ≡ List.iterate f x n +toList-iterate f x zero = refl +toList-iterate f x (suc n) = cong (_ List.∷_) (toList-iterate f (f x) n) + ------------------------------------------------------------------------ -- tabulate