[ fix agda#1443 ] Also add cast for Vec

Author: gallais

CHANGELOG.md

@@ -1836,6 +1836,8 @@ Other minor changes
   diagonal           : Vec (Vec A n) n → Vec A n
   DiagonalBind._>>=_ : Vec A n → (A → Vec B n) → Vec B n
   _ʳ++_              : Vec A m → Vec A n → Vec A (m + n)
+
+  cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
 
 * Added new instance in `Data.Vec.Categorical`:
@@ -1894,6 +1896,15 @@ Other minor changes
   reverse-injective  : reverse xs ≡ reverse ys → xs ≡ ys
 
   transpose-replicate : transpose (replicate xs) ≡ map replicate xs
+
+  toList-cast   : toList (cast eq xs) ≡ toList xs
+  cast-is-id    : cast eq xs ≡ xs
+  cast-is-subst : cast eq xs ≡ subst (Vec A) eq xs
+  cast-trans    : cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
+  map-cast      : map f (cast eq xs) ≡ cast eq (map f xs)
+  lookup-cast   : lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
+  lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
+  lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
   ```
 
 * Added new proofs in `Data.Vec.Functional.Properties`:

src/Data/Fin/Properties.agda

@@ -257,7 +257,7 @@ toℕ-cast {n = suc n} eq zero    = refl
 toℕ-cast {n = suc n} eq (suc k) = cong suc (toℕ-cast (cong ℕ.pred eq) k)
 
 cast-is-id : .(eq : m ≡ m) (k : Fin m) → cast eq k ≡ k
-cast-is-id eq zero = refl
+cast-is-id eq zero    = refl
 cast-is-id eq (suc k) = cong suc (cast-is-id (ℕₚ.suc-injective eq) k)
 
 cast-is-subst : (eq : m ≡ n) (k : Fin m) → cast eq k ≡ subst Fin eq k

src/Data/Vec/Base.agda

@@ -16,7 +16,7 @@ open import Data.Product as Prod using (∃; ∃₂; _×_; _,_)
 open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (const; _∘′_; id; _∘_)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 open import Relation.Nullary using (does)
 open import Relation.Unary using (Pred; Decidable)
 
@@ -93,6 +93,10 @@ xs [ i ]≔ y = xs [ i ]%= const y
 ------------------------------------------------------------------------
 -- Operations for transforming vectors
 
+cast : .(eq : m ≡ n) → Vec A m → Vec A n
+cast {n = zero}  eq []       = []
+cast {n = suc _} eq (x ∷ xs) = x ∷ cast (cong pred eq) xs
+
 map : (A → B) → Vec A n → Vec B n
 map f []       = []
 map f (x ∷ xs) = f x ∷ map f xs

src/Data/Vec/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ; _↑ˡ_; _↑ʳ_)
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base
-open import Data.Nat.Properties
+open import Data.Nat.Properties as ℕₚ
   using (+-assoc; ≤-step; ≤-refl; ≤-trans)
 open import Data.Product as Prod
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
@@ -25,7 +25,7 @@ open import Function.Inverse using (_↔_; inverse)
 open import Level using (Level)
 open import Relation.Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
+  using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary using (Dec; does; yes; no)
 open import Relation.Nullary.Decidable using (map′)
@@ -39,7 +39,7 @@ private
     a b c d p : Level
     A B C D : Set a
     w x y z : A
-    m n : ℕ
+    m n o : ℕ
     ws xs ys zs : Vec A n
 
 ------------------------------------------------------------------------
@@ -386,6 +386,27 @@ lookup∘update′ : ∀ {i j} → i ≢ j → ∀ (xs : Vec A n) y →
                  lookup (xs [ j ]≔ y) i ≡ lookup xs i
 lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs
 
+------------------------------------------------------------------------
+-- cast
+
+toList-cast : ∀ .(eq : m ≡ n) (xs : Vec A m) → toList (cast eq xs) ≡ toList xs
+toList-cast {n = zero}  eq []       = refl
+toList-cast {n = suc _} eq (x ∷ xs) =
+  cong (x List.∷_) (toList-cast (cong pred eq) xs)
+
+cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
+cast-is-id eq []       = refl
+cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (ℕₚ.suc-injective eq) xs)
+
+cast-is-subst : (eq : m ≡ n) (xs : Vec A m) → cast eq xs ≡ subst (Vec A) eq xs
+cast-is-subst refl xs = cast-is-id refl xs
+
+cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (xs : Vec A m) →
+             cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
+cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
+cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
+  cong (x ∷_) (cast-trans (ℕₚ.suc-injective eq₁) (ℕₚ.suc-injective eq₂) xs)
+
 ------------------------------------------------------------------------
 -- map
 
@@ -397,6 +418,12 @@ map-const : ∀ (xs : Vec A n) (y : B) → map (const y) xs ≡ replicate y
 map-const []       _ = refl
 map-const (_ ∷ xs) y = cong (y ∷_) (map-const xs y)
 
+map-cast : (f : A → B) .(eq : m ≡ n) (xs : Vec A m) →
+           map f (cast eq xs) ≡ cast eq (map f xs)
+map-cast {n = zero}  f eq []       = refl
+map-cast {n = suc _} f eq (x ∷ xs)
+  = cong (f x ∷_) (map-cast f (ℕₚ.suc-injective eq) xs)
+
 map-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) →
          map f (xs ++ ys) ≡ map f xs ++ map f ys
 map-++ f []       ys = refl
@@ -487,9 +514,34 @@ lookup-splitAt (suc m) (x ∷ xs) ys (suc i) = trans
 ------------------------------------------------------------------------
 -- concat
 
-lookup-concat : ∀ (xss : Vec (Vec A m) n) i j → lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j
+lookup-cast : .(eq : m ≡ n) (xs : Vec A m) (i : Fin m) →
+              lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
+lookup-cast {n = suc _} eq (x ∷ _)  zero    = refl
+lookup-cast {n = suc _} eq (_ ∷ xs) (suc i) =
+  lookup-cast (ℕₚ.suc-injective eq) xs i
+
+lookup-cast₁ : .(eq : m ≡ n) (xs : Vec A m) (i : Fin n) →
+               lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
+lookup-cast₁ eq (x ∷ _)  zero    = refl
+lookup-cast₁ eq (_ ∷ xs) (suc i) =
+  lookup-cast₁ (ℕₚ.suc-injective eq) xs i
+
+lookup-cast₂ : .(eq : m ≡ n) (xs : Vec A n) (i : Fin m) →
+               lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
+lookup-cast₂ {n = suc _} eq (x ∷ _)  zero    = refl
+lookup-cast₂ {n = suc _} eq (_ ∷ xs) (suc i) =
+  lookup-cast₂ (ℕₚ.suc-injective eq) xs i
+
+lookup-concat : ∀ (xss : Vec (Vec A m) n) i j →
+                lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j
 lookup-concat (xs ∷ xss) zero j = lookup-++ˡ xs (concat xss) j
-lookup-concat (xs ∷ xss) (suc i) j = trans (lookup-++ʳ xs (concat xss) (Fin.combine i j)) (lookup-concat xss i j)
+lookup-concat (xs ∷ xss) (suc i) j = begin
+  lookup (concat (xs ∷ xss)) (Fin.combine (suc i) j)
+    ≡⟨ lookup-++ʳ xs (concat xss) (Fin.combine i j) ⟩
+  lookup (concat xss) (Fin.combine i j)
+    ≡⟨ lookup-concat xss i j ⟩
+  lookup (lookup (xs ∷ xss) (suc i)) j
+    ∎ where open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- zipWith