12
12
open import Category.Monad.Identity
13
13
open import Data.Vec
14
14
open import Data.Nat
15
open import Data.Empty using (⊥-elim)
15
16
import Data.Nat.Properties as Nat
16
17
open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
17
18
open import Data.Fin.Props using (_+′_)
42
43
map-++-commute f [] = refl _
43
44
map-++-commute f (x ∷ xs) = SS.refl ∷-cong map-++-commute f xs
45
open import Relation.Binary.PropositionalEquality as PropEq
46
open import Relation.Binary.HeterogeneousEquality as HetEq
46
open import Relation.Binary.PropositionalEquality as P
47
using (_≡_; _≢_; refl; _≗_)
48
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
48
50
-- lookup is an applicative functor morphism.
78
80
tabulate∘lookup : ∀ {a n} {A : Set a} (xs : Vec A n) →
79
81
tabulate (flip lookup xs) ≡ xs
80
82
tabulate∘lookup [] = refl
81
tabulate∘lookup (x ∷ xs) = PropEq.cong (_∷_ x) $ tabulate∘lookup xs
83
tabulate∘lookup (x ∷ xs) = P.cong (_∷_ x) $ tabulate∘lookup xs
83
85
-- If you look up an index in allFin n, then you get the index.
121
123
map-cong : ∀ {a b n} {A : Set a} {B : Set b} {f g : A → B} →
122
124
f ≗ g → _≗_ {A = Vec A n} (map f) (map g)
123
125
map-cong f≗g [] = refl
124
map-cong f≗g (x ∷ xs) = PropEq.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
126
map-cong f≗g (x ∷ xs) = P.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
126
128
-- map is functorial.
128
130
map-id : ∀ {a n} {A : Set a} → _≗_ {A = Vec A n} (map id) id
130
map-id (x ∷ xs) = PropEq.cong (_∷_ x) (map-id xs)
132
map-id (x ∷ xs) = P.cong (_∷_ x) (map-id xs)
132
134
map-∘ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c}
133
135
(f : B → C) (g : A → B) →
134
136
_≗_ {A = Vec A n} (map (f ∘ g)) (map f ∘ map g)
135
137
map-∘ f g [] = refl
136
map-∘ f g (x ∷ xs) = PropEq.cong (_∷_ (f (g x))) (map-∘ f g xs)
138
map-∘ f g (x ∷ xs) = P.cong (_∷_ (f (g x))) (map-∘ f g xs)
138
140
-- tabulate can be expressed using map and allFin.
142
144
tabulate (f ∘ g) ≡ map f (tabulate g)
143
145
tabulate-∘ {zero} f g = refl
144
146
tabulate-∘ {suc n} f g =
145
PropEq.cong (_∷_ (f (g zero))) (tabulate-∘ f (g ∘ suc))
147
P.cong (_∷_ (f (g zero))) (tabulate-∘ f (g ∘ suc))
147
149
tabulate-allFin : ∀ {n a} {A : Set a} (f : Fin n → A) →
148
150
tabulate f ≡ map f (allFin n)
151
153
-- The positive case of allFin can be expressed recursively using map.
153
155
allFin-map : ∀ n → allFin (suc n) ≡ zero ∷ map suc (allFin n)
154
allFin-map n = PropEq.cong (_∷_ zero) $ tabulate-∘ suc id
156
allFin-map n = P.cong (_∷_ zero) $ tabulate-∘ suc id
156
158
-- If you look up every possible index, in increasing order, then you
157
159
-- get back the vector you started with.
159
161
map-lookup-allFin : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
160
162
map (λ x → lookup x xs) (allFin n) ≡ xs
161
163
map-lookup-allFin {n = n} xs = begin
162
map (λ x → lookup x xs) (allFin n) ≡⟨ PropEq.sym $ tabulate-∘ (λ x → lookup x xs) id ⟩
164
map (λ x → lookup x xs) (allFin n) ≡⟨ P.sym $ tabulate-∘ (λ x → lookup x xs) id ⟩
163
165
tabulate (λ x → lookup x xs) ≡⟨ tabulate∘lookup xs ⟩
165
where open ≡-Reasoning
167
where open P.≡-Reasoning
167
169
-- sum commutes with _++_.
171
173
sum-++-commute [] = refl
172
174
sum-++-commute (x ∷ xs) {ys} = begin
173
175
x + sum (xs ++ ys)
174
≡⟨ PropEq.cong (λ p → x + p) (sum-++-commute xs) ⟩
176
≡⟨ P.cong (λ p → x + p) (sum-++-commute xs) ⟩
175
177
x + (sum xs + sum ys)
176
≡⟨ PropEq.sym (+-assoc x (sum xs) (sum ys)) ⟩
178
≡⟨ P.sym (+-assoc x (sum xs) (sum ys)) ⟩
177
179
sum (x ∷ xs) + sum ys
181
183
open CommutativeSemiring Nat.commutativeSemiring hiding (_+_; sym)
183
185
-- foldr is a congruence.
252
254
(p q : xs [ i ]= x) → p ≡ q
253
255
proof-irrelevance-[]= here here = refl
254
256
proof-irrelevance-[]= (there xs[i]=x) (there xs[i]=x') =
255
PropEq.cong there (proof-irrelevance-[]= xs[i]=x xs[i]=x')
257
P.cong there (proof-irrelevance-[]= xs[i]=x xs[i]=x')
257
259
-- _[_]=_ can be expressed using lookup and _≡_.
259
261
[]=↔lookup : ∀ {a n i} {A : Set a} {x} {xs : Vec A n} →
260
262
xs [ i ]= x ↔ lookup i xs ≡ x
261
263
[]=↔lookup {i = i} {x = x} {xs} = record
262
{ to = PropEq.→-to-⟶ to
263
; from = PropEq.→-to-⟶ (from i xs)
265
; from = P.→-to-⟶ (from i xs)
264
266
; inverse-of = record
265
267
{ left-inverse-of = λ _ → proof-irrelevance-[]= _ _
266
; right-inverse-of = λ _ → PropEq.proof-irrelevance _ _
268
; right-inverse-of = λ _ → P.proof-irrelevance _ _
274
276
from : ∀ {n} (i : Fin n) xs → lookup i xs ≡ x → xs [ i ]= x
275
277
from zero (.x ∷ _) refl = here
276
278
from (suc i) (_ ∷ xs) p = there (from i xs p)
280
------------------------------------------------------------------------
281
-- Some properties related to _[_]≔_
284
∀ {n a} {A : Set a} (xs : Vec A n) (i : Fin n) {x₁ x₂ : A} →
285
(xs [ i ]≔ x₁) [ i ]≔ x₂ ≡ xs [ i ]≔ x₂
287
[]≔-idempotent (x ∷ xs) zero = refl
288
[]≔-idempotent (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-idempotent xs i
291
∀ {n a} {A : Set a} (xs : Vec A n) (i j : Fin n) {x y : A} →
292
i ≢ j → (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
293
[]≔-commutes [] () () _
294
[]≔-commutes (x ∷ xs) zero zero 0≢0 = ⊥-elim $ 0≢0 refl
295
[]≔-commutes (x ∷ xs) zero (suc i) _ = refl
296
[]≔-commutes (x ∷ xs) (suc i) zero _ = refl
297
[]≔-commutes (x ∷ xs) (suc i) (suc j) i≢j =
298
P.cong (_∷_ x) $ []≔-commutes xs i j (i≢j ∘ P.cong suc)
300
[]≔-updates : ∀ {n a} {A : Set a} (xs : Vec A n) (i : Fin n) {x : A} →
301
(xs [ i ]≔ x) [ i ]= x
303
[]≔-updates (x ∷ xs) zero = here
304
[]≔-updates (x ∷ xs) (suc i) = there ([]≔-updates xs i)
307
∀ {n a} {A : Set a} (xs : Vec A n) (i j : Fin n) {x y : A} →
308
i ≢ j → xs [ i ]= x → (xs [ j ]≔ y) [ i ]= x
309
[]≔-minimal [] () () _ _
310
[]≔-minimal (x ∷ xs) .zero zero 0≢0 here = ⊥-elim $ 0≢0 refl
311
[]≔-minimal (x ∷ xs) .zero (suc j) _ here = here
312
[]≔-minimal (x ∷ xs) (suc i) zero _ (there loc) = there loc
313
[]≔-minimal (x ∷ xs) (suc i) (suc j) i≢j (there loc) =
314
there ([]≔-minimal xs i j (i≢j ∘ P.cong suc) loc)
316
map-[]≔ : ∀ {n a b} {A : Set a} {B : Set b}
317
(f : A → B) (xs : Vec A n) (i : Fin n) {x : A} →
318
map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
320
map-[]≔ f (x ∷ xs) zero = refl
321
map-[]≔ f (x ∷ xs) (suc i) = P.cong (_∷_ _) $ map-[]≔ f xs i
323
[]≔-lookup : ∀ {a} {A : Set a} {n} (xs : Vec A n) (i : Fin n) →
324
xs [ i ]≔ lookup i xs ≡ xs
326
[]≔-lookup (x ∷ xs) zero = refl
327
[]≔-lookup (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-lookup xs i
added
removed
src/Data/Vec/Properties.agda
