blob: 6342fc50bef4f89857bf038144fe29f112da5785 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
module FinMap where
open import Level using () renaming (zero to ℓ₀)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Maybe using (Maybe ; just ; nothing ; maybe′ ; just-injective)
open import Data.Fin using (Fin ; zero ; suc)
open import Data.Fin.Properties using (_≟_)
open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
open import Data.Vec.Properties using (lookup∘update ; lookup∘update′ ; lookup-replicate ; tabulate-cong ; lookup∘tabulate)
open import Data.Product using (_×_ ; _,_)
open import Data.List.All as All using (All)
import Data.List.All.Properties as AllP
import Data.List.Any as Any
import Data.List.Membership.Setoid
open import Function using (id ; _∘_ ; flip ; const)
open import Function.Equality using (module Π)
open import Function.Surjection using (module Surjection)
open import Relation.Nullary using (yes ; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.Core using (Decidable)
open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; _≗_)
open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
_∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set
_∈_ {A} x xs = Data.List.Membership.Setoid._∈_ (P.setoid A) x (toList xs)
_∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set
_∉_ {A} x xs = All (_≢_ x) (toList xs)
data Dec∈ {A : Set} {n : ℕ} (x : A) (xs : Vec A n) : Set where
yes-∈ : x ∈ xs → Dec∈ x xs
no-∉ : x ∉ xs → Dec∈ x xs
is-∈ : {A : Set} {n : ℕ} → Decidable (_≡_ {A = A}) → (x : A) → (xs : Vec A n) → Dec∈ x xs
is-∈ eq? x xs with Any.any (eq? x) (toList xs)
... | yes x∈xs = yes-∈ x∈xs
... | no x∉xs = no-∉ (Π._⟨$⟩_ (Surjection.to AllP.¬Any↠All¬) x∉xs)
FinMapMaybe : ℕ → Set → Set
FinMapMaybe n A = Vec (Maybe A) n
lookupM : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → Maybe A
lookupM = lookupVec
insert : {A : Set} {n : ℕ} → Fin n → A → FinMapMaybe n A → FinMapMaybe n A
insert f a m = m [ f ]≔ (just a)
empty : {A : Set} {n : ℕ} → FinMapMaybe n A
empty = replicate nothing
fromAscList : {A : Set} {n m : ℕ} → Vec (Fin n × A) m → FinMapMaybe n A
fromAscList [] = empty
fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs)
fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A
fromFunc = tabulate ∘ _∘_ Maybe.just
reshape : {n : ℕ} {A : Set} → FinMapMaybe n A → (l : ℕ) → FinMapMaybe l A
reshape m zero = []
reshape [] (suc l) = nothing ∷ (reshape [] l)
reshape (x ∷ xs) (suc l) = x ∷ (reshape xs l)
union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A
union m1 m2 = tabulate (λ f → maybe′ just (lookupM f m2) (lookupM f m1))
restrict : {A : Set} {n m : ℕ} → (Fin n → A) → Vec (Fin n) m → FinMapMaybe n A
restrict f is = fromAscList (zip is (mapV f is))
delete : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → FinMapMaybe n A
delete i m = m [ i ]≔ nothing
delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A
delete-many = flip (foldr (const _) delete)
lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → {a : A} → lookupM f m ≡ just a → m ≡ insert f a m
lemma-insert-same [] () p
lemma-insert-same {suc n} (x ∷ xs) zero p = P.cong (flip _∷_ xs) p
lemma-insert-same (x ∷ xs) (suc i) p = P.cong (_∷_ x) (lemma-insert-same xs i p)
lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a
lemma-lookupM-restrict i f [] p = contradiction (P.trans (P.sym p) (lookup-replicate i nothing)) (λ ())
lemma-lookupM-restrict i f (i' ∷ is) p with i ≟ i'
lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes P.refl = just-injective (begin
just (f i)
≡⟨ P.sym (lookup∘update i (restrict f is) (just (f i))) ⟩
lookupM i (insert i (f i) (restrict f is))
≡⟨ p ⟩
just a ∎)
lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin
lookupM i (restrict f is)
≡⟨ P.sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩
lookupM i (insert i' (f i') (restrict f is))
≡⟨ p ⟩
just a ∎)
lemma-lookupM-restrict-∈ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∈ js → lookupM i (restrict f js) ≡ just (f i)
lemma-lookupM-restrict-∈ i f [] ()
lemma-lookupM-restrict-∈ i f (j ∷ js) p with i ≟ j
lemma-lookupM-restrict-∈ i f (.i ∷ js) p | yes P.refl = lookup∘update i (restrict f js) (just (f i))
lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j
lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p) | no i≢j =
P.trans (lookup∘update′ i≢j (restrict f js) (just (f j)))
(lemma-lookupM-restrict-∈ i f js p)
lemma-lookupM-restrict-∉ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (restrict f js) ≡ nothing
lemma-lookupM-restrict-∉ i f [] i∉[] = lookup-replicate i nothing
lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs =
P.trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j)))
(lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs))
lemma-lookupM-delete-many : {n m : ℕ} {A : Set} (h : FinMapMaybe n A) → (i : Fin n) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (delete-many js h) ≡ lookupM i h
lemma-lookupM-delete-many {n} h i [] i∉[] = P.refl
lemma-lookupM-delete-many {n} h i (j ∷ js) i∉jjs =
P.trans (lookup∘update′ (All.head i∉jjs) (delete-many js h) nothing)
(lemma-lookupM-delete-many h i js (All.tail i∉jjs))
lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m
lemma-reshape-id [] = P.refl
lemma-reshape-id (x ∷ xs) = P.cong (_∷_ x) (lemma-reshape-id xs)
lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f t) (delete-many t (fromFunc f)) ≡ fromFunc f
lemma-disjoint-union {n} f t = tabulate-cong inner
where inner : (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t)) ≡ just (f x)
inner x with is-∈ _≟_ x t
inner x | yes-∈ x∈t = P.cong (maybe′ just (lookupM x (delete-many t (fromFunc f)))) (lemma-lookupM-restrict-∈ x f t x∈t)
inner x | no-∉ x∉t = begin
maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t))
≡⟨ P.cong₂ (maybe′ just) (lemma-lookupM-delete-many (fromFunc f) x t x∉t) (lemma-lookupM-restrict-∉ x f t x∉t) ⟩
maybe′ just (lookupM x (fromFunc f)) nothing
≡⟨ P.cong (flip (maybe′ just) nothing) (lookup∘tabulate (just ∘ f) x) ⟩
just (f x) ∎
lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
lemma-exchange-maps h≈h′ {[]} All.[] = P.refl
lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis)
|
