{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Functional.Properties where
open import Data.Empty using (⊥-elim)
open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ<; reduce≥;
_↑ˡ_; _↑ʳ_; punchIn; punchOut)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
import Data.Nat.Properties as ℕ
open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
open import Data.List.Base as List using (List)
import Data.List.Properties as List
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Data.Vec.Base as Vec using (Vec)
import Data.Vec.Properties as Vec
open import Data.Vec.Functional using (Vector; head; tail; updateAt;
map; _++_; insertAt; removeAt; toVec; fromVec; toList; fromList)
open import Function.Base using (_∘_; id)
open import Level using (Level)
open import Relation.Binary.Definitions using (DecidableEquality; Decidable)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; _≗_; refl; _≢_; cong)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning)
open import Relation.Nullary.Decidable
using (Dec; does; yes; no; map′; _×-dec_)
import Data.Fin.Properties as Finₚ
private
variable
a b c : Level
A B C : Set a
m n : ℕ
module _ {xs ys : Vector A (suc n)} where
∷-cong : head xs ≡ head ys → tail xs ≗ tail ys → xs ≗ ys
∷-cong eq _ zero = eq
∷-cong _ eq (suc i) = eq i
∷-injective : xs ≗ ys → head xs ≡ head ys × tail xs ≗ tail ys
∷-injective eq = eq zero , eq ∘ suc
≗-dec : DecidableEquality A → Decidable {A = Vector A n} _≗_
≗-dec {n = zero} _≟_ xs ys = yes λ ()
≗-dec {n = suc n} _≟_ xs ys =
map′ (Product.uncurry ∷-cong) ∷-injective
(head xs ≟ head ys ×-dec ≗-dec _≟_ (tail xs) (tail ys))
updateAt-updates : ∀ (i : Fin n) {f : A → A} (xs : Vector A n) →
updateAt xs i f i ≡ f (xs i)
updateAt-updates zero xs = refl
updateAt-updates (suc i) xs = updateAt-updates i (tail xs)
updateAt-minimal : ∀ (i j : Fin n) {f : A → A} (xs : Vector A n) →
i ≢ j → updateAt xs j f i ≡ xs i
updateAt-minimal zero zero xs 0≢0 = ⊥-elim (0≢0 refl)
updateAt-minimal zero (suc j) xs _ = refl
updateAt-minimal (suc i) zero xs _ = refl
updateAt-minimal (suc i) (suc j) xs i≢j = updateAt-minimal i j (tail xs) (i≢j ∘ cong suc)
updateAt-id-local : ∀ (i : Fin n) {f : A → A} (xs : Vector A n) →
f (xs i) ≡ xs i →
updateAt xs i f ≗ xs
updateAt-id-local zero xs eq zero = eq
updateAt-id-local zero xs eq (suc j) = refl
updateAt-id-local (suc i) xs eq zero = refl
updateAt-id-local (suc i) xs eq (suc j) = updateAt-id-local i (tail xs) eq j
updateAt-id : ∀ (i : Fin n) (xs : Vector A n) →
updateAt xs i id ≗ xs
updateAt-id i xs = updateAt-id-local i xs refl
updateAt-updateAt-local : ∀ (i : Fin n) {f g h : A → A} (xs : Vector A n) →
f (g (xs i)) ≡ h (xs i) →
updateAt (updateAt xs i g) i f ≗ updateAt xs i h
updateAt-updateAt-local zero xs eq zero = eq
updateAt-updateAt-local zero xs eq (suc j) = refl
updateAt-updateAt-local (suc i) xs eq zero = refl
updateAt-updateAt-local (suc i) xs eq (suc j) = updateAt-updateAt-local i (tail xs) eq j
updateAt-updateAt : ∀ (i : Fin n) {f g : A → A} (xs : Vector A n) →
updateAt (updateAt xs i g) i f ≗ updateAt xs i (f ∘ g)
updateAt-updateAt i xs = updateAt-updateAt-local i xs refl
updateAt-cong-local : ∀ (i : Fin n) {f g : A → A} (xs : Vector A n) →
f (xs i) ≡ g (xs i) →
updateAt xs i f ≗ updateAt xs i g
updateAt-cong-local zero xs eq zero = eq
updateAt-cong-local zero xs eq (suc j) = refl
updateAt-cong-local (suc i) xs eq zero = refl
updateAt-cong-local (suc i) xs eq (suc j) = updateAt-cong-local i (tail xs) eq j
updateAt-cong : ∀ (i : Fin n) {f g : A → A} → f ≗ g → (xs : Vector A n) →
updateAt xs i f ≗ updateAt xs i g
updateAt-cong i eq xs = updateAt-cong-local i xs (eq (xs i))
updateAt-commutes : ∀ (i j : Fin n) {f g : A → A} → i ≢ j → (xs : Vector A n) →
updateAt (updateAt xs j g) i f ≗ updateAt (updateAt xs i f) j g
updateAt-commutes zero zero 0≢0 xs k = ⊥-elim (0≢0 refl)
updateAt-commutes zero (suc j) _ xs zero = refl
updateAt-commutes zero (suc j) _ xs (suc k) = refl
updateAt-commutes (suc i) zero _ xs zero = refl
updateAt-commutes (suc i) zero _ xs (suc k) = refl
updateAt-commutes (suc i) (suc j) _ xs zero = refl
updateAt-commutes (suc i) (suc j) i≢j xs (suc k) = updateAt-commutes i j (i≢j ∘ cong suc) (tail xs) k
map-id : (xs : Vector A n) → map id xs ≗ xs
map-id xs = λ _ → refl
map-cong : ∀ {f g : A → B} → f ≗ g → (xs : Vector A n) → map f xs ≗ map g xs
map-cong f≗g xs = f≗g ∘ xs
map-∘ : ∀ {f : B → C} {g : A → B} (xs : Vector A n) →
map (f ∘ g) xs ≗ map f (map g xs)
map-∘ xs = λ _ → refl
lookup-map : ∀ (i : Fin n) (f : A → B) (xs : Vector A n) →
map f xs i ≡ f (xs i)
lookup-map i f xs = refl
map-updateAt-local : ∀ {f : A → B} {g : A → A} {h : B → B}
(xs : Vector A n) (i : Fin n) →
f (g (xs i)) ≡ h (f (xs i)) →
map f (updateAt xs i g) ≗ updateAt (map f xs) i h
map-updateAt-local {n = suc n} {f = f} xs zero eq zero = eq
map-updateAt-local {n = suc n} {f = f} xs zero eq (suc j) = refl
map-updateAt-local {n = suc (suc n)} {f = f} xs (suc i) eq zero = refl
map-updateAt-local {n = suc (suc n)} {f = f} xs (suc i) eq (suc j) = map-updateAt-local {f = f} (tail xs) i eq j
map-updateAt : ∀ {f : A → B} {g : A → A} {h : B → B} →
f ∘ g ≗ h ∘ f →
(xs : Vector A n) (i : Fin n) →
map f (updateAt xs i g) ≗ updateAt (map f xs) i h
map-updateAt {f = f} {g = g} f∘g≗h∘f xs i = map-updateAt-local {f = f} {g = g} xs i (f∘g≗h∘f (xs i))
lookup-++-< : ∀ (xs : Vector A m) (ys : Vector A n) →
∀ i (i<m : toℕ i ℕ.< m) →
(xs ++ ys) i ≡ xs (fromℕ< i<m)
lookup-++-< {m = m} xs ys i i<m = cong Sum.[ xs , ys ] (Finₚ.splitAt-< m i i<m)
lookup-++-≥ : ∀ (xs : Vector A m) (ys : Vector A n) →
∀ i (i≥m : toℕ i ℕ.≥ m) →
(xs ++ ys) i ≡ ys (reduce≥ i i≥m)
lookup-++-≥ {m = m} xs ys i i≥m = cong Sum.[ xs , ys ] (Finₚ.splitAt-≥ m i i≥m)
lookup-++ˡ : ∀ (xs : Vector A m) (ys : Vector A n) i →
(xs ++ ys) (i ↑ˡ n) ≡ xs i
lookup-++ˡ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-↑ˡ m i n)
lookup-++ʳ : ∀ (xs : Vector A m) (ys : Vector A n) i →
(xs ++ ys) (m ↑ʳ i) ≡ ys i
lookup-++ʳ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-↑ʳ m n i)
module _ {ys ys′ : Vector A m} where
++-cong : ∀ (xs xs′ : Vector A n) →
xs ≗ xs′ → ys ≗ ys′ → xs ++ ys ≗ xs′ ++ ys′
++-cong {n} xs xs′ eq₁ eq₂ i with toℕ i ℕ.<? n
... | yes i<n = begin
(xs ++ ys) i ≡⟨ lookup-++-< xs ys i i<n ⟩
xs (fromℕ< i<n) ≡⟨ eq₁ (fromℕ< i<n) ⟩
xs′ (fromℕ< i<n) ≡⟨ lookup-++-< xs′ ys′ i i<n ⟨
(xs′ ++ ys′) i ∎
where open ≡-Reasoning
... | no i≮n = begin
(xs ++ ys) i ≡⟨ lookup-++-≥ xs ys i (ℕ.≮⇒≥ i≮n) ⟩
ys (reduce≥ i (ℕ.≮⇒≥ i≮n)) ≡⟨ eq₂ (reduce≥ i (ℕ.≮⇒≥ i≮n)) ⟩
ys′ (reduce≥ i (ℕ.≮⇒≥ i≮n)) ≡⟨ lookup-++-≥ xs′ ys′ i (ℕ.≮⇒≥ i≮n) ⟨
(xs′ ++ ys′) i ∎
where open ≡-Reasoning
++-injectiveˡ : ∀ (xs xs′ : Vector A n) →
xs ++ ys ≗ xs′ ++ ys′ → xs ≗ xs′
++-injectiveˡ xs xs′ eq i = begin
xs i ≡⟨ lookup-++ˡ xs ys i ⟨
(xs ++ ys) (i ↑ˡ m) ≡⟨ eq (i ↑ˡ m) ⟩
(xs′ ++ ys′) (i ↑ˡ m) ≡⟨ lookup-++ˡ xs′ ys′ i ⟩
xs′ i ∎
where open ≡-Reasoning
++-injectiveʳ : ∀ (xs xs′ : Vector A n) → xs ++ ys ≗ xs′ ++ ys′ → ys ≗ ys′
++-injectiveʳ {n} xs xs′ eq i = begin
ys i ≡⟨ lookup-++ʳ xs ys i ⟨
(xs ++ ys) (n ↑ʳ i) ≡⟨ eq (n ↑ʳ i) ⟩
(xs′ ++ ys′) (n ↑ʳ i) ≡⟨ lookup-++ʳ xs′ ys′ i ⟩
ys′ i ∎
where open ≡-Reasoning
++-injective : ∀ (xs xs′ : Vector A n) →
xs ++ ys ≗ xs′ ++ ys′ → xs ≗ xs′ × ys ≗ ys′
++-injective xs xs′ eq = ++-injectiveˡ xs xs′ eq , ++-injectiveʳ xs xs′ eq
insertAt-lookup : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A) →
insertAt xs i v i ≡ v
insertAt-lookup {n = n} xs zero v = refl
insertAt-lookup {n = suc n} xs (suc i) v = insertAt-lookup (tail xs) i v
insertAt-punchIn : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A)
(j : Fin n) →
insertAt xs i v (punchIn i j) ≡ xs j
insertAt-punchIn {n = suc n} xs zero v j = refl
insertAt-punchIn {n = suc n} xs (suc i) v zero = refl
insertAt-punchIn {n = suc n} xs (suc i) v (suc j) = insertAt-punchIn (tail xs) i v j
removeAt-punchOut : ∀ (xs : Vector A (suc n))
{i : Fin (suc n)} {j : Fin (suc n)} (i≢j : i ≢ j) →
removeAt xs i (punchOut i≢j) ≡ xs j
removeAt-punchOut {n = n} xs {zero} {zero} i≢j = ⊥-elim (i≢j refl)
removeAt-punchOut {n = suc n} xs {zero} {suc j} i≢j = refl
removeAt-punchOut {n = suc n} xs {suc i} {zero} i≢j = refl
removeAt-punchOut {n = suc n} xs {suc i} {suc j} i≢j = removeAt-punchOut (tail xs) (i≢j ∘ cong suc)
removeAt-insertAt : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A) →
removeAt (insertAt xs i v) i ≗ xs
removeAt-insertAt xs zero v j = refl
removeAt-insertAt xs (suc i) v zero = refl
removeAt-insertAt xs (suc i) v (suc j) = removeAt-insertAt (tail xs) i v j
insertAt-removeAt : ∀ (xs : Vector A (suc n)) (i : Fin (suc n)) →
insertAt (removeAt xs i) i (xs i) ≗ xs
insertAt-removeAt {n = n} xs zero zero = refl
insertAt-removeAt {n = n} xs zero (suc j) = refl
insertAt-removeAt {n = suc n} xs (suc i) zero = refl
insertAt-removeAt {n = suc n} xs (suc i) (suc j) = insertAt-removeAt (tail xs) i j
toVec∘fromVec : (xs : Vec A n) → toVec (fromVec xs) ≡ xs
toVec∘fromVec = Vec.tabulate∘lookup
fromVec∘toVec : (xs : Vector A n) → fromVec (toVec xs) ≗ xs
fromVec∘toVec = Vec.lookup∘tabulate
toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
toList∘fromList = List.tabulate-lookup
updateAt-id-relative = updateAt-id-local
{-# WARNING_ON_USAGE updateAt-id-relative
"Warning: updateAt-id-relative was deprecated in v2.0.
Please use updateAt-id-local instead."
#-}
updateAt-compose-relative = updateAt-updateAt-local
{-# WARNING_ON_USAGE updateAt-compose-relative
"Warning: updateAt-compose-relative was deprecated in v2.0.
Please use updateAt-updateAt-local instead."
#-}
updateAt-compose = updateAt-updateAt
{-# WARNING_ON_USAGE updateAt-compose
"Warning: updateAt-compose was deprecated in v2.0.
Please use updateAt-updateAt instead."
#-}
updateAt-cong-relative = updateAt-cong-local
{-# WARNING_ON_USAGE updateAt-cong-relative
"Warning: updateAt-cong-relative was deprecated in v2.0.
Please use updateAt-cong-local instead."
#-}
insert-lookup = insertAt-lookup
{-# WARNING_ON_USAGE insert-lookup
"Warning: insert-lookup was deprecated in v2.0.
Please use insertAt-lookup instead."
#-}
insert-punchIn = insertAt-punchIn
{-# WARNING_ON_USAGE insert-punchIn
"Warning: insert-punchIn was deprecated in v2.0.
Please use insertAt-punchIn instead."
#-}
remove-punchOut = removeAt-punchOut
{-# WARNING_ON_USAGE remove-punchOut
"Warning: remove-punchOut was deprecated in v2.0.
Please use removeAt-punchOut instead."
#-}
remove-insert = removeAt-insertAt
{-# WARNING_ON_USAGE remove-insert
"Warning: remove-insert was deprecated in v2.0.
Please use removeAt-insertAt instead."
#-}
insert-remove = insertAt-removeAt
{-# WARNING_ON_USAGE insert-remove
"Warning: insert-remove was deprecated in v2.0.
Please use insertAt-removeAt instead."
#-}