From dbf17ecdab831003c9eb7f000fbfd68a8d75d5e6 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Mon, 14 Jul 2025 10:29:14 -0400
Subject: [PATCH 1/9] padRight final vers

l
---
 src/takeListdraft.agda    | 103 ++++++++++++++++++++++++++++++++++++++
 src/takeVecdraft.agda     |  54 ++++++++++++++++++++
 src/vecPadRightDraft.agda |  88 ++++++++++++++++++++++++++++++++
 3 files changed, 245 insertions(+)
 create mode 100644 src/takeListdraft.agda
 create mode 100644 src/takeVecdraft.agda
 create mode 100644 src/vecPadRightDraft.agda

diff --git a/src/takeListdraft.agda b/src/takeListdraft.agda
new file mode 100644
index 0000000000..93ddf05d0d
--- /dev/null
+++ b/src/takeListdraft.agda
@@ -0,0 +1,103 @@
+-- List-related properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
+
+module takeListdraft where
+
+open import Algebra.Bundles using (Semigroup; Monoid)
+open import Algebra.Consequences.Propositional
+ using (selfInverse⇒involutive; selfInverse⇒injective)
+open import Algebra.Definitions as AlgebraicDefinitions using (SelfInverse; Involutive)
+open import Algebra.Morphism.Structures using (IsMagmaHomomorphism; IsMonoidHomomorphism)
+import Algebra.Structures as AlgebraicStructures
+open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
+open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ)
+open import Data.List.Base as List
+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.Relation.Unary.Any using (just) renaming (Any to MAny)
+open import Data.Nat.Base
+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 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)
+open import Function.Definitions using (Injective)
+open import Level using (Level)
+open import Relation.Binary.Definitions as B using (DecidableEquality)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+open import Relation.Binary.PropositionalEquality.Core as ≡
+open import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _because_; does)
+open import Relation.Nullary.Negation.Core using (contradiction; ¬_)
+open import Relation.Nullary.Decidable as Decidable
+  using (isYes; map′; ⌊_⌋; ¬?; _×-dec_; dec-true; dec-false)
+open import Relation.Unary using (Pred; Decidable; ∁; _≐_)
+open import Relation.Unary.Properties using (∁?)
+import Data.Nat.GeneralisedArithmetic as ℕ
+
+open import Data.List.Properties using (++-identity)
+
+open ≡-Reasoning
+
+private
+  variable
+    a b c d e p q ℓ : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+    E : Set e
+    x y z w : A
+    xs ys zs ws : List A
+
+------------------------------------------------------------------------
+-- Take++ : When you append 2 lists together and then take the length of the first list, you get the first list back
+take-++ : (n : ℕ) (xs ys : List A) → n ≤ length xs → take n (xs ++ ys) ≡ take n xs
+take-++ zero xs ys n≤len = refl
+take-++ (suc n) [] ys () 
+take-++ (suc n) (x ∷ xs) ys (s≤s n≤len) = cong (x ∷_) (take-++ n xs ys n≤len)
+
+-- Take++₁ : When you append 2 lists together and then take more than the length of the first list, you get the first list back and some of the second list
+-- lemma : 
+lengthxs : {A : Set} {n : ℕ} (x : A) (xs : List A) → ((suc n) ≡ length (x ∷ xs)) → (n ≡ length xs)
+lengthxs {A} {n} x xs sucn=len = 
+  begin
+    n
+  ≡⟨ cong pred sucn=len ⟩
+    pred (length (x ∷ xs))
+  ≡⟨ refl ⟩
+    length xs
+  ∎
+
+take-++₁ : {A : Set} {n i : ℕ} (xs ys : List A) → (n ≡ length xs) → take (n + i) (xs ++ ys) ≡ xs ++ take i ys
+take-++₁ {A} {n = zero} {i} [] ys n=len = refl
+take-++₁ {A} {n = suc n} {i} (x ∷ xs) ys sucn=len =
+  begin
+    x ∷ take (n + i) (xs ++ ys) 
+  ≡⟨ cong (x ∷_) (take-++₁ xs ys (lengthxs x xs sucn=len)) ⟩
+    x ∷ (xs ++ take i ys)
+  ≡⟨ refl ⟩
+    (x ∷ xs) ++ take i ys
+  ∎
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/takeVecdraft.agda b/src/takeVecdraft.agda
new file mode 100644
index 0000000000..a06dca127c
--- /dev/null
+++ b/src/takeVecdraft.agda
@@ -0,0 +1,54 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module takeVecdraft where
+
+open import Data.Fin.Base using (Fin; zero; suc; inject≤; _↑ˡ_)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _∸_)
+open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m+n; +-assoc)
+open import Data.Vec.Base
+open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans; map-++; lookup-++ˡ)
+open import Function.Base using (_∘_; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; cong; sym; trans; subst)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
+open Eq.≡-Reasoning
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    m n p : ℕ
+ 
+------------------------------------------------------------------------
+
+-- When you append 2 vectors together and then take the length or less than the length of the first, you get the first vector back or less than the first
+
+take-++ : ∀ {A : Set} {m n : ℕ} → (xs : Vec A m) → (ys : Vec A n) → take m (xs ++ ys) ≡ xs
+take-++ [] ys = refl
+take-++ (x ∷ xs) ys = cong (x ∷_) (take-++ xs ys)
+
+-- When you append 2 vectors together and then take the length or less than the length of the first, you get the first vector back or less than the first
+
+{--
+take-++-more : ∀ {A : Set} {m k n : ℕ} (p : ℕ) → (xs : Vec A m) → (ys : Vec A n) → (p≡m+k : p ≡ m + k) →
+               take p (xs ++ ys) ≡ xs ++ take k ys
+
+-- Proof by induction on xs
+take-++-more {A} {zero} {k} {n} .k [] ys refl = refl
+
+take-++-more {A} {suc m} {k} {n} .(suc m + k) (x ∷ xs) ys refl = 
+  begin
+    take (suc m + k) (x ∷ xs ++ ys)
+  ≡⟨⟩
+    x ∷ take (m + k) (xs ++ ys)
+  ≡⟨ cong (x ∷_) (take-++-more (m + k) xs ys refl) ⟩
+    x ∷ (xs ++ take k ys)
+  ≡⟨⟩
+    (x ∷ xs) ++ take k ys
+  ∎
+  --}
\ No newline at end of file
diff --git a/src/vecPadRightDraft.agda b/src/vecPadRightDraft.agda
new file mode 100644
index 0000000000..df17d341ff
--- /dev/null
+++ b/src/vecPadRightDraft.agda
@@ -0,0 +1,88 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of padRight for Vec
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module vecPadRightDraft where
+
+open import Data.Fin.Base using (Fin; zero; suc; inject≤; _↑ˡ_; inject+)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s)
+open import Data.Nat using (_⊔_)
+open import Data.Nat.Properties using (≤-trans; m≤m+n)
+open import Data.Vec.Base
+open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans; map-++; lookup-++ˡ; zipWith-++)
+open import Function.Base using (_∘_; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; cong; sym; trans; subst)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong; cong₂)
+open Eq.≡-Reasoning
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    m n p : ℕ
+
+
+------------------------------------------------------------------------
+-- Interaction with map
+
+padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
+               map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
+padRight-map f z≤n a [] = map-replicate f a _
+padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs)
+
+-- Interaction with lookup
+
+padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
+                  lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
+padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl
+padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i
+
+------------------------------------------------------------------------
+-- Interaction with zipWith
+
+-- When both vectors have the same original length
+padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B)
+                   (xs : Vec A m) (ys : Vec B m) →
+                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys)
+padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b
+padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys)
+
+-- When vectors have different original lengths
+padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m)
+                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) →
+                    zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡
+                    padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys))
+padRight-zipWith₁ {p} f m≤n p≤m a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
+                                            (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
+
+------------------------------------------------------------------------
+-- Interaction with take and drop
+
+padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
+                take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs
+padRight-take {m = zero} z≤n a [] refl = refl
+padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = cong (x ∷_) (padRight-take {p = p} m≤n a xs refl)
+
+padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
+                drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a
+padRight-drop {m = zero} z≤n a [] refl = refl
+padRight-drop {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = padRight-drop {p = p} m≤n a xs refl
+
+------------------------------------------------------------------------
+-- Interaction with updateAt
+
+padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
+                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
+                    padRight m≤n x (updateAt xs i f)
+padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
+padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x)
+
+------------------------------------------------------------------------
\ No newline at end of file

From f20c9d53996578b2eae5c87cba29562212e1fe3d Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Mon, 14 Jul 2025 10:43:59 -0400
Subject: [PATCH 2/9] Adding padRight proprities

---
 src/Data/Vec/Properties.agda | 73 ++++++++++++++++++++-------
 src/draftPadright.agda       | 97 ++++++++++++++++++++++++++++++++++++
 2 files changed, 153 insertions(+), 17 deletions(-)
 create mode 100644 src/draftPadright.agda

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 0960f1ea0f..dbdf4578c6 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -11,7 +11,7 @@ module Data.Vec.Properties where
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base as Fin
-  using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_)
+  using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_; inject≤)
 open import Data.List.Base as List using (List)
 import Data.List.Properties as List
 open import Data.Nat.Base
