use the indexed version of the Vec Setoid
[~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_)
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)
12 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
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 ; free-theorem)
17 open FreeTheorems.VecVec using () renaming (get-type to getV-type)
18
19 getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
20 getVec-to-getList get = toList ∘ get ∘ fromList
21
22 getList-to-getlen : get-type → ℕ → ℕ
23 getList-to-getlen get = length ∘ get ∘ flip replicate tt
24
25 replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt
26 replicate-length [] = refl
27 replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l)
28
29 getList-length : (get : get-type) → {B : Set} → (l : List B) → length (get l) ≡ getList-to-getlen get (length l)
30 getList-length get l = begin
31   length (get l)
32     ≡⟨ sym (length-map (const tt) (get l)) ⟩
33   length (map (const tt) (get l))
34     ≡⟨ cong length (sym (free-theorem get (const tt) l)) ⟩
35   length (get (map (const tt) l))
36     ≡⟨ cong (length ∘ get) (replicate-length l) ⟩
37   length (get (replicate (length l) tt)) ∎
38
39 length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ n
40 length-toList []V = refl
41 length-toList (x ∷V xs) = cong suc (length-toList xs) 
42
43 getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt))
44 getList-to-getVec-length-property get {_} {m} v = begin
45     length (get (toList v))
46       ≡⟨ getList-length get (toList v) ⟩
47     length (get (replicate (length (toList v)) tt))
48       ≡⟨ cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
49     length (get (replicate m tt)) ∎
50
51 getList-to-getVec : get-type → ∃ λ (getlen : ℕ → ℕ) → (getV-type getlen)
52 getList-to-getVec get = getlen , get'
53   where getlen : ℕ → ℕ
54         getlen = getList-to-getlen get
55         get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
56         get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))
57
58 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))
59 get-commut-1 get {A} l = begin
60   fromList (get l)
61     ≡⟨ sym (subst-fromList (cong get (toList-fromList l))) ⟩
62   subst (Vec A) (cong length (cong get (toList-fromList l))) (fromList (get (toList (fromList l))))
63     ≡⟨ cong (flip (subst (Vec A)) (fromList (get (toList (fromList l))))) (proof-irrelevance (cong length (cong get (toList-fromList l))) (trans p p')) ⟩
64   subst (Vec A) (trans p p') (fromList (get (toList (fromList l))))
65     ≡⟨ sym (subst-subst (Vec A) p p' (fromList (get (toList (fromList l))))) ⟩
66   subst (Vec A) p' (subst (Vec A) p (fromList (get (toList (fromList l)))))
67     ≡⟨ refl ⟩
68   subst (Vec A) p' (proj₂ (getList-to-getVec get) (fromList l)) ∎
69     where p : length (get (toList (fromList l))) ≡ length (get (replicate (length l) tt))
70           p = getList-to-getVec-length-property get (fromList l)
71           p' : length (get (replicate (length l) tt)) ≡ length (get l)
72           p' = sym (getList-length get l)
73
74 get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B}
75 get-trafo-1 get {B} l = begin
76   getVec-to-getList (proj₂ (getList-to-getVec get)) l
77     ≡⟨ refl ⟩
78   toList (proj₂ (getList-to-getVec get) (fromList l))
79     ≡⟨ refl ⟩
80   toList (subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
81     ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩
82   toList (fromList (get (toList (fromList l))))
83     ≡⟨ toList-fromList (get (toList (fromList l))) ⟩
84   get (toList (fromList l))
85     ≡⟨ cong get (toList-fromList l) ⟩
86   get l ∎
87
88 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
89 vec-len {_} {n} _ = n
90
91 fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≡ subst (Vec A) (sym (length-toList v)) v
92 fromList-toList     []V       = refl
93 fromList-toList {A} (x ∷V xs) = begin
94   x ∷V fromList (toList xs)
95     ≡⟨ cong (_∷V_ x) (fromList-toList xs) ⟩
96   x ∷V subst (Vec A) (sym (length-toList xs)) xs
97     ≡⟨ subst-cong (Vec A) (_∷V_ x) (sym (length-toList xs)) xs ⟩
98   subst (Vec A) (cong suc (sym (length-toList xs))) (x ∷V xs)
99     ≡⟨ cong (λ p →  subst (Vec A) p (x ∷V xs)) (proof-irrelevance (cong suc (sym (length-toList xs))) (sym (cong suc (length-toList xs)))) ⟩
100   subst (Vec A) (sym (length-toList (x ∷V xs))) (x ∷V xs) ∎
101
102 get-commut-2 : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList
103 get-commut-2 getlen get {B} v = begin
104   toList (get v)
105     ≡⟨ sym (toList-subst (get v) (cong getlen (sym (length-toList v)))) ⟩
106   toList (subst (Vec B) (cong getlen (sym (length-toList v))) (get v))
107     ≡⟨ cong toList (sym (subst-cong (Vec B) get (sym (length-toList v)) v)) ⟩
108   toList (get (subst (Vec B) (sym (length-toList v)) v))
109     ≡⟨ cong (toList ∘ get) (sym (fromList-toList v)) ⟩
110   toList (get (fromList (toList v))) ∎
111
112 get-trafo-2-getlen : (getlen : ℕ → ℕ) → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen
113 get-trafo-2-getlen getlen get n = begin
114   proj₁ (getList-to-getVec (getVec-to-getList get)) n
115     ≡⟨ refl ⟩
116   length (toList (get (fromList (replicate n tt))))
117     ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩
118   vec-len (get (fromList (replicate n tt)))
119     ≡⟨ cong getlen (length-replicate n) ⟩
120   getlen n ∎
121
122 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
123 get-trafo-2-get getlen get {B} {n} v = begin
124   proj₂ (getList-to-getVec (getVec-to-getList get)) v
125     ≡⟨ refl ⟩
126   subst (Vec B) p (fromList (toList (get (fromList (toList v)))))
127     ≡⟨ cong (subst (Vec B) p) (fromList-toList (get (fromList (toList v)))) ⟩
128   subst (Vec B) p (subst (Vec B) p' (get (fromList (toList v))))
129     ≡⟨ subst-subst (Vec B) p' p (get (fromList (toList v))) ⟩
130   subst (Vec B) (trans p' p) (get (fromList (toList v)))
131     ≡⟨ cong (subst (Vec B) (trans p' p) ∘ get) (fromList-toList v) ⟩
132   subst (Vec B) (trans p' p) (get (subst (Vec B) (sym (length-toList v)) v))
133     ≡⟨ cong (subst (Vec B) (trans p' p)) (subst-cong (Vec B) get (sym (length-toList v)) v) ⟩
134   subst (Vec B) (trans p' p) (subst (Vec B) (cong getlen (sym (length-toList v))) (get v))
135     ≡⟨ subst-subst (Vec B) (cong getlen (sym (length-toList v))) (trans p' p) (get v) ⟩
136   subst (Vec B) (trans (cong getlen (sym (length-toList v))) (trans p' p)) (get v)
137     ≡⟨ cong (flip (subst (Vec B)) (get v)) (proof-irrelevance (trans (cong getlen (sym (length-toList v))) (trans p' p)) p'') ⟩
138   subst (Vec B) p'' (get v) ∎
139     where n' : ℕ
140           n' = length (toList (get (fromList (replicate n tt))))
141           p : length (toList (get (fromList (toList v)))) ≡ n'
142           p = getList-to-getVec-length-property (getVec-to-getList get) v
143           p' : getlen (length (toList v)) ≡ length (toList (get (fromList (toList v))))
144           p' = sym (length-toList (get (fromList (toList v))))
145           p'' : getlen n ≡ n'
146           p'' = sym (get-trafo-2-getlen getlen get (vec-len v))