module Data.Vec.All.Properties where
open import Data.Vec as Vec using (Vec; []; _∷_; zip; concat; _++_)
open import Data.Vec.Properties using (map-id; lookup-zip)
open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
open import Data.Vec.All as All using (All; []; _∷_)
open import Function
open import Function.Inverse using (_↔_)
open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
open import Relation.Binary using (REL; Trans)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
All-irrelevance : ∀ {a p} {A : Set a} {P : Pred A p} →
P.IrrelevantPred P →
∀ {n} → P.IrrelevantPred (All P {n})
All-irrelevance irr [] [] = P.refl
All-irrelevance irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
P.cong₂ _∷_ (irr px₁ px₂) (All-irrelevance irr pxs₁ pxs₂)
All-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
{f : A → B} {k} {xs : Vec A k} →
All (P ∘ f) xs → All P (Vec.map f xs)
All-map [] = []
All-map (px ∷ pxs) = px ∷ All-map pxs
map-All : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
{f : A → B} {k} {xs : Vec A k} →
All P (Vec.map f xs) → All (P ∘ f) xs
map-All {xs = []} [] = []
map-All {xs = _ ∷ _} (px ∷ pxs) = px ∷ map-All pxs
gmap : ∀ {a b p q}
{A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
{f : A → B} {k} →
P ⋐ Q ∘ f → All P {k} ⋐ All Q {k} ∘ Vec.map f
gmap g = All-map ∘ All.map g
module _ {a n p} {A : Set a} {P : A → Set p} where
All-++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
All P xs → All P ys → All P (xs ++ ys)
All-++⁺ [] pys = pys
All-++⁺ (px ∷ pxs) pys = px ∷ All-++⁺ pxs pys
All-++ˡ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
All P (xs ++ ys) → All P xs
All-++ˡ⁻ [] _ = []
All-++ˡ⁻ (x ∷ xs) (px ∷ pxs) = px ∷ All-++ˡ⁻ xs pxs
All-++ʳ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
All P (xs ++ ys) → All P ys
All-++ʳ⁻ [] pys = pys
All-++ʳ⁻ (x ∷ xs) (px ∷ pxs) = All-++ʳ⁻ xs pxs
All-++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
All P (xs ++ ys) → All P xs × All P ys
All-++⁻ [] p = [] , p
All-++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (px ∷_) id (All-++⁻ _ pxs)
All-++⁺∘++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
(p : All P (xs ++ ys)) →
uncurry′ All-++⁺ (All-++⁻ xs p) ≡ p
All-++⁺∘++⁻ [] p = P.refl
All-++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = P.cong (px ∷_) (All-++⁺∘++⁻ xs pxs)
All-++⁻∘++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
(p : All P xs × All P ys) →
All-++⁻ xs (uncurry All-++⁺ p) ≡ p
All-++⁻∘++⁺ ([] , pys) = P.refl
All-++⁻∘++⁺ (px ∷ pxs , pys) rewrite All-++⁻∘++⁺ (pxs , pys) = P.refl
++↔ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
(All P xs × All P ys) ↔ All P (xs ++ ys)
++↔ {xs = xs} = record
{ to = P.→-to-⟶ $ uncurry All-++⁺
; from = P.→-to-⟶ $ All-++⁻ xs
; inverse-of = record
{ left-inverse-of = All-++⁻∘++⁺
; right-inverse-of = All-++⁺∘++⁻ xs
}
}
module _ {a m p} {A : Set a} {P : A → Set p} where
All-concat⁺ : ∀ {n} {xss : Vec (Vec A m) n} →
All (All P) xss → All P (concat xss)
All-concat⁺ [] = []
All-concat⁺ (pxs ∷ pxss) = All-++⁺ pxs (All-concat⁺ pxss)
All-concat⁻ : ∀ {n} (xss : Vec (Vec A m) n) →
All P (concat xss) → All (All P) xss
All-concat⁻ [] [] = []
All-concat⁻ (xs ∷ xss) pxss = All-++ˡ⁻ xs pxss ∷ All-concat⁻ xss (All-++ʳ⁻ xs pxss)