replace rewrite with cong where feasible
[~helmut/bidiragda.git] / LiftGet.agda
1 module LiftGet where
2
3 open import Data.Unit using (⊤ ; tt)
4 open import Data.Nat using (ℕ ; suc)
5 open import Data.Vec using (Vec ; toList ; fromList) renaming ([] to []V ; _∷_ to _∷V_ ; map to mapV)
6 open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
7 open import Data.List.Properties using (length-map)
8 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
9 open import Function using (_∘_ ; flip ; const)
10 open import Relation.Binary.Core using (_≡_)
11 open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance ; module ≡-Reasoning)
12 open import Relation.Binary.HeterogeneousEquality using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-subst-removable) renaming (refl to het-refl ; sym to het-sym ; cong to het-cong ; reflexive to het-reflexive)
13
14 import FreeTheorems
15 open import Generic using (length-replicate ; subst-cong ; subst-fromList ; subst-subst ; toList-fromList ; toList-subst)
16 open FreeTheorems.ListList using (get-type) renaming (free-theorem to free-theoremL ; Get to GetL ; module Get to GetL)
17 open FreeTheorems.VecVec using () renaming (get-type to getV-type ; Get to GetV ; module Get to GetV)
18
19 getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
20 getVec-to-getList get = toList ∘ get ∘ fromList
21
22 fromList∘map : {α β : Set} → (f : α → β) → (l : List α) → fromList (map f l) ≡ subst (Vec β) (sym (length-map f l)) (mapV f (fromList l))
23 fromList∘map f []       = refl
24 fromList∘map f (x ∷ xs) rewrite fromList∘map f xs = trans (subst-cong (Vec _) (_∷V_ (f x)) (sym (length-map f xs)) (mapV f (fromList xs)))
25                                                           (cong (flip (subst (Vec _)) (f x ∷V mapV f (fromList xs))) (proof-irrelevance (cong suc (sym (length-map f xs)))
26                                                                                                                                         (sym (cong suc (length-map f xs)))))
27
28 toList∘map : {α β : Set} {n : ℕ} → (f : α → β) → (v : Vec α n) → toList (mapV f v) ≡ map f (toList v)
29 toList∘map f []V       = refl
30 toList∘map f (x ∷V xs) = cong (_∷_ (f x)) (toList∘map f xs)
31
32 GetV-to-GetL : GetV → GetL
33 GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theorem = ft }
34   where open GetV getrecord
35         open ≡-Reasoning
36         ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs)))
37         ft f xs = begin
38           toList (get (fromList (map f xs)))
39             ≡⟨ cong (toList ∘ get) (fromList∘map f xs) ⟩
40           toList (get (subst (Vec _) (sym (length-map f xs)) (mapV f (fromList xs))))
41             ≡⟨ cong toList (subst-cong (Vec _) get (sym (length-map f xs)) (mapV f (fromList xs))) ⟩
42           toList (subst (Vec _) (cong getlen (sym (length-map f xs))) (get (mapV f (fromList xs))))
43             ≡⟨ toList-subst (get (mapV f (fromList xs))) (cong getlen (sym (length-map f xs))) ⟩
44           toList (get (mapV f (fromList xs)))
45             ≡⟨ cong toList (free-theorem f (fromList xs)) ⟩
46           toList (mapV f (get (fromList xs)))
47             ≡⟨ toList∘map f (get (fromList xs)) ⟩
48           map f (toList (get (fromList xs))) ∎
49
50 getList-to-getlen : get-type → ℕ → ℕ
51 getList-to-getlen get = length ∘ get ∘ flip replicate tt
52
53 replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt
54 replicate-length [] = refl
55 replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l)
56
57 getList-length : (get : get-type) → {B : Set} → (l : List B) → length (get l) ≡ getList-to-getlen get (length l)
58 getList-length get l = begin
59   length (get l)
60     ≡⟨ sym (length-map (const tt) (get l)) ⟩
61   length (map (const tt) (get l))
62     ≡⟨ cong length (sym (free-theoremL get (const tt) l)) ⟩
63   length (get (map (const tt) l))
64     ≡⟨ cong (length ∘ get) (replicate-length l) ⟩
65   length (get (replicate (length l) tt)) ∎
66   where open ≡-Reasoning
67
68 length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ n
69 length-toList []V = refl
70 length-toList (x ∷V xs) = cong suc (length-toList xs) 
71
72 getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt))
73 getList-to-getVec-length-property get {_} {m} v = begin
74     length (get (toList v))
75       ≡⟨ getList-length get (toList v) ⟩
76     length (get (replicate (length (toList v)) tt))
77       ≡⟨ cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
78     length (get (replicate m tt)) ∎
79     where open ≡-Reasoning
80
81 getList-to-getVec : get-type → ∃ λ (getlen : ℕ → ℕ) → (getV-type getlen)
82 getList-to-getVec get = getlen , get'
83   where getlen : ℕ → ℕ
84         getlen = getList-to-getlen get
85         get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
86         get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))
87
88 ind-cong : {I : Set} → (X Y : I → Set) → (f : {i : I} → X i → Y i) → {i j : I} → (i ≡ j) → {x : X i} → {y : X j} → x ≅ y → f x ≅ f y
89 ind-cong X Y f refl het-refl = het-refl
90
91 private
92   module GetV-Implementation (getrecord : GetL) where
93
94     open GetL getrecord
95
96     getlen = length ∘ get ∘ flip replicate tt
97
98
99     length-property : {C : Set} {m : ℕ} → (s : Vec C m) → length (get (toList s)) ≡ getlen m
100     length-property {m = m} s = begin
101       length (get (toList s))
102         ≡⟨ sym (length-map (const tt) (get (toList s))) ⟩
103       length (map (const tt) (get (toList s)))
104         ≡⟨ cong length (sym (free-theorem (const tt) (toList s))) ⟩
105       length (get (map (const tt) (toList s)))
106         ≡⟨ cong (length ∘ get) (replicate-length (toList s)) ⟩
107       length (get (replicate (length (toList s)) tt))
108         ≡⟨ cong getlen (length-toList s) ⟩
109       getlen m ∎
110       where open ≡-Reasoning
111
112     getV : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
113     getV s = subst (Vec _) (length-property s) (fromList (get (toList s)))
114
115     ft : {α β : Set} (f : α → β) {n : ℕ} (v : Vec α n) → getV (mapV f v) ≡ mapV f (getV v)
116     ft f v = ≅-to-≡ (begin
117       subst (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v))))
118         ≅⟨ ≡-subst-removable (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v)))) ⟩
119       fromList (get (toList (mapV f v)))
120         ≅⟨ het-cong (fromList ∘ get) (het-reflexive (toList∘map f v)) ⟩
121       fromList (get (map f (toList v)))
122         ≅⟨ het-cong fromList (het-reflexive (free-theorem f (toList v))) ⟩
123       fromList (map f (get (toList v)))
124         ≡⟨ fromList∘map f (get (toList v)) ⟩
125       subst (Vec _) (sym (length-map f (get (toList v)))) (mapV f (fromList (get (toList v))))
126         ≅⟨ ≡-subst-removable (Vec _) (sym (length-map f (get (toList v)))) (mapV f (fromList (get (toList v)))) ⟩
127       mapV f (fromList (get (toList v)))
128         ≅⟨ ind-cong (Vec _) (Vec _) (mapV f) (length-property v) (het-sym (≡-subst-removable (Vec _) (length-property v) (fromList (get (toList v))))) ⟩
129       mapV f (subst (Vec _) (length-property v) (fromList (get (toList v)))) ∎)
130       where open ≅-Reasoning
131
132 GetL-to-GetV : GetL → GetV
133 GetL-to-GetV getrecord = record { getlen = getlen; get = getV; free-theorem = ft }
134   where open GetV-Implementation getrecord
135
136 get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ subst (Vec A) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))
137 get-commut-1 get {A} l = begin
138   fromList (get l)
139     ≡⟨ sym (subst-fromList (cong get (toList-fromList l))) ⟩
140   subst (Vec A) (cong length (cong get (toList-fromList l))) (fromList (get (toList (fromList l))))
141     ≡⟨ cong (flip (subst (Vec A)) (fromList (get (toList (fromList l))))) (proof-irrelevance (cong length (cong get (toList-fromList l))) (trans p p')) ⟩
142   subst (Vec A) (trans p p') (fromList (get (toList (fromList l))))
143     ≡⟨ sym (subst-subst (Vec A) p p' (fromList (get (toList (fromList l))))) ⟩
144   subst (Vec A) p' (subst (Vec A) p (fromList (get (toList (fromList l)))))
145     ≡⟨ refl ⟩
146   subst (Vec A) p' (proj₂ (getList-to-getVec get) (fromList l)) ∎
147     where open ≡-Reasoning
148           p : length (get (toList (fromList l))) ≡ length (get (replicate (length l) tt))
149           p = getList-to-getVec-length-property get (fromList l)
150           p' : length (get (replicate (length l) tt)) ≡ length (get l)
151           p' = sym (getList-length get l)
152
153 get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B}
154 get-trafo-1 get {B} l = begin
155   getVec-to-getList (proj₂ (getList-to-getVec get)) l
156     ≡⟨ refl ⟩
157   toList (proj₂ (getList-to-getVec get) (fromList l))
158     ≡⟨ refl ⟩
159   toList (subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
160     ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩
161   toList (fromList (get (toList (fromList l))))
162     ≡⟨ toList-fromList (get (toList (fromList l))) ⟩
163   get (toList (fromList l))
164     ≡⟨ cong get (toList-fromList l) ⟩
165   get l ∎
166   where open ≡-Reasoning
167
168 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
169 vec-len {_} {n} _ = n
170
171 fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≡ subst (Vec A) (sym (length-toList v)) v
172 fromList-toList     []V       = refl
173 fromList-toList {A} (x ∷V xs) = begin
174   x ∷V fromList (toList xs)
175     ≡⟨ cong (_∷V_ x) (fromList-toList xs) ⟩
176   x ∷V subst (Vec A) (sym (length-toList xs)) xs
177     ≡⟨ subst-cong (Vec A) (_∷V_ x) (sym (length-toList xs)) xs ⟩
178   subst (Vec A) (cong suc (sym (length-toList xs))) (x ∷V xs)
179     ≡⟨ cong (λ p →  subst (Vec A) p (x ∷V xs)) (proof-irrelevance (cong suc (sym (length-toList xs))) (sym (cong suc (length-toList xs)))) ⟩
180   subst (Vec A) (sym (length-toList (x ∷V xs))) (x ∷V xs) ∎
181   where open ≡-Reasoning
182
183 get-commut-2 : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList
184 get-commut-2 getlen get {B} v = begin
185   toList (get v)
186     ≡⟨ sym (toList-subst (get v) (cong getlen (sym (length-toList v)))) ⟩
187   toList (subst (Vec B) (cong getlen (sym (length-toList v))) (get v))
188     ≡⟨ cong toList (sym (subst-cong (Vec B) get (sym (length-toList v)) v)) ⟩
189   toList (get (subst (Vec B) (sym (length-toList v)) v))
190     ≡⟨ cong (toList ∘ get) (sym (fromList-toList v)) ⟩
191   toList (get (fromList (toList v))) ∎
192   where open ≡-Reasoning
193
194 get-trafo-2-getlen : (getlen : ℕ → ℕ) → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen
195 get-trafo-2-getlen getlen get n = begin
196   proj₁ (getList-to-getVec (getVec-to-getList get)) n
197     ≡⟨ refl ⟩
198   length (toList (get (fromList (replicate n tt))))
199     ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩
200   vec-len (get (fromList (replicate n tt)))
201     ≡⟨ cong getlen (length-replicate n) ⟩
202   getlen n ∎
203   where open ≡-Reasoning
204
205 get-trafo-2-get : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ subst (Vec B) (sym (get-trafo-2-getlen getlen get n)) ∘ get
206 get-trafo-2-get getlen get {B} {n} v = begin
207   proj₂ (getList-to-getVec (getVec-to-getList get)) v
208     ≡⟨ refl ⟩
209   subst (Vec B) p (fromList (toList (get (fromList (toList v)))))
210     ≡⟨ cong (subst (Vec B) p) (fromList-toList (get (fromList (toList v)))) ⟩
211   subst (Vec B) p (subst (Vec B) p' (get (fromList (toList v))))
212     ≡⟨ subst-subst (Vec B) p' p (get (fromList (toList v))) ⟩
213   subst (Vec B) (trans p' p) (get (fromList (toList v)))
214     ≡⟨ cong (subst (Vec B) (trans p' p) ∘ get) (fromList-toList v) ⟩
215   subst (Vec B) (trans p' p) (get (subst (Vec B) (sym (length-toList v)) v))
216     ≡⟨ cong (subst (Vec B) (trans p' p)) (subst-cong (Vec B) get (sym (length-toList v)) v) ⟩
217   subst (Vec B) (trans p' p) (subst (Vec B) (cong getlen (sym (length-toList v))) (get v))
218     ≡⟨ subst-subst (Vec B) (cong getlen (sym (length-toList v))) (trans p' p) (get v) ⟩
219   subst (Vec B) (trans (cong getlen (sym (length-toList v))) (trans p' p)) (get v)
220     ≡⟨ cong (flip (subst (Vec B)) (get v)) (proof-irrelevance (trans (cong getlen (sym (length-toList v))) (trans p' p)) p'') ⟩
221   subst (Vec B) p'' (get v) ∎
222     where open ≡-Reasoning
223           n' : ℕ
224           n' = length (toList (get (fromList (replicate n tt))))
225           p : length (toList (get (fromList (toList v)))) ≡ n'
226           p = getList-to-getVec-length-property (getVec-to-getList get) v
227           p' : getlen (length (toList v)) ≡ length (toList (get (fromList (toList v))))
228           p' = sym (length-toList (get (fromList (toList v))))
229           p'' : getlen n ≡ n'
230           p'' = sym (get-trafo-2-getlen getlen get (vec-len v))