------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Functional.Relation.Unary.All.Properties where
open import Data.Nat.Base using (ℕ)
open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt)
open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ)
open import Data.Product.Base as Σ using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Functional as VF hiding (map)
open import Data.Vec.Functional.Relation.Unary.All
open import Function.Base using (const; _∘_)
open import Level using (Level)
open import Relation.Unary using (Pred; _⟨×⟩_)
private
variable
a p ℓ : Level
A B C : Set a
P Q R : Pred A p
m n : ℕ
x y : A
xs ys : Vector A n
------------------------------------------------------------------------
-- map
map⁺ : ∀ {f : A → B} → (∀ {x} → P x → Q (f x)) →
All P xs → All Q (VF.map f xs)
map⁺ pq ps i = pq (ps i)
------------------------------------------------------------------------
-- replicate
replicate⁺ : P x → All P (replicate n x)
replicate⁺ = const
------------------------------------------------------------------------
-- _⊛_
⊛⁺ : ∀ {fs : Vector (A → B) n} →
All (λ f → ∀ {x} → P x → Q (f x)) fs →
All P xs → All Q (fs ⊛ xs)
⊛⁺ pqs ps i = (pqs i) (ps i)
------------------------------------------------------------------------
-- zipWith
zipWith⁺ : ∀ {f} → (∀ {x y} → P x → Q y → R (f x y)) →
All P xs → All Q ys → All R (zipWith f xs ys)
zipWith⁺ pqr ps qs i = pqr (ps i) (qs i)
------------------------------------------------------------------------
-- zip
zip⁺ : All P xs → All Q ys → All (P ⟨×⟩ Q) (zip xs ys)
zip⁺ ps qs i = ps i , qs i
zip⁻ : All (P ⟨×⟩ Q) (zip xs ys) → All P xs × All Q ys
zip⁻ pqs = proj₁ ∘ pqs , proj₂ ∘ pqs
------------------------------------------------------------------------
-- head
head⁺ : ∀ (P : Pred A p) → All P xs → P (head xs)
head⁺ P ps = ps zero
------------------------------------------------------------------------
-- tail
tail⁺ : ∀ (P : Pred A p) → All P xs → All P (tail xs)
tail⁺ P xs = xs ∘ suc
------------------------------------------------------------------------
-- ++
module _ (P : Pred A p) {xs : Vector A m} {ys : Vector A n} where
++⁺ : All P xs → All P ys → All P (xs ++ ys)
++⁺ pxs pys i with splitAt m i
... | inj₁ i′ = pxs i′
... | inj₂ j′ = pys j′
module _ (P : Pred A p) (xs : Vector A m) {ys : Vector A n} where
++⁻ˡ : All P (xs ++ ys) → All P xs
++⁻ˡ ps i with ps (i ↑ˡ n)
... | p rewrite splitAt-↑ˡ m i n = p
++⁻ʳ : All P (xs ++ ys) → All P ys
++⁻ʳ ps i with ps (m ↑ʳ i)
... | p rewrite splitAt-↑ʳ m n i = p
++⁻ : All P (xs ++ ys) → All P xs × All P ys
++⁻ ps = ++⁻ˡ ps , ++⁻ʳ ps
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