diff --git a/CHANGELOG.md b/CHANGELOG.md index 081dda5b66..6ab28e935c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,14 @@ Non-backwards compatible changes Minor improvements ------------------ +* The types of `Data.Vec.Base.{truncate|padRight}` have been weakened so + that the argument of type `m ≤ n` is marked as irrelevant. This should be + backwards compatible, but does change the equational behaviour of these + functions to be more eager, because no longer blocking on pattern matching + on that argument. Corresponding changes have been made to the types of their + properties (and their proofs). In particular, `truncate-irrelevant` is now + deprecated, because definitionally trivial. + * The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`. @@ -41,6 +49,11 @@ Deprecated names interchange ↦ medial ``` +* In `Data.Vec.Properties`: + ```agda + truncate-irrelevant ↦ + ``` + New modules ----------- @@ -93,8 +106,16 @@ Additions to existing modules 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 : m ≤ n) (a : A) (xs : Vec A m) → + let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in take m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ xs + 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≤n : m ≤ n) (a : A) (xs : Vec A m) → + let o , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in drop m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ replicate o 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) ``` diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 8c03fb8a83..b4153db297 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -289,14 +289,14 @@ uncons (x ∷ xs) = x , xs -- Operations involving ≤ -- Take the first 'm' elements of a vector. -truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m -truncate {m = zero} _ _ = [] -truncate (s≤s le) (x ∷ xs) = x ∷ (truncate le xs) +truncate : .(m ≤ n) → Vec A n → Vec A m +truncate {m = zero} _ _ = [] +truncate {m = suc _} le (x ∷ xs) = x ∷ (truncate (s≤s⁻¹ le) xs) -- Pad out a vector with extra elements. -padRight : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n -padRight z≤n a xs = replicate _ a -padRight (s≤s le) a (x ∷ xs) = x ∷ padRight le a xs +padRight : .(m ≤ n) → A → Vec A m → Vec A n +padRight {n = n} _ a [] = replicate n a +padRight {n = suc _} le a (x ∷ xs) = x ∷ padRight (s≤s⁻¹ le) a xs ------------------------------------------------------------------------ -- Operations for converting between lists diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 73d8d94f26..101c54169c 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -17,8 +17,10 @@ import Data.List.Properties as List open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s; uncurry) open import Data.Sum.Base using ([_,_]′) @@ -136,18 +138,17 @@ truncate-refl : (xs : Vec A n) → truncate ≤-refl xs ≡ xs truncate-refl [] = refl truncate-refl (x ∷ xs) = cong (x ∷_) (truncate-refl xs) -truncate-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (xs : Vec A p) → - truncate (≤-trans m≤n n≤p) xs ≡ truncate m≤n (truncate n≤p xs) -truncate-trans z≤n n≤p xs = refl -truncate-trans (s≤s m≤n) (s≤s n≤p) (x ∷ xs) = cong (x ∷_) (truncate-trans m≤n n≤p xs) +truncate-trans : ∀ .(m≤n : m ≤ n) .(n≤o : n ≤ o) (xs : Vec A o) → + truncate (≤-trans m≤n n≤o) xs ≡ truncate m≤n (truncate n≤o xs) +truncate-trans {m = zero} _ _ _ = refl +truncate-trans {m = suc _} {n = suc _} m≤n n≤o (x ∷ xs) = + cong (x ∷_) (truncate-trans (s≤s⁻¹ m≤n) (s≤s⁻¹ n≤o) xs) -truncate-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) → truncate {A = A} m≤n₁ ≗ truncate m≤n₂ -truncate-irrelevant m≤n₁ m≤n₂ xs = cong (λ m≤n → truncate m≤n xs) (≤-irrelevant m≤n₁ m≤n₂) - -truncate≡take : (m≤n : m ≤ n) (xs : Vec A n) .(eq : n ≡ m + o) → +truncate≡take : .(m≤n : m ≤ n) (xs : Vec A n) .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs) -truncate≡take z≤n _ eq = refl -truncate≡take (s≤s m≤n) (x ∷ xs) eq = cong (x ∷_) (truncate≡take m≤n xs (suc-injective eq)) +truncate≡take {m = zero} _ _ _ = refl +truncate≡take {m = suc _} m≤n (x ∷ xs) eq = + cong (x ∷_) (truncate≡take (s≤s⁻¹ m≤n) xs (suc-injective eq)) take≡truncate : ∀ m (xs : Vec A (m + n)) → take m xs ≡ truncate (m≤m+n m n) xs @@ -157,10 +158,11 @@ take≡truncate (suc m) (x ∷ xs) = cong (x ∷_) (take≡truncate m xs) ------------------------------------------------------------------------ -- truncate and padRight together -truncate-padRight : (m≤n : m ≤ n) (a : A) (xs : Vec A m) → +truncate-padRight : .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → truncate m≤n (padRight m≤n a xs) ≡ xs -truncate-padRight z≤n a [] = refl -truncate-padRight (s≤s m≤n) a (x ∷ xs) = cong (x ∷_) (truncate-padRight m≤n a xs) +truncate-padRight _ a [] = refl +truncate-padRight {n = suc _} m≤n a (x ∷ xs) = + cong (x ∷_) (truncate-padRight (s≤s⁻¹ m≤n) a xs) ------------------------------------------------------------------------ -- lookup @@ -187,10 +189,10 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero refl = refl []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p = []=⇒lookup∘lookup⇒[]= xs i p -lookup-truncate : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) → +lookup-truncate : .(m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) → lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n) -lookup-truncate (s≤s m≤m+n) (_ ∷ _) zero = refl -lookup-truncate (s≤s m≤m+n) (_ ∷ xs) (suc i) = lookup-truncate m≤m+n xs i +lookup-truncate _ (_ ∷ _) zero = refl +lookup-truncate m≤n (_ ∷ xs) (suc i) = lookup-truncate (suc[m]≤n⇒m≤pred[n] m≤n) xs i lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) @@ -1127,6 +1129,10 @@ sum-++ {ys = ys} (x ∷ xs) = begin ------------------------------------------------------------------------ -- replicate +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) + lookup-replicate : ∀ (i : Fin n) (x : A) → lookup (replicate n x) i ≡ x lookup-replicate zero x = refl lookup-replicate (suc i) x = lookup-replicate i x @@ -1168,10 +1174,6 @@ 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 _} m≡n x = cong (x ∷_) (cast-replicate (suc-injective m≡n) x) - ------------------------------------------------------------------------ -- pad @@ -1179,54 +1181,72 @@ 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-replicate : ∀ .(m≤n : m ≤ n) (a : A) → + replicate n a ≡ padRight m≤n a (replicate m a) +padRight-replicate {m = zero} _ a = refl +padRight-replicate {m = suc _} {n = suc _} m≤n a = + cong (a ∷_) (padRight-replicate (s≤s⁻¹ m≤n) a) -padRight-trans : ∀ (m≤n : m ≤ n) (n≤o : n ≤ o) (a : A) (xs : Vec A m) → +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-trans _ n≤o a [] = padRight-replicate n≤o a +padRight-trans {n = suc _} {o = suc _} m≤n n≤o a (x ∷ xs) = + cong (x ∷_) (padRight-trans (s≤s⁻¹ m≤n) (s≤s⁻¹ n≤o) a xs) -padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → +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-lookup {n = suc _} _ a (x ∷ xs) zero = refl +padRight-lookup {n = suc _} m≤n a (x ∷ xs) (suc i) = padRight-lookup (s≤s⁻¹ m≤n) a xs i -padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → +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-map f _ a [] = map-replicate f a _ +padRight-map {n = suc _} f m≤n a (x ∷ xs) = cong (f x ∷_) (padRight-map f (s≤s⁻¹ m≤n) a xs) -padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) +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 f _ a b [] [] = zipWith-replicate f a b +padRight-zipWith {n = suc _} f m≤n a b (x ∷ xs) (y ∷ ys) = + cong (f x y ∷_) (padRight-zipWith f (s≤s⁻¹ m≤n) a b xs ys) + +padRight-zipWith₁ : ∀ (f : A → B → C) .(m≤n : m ≤ n) .(n≤o : n ≤ o) + (a : A) (b : B) (xs : Vec A n) (ys : Vec B m) → + zipWith f (padRight n≤o a xs) (padRight (≤-trans m≤n n≤o) b ys) ≡ + padRight n≤o (f a b) (zipWith f xs (padRight m≤n b ys)) +padRight-zipWith₁ f m≤n n≤o a b xs ys = + trans (cong (zipWith f (padRight n≤o a xs)) (padRight-trans m≤n n≤o b ys)) + (padRight-zipWith f n≤o a b xs (padRight m≤n b ys)) + +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} _ a [] eq = cast-replicate eq a +padRight-drop {m = suc _} {n = suc _} m≤n a (x ∷ xs) eq = padRight-drop (s≤s⁻¹ m≤n) a xs (suc-injective eq) -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-drop′ : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → + let o , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in drop m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ replicate o a +padRight-drop′ m≤n a xs = let o , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in padRight-drop m≤n a xs (sym n≡m+o) -padRight-take : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → +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 [] 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-take {m = zero} _ a [] _ = refl +padRight-take {m = suc _} {n = suc _} m≤n a (x ∷ xs) eq = cong (x ∷_) (padRight-take (s≤s⁻¹ m≤n) a xs (suc-injective eq)) -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 [] 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-take′ : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → + let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in take m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ xs +padRight-take′ m≤n a xs = let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in padRight-take m≤n a xs (sym n≡m+o) -padRight-updateAt : ∀ (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) → +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 _} (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) +padRight-updateAt {n = suc _} m≤n (y ∷ xs) f zero x = refl +padRight-updateAt {n = suc _} m≤n (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt (s≤s⁻¹ m≤n) xs f i x) +-- ------------------------------------------------------------------------ -- iterate @@ -1618,3 +1638,13 @@ lookup-inject≤-take m m≤m+n i xs = sym (begin "Warning: lookup-inject≤-take was deprecated in v2.0. Please use lookup-take-inject≤ or lookup-truncate, take≡truncate instead." #-} + +-- Version 2.4 + +truncate-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) → truncate {A = A} m≤n₁ ≗ truncate m≤n₂ +truncate-irrelevant _ _ xs = refl +{-# WARNING_ON_USAGE truncate-irrelevant +"Warning: truncate-irrelevant was deprecated in v2.4. +Definition of truncate has been made definitionally proof-irrelevant." +#-} +