blob: 376adffd1de6923d9326059aaf4783129461c13e (
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
|
module FinMap where
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
open import Data.Fin using (Fin ; zero ; suc)
open import Data.Fin.Props using (_≟_)
open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate) renaming (lookup to lookupVec)
open import Data.Vec.Properties using (lookup∘tabulate)
open import Data.List using (List ; [] ; _∷_ ; map ; zip)
open import Data.Product using (_×_ ; _,_)
open import Function using (id ; _∘_ ; flip)
open import Relation.Nullary using (¬_ ; yes ; no)
open import Relation.Nullary.Negation using (contradiction ; contraposition)
open import Relation.Binary.Core using (_≡_ ; refl)
open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_)
open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
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 : ℕ} → List (Fin n × A) → FinMapMaybe n A
fromAscList [] = empty
fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs)
FinMap : ℕ → Set → Set
FinMap n A = Vec A n
lookup : {A : Set} {n : ℕ} → Fin n → FinMap n A → A
lookup = lookupVec
fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMap n A
fromFunc = tabulate
union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMap n A → FinMap n A
union m1 m2 = tabulate (λ f → maybe′ id (lookup f m2) (lookupM f m1))
restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A
restrict f is = fromAscList (zip is (map f is))
lemma-insert-same : {τ : Set} {n : ℕ} → (m : FinMapMaybe n τ) → (f : Fin n) → (a : τ) → lookupM f m ≡ just a → m ≡ insert f a m
lemma-insert-same [] () a p
lemma-insert-same (.(just a) ∷ xs) zero a refl = refl
lemma-insert-same (x ∷ xs) (suc i) a p = cong (_∷_ x) (lemma-insert-same xs i a p)
lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing
lemma-lookupM-empty zero = refl
lemma-lookupM-empty (suc i) = lemma-lookupM-empty i
lemma-lookupM-insert : {A : Set} {n : ℕ} → (i : Fin n) → (a : A) → (m : FinMapMaybe n A) → lookupM i (insert i a m) ≡ just a
lemma-lookupM-insert zero _ (_ ∷ _) = refl
lemma-lookupM-insert (suc i) a (_ ∷ xs) = lemma-lookupM-insert i a xs
lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → ¬(i ≡ j) → lookupM i m ≡ lookupM i (insert j a m)
lemma-lookupM-insert-other zero zero a m p = contradiction refl p
lemma-lookupM-insert-other zero (suc j) a (x ∷ xs) p = refl
lemma-lookupM-insert-other (suc i) zero a (x ∷ xs) p = refl
lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (contraposition (cong suc) p)
lemma-from-just : {A : Set} → {x y : A} → _≡_ {_} {Maybe A} (just x) (just y) → x ≡ y
lemma-from-just refl = refl
lemma-lookupM-restrict : {A : Set} {n : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : List (Fin n)) → (a : A) → lookupM i (restrict f is) ≡ just a → f i ≡ a
lemma-lookupM-restrict {A} i f [] a p with begin
just a
≡⟨ sym p ⟩
lookupM i (restrict f [])
≡⟨ refl ⟩
lookupM i empty
≡⟨ lemma-lookupM-empty i ⟩
nothing ∎
lemma-lookupM-restrict i f [] a p | ()
lemma-lookupM-restrict i f (i' ∷ is) a p with i ≟ i'
lemma-lookupM-restrict i f (.i ∷ is) a p | yes refl = lemma-from-just (begin
just (f i)
≡⟨ sym (lemma-lookupM-insert i (f i) (restrict f is)) ⟩
lookupM i (insert i (f i) (restrict f is))
≡⟨ refl ⟩
lookupM i (restrict f (i ∷ is))
≡⟨ p ⟩
just a ∎)
lemma-lookupM-restrict i f (i' ∷ is) a p | no ¬p2 = lemma-lookupM-restrict i f is a (begin
lookupM i (restrict f is)
≡⟨ lemma-lookupM-insert-other i i' (f i') (restrict f is) ¬p2 ⟩
lookupM i (insert i' (f i') (restrict f is))
≡⟨ refl ⟩
lookupM i (restrict f (i' ∷ is))
≡⟨ p ⟩
just a ∎)
lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = refl
lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = begin
f zero ∷ tabulate (f ∘ suc)
≡⟨ cong (flip Vec._∷_ (tabulate (f ∘ suc))) (f≗g zero) ⟩
g zero ∷ tabulate (f ∘ suc)
≡⟨ cong (Vec._∷_ (g zero)) (lemma-tabulate-∘ (f≗g ∘ suc)) ⟩
g zero ∷ tabulate (g ∘ suc) ∎
lemma-union-restrict : {n : ℕ} {A : Set} → (f : Fin n → A) → (is : List (Fin n)) → union (restrict f is) (fromFunc f) ≡ fromFunc f
lemma-union-restrict f is = begin
union (restrict f is) (fromFunc f)
≡⟨ refl ⟩
tabulate (λ j → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)))
≡⟨ lemma-tabulate-∘ (lemma-inner f is) ⟩
tabulate f ∎
where lemma-inner : {n : ℕ} {A : Set} (f : Fin n → A) → (is : List (Fin n)) → (j : Fin n) → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡ f j
lemma-inner f [] j = begin
maybe′ id (lookup j (fromFunc f)) (lookupM j empty)
≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-empty j) ⟩
maybe′ id (lookup j (fromFunc f)) nothing
≡⟨ refl ⟩
lookup j (fromFunc f)
≡⟨ lookup∘tabulate f j ⟩
f j ∎
lemma-inner f (i ∷ is) j with i ≟ j
lemma-inner f (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-insert j (f j) (restrict f is))
lemma-inner f (i ∷ is) j | no i≢j = begin
maybe′ id (lookup j (fromFunc f)) (lookupM j (insert i (f i) (restrict f is)))
≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (restrict f is) (i≢j ∘ sym) )) ⟩
maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is))
≡⟨ lemma-inner f is j ⟩
f j ∎
|