@@ -145,22 +145,6 @@ take≡truncate : ∀ m (xs : Vec A (m + n)) →
 take≡truncate zero    _        = refl
 take≡truncate (suc m) (x ∷ xs) = cong (x ∷_) (take≡truncate m xs)
 
-------------------------------------------------------------------------
--- pad
-
-padRight-refl : (a : A) (xs : Vec A n) → padRight ≤-refl a xs ≡ xs
-padRight-refl a []       = refl
-padRight-refl a (x ∷ xs) = cong (x ∷_) (padRight-refl a xs)
-
-padRight-replicate : (m≤n : m ≤ n) (a : A) → replicate n a ≡ padRight m≤n a (replicate m a)
-padRight-replicate z≤n       a = refl
-padRight-replicate (s≤s m≤n) a = cong (a ∷_) (padRight-replicate m≤n a)
-
-padRight-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (a : A) (xs : Vec A m) →
-            padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs)
-padRight-trans z≤n       n≤p       a []       = padRight-replicate n≤p a
-padRight-trans (s≤s m≤n) (s≤s n≤p) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤p a xs)
-
 ------------------------------------------------------------------------
 -- truncate and padRight together
 
@@ -1156,6 +1140,61 @@ toList-replicate : ∀ (n : ℕ) (x : A) →
 toList-replicate zero    x = refl
 toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
 
