formulate List <-> Vec isomorphism problems
[~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)
12 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
13
14 get-type : Set₁
15 get-type = {A : Set} → List A → List A
16
17 getV-type : (ℕ → ℕ) → Set₁
18 getV-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
19
20 getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
21 getVec-to-getList get = toList ∘ get ∘ fromList
22
23 getList-to-getlen : get-type → ℕ → ℕ
24 getList-to-getlen get = length ∘ get ∘ flip replicate tt
25
26 postulate
27   free-theorem-list-list : {β γ : Set} → (get : get-type) → (f : β → γ) → get ∘ map f ≗ map f ∘ get
28
29 replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt
30 replicate-length [] = refl
31 replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l)
32
33 getList-length : (get : get-type) → {B : Set} → (l : List B) → length (get l) ≡ getList-to-getlen get (length l)
34 getList-length get l = begin
35   length (get l)
36     ≡⟨ sym (length-map (const tt) (get l)) ⟩
37   length (map (const tt) (get l))
38     ≡⟨ cong length (sym (free-theorem-list-list get (const tt) l)) ⟩
39   length (get (map (const tt) l))
40     ≡⟨ cong (length ∘ get) (replicate-length l) ⟩
41   length (get (replicate (length l) tt)) ∎
42
43 length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ n
44 length-toList []V = refl
45 length-toList (x ∷V xs) = cong suc (length-toList xs) 
46
47 vec-length : {A : Set} {n m : ℕ} → n ≡ m → Vec A n → Vec A m
48 vec-length refl v = v
49
50 toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l
51 toList-fromList []       = refl
52 toList-fromList (x ∷ xs) = cong (_∷_ x) (toList-fromList xs)
53
54 vec-length-same : {A : Set} → (l : List A) → {n : ℕ} → (p : length l ≡ n) → toList (vec-length p (fromList l)) ≡ l
55 vec-length-same l refl = toList-fromList l
56
57 getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt))
58 getList-to-getVec-length-property get {_} {m} v = begin
59     length (get (toList v))
60       ≡⟨ getList-length get (toList v) ⟩
61     length (get (replicate (length (toList v)) tt))
62       ≡⟨ cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
63     length (get (replicate m tt)) ∎
64
65 getList-to-getVec : get-type → ∃ λ (getlen : ℕ → ℕ) → (getV-type getlen)
66 getList-to-getVec get = getlen , get'
67   where getlen : ℕ → ℕ
68         getlen = getList-to-getlen get
69         get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
70         get' v = vec-length (getList-to-getVec-length-property get v) (fromList (get (toList v)))
71
72 {-
73 -- We cannot formulate the first commutation property, because the type of
74 -- fromList (get l) depends on the concrete l, more specifically its length.
75 get-commut-1 : (get : get-type) → (fromList ∘ get) ≗ (proj₂ (getList-to-getVec get)) ∘ fromList
76 get-commut-1 get l = ?
77 -}
78
79 get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B}
80 get-trafo-1 get l = begin
81   getVec-to-getList (proj₂ (getList-to-getVec get)) l
82     ≡⟨ refl ⟩
83   toList (proj₂ (getList-to-getVec get) (fromList l))
84     ≡⟨ refl ⟩
85   toList (vec-length (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
86     ≡⟨ vec-length-same (get (toList (fromList l))) (getList-to-getVec-length-property get (fromList l)) ⟩
87   get (toList (fromList l))
88     ≡⟨ cong get (toList-fromList l) ⟩
89   get l ∎
90
91 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
92 vec-len {_} {n} _ = n
93
94 vec-len-via-list : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ vec-len v
95 vec-len-via-list []V       = refl
96 vec-len-via-list (x ∷V xs) = cong suc (vec-len-via-list xs)
97
98 length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
99 length-replicate 0       = refl
100 length-replicate (suc n) = cong suc (length-replicate n)
101
102 {-
103 -- We cannot write the following property, because the expressions
104 -- fromList (toList v) and v have different type. The type differs in the
105 -- length. Somehow we would have to embed a proof that those types are in fact
106 -- the same into the type signature of the function.
107 fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≡ v
108 fromList-toList v = ?
109 -}
110
111 get-commut-2 : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList
112 get-commut-2 getlen get v = {!!}
113
114 get-trafo-2-getlen : (getlen : ℕ → ℕ) → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen
115 get-trafo-2-getlen getlen get n = begin
116   proj₁ (getList-to-getVec (getVec-to-getList get)) n
117     ≡⟨ refl ⟩
118   length (toList (get (fromList (replicate n tt))))
119     ≡⟨ vec-len-via-list (get (fromList (replicate n tt))) ⟩
120   vec-len (get (fromList (replicate n tt)))
121     ≡⟨ cong getlen (length-replicate n) ⟩
122   getlen n ∎
123
124 getVec-getlen : {getlen₁ getlen₂ : ℕ → ℕ} → (get : getV-type getlen₁) → getlen₁ ≗ getlen₂ → getV-type getlen₂
125 getVec-getlen get p {B} {n} v = vec-length (p n) (get v)
126
127 get-trafo-2-get : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) {B} {n} ≗ getVec-getlen get (sym ∘ (get-trafo-2-getlen getlen get))
128 get-trafo-2-get getlen get v = begin
129   proj₂ (getList-to-getVec (getVec-to-getList get)) v
130     ≡⟨ refl ⟩
131   vec-length (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v)))))
132     ≡⟨ {!!} ⟩
133   vec-length (sym (get-trafo-2-getlen getlen get (vec-len v))) (vec-length (cong getlen (length-toList v)) (get (fromList (toList v))))
134     ≡⟨ {!!} ⟩
135   vec-length (sym (get-trafo-2-getlen getlen get (vec-len v))) (get v)
136     ≡⟨ refl ⟩
137   getVec-getlen get (sym ∘ (get-trafo-2-getlen getlen get)) v ∎