88
99module Data.Vec.Relation.Unary.All.Properties where
1010
11- open import Data.Nat.Base using (zero; suc; _+_)
11+ open import Data.Nat.Base using (ℕ; zero; suc; _+_)
1212open import Data.Fin.Base using (Fin; zero; suc)
1313open import Data.List.Base using ([]; _∷_)
1414open import Data.List.Relation.Unary.All as List using ([]; _∷_)
@@ -29,82 +29,89 @@ private
2929 a b p q : Level
3030 A : Set a
3131 B : Set b
32+ P : Pred A p
33+ Q : Pred B q
34+ m n : ℕ
35+ xs : Vec A n
3236
3337------------------------------------------------------------------------
34- -- map
35-
36- module _ {P : Pred B p} {f : A → B} where
37-
38- map⁺ : ∀ {n} {xs : Vec A n} → All (P ∘ f) xs → All P (map f xs)
39- map⁺ [] = []
40- map⁺ (px ∷ pxs) = px ∷ map⁺ pxs
41-
42- map⁻ : ∀ {n} {xs : Vec A n} → All P (map f xs) → All (P ∘ f) xs
43- map⁻ {xs = []} [] = []
44- map⁻ {xs = _ ∷ _} (px ∷ pxs) = px ∷ map⁻ pxs
38+ -- lookup
4539
46- -- A variant of All.map
47-
48- module _ {f : A → B} {P : Pred A p} {Q : Pred B q} where
40+ lookup⁺ : (i : Fin n) → All P xs → P (Vec.lookup xs i)
41+ lookup⁺ zero (px ∷ pxs) = px
42+ lookup⁺ (suc i) (px ∷ pxs) = lookup⁺ i pxs
4943
50- gmap : ∀ {n} → P ⋐ Q ∘ f → All P {n} ⋐ All Q {n} ∘ map f
51- gmap g = map⁺ ∘ All.map g
44+ lookup⁻ : (∀ i → P (Vec.lookup xs i)) → All P xs
45+ lookup⁻ {xs = []} pxs = []
46+ lookup⁻ {xs = _ ∷ _} pxs = pxs zero ∷ lookup⁻ (pxs ∘ suc)
5247
5348------------------------------------------------------------------------
54- -- _++_
55-
56- module _ {n} {P : Pred A p} where
57-
58- ++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
59- All P xs → All P ys → All P (xs ++ ys)
60- ++⁺ [] pys = pys
61- ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys
49+ -- map
6250
63- ++ˡ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
64- All P (xs ++ ys) → All P xs
65- ++ˡ⁻ [] _ = []
66- ++ˡ⁻ (x ∷ xs) (px ∷ pxs) = px ∷ ++ˡ⁻ xs pxs
51+ map⁺ : {f : A → B} → All (P ∘ f) xs → All P (map f xs)
52+ map⁺ [] = []
53+ map⁺ (px ∷ pxs) = px ∷ map⁺ pxs
6754
68- ++ʳ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
69- All P (xs ++ ys) → All P ys
70- ++ʳ⁻ [] pys = pys
71- ++ʳ⁻ (x ∷ xs) (px ∷ pxs) = ++ʳ⁻ xs pxs
55+ map⁻ : {f : A → B} → All P (map f xs) → All (P ∘ f) xs
56+ map⁻ {xs = []} [] = []
57+ map⁻ {xs = _ ∷ _} (px ∷ pxs) = px ∷ map⁻ pxs
7258
73- ++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
74- All P (xs ++ ys) → All P xs × All P ys
75- ++⁻ [] p = [] , p
76- ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map₁ (px ∷_) (++⁻ _ pxs)
59+ -- A variant of All.map
7760
78- ++⁺∘++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
79- (p : All P (xs ++ ys)) →
80- uncurry′ ++⁺ (++⁻ xs p) ≡ p
81- ++⁺∘++⁻ [] p = refl
82- ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = cong (px ∷_) (++⁺∘++⁻ xs pxs)
61+ gmap : {f : A → B} → P ⋐ Q ∘ f → All P {n} ⋐ All Q {n} ∘ map f
62+ gmap g = map⁺ ∘ All.map g
8363
84- ++⁻∘++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
85- (p : All P xs × All P ys) →
86- ++⁻ xs (uncurry ++⁺ p) ≡ p
87- ++⁻∘++⁺ ([] , pys) = refl
88- ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = refl
64+ ------------------------------------------------------------------------
65+ -- _++_
8966
90- ++↔ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
91- (All P xs × All P ys) ↔ All P (xs ++ ys)
92- ++↔ {xs = xs} = inverse (uncurry ++⁺) (++⁻ xs) ++⁻∘++⁺ (++⁺∘++⁻ xs)
67+ ++⁺ : {xs : Vec A m} {ys : Vec A n} →
68+ All P xs → All P ys → All P (xs ++ ys)
69+ ++⁺ [] pys = pys
70+ ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys
71+
72+ ++ˡ⁻ : (xs : Vec A m) {ys : Vec A n} →
73+ All P (xs ++ ys) → All P xs
74+ ++ˡ⁻ [] _ = []
75+ ++ˡ⁻ (x ∷ xs) (px ∷ pxs) = px ∷ ++ˡ⁻ xs pxs
76+
77+ ++ʳ⁻ : (xs : Vec A m) {ys : Vec A n} →
78+ All P (xs ++ ys) → All P ys
79+ ++ʳ⁻ [] pys = pys
80+ ++ʳ⁻ (x ∷ xs) (px ∷ pxs) = ++ʳ⁻ xs pxs
81+
82+ ++⁻ : (xs : Vec A m) {ys : Vec A n} →
83+ All P (xs ++ ys) → All P xs × All P ys
84+ ++⁻ [] p = [] , p
85+ ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map₁ (px ∷_) (++⁻ _ pxs)
86+
87+ ++⁺∘++⁻ : (xs : Vec A m) {ys : Vec A n} →
88+ (p : All P (xs ++ ys)) →
89+ uncurry′ ++⁺ (++⁻ xs p) ≡ p
90+ ++⁺∘++⁻ [] p = refl
91+ ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = cong (px ∷_) (++⁺∘++⁻ xs pxs)
92+
93+ ++⁻∘++⁺ : {xs : Vec A m} {ys : Vec A n} →
94+ (p : All P xs × All P ys) →
95+ ++⁻ xs (uncurry ++⁺ p) ≡ p
96+ ++⁻∘++⁺ ([] , pys) = refl
97+ ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = refl
98+
99+ ++↔ : {xs : Vec A m} {ys : Vec A n} →
100+ (All P xs × All P ys) ↔ All P (xs ++ ys)
101+ ++↔ {xs = xs} = inverse (uncurry ++⁺) (++⁻ xs) ++⁻∘++⁺ (++⁺∘++⁻ xs)
93102
94103------------------------------------------------------------------------
95104-- concat
96105
97- module _ {m} {P : Pred A p} where
98-
99- concat⁺ : ∀ {n} {xss : Vec (Vec A m) n} →
100- All (All P) xss → All P (concat xss)
101- concat⁺ [] = []
102- concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)
106+ concat⁺ : {xss : Vec (Vec A m) n} →
107+ All (All P) xss → All P (concat xss)
108+ concat⁺ [] = []
109+ concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)
103110
104- concat⁻ : ∀ {n} (xss : Vec (Vec A m) n) →
105- All P (concat xss) → All (All P) xss
106- concat⁻ [] [] = []
107- concat⁻ (xs ∷ xss) pxss = ++ˡ⁻ xs pxss ∷ concat⁻ xss (++ʳ⁻ xs pxss)
111+ concat⁻ : (xss : Vec (Vec A m) n) →
112+ All P (concat xss) → All (All P) xss
113+ concat⁻ [] [] = []
114+ concat⁻ (xs ∷ xss) pxss = ++ˡ⁻ xs pxss ∷ concat⁻ xss (++ʳ⁻ xs pxss)
108115
109116------------------------------------------------------------------------
110117-- swap
@@ -139,17 +146,15 @@ module _ {P : A → Set p} where
139146------------------------------------------------------------------------
140147-- take and drop
141148
142- module _ {P : A → Set p} where
143-
144- drop⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {n} (drop m xs)
145- drop⁺ zero pxs = pxs
146- drop⁺ (suc m) {x ∷ xs} (px ∷ pxs)
147- rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs
149+ drop⁺ : ∀ m {xs} → All P {m + n} xs → All P {n} (drop m xs)
150+ drop⁺ zero pxs = pxs
151+ drop⁺ (suc m) {x ∷ xs} (px ∷ pxs)
152+ rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs
148153
149- take⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {m} (take m xs)
150- take⁺ zero pxs = []
151- take⁺ (suc m) {x ∷ xs} (px ∷ pxs)
152- rewrite Vecₚ.unfold-take m x xs = px ∷ take⁺ m pxs
154+ take⁺ : ∀ m {xs} → All P {m + n} xs → All P {m} (take m xs)
155+ take⁺ zero pxs = []
156+ take⁺ (suc m) {x ∷ xs} (px ∷ pxs)
157+ rewrite Vecₚ.unfold-take m x xs = px ∷ take⁺ m pxs
153158
154159------------------------------------------------------------------------
155160-- toList
0 commit comments