+------------------------------------------------------------------------
+-- pad
+
+padRight-refl : (a : A) (xs : Vec A n) → padRight ≤-refl a xs ≡ xs
+padRight-refl a []       = refl
+padRight-refl a (x ∷ xs) = cong (x ∷_) (padRight-refl a xs)
+
+padRight-replicate : (m≤n : m ≤ n) (a : A) → replicate n a ≡ padRight m≤n a (replicate m a)
+padRight-replicate z≤n       a = refl
+padRight-replicate (s≤s m≤n) a = cong (a ∷_) (padRight-replicate m≤n a)
+
+padRight-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (a : A) (xs : Vec A m) →
+            padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs)
+padRight-trans z≤n       n≤p       a []       = padRight-replicate n≤p a
+padRight-trans (s≤s m≤n) (s≤s n≤p) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤p a xs)
+
+padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
+                  lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
+padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl
+padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i
+
+padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
+               map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
+padRight-map f z≤n a [] = map-replicate f a _
+padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs)
+
+padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B)
+                   (xs : Vec A m) (ys : Vec B m) →
+                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys)
+padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b
+padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys)
+
+padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m)
+                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) →
+                    zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡
+                    padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys))
+padRight-zipWith₁ {p} f m≤n p≤m a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
+                                            (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
+
+padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
+                take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs
+padRight-take {m = zero} z≤n a [] refl = refl
+padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = cong (x ∷_) (padRight-take {p = p} m≤n a xs refl)
+
+padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
+                drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a
+padRight-drop {m = zero} z≤n a [] refl = refl
+padRight-drop {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = padRight-drop {p = p} m≤n a xs refl
+
+padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
+                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
+                    padRight m≤n x (updateAt xs i f)
+padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
+padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x)
+
 ------------------------------------------------------------------------
 -- iterate
 
diff --git a/src/draftPadright.agda b/src/draftPadright.agda
new file mode 100644
index 0000000000..1e48be59cc
--- /dev/null
+++ b/src/draftPadright.agda
@@ -0,0 +1,97 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of padRight for Vec
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module draftPadright where
+
+open import Data.Fin.Base using (Fin; zero; suc; inject≤)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s)
+open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m+n)
+open import Data.Vec.Base
+open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans)
+open import Function.Base using (_∘_; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; cong; sym; trans; subst)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    m n p : ℕ
+
+
+------------------------------------------------------------------------
+-- Interaction with map
+
+padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
+               map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
+padRight-map f z≤n a [] = map-replicate f a _
+padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs)
+
+------------------------------------------------------------------------
+-- Interaction with lookup
+
+padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
+                  lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
+padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl
+padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i
+
+------------------------------------------------------------------------
+-- Interaction with zipWith
+
+-- When both vectors have the same original length
+padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B)
+                   (xs : Vec A m) (ys : Vec B m) →
+                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡
+                   padRight m≤n (f a b) (zipWith f xs ys)
+padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b
+padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) =
+  cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys)
+
+-- When vectors have different original lengths
+padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m)
+                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) →
+                    zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡
+                    padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys))
+padRight-zipWith₁ {p} f m≤n p≤m a b xs ys =
+  trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
+        (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
+
+------------------------------------------------------------------------
+-- Interaction with take and drop
+
+padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
+                take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs
+padRight-take {m = zero} z≤n a [] refl = refl
+padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl =
+  cong (x ∷_) (padRight-take {p = p} m≤n a xs refl)
+
+padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
+                drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a
+padRight-drop {m = zero} z≤n a [] refl = refl
+padRight-drop {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl =
+  padRight-drop {p = p} m≤n a xs refl
+
+------------------------------------------------------------------------
+-- Interaction with updateAt
+
+padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
+                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
+                    padRight m≤n x (updateAt xs i f)
+padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
+padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x =
+  cong (y ∷_) (padRight-updateAt m≤n xs f i x)
+
+
+
+
+

From 74604c326cdfac1b668bfb9396de86fd8eea0953 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Mon, 14 Jul 2025 10:48:05 -0400
Subject: [PATCH 3/9] Cleaning the drafts

---
 src/takeListdraft.agda    | 103 --------------------------------------
 src/takeVecdraft.agda     |  54 --------------------
 src/vecPadRightDraft.agda |  88 --------------------------------
 3 files changed, 245 deletions(-)
 delete mode 100644 src/takeListdraft.agda
 delete mode 100644 src/takeVecdraft.agda
 delete mode 100644 src/vecPadRightDraft.agda

diff --git a/src/takeListdraft.agda b/src/takeListdraft.agda
deleted file mode 100644
index 93ddf05d0d..0000000000
--- a/src/takeListdraft.agda
+++ /dev/null
@@ -1,103 +0,0 @@
--- List-related properties
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
-
-module takeListdraft where
-
-open import Algebra.Bundles using (Semigroup; Monoid)
-open import Algebra.Consequences.Propositional
- using (selfInverse⇒involutive; selfInverse⇒injective)
-open import Algebra.Definitions as AlgebraicDefinitions using (SelfInverse; Involutive)
-open import Algebra.Morphism.Structures using (IsMagmaHomomorphism; IsMonoidHomomorphism)
-import Algebra.Structures as AlgebraicStructures
-open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
-open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ)
-open import Data.List.Base as List
-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.Relation.Unary.Any using (just) renaming (Any to MAny)
-open import Data.Nat.Base
-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 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)
-open import Function.Definitions using (Injective)
-open import Level using (Level)
-open import Relation.Binary.Definitions as B using (DecidableEquality)
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-open import Relation.Binary.PropositionalEquality.Core as ≡
-open import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _because_; does)
-open import Relation.Nullary.Negation.Core using (contradiction; ¬_)
-open import Relation.Nullary.Decidable as Decidable
-  using (isYes; map′; ⌊_⌋; ¬?; _×-dec_; dec-true; dec-false)
-open import Relation.Unary using (Pred; Decidable; ∁; _≐_)
-open import Relation.Unary.Properties using (∁?)
-import Data.Nat.GeneralisedArithmetic as ℕ
-
-open import Data.List.Properties using (++-identity)
-
-open ≡-Reasoning
-
-private
-  variable
-    a b c d e p q ℓ : Level
-    A : Set a
-    B : Set b
-    C : Set c
-    D : Set d
-    E : Set e
-    x y z w : A
-    xs ys zs ws : List A
-
-------------------------------------------------------------------------
--- Take++ : When you append 2 lists together and then take the length of the first list, you get the first list back
-take-++ : (n : ℕ) (xs ys : List A) → n ≤ length xs → take n (xs ++ ys) ≡ take n xs
-take-++ zero xs ys n≤len = refl
-take-++ (suc n) [] ys () 
-take-++ (suc n) (x ∷ xs) ys (s≤s n≤len) = cong (x ∷_) (take-++ n xs ys n≤len)
-
--- Take++₁ : When you append 2 lists together and then take more than the length of the first list, you get the first list back and some of the second list
--- lemma : 
-lengthxs : {A : Set} {n : ℕ} (x : A) (xs : List A) → ((suc n) ≡ length (x ∷ xs)) → (n ≡ length xs)
-lengthxs {A} {n} x xs sucn=len = 
-  begin
-    n
-  ≡⟨ cong pred sucn=len ⟩
-    pred (length (x ∷ xs))
-  ≡⟨ refl ⟩
-    length xs
-  ∎
-
-take-++₁ : {A : Set} {n i : ℕ} (xs ys : List A) → (n ≡ length xs) → take (n + i) (xs ++ ys) ≡ xs ++ take i ys
-take-++₁ {A} {n = zero} {i} [] ys n=len = refl
-take-++₁ {A} {n = suc n} {i} (x ∷ xs) ys sucn=len =
-  begin
-    x ∷ take (n + i) (xs ++ ys) 
-  ≡⟨ cong (x ∷_) (take-++₁ xs ys (lengthxs x xs sucn=len)) ⟩
-    x ∷ (xs ++ take i ys)
-  ≡⟨ refl ⟩
-    (x ∷ xs) ++ take i ys
-  ∎
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/src/takeVecdraft.agda b/src/takeVecdraft.agda
deleted file mode 100644
index a06dca127c..0000000000
--- a/src/takeVecdraft.agda
+++ /dev/null
@@ -1,54 +0,0 @@
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module takeVecdraft where
-
-open import Data.Fin.Base using (Fin; zero; suc; inject≤; _↑ˡ_)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _∸_)
-open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m+n; +-assoc)
-open import Data.Vec.Base
-open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans; map-++; lookup-++ˡ)
-open import Function.Base using (_∘_; _$_)
-open import Level using (Level)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong; sym; trans; subst)
-open import Relation.Binary.PropositionalEquality.Properties
-  using (module ≡-Reasoning)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
-open Eq.≡-Reasoning
-
-private
-  variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
-    m n p : ℕ
- 
-------------------------------------------------------------------------
-
--- When you append 2 vectors together and then take the length or less than the length of the first, you get the first vector back or less than the first
-
-take-++ : ∀ {A : Set} {m n : ℕ} → (xs : Vec A m) → (ys : Vec A n) → take m (xs ++ ys) ≡ xs
-take-++ [] ys = refl
-take-++ (x ∷ xs) ys = cong (x ∷_) (take-++ xs ys)
-
--- When you append 2 vectors together and then take the length or less than the length of the first, you get the first vector back or less than the first
-
-{--
-take-++-more : ∀ {A : Set} {m k n : ℕ} (p : ℕ) → (xs : Vec A m) → (ys : Vec A n) → (p≡m+k : p ≡ m + k) →
-               take p (xs ++ ys) ≡ xs ++ take k ys
-
--- Proof by induction on xs
-take-++-more {A} {zero} {k} {n} .k [] ys refl = refl
-
-take-++-more {A} {suc m} {k} {n} .(suc m + k) (x ∷ xs) ys refl = 
-  begin
-    take (suc m + k) (x ∷ xs ++ ys)
-  ≡⟨⟩
-    x ∷ take (m + k) (xs ++ ys)
-  ≡⟨ cong (x ∷_) (take-++-more (m + k) xs ys refl) ⟩
-    x ∷ (xs ++ take k ys)
-  ≡⟨⟩
-    (x ∷ xs) ++ take k ys
-  ∎
-  --}
\ No newline at end of file
diff --git a/src/vecPadRightDraft.agda b/src/vecPadRightDraft.agda
deleted file mode 100644
index df17d341ff..0000000000
--- a/src/vecPadRightDraft.agda
+++ /dev/null
@@ -1,88 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Properties of padRight for Vec
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module vecPadRightDraft where
-
-open import Data.Fin.Base using (Fin; zero; suc; inject≤; _↑ˡ_; inject+)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s)
-open import Data.Nat using (_⊔_)
-open import Data.Nat.Properties using (≤-trans; m≤m+n)
-open import Data.Vec.Base
-open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans; map-++; lookup-++ˡ; zipWith-++)
-open import Function.Base using (_∘_; _$_)
-open import Level using (Level)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong; sym; trans; subst)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong; cong₂)
-open Eq.≡-Reasoning
-
-private
-  variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
-    m n p : ℕ
-
-
-------------------------------------------------------------------------
--- Interaction with map
-
-padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
-               map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
-padRight-map f z≤n a [] = map-replicate f a _
-padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs)
-
--- Interaction with lookup
-
-padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
-                  lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
-padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl
-padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i
-
-------------------------------------------------------------------------
--- Interaction with zipWith
-
--- When both vectors have the same original length
-padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B)
-                   (xs : Vec A m) (ys : Vec B m) →
-                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys)
-padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b
-padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys)
-
--- When vectors have different original lengths
-padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m)
-                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) →
-                    zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡
-                    padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys))
-padRight-zipWith₁ {p} f m≤n p≤m a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
-                                            (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
-
-------------------------------------------------------------------------
--- Interaction with take and drop
-
-padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
-                take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs
-padRight-take {m = zero} z≤n a [] refl = refl
-padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = cong (x ∷_) (padRight-take {p = p} m≤n a xs refl)
-
-padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
-                drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a
-padRight-drop {m = zero} z≤n a [] refl = refl
-padRight-drop {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = padRight-drop {p = p} m≤n a xs refl
-
-------------------------------------------------------------------------
--- Interaction with updateAt
-
-padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
-                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
-                    padRight m≤n x (updateAt xs i f)
-padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
-padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x)
-
-------------------------------------------------------------------------
\ No newline at end of file

From 28cc0c0e557229f16f29bdb483879aa0a8309d79 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Mon, 14 Jul 2025 10:57:33 -0400
Subject: [PATCH 4/9] cleaning drafts

---
 src/draftPadright.agda | 97 ------------------------------------------
 1 file changed, 97 deletions(-)
 delete mode 100644 src/draftPadright.agda

diff --git a/src/draftPadright.agda b/src/draftPadright.agda
deleted file mode 100644
index 1e48be59cc..0000000000
--- a/src/draftPadright.agda
+++ /dev/null
@@ -1,97 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Properties of padRight for Vec
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module draftPadright where
-
-open import Data.Fin.Base using (Fin; zero; suc; inject≤)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s)
-open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m+n)
-open import Data.Vec.Base
-open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans)
-open import Function.Base using (_∘_; _$_)
-open import Level using (Level)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong; sym; trans; subst)
-open import Relation.Binary.PropositionalEquality.Properties
-  using (module ≡-Reasoning)
-
-private
-  variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
-    m n p : ℕ
-
-
-------------------------------------------------------------------------
--- Interaction with map
-
-padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
-               map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
-padRight-map f z≤n a [] = map-replicate f a _
-padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs)
-
-------------------------------------------------------------------------
--- Interaction with lookup
-
-padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
-                  lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
-padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl
-padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i
-
-------------------------------------------------------------------------
--- Interaction with zipWith
-
--- When both vectors have the same original length
-padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B)
-                   (xs : Vec A m) (ys : Vec B m) →
-                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡
-                   padRight m≤n (f a b) (zipWith f xs ys)
-padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b
-padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) =
-  cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys)
-
--- When vectors have different original lengths
-padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m)
-                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) →
-                    zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡
-                    padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys))
-padRight-zipWith₁ {p} f m≤n p≤m a b xs ys =
-  trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
-        (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
-
-------------------------------------------------------------------------
--- Interaction with take and drop
-
-padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
-                take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs
-padRight-take {m = zero} z≤n a [] refl = refl
-padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl =
-  cong (x ∷_) (padRight-take {p = p} m≤n a xs refl)
-
-padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
-                drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a
-padRight-drop {m = zero} z≤n a [] refl = refl
-padRight-drop {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl =
-  padRight-drop {p = p} m≤n a xs refl
-
-------------------------------------------------------------------------
--- Interaction with updateAt
-
-padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
-                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
-                    padRight m≤n x (updateAt xs i f)
-padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
-padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x =
-  cong (y ∷_) (padRight-updateAt m≤n xs f i x)
-
-
-
-
-

From 4f649c19a037cf2fa7a83d31e75dfc67a6126d0f Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Wed, 16 Jul 2025 16:03:45 -0400
Subject: [PATCH 5/9] modification after reviews

---
 src/Data/Vec/Properties.agda | 26 ++++++++++++++++----------
 1 file changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 22f8d8c16b..85df41947d 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1207,21 +1207,27 @@ padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p 
 padRight-zipWith₁ {p} f m≤n p≤m a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
                                             (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
 
-padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
-                take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs
-padRight-take {m = zero} z≤n a [] refl = refl
-padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = cong (x ∷_) (padRight-take {p = p} m≤n a xs refl)
+padRight-take : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) →
+                take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs
+padRight-take m≤n a [] p = refl
+padRight-take (s≤s m≤n) a (x ∷ xs) p = cong (x ∷_) (padRight-take m≤n a xs (suc-injective p))
+
+
+cast-replicate : ∀ .(m≡n : m ≡ n) (x : A) → cast m≡n (replicate m x) ≡ replicate n x
+cast-replicate {m = zero}  {n = zero}  _  _  = refl
+cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc-injective eq) x)
+
+padRight-drop : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) →
+                drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
+padRight-drop {m = zero}  z≤n a [] eq = cast-replicate eq a
+padRight-drop {m = suc _} {n = suc _} (s≤s m≤n) a (x ∷ xs) eq = padRight-drop m≤n a xs ((suc-injective eq))
 
-padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
-                drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a
-padRight-drop {m = zero} z≤n a [] refl = refl
-padRight-drop {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = padRight-drop {p = p} m≤n a xs refl
 
 padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
                     padRight m≤n x (updateAt xs i f)
-padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
-padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x)
+padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f zero x = refl
+padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) ((padRight-updateAt m≤n xs f i x))
 
 ------------------------------------------------------------------------
 -- iterate

From e46a5c8c7569adf76c8c01387a724a8dc4c78f09 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Thu, 17 Jul 2025 12:57:01 -0400
Subject: [PATCH 6/9] suppr double parentheses

---
 src/Data/Vec/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 85df41947d..91d24ead8e 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1220,14 +1220,14 @@ cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc
 padRight-drop : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) →
                 drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
 padRight-drop {m = zero}  z≤n a [] eq = cast-replicate eq a
-padRight-drop {m = suc _} {n = suc _} (s≤s m≤n) a (x ∷ xs) eq = padRight-drop m≤n a xs ((suc-injective eq))
+padRight-drop {m = suc _} {n = suc _} (s≤s m≤n) a (x ∷ xs) eq = padRight-drop m≤n a xs (suc-injective eq)
 
 
 padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
                     padRight m≤n x (updateAt xs i f)
 padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f zero x = refl
-padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) ((padRight-updateAt m≤n xs f i x))
+padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x)
 
 ------------------------------------------------------------------------
 -- iterate

From 0f7f3a4b9f73a5cbe6d0beac977e599bb4e81005 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Fri, 18 Jul 2025 11:24:30 -0400
Subject: [PATCH 7/9] moved cast-replicate

---
 src/Data/Vec/Properties.agda | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 91d24ead8e..bd80976dda 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1168,6 +1168,10 @@ toList-replicate : ∀ (n : ℕ) (x : A) →
 toList-replicate zero    x = refl
 toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
 
+cast-replicate : ∀ .(m≡n : m ≡ n) (x : A) → cast m≡n (replicate m x) ≡ replicate n x
+cast-replicate {m = zero}  {n = zero}  _  _  = refl
+cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc-injective eq) x)
+
 ------------------------------------------------------------------------
 -- pad
 
@@ -1212,17 +1216,11 @@ padRight-take : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m
 padRight-take m≤n a [] p = refl
 padRight-take (s≤s m≤n) a (x ∷ xs) p = cong (x ∷_) (padRight-take m≤n a xs (suc-injective p))
 
-
-cast-replicate : ∀ .(m≡n : m ≡ n) (x : A) → cast m≡n (replicate m x) ≡ replicate n x
-cast-replicate {m = zero}  {n = zero}  _  _  = refl
-cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc-injective eq) x)
-
 padRight-drop : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) →
                 drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
 padRight-drop {m = zero}  z≤n a [] eq = cast-replicate eq a
 padRight-drop {m = suc _} {n = suc _} (s≤s m≤n) a (x ∷ xs) eq = padRight-drop m≤n a xs (suc-injective eq)
 
