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