------------------------------------------------------------------------ -- The Agda standard library -- -- Some Vector-related properties ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Vec.Functional.Properties where 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_) open import Relation.Nullary.Negation using (contradiction) 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 -- (+) updateAt i actually updates the element at index i. 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 i does not touch the elements at other indices. 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 = contradiction refl 0≢0 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 i is a monoid morphism from A → A to Vector A n → Vector A n. 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)) -- The order of updates at different indices i ≢ j does not matter. 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 = contradiction refl 0≢0 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 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 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 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 = contradiction refl i≢j 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 ------------------------------------------------------------------------ -- Conversion functions 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 ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 2.0 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." #-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4