diff options
Diffstat (limited to 'LiftGet.agda')
| -rw-r--r-- | LiftGet.agda | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/LiftGet.agda b/LiftGet.agda index 9e2a805..4ddf26f 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -3,6 +3,7 @@ module LiftGet where open import Data.Unit using (⊤ ; tt) open import Data.Nat using (ℕ ; suc) open import Data.Vec using (Vec ; toList ; fromList) renaming ([] to []V ; _∷_ to _∷V_ ; map to mapV) +open import Data.Vec.Properties using (toList∘fromList) open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map) open import Data.List.Properties using (length-map ; length-replicate) open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) @@ -11,7 +12,7 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; pr open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable) import FreeTheorems -open import Generic using (toList-fromList ; toList-subst) +open import Generic using (toList-subst) open FreeTheorems.ListList using (get-type) renaming (free-theorem to free-theoremL ; Get to GetL ; module Get to GetL) open FreeTheorems.VecVec using () renaming (get-type to getV-type ; Get to GetV ; module Get to GetV) @@ -114,7 +115,7 @@ GetL-to-GetV getrecord = record { getlen = getlen; get = getV; free-theorem = ft get-commut-1-≅ : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≅ proj₂ (getList-to-getVec get) (fromList l) get-commut-1-≅ get l = begin fromList (get l) - ≅⟨ H.cong (fromList ∘ get) (≡-to-≅ (P.sym (toList-fromList l))) ⟩ + ≅⟨ H.cong (fromList ∘ get) (≡-to-≅ (P.sym (toList∘fromList l))) ⟩ fromList (get (toList (fromList l))) ≅⟨ H.sym (≡-subst-removable (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ⟩ P.subst (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))) ∎ @@ -138,9 +139,9 @@ get-trafo-1 get {B} l = begin toList (P.subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩ toList (fromList (get (toList (fromList l)))) - ≡⟨ toList-fromList (get (toList (fromList l))) ⟩ + ≡⟨ toList∘fromList (get (toList (fromList l))) ⟩ get (toList (fromList l)) - ≡⟨ P.cong get (toList-fromList l) ⟩ + ≡⟨ P.cong get (toList∘fromList l) ⟩ get l ∎ where open ≡-Reasoning |