port to agda/2.6.0.1 and agda-stdlib/1.1
[~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.Vec.Properties using (toList∘fromList)
7 open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
8 open import Data.List.Properties using (length-map ; length-replicate)
9 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
10 open import Function using (_∘_ ; flip ; const)
11 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning)
12 open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable)
13
14 import FreeTheorems
15 open import Generic using (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) ≅ mapV f (fromList l)
23 fromList∘map f []       = H.refl
24 fromList∘map f (x ∷ xs) = H.cong₂ (λ n → _∷V_ {n = n} (f x)) (H.reflexive (length-map f xs)) (fromList∘map f xs)
25
26 toList∘map : {α β : Set} {n : ℕ} → (f : α → β) → (v : Vec α n) → toList (mapV f v) ≡ map f (toList v)
27 toList∘map f []V       = P.refl
28 toList∘map f (x ∷V xs) = P.cong (_∷_ (f x)) (toList∘map f xs)
29
30 GetV-to-GetL : GetV → GetL
31 GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theorem = ft }
32   where open GetV getrecord
33         open ≅-Reasoning
34         ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs)))
35         ft f xs = ≅-to-≡ (begin
36           toList (get (fromList (map f xs)))
37             ≅⟨ H.cong₂ {B = Vec _} (λ n → toList ∘ get) (H.reflexive (length-map f xs)) (fromList∘map f xs) ⟩
38           toList (get (mapV f (fromList xs)))
39             ≡⟨ P.cong toList (free-theorem f (fromList xs)) ⟩
40           toList (mapV f (get (fromList xs)))
41             ≡⟨ toList∘map f (get (fromList xs)) ⟩
42           map f (toList (get (fromList xs))) ∎)
43
44 getList-to-getlen : get-type → ℕ → ℕ
45 getList-to-getlen get = length ∘ get ∘ flip replicate tt
46
47 replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt
48 replicate-length []      = P.refl
49 replicate-length (_ ∷ l) = P.cong (_∷_ tt) (replicate-length l)
50
51 getList-length : (get : get-type) → {B : Set} → (l : List B) → length (get l) ≡ getList-to-getlen get (length l)
52 getList-length get l = begin
53   length (get l)
54     ≡⟨ P.sym (length-map (const tt) (get l)) ⟩
55   length (map (const tt) (get l))
56     ≡⟨ P.cong length (P.sym (free-theoremL get (const tt) l)) ⟩
57   length (get (map (const tt) l))
58     ≡⟨ P.cong (length ∘ get) (replicate-length l) ⟩
59   length (get (replicate (length l) tt)) ∎
60   where open ≡-Reasoning
61
62 length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ n
63 length-toList []V       = P.refl
64 length-toList (x ∷V xs) = P.cong suc (length-toList xs) 
65
66 getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt))
67 getList-to-getVec-length-property get {_} {m} v = begin
68     length (get (toList v))
69       ≡⟨ getList-length get (toList v) ⟩
70     length (get (replicate (length (toList v)) tt))
71       ≡⟨ P.cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
72     length (get (replicate m tt)) ∎
73     where open ≡-Reasoning
74
75 getList-to-getVec : get-type → ∃ λ (getlen : ℕ → ℕ) → (getV-type getlen)
76 getList-to-getVec get = getlen , get'
77   where getlen : ℕ → ℕ
78         getlen = getList-to-getlen get
79         get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
80         get' {C} v = P.subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))
81
82 private
83   module GetV-Implementation (getrecord : GetL) where
84
85     open GetL getrecord
86
87     getlen = length ∘ get ∘ flip replicate tt
88
89
90     length-property : {C : Set} {m : ℕ} → (s : Vec C m) → length (get (toList s)) ≡ getlen m
91     length-property = getList-to-getVec-length-property get
92
93     getV : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
94     getV s = P.subst (Vec _) (length-property s) (fromList (get (toList s)))
95
96     ft : {α β : Set} (f : α → β) {n : ℕ} (v : Vec α n) → getV (mapV f v) ≡ mapV f (getV v)
97     ft f v = ≅-to-≡ (begin
98       P.subst (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v))))
99         ≅⟨ ≡-subst-removable (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v)))) ⟩
100       fromList (get (toList (mapV f v)))
101         ≅⟨ H.cong (fromList ∘ get) (H.reflexive (toList∘map f v)) ⟩
102       fromList (get (map f (toList v)))
103         ≅⟨ H.cong fromList (H.reflexive (free-theorem f (toList v))) ⟩
104       fromList (map f (get (toList v)))
105         ≅⟨ fromList∘map f (get (toList v)) ⟩
106       mapV f (fromList (get (toList v)))
107         ≅⟨ H.cong₂ (λ n → mapV {n = n} f) (H.reflexive (length-property v)) (H.sym (≡-subst-removable (Vec _) (length-property v) (fromList (get (toList v))))) ⟩
108       mapV f (P.subst (Vec _) (length-property v) (fromList (get (toList v)))) ∎)
109       where open ≅-Reasoning
110
111 GetL-to-GetV : GetL → GetV
112 GetL-to-GetV getrecord = record { getlen = getlen; get = getV; free-theorem = ft }
113   where open GetV-Implementation getrecord
114
115 get-commut-1-≅ : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≅ proj₂ (getList-to-getVec get) (fromList l)
116 get-commut-1-≅ get l = begin
117   fromList (get l)
118     ≅⟨ H.cong (fromList ∘ get) (≡-to-≅ (P.sym (toList∘fromList l))) ⟩
119   fromList (get (toList (fromList l)))
120     ≅⟨ H.sym (≡-subst-removable (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ⟩
121   P.subst (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))) ∎
122   where open ≅-Reasoning
123
124 get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ P.subst (Vec A) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))
125 get-commut-1 get {A} l = ≅-to-≡ (begin
126   fromList (get l)
127     ≅⟨ get-commut-1-≅ get l ⟩
128   proj₂ (getList-to-getVec get) (fromList l)
129     ≅⟨ H.sym (≡-subst-removable (Vec _) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))) ⟩
130   P.subst (Vec _) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l)) ∎)
131   where open ≅-Reasoning
132
133 get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B}
134 get-trafo-1 get {B} l = begin
135   getVec-to-getList (proj₂ (getList-to-getVec get)) l
136     ≡⟨ P.refl ⟩
137   toList (proj₂ (getList-to-getVec get) (fromList l))
138     ≡⟨ P.refl ⟩
139   toList (P.subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
140     ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩
141   toList (fromList (get (toList (fromList l))))
142     ≡⟨ toList∘fromList (get (toList (fromList l))) ⟩
143   get (toList (fromList l))
144     ≡⟨ P.cong get (toList∘fromList l) ⟩
145   get l ∎
146   where open ≡-Reasoning
147
148 GetLVL-identity : (G : GetL) → {A : Set} → GetL.get (GetV-to-GetL (GetL-to-GetV G)) ≗ GetL.get G {A}
149 GetLVL-identity G = get-trafo-1 (GetL.get G)
150
151 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
152 vec-len {_} {n} _ = n
153
154 fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≅ v
155 fromList-toList []V       = H.refl
156 fromList-toList (x ∷V xs) = H.cong₂ (λ n → _∷V_ {n = n} x) (H.reflexive (length-toList xs)) (fromList-toList xs)
157
158 get-commut-2 : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList
159 get-commut-2 get {B} v = P.sym (≅-to-≡ (H.cong₂ (λ n → toList ∘ get {n = n}) (H.reflexive (length-toList v)) (fromList-toList v)))
160
161 get-trafo-2-getlen : {getlen : ℕ → ℕ} → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen
162 get-trafo-2-getlen {getlen} get n = begin
163   proj₁ (getList-to-getVec (getVec-to-getList get)) n
164     ≡⟨ P.refl ⟩
165   length (toList (get (fromList (replicate n tt))))
166     ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩
167   vec-len (get (fromList (replicate n tt)))
168     ≡⟨ P.cong getlen (length-replicate n) ⟩
169   getlen n ∎
170   where open ≡-Reasoning
171
172 get-trafo-2-get-≅ : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → (v : Vec B n) → proj₂ (getList-to-getVec (getVec-to-getList get)) v ≅ get v
173 get-trafo-2-get-≅ {getlen} get v = begin
174   P.subst (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v)))))
175     ≅⟨ ≡-subst-removable (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v))))) ⟩
176   fromList (toList (get (fromList (toList v))))
177     ≅⟨ fromList-toList (get (fromList (toList v))) ⟩
178   get (fromList (toList v))
179     ≅⟨ H.cong₂ (λ n → get {n = n}) (H.reflexive (length-toList v)) (fromList-toList v) ⟩
180   get v ∎
181   where open ≅-Reasoning
182
183 get-trafo-2-get : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ P.subst (Vec B) (P.sym (get-trafo-2-getlen get n)) ∘ get
184 get-trafo-2-get get v = ≅-to-≡ (begin
185   proj₂ (getList-to-getVec (getVec-to-getList get)) v
186     ≅⟨ get-trafo-2-get-≅ get v ⟩
187   get v
188     ≅⟨ H.sym (≡-subst-removable (Vec _) (P.sym (get-trafo-2-getlen get (vec-len v))) (get v)) ⟩
189   P.subst (Vec _) (P.sym (get-trafo-2-getlen get (vec-len v))) (get v) ∎)
190   where open ≅-Reasoning