-
 padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
                     padRight m≤n x (updateAt xs i f)
@@ -1235,7 +1233,6 @@ padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷
 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 (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))

From b98ac6a64d7f8df7eecce1bca26f9cdb01dab9bf Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Mon, 21 Jul 2025 13:50:45 -0400
Subject: [PATCH 8/9] modif after reviews and changelog

---
 CHANGELOG.md                 | 18 +++++++++++++++++
 src/Data/Vec/Properties.agda | 38 ++++++++++++++++++------------------
 2 files changed, 37 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f28e0f0e05..f6f34b1c39 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -444,6 +444,24 @@ Additions to existing modules
   fromList-reverse : (xs : List A) → (fromList (List.reverse xs)) ≈[ List.length-reverse xs ] reverse (fromList xs)
 
   fromList∘toList : ∀  (xs : Vec A n) → fromList (toList xs) ≈[ length-toList xs ] xs
+
+  padRight-lookup : ∀ {m n} → (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
+
+  padRight-map : ∀ {m n} → (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
+
+  padRight-zipWith : ∀ {m n} → (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B m) →
+                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys)
+
+  padRight-zipWith₁ : ∀ {o m n} → (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B o) →
+                    zipWith f (padRight m≤n a xs) (padRight (≤-trans o≤m m≤n) b ys) ≡
+                    padRight m≤n (f a b) (zipWith f xs (padRight o≤m b ys))
+
+  padRight-take : ∀ {m n o} → (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs
+
+  padRight-drop : ∀ {m n o} → (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
+
+  padRight-updateAt : ∀ {m n} → (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) →
+                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f)
   ```
 
 * In `Data.Product.Nary.NonDependent`:
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index bd80976dda..73d8d94f26 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1169,8 +1169,8 @@ toList-replicate zero    x = refl
 toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
 
 cast-replicate : ∀ .(m≡n : m ≡ n) (x : A) → cast m≡n (replicate m x) ≡ replicate n x
-cast-replicate {m = zero}  {n = zero}  _  _  = refl
-cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc-injective eq) x)
+cast-replicate {m = zero}  {n = zero}  _  _ = refl
+cast-replicate {m = suc _} {n = suc _} m≡n x = cong (x ∷_) (cast-replicate (suc-injective m≡n) x)
 
 ------------------------------------------------------------------------
 -- pad
@@ -1183,10 +1183,10 @@ padRight-replicate : (m≤n : m ≤ n) (a : A) → replicate n a ≡ padRight m
 padRight-replicate z≤n       a = refl
 padRight-replicate (s≤s m≤n) a = cong (a ∷_) (padRight-replicate m≤n a)
 
-padRight-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (a : A) (xs : Vec A m) →
-            padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs)
-padRight-trans z≤n       n≤p       a []       = padRight-replicate n≤p a
-padRight-trans (s≤s m≤n) (s≤s n≤p) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤p a xs)
+padRight-trans : ∀ (m≤n : m ≤ n) (n≤o : n ≤ o) (a : A) (xs : Vec A m) →
+            padRight (≤-trans m≤n n≤o) a xs ≡ padRight n≤o a (padRight m≤n a xs)
+padRight-trans z≤n       n≤o       a []       = padRight-replicate n≤o a
+padRight-trans (s≤s m≤n) (s≤s n≤o) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤o a xs)
 
 padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
                   lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
@@ -1204,28 +1204,28 @@ padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B)
 padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b
 padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys)
 
-padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m)
-                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) →
-                    zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡
-                    padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys))
-padRight-zipWith₁ {p} f m≤n p≤m a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
-                                            (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
+padRight-zipWith₁ : ∀ (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n)
+                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B o) →
+                    zipWith f (padRight m≤n a xs) (padRight (≤-trans o≤m m≤n) b ys) ≡
+                    padRight m≤n (f a b) (zipWith f xs (padRight o≤m b ys))
+padRight-zipWith₁ f o≤m m≤n a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans o≤m m≤n b ys))
+                                            (padRight-zipWith f m≤n a b xs (padRight o≤m b ys))
 
 padRight-take : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) →
                 take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs
-padRight-take m≤n a [] p = refl
-padRight-take (s≤s m≤n) a (x ∷ xs) p = cong (x ∷_) (padRight-take m≤n a xs (suc-injective p))
+padRight-take m≤n a [] n≡m+o = refl
+padRight-take (s≤s m≤n) a (x ∷ xs) n≡m+o = cong (x ∷_) (padRight-take m≤n a xs (suc-injective n≡m+o))
 
 padRight-drop : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) →
                 drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
-padRight-drop {m = zero}  z≤n a [] eq = cast-replicate eq a
-padRight-drop {m = suc _} {n = suc _} (s≤s m≤n) a (x ∷ xs) eq = padRight-drop m≤n a xs (suc-injective eq)
+padRight-drop {m = zero}  z≤n a [] n≡m+o = cast-replicate n≡m+o a
+padRight-drop {m = suc _} {n = suc _} (s≤s m≤n) a (x ∷ xs) n≡m+o = padRight-drop m≤n a xs (suc-injective n≡m+o)
 
-padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
+padRight-updateAt : ∀ (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) →
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
                     padRight m≤n x (updateAt xs i f)
-padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f zero x = refl
-padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x)
+padRight-updateAt {n = suc _} (s≤s m≤n) x (y ∷ xs) f zero = refl
+padRight-updateAt {n = suc _} (s≤s m≤n) x (y ∷ xs) f (suc i) = cong (y ∷_) (padRight-updateAt m≤n x xs f i)
 
 ------------------------------------------------------------------------
 -- iterate

From c2de6d8a0d754d9ba28e506fe030123085c0583b Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Tue, 22 Jul 2025 14:45:09 -0400
Subject: [PATCH 9/9] changes to changelog

---
 CHANGELOG.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f6f34b1c39..bc558ac5ba 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -445,22 +445,22 @@ Additions to existing modules
 
   fromList∘toList : ∀  (xs : Vec A n) → fromList (toList xs) ≈[ length-toList xs ] xs
 
-  padRight-lookup : ∀ {m n} → (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
+  padRight-lookup : (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
 
-  padRight-map : ∀ {m n} → (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
+  padRight-map : (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
 
-  padRight-zipWith : ∀ {m n} → (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B m) →
+  padRight-zipWith : (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B m) →
                    zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys)
 
-  padRight-zipWith₁ : ∀ {o m n} → (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B o) →
+  padRight-zipWith₁ : (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B o) →
                     zipWith f (padRight m≤n a xs) (padRight (≤-trans o≤m m≤n) b ys) ≡
                     padRight m≤n (f a b) (zipWith f xs (padRight o≤m b ys))
 
-  padRight-take : ∀ {m n o} → (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs
+  padRight-take : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs
 
-  padRight-drop : ∀ {m n o} → (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
+  padRight-drop : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
 
-  padRight-updateAt : ∀ {m n} → (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) →
+  padRight-updateAt : (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) →
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f)
   ```