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 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 toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l
  48 toList-fromList []       = refl
  49 toList-fromList (x ∷ xs) = cong (_∷_ x) (toList-fromList xs)
  50
  51 toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) → toList (subst (Vec A) p v) ≡ toList v
  52 toList-subst v refl = refl
  53
  54 getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt))
  55 getList-to-getVec-length-property get {_} {m} v = begin
  56     length (get (toList v))
  57       ≡⟨ getList-length get (toList v) ⟩
  58     length (get (replicate (length (toList v)) tt))
  59       ≡⟨ cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
  60     length (get (replicate m tt)) ∎
  61
  62 getList-to-getVec : get-type → ∃ λ (getlen : ℕ → ℕ) → (getV-type getlen)
  63 getList-to-getVec get = getlen , get'
  64   where getlen : ℕ → ℕ
  65         getlen = getList-to-getlen get
  66         get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
  67         get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))
  68
  69 subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p' : b ≡ c) → (x : T a)→ subst T p' (subst T p x) ≡ subst T (trans p p') x
  70 subst-subst T refl p' x = refl
  71
  72 subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) → subst (Vec A) (cong length p) (fromList y) ≡ fromList x
  73 subst-fromList refl = refl
  74
  75 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))
  76 get-commut-1 get {A} l = begin
  77   fromList (get l)
  78     ≡⟨ sym (subst-fromList (cong get (toList-fromList l))) ⟩
  79   subst (Vec A) (cong length (cong get (toList-fromList l))) (fromList (get (toList (fromList l))))
  80     ≡⟨ cong (flip (subst (Vec A)) (fromList (get (toList (fromList l))))) (proof-irrelevance (cong length (cong get (toList-fromList l))) (trans p p')) ⟩
  81   subst (Vec A) (trans p p') (fromList (get (toList (fromList l))))
  82     ≡⟨ sym (subst-subst (Vec A) p p' (fromList (get (toList (fromList l))))) ⟩
  83   subst (Vec A) p' (subst (Vec A) p (fromList (get (toList (fromList l)))))
  84     ≡⟨ refl ⟩
  85   subst (Vec A) p' (proj₂ (getList-to-getVec get) (fromList l)) ∎
  86     where p : length (get (toList (fromList l))) ≡ length (get (replicate (length l) tt))
  87           p = getList-to-getVec-length-property get (fromList l)
  88           p' : length (get (replicate (length l) tt)) ≡ length (get l)
  89           p' = sym (getList-length get l)
  90
  91 get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B}
  92 get-trafo-1 get {B} l = begin
  93   getVec-to-getList (proj₂ (getList-to-getVec get)) l
  94     ≡⟨ refl ⟩
  95   toList (proj₂ (getList-to-getVec get) (fromList l))
  96     ≡⟨ refl ⟩
  97   toList (subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
  98     ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩
  99   toList (fromList (get (toList (fromList l))))
 100     ≡⟨ toList-fromList (get (toList (fromList l))) ⟩
 101   get (toList (fromList l))
 102     ≡⟨ cong get (toList-fromList l) ⟩
 103   get l ∎
 104
 105 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
 106 vec-len {_} {n} _ = n
 107
 108 vec-len-via-list : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ vec-len v
 109 vec-len-via-list []V       = refl
 110 vec-len-via-list (x ∷V xs) = cong suc (vec-len-via-list xs)
 111
 112 length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
 113 length-replicate 0       = refl
 114 length-replicate (suc n) = cong suc (length-replicate n)
 115
 116 ∷-subst : {A : Set} {n m : ℕ} → (x : A) → (xs : Vec A n) → (p : n ≡ m) → x ∷V subst (Vec A) p xs ≡ subst (Vec A) (cong suc p) (x ∷V xs)
 117 ∷-subst x xs refl = refl
 118
 119 fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≡ subst (Vec A) (sym (length-toList v)) v
 120 fromList-toList     []V       = refl
 121 fromList-toList {A} (x ∷V xs) = begin
 122   x ∷V fromList (toList xs)
 123     ≡⟨ cong (_∷V_ x) (fromList-toList xs) ⟩
 124   x ∷V subst (Vec A) (sym (length-toList xs)) xs
 125     ≡⟨ ∷-subst x xs (sym (length-toList xs)) ⟩
 126   subst (Vec A) (cong suc (sym (length-toList xs))) (x ∷V xs)
 127     ≡⟨ cong (λ p →  subst (Vec A) p (x ∷V xs)) (proof-irrelevance (cong suc (sym (length-toList xs))) (sym (cong suc (length-toList xs)))) ⟩
 128   subst (Vec A) (sym (length-toList (x ∷V xs))) (x ∷V xs) ∎
 129
 130 subst-cong : {A : Set} (T : A → Set) {a b : A} → (f' : A → A) → (f : {c : A} → T c → T (f' c)) → (x : T a) → (p : a ≡ b) → f (subst T p x) ≡ subst T (cong f' p) (f x)
 131 subst-cong T f' f x refl = refl
 132
 133 get-commut-2 : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList
 134 get-commut-2 getlen get {B} v = begin
 135   toList (get v)
 136     ≡⟨ sym (toList-subst (get v) (cong getlen (sym (length-toList v)))) ⟩
 137   toList (subst (Vec B) (cong getlen (sym (length-toList v))) (get v))
 138     ≡⟨ cong toList (sym (subst-cong (Vec B) getlen get v (sym (length-toList v)))) ⟩
 139   toList (get (subst (Vec B) (sym (length-toList v)) v))
 140     ≡⟨ cong (toList ∘ get) (sym (fromList-toList v)) ⟩
 141   toList (get (fromList (toList v))) ∎
 142
 143 get-trafo-2-getlen : (getlen : ℕ → ℕ) → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen
 144 get-trafo-2-getlen getlen get n = begin
 145   proj₁ (getList-to-getVec (getVec-to-getList get)) n
 146     ≡⟨ refl ⟩
 147   length (toList (get (fromList (replicate n tt))))
 148     ≡⟨ vec-len-via-list (get (fromList (replicate n tt))) ⟩
 149   vec-len (get (fromList (replicate n tt)))
 150     ≡⟨ cong getlen (length-replicate n) ⟩
 151   getlen n ∎
 152
 153 getVec-getlen : {getlen₁ getlen₂ : ℕ → ℕ} → (get : getV-type getlen₁) → getlen₁ ≗ getlen₂ → getV-type getlen₂
 154 getVec-getlen get p {B} {n} v = subst (Vec B) (p n) (get v)
 155
 156 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))
 157 get-trafo-2-get getlen get {B} {n} v = begin
 158   proj₂ (getList-to-getVec (getVec-to-getList get)) v
 159     ≡⟨ refl ⟩
 160   subst (Vec B) p (fromList (toList (get (fromList (toList v)))))
 161     ≡⟨ cong (subst (Vec B) p) (fromList-toList (get (fromList (toList v)))) ⟩
 162   subst (Vec B) p (subst (Vec B) p' (get (fromList (toList v))))
 163     ≡⟨ subst-subst (Vec B) p' p (get (fromList (toList v))) ⟩
 164   subst (Vec B) (trans p' p) (get (fromList (toList v)))
 165     ≡⟨ cong (subst (Vec B) (trans p' p) ∘ get) (fromList-toList v) ⟩
 166   subst (Vec B) (trans p' p) (get (subst (Vec B) (sym (length-toList v)) v))
 167     ≡⟨ cong (subst (Vec B) (trans p' p)) (subst-cong (Vec B) getlen get v (sym (length-toList v))) ⟩
 168   subst (Vec B) (trans p' p) (subst (Vec B) (cong getlen (sym (length-toList v))) (get v))
 169     ≡⟨ subst-subst (Vec B) (cong getlen (sym (length-toList v))) (trans p' p) (get v) ⟩
 170   subst (Vec B) (trans (cong getlen (sym (length-toList v))) (trans p' p)) (get v)
 171     ≡⟨ cong (flip (subst (Vec B)) (get v)) (proof-irrelevance (trans (cong getlen (sym (length-toList v))) (trans p' p)) p'') ⟩
 172   subst (Vec B) p'' (get v)
 173     ≡⟨ refl ⟩
 174   getVec-getlen get (sym ∘ (get-trafo-2-getlen getlen get)) v ∎
 175     where n' : ℕ
 176           n' = length (toList (get (fromList (replicate n tt))))
 177           p : length (toList (get (fromList (toList v)))) ≡ n'
 178           p = getList-to-getVec-length-property (getVec-to-getList get) v
 179           p' : getlen (length (toList v)) ≡ length (toList (get (fromList (toList v))))
 180           p' = sym (length-toList (get (fromList (toList v))))
 181           p'' : getlen n ≡ n'
 182           p'' = sym (get-trafo-2-getlen getlen get (vec-len v))