diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-09-11 23:33:29 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-09-11 23:33:29 +0200 |
| commit | d3f12c72cb10462ac5ebce3a8cda462c70bff3d9 (patch) | |
| tree | e8de507287efc13ebbf8c9e614d1b79fdf76fab8 | |
| parent | 6aba617941bc5e66f414846131a3e02d9ae1fc41 (diff) | |
| download | bidiragda-d3f12c72cb10462ac5ebce3a8cda462c70bff3d9.tar.gz | |
LiftGet: replace vec-length-same with toList-subst
The name vec-length-same hides the fact that it eliminates a toList and
a fromList. Actually a more generic form without fromList is possible.
Thanks to Joachim Breitner for spotting.
| -rw-r--r-- | LiftGet.agda | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/LiftGet.agda b/LiftGet.agda index 982277f..98ad66d 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -48,8 +48,8 @@ toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l toList-fromList [] = refl toList-fromList (x ∷ xs) = cong (_∷_ x) (toList-fromList xs) -vec-length-same : {A : Set} → (l : List A) → {n : ℕ} → (p : length l ≡ n) → toList (subst (Vec A) p (fromList l)) ≡ l -vec-length-same l refl = toList-fromList l +toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) → toList (subst (Vec A) p v) ≡ toList v +toList-subst v refl = refl getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt)) getList-to-getVec-length-property get {_} {m} v = begin @@ -80,7 +80,9 @@ get-trafo-1 get {B} l = begin toList (proj₂ (getList-to-getVec get) (fromList l)) ≡⟨ refl ⟩ toList (subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) - ≡⟨ vec-length-same (get (toList (fromList l))) (getList-to-getVec-length-property get (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))) ⟩ get (toList (fromList l)) ≡⟨ cong get (toList-fromList l) ⟩ get l ∎ |