complete missing parts of LiftGet
authorHelmut Grohne <helmut@subdivi.de>
Fri, 14 Sep 2012 12:00:57 +0000 (14:00 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 14 Sep 2012 12:00:57 +0000 (14:00 +0200)
Thanks to Joachim Breitner and Wouter Swierstra for their encouragement
and hints. Note that the result duplicates work at this point, but the
proofs are complete.

LiftGet.agda

index eaa2849..c3c5294 100644 (file)
@@ -8,7 +8,7 @@ open import Data.List.Properties using (length-map)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (_∘_ ; flip ; const)
 open import Relation.Binary.Core using (_≡_)
-open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; proof-irrelevance)
+open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 get-type : Set₁
@@ -66,12 +66,27 @@ getList-to-getVec get = getlen , get'
         get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
         get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))
 
-{-
--- We cannot formulate the first commutation property, because the type of
--- fromList (get l) depends on the concrete l, more specifically its length.
-get-commut-1 : (get : get-type) → (fromList ∘ get) ≗ (proj₂ (getList-to-getVec get)) ∘ fromList
-get-commut-1 get l = ?
--}
+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
+subst-subst T refl p' x = refl
+
+subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) → subst (Vec A) (cong length p) (fromList y) ≡ fromList x
+subst-fromList refl = refl
+
+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))
+get-commut-1 get {A} l = begin
+  fromList (get l)
+    ≡⟨ sym (subst-fromList (cong get (toList-fromList l))) ⟩
+  subst (Vec A) (cong length (cong get (toList-fromList l))) (fromList (get (toList (fromList l))))
+    ≡⟨ cong (flip (subst (Vec A)) (fromList (get (toList (fromList l))))) (proof-irrelevance (cong length (cong get (toList-fromList l))) (trans p p')) ⟩
+  subst (Vec A) (trans p p') (fromList (get (toList (fromList l))))
+    ≡⟨ sym (subst-subst (Vec A) p p' (fromList (get (toList (fromList l))))) ⟩
+  subst (Vec A) p' (subst (Vec A) p (fromList (get (toList (fromList l)))))
+    ≡⟨ refl ⟩
+  subst (Vec A) p' (proj₂ (getList-to-getVec get) (fromList l)) ∎
+    where p : length (get (toList (fromList l))) ≡ length (get (replicate (length l) tt))
+          p = getList-to-getVec-length-property get (fromList l)
+          p' : length (get (replicate (length l) tt)) ≡ length (get l)
+          p' = sym (getList-length get l)
 
 get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B}
 get-trafo-1 get {B} l = begin
@@ -112,8 +127,18 @@ fromList-toList {A} (x ∷V xs) = begin
     ≡⟨ cong (λ p →  subst (Vec A) p (x ∷V xs)) (proof-irrelevance (cong suc (sym (length-toList xs))) (sym (cong suc (length-toList xs)))) ⟩
   subst (Vec A) (sym (length-toList (x ∷V xs))) (x ∷V xs) ∎
 
+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)
+subst-cong T f' f x refl = refl
+
 get-commut-2 : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList
-get-commut-2 getlen get v = {!!}
+get-commut-2 getlen get {B} v = begin
+  toList (get v)
+    ≡⟨ sym (toList-subst (get v) (cong getlen (sym (length-toList v)))) ⟩
+  toList (subst (Vec B) (cong getlen (sym (length-toList v))) (get v))
+    ≡⟨ cong toList (sym (subst-cong (Vec B) getlen get v (sym (length-toList v)))) ⟩
+  toList (get (subst (Vec B) (sym (length-toList v)) v))
+    ≡⟨ cong (toList ∘ get) (sym (fromList-toList v)) ⟩
+  toList (get (fromList (toList v))) ∎
 
 get-trafo-2-getlen : (getlen : ℕ → ℕ) → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen
 get-trafo-2-getlen getlen get n = begin
@@ -129,13 +154,29 @@ getVec-getlen : {getlen₁ getlen₂ : ℕ → ℕ} → (get : getV-type getlen
 getVec-getlen get p {B} {n} v = subst (Vec B) (p n) (get v)
 
 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))
-get-trafo-2-get getlen get {B} v = begin
+get-trafo-2-get getlen get {B} {n} v = begin
   proj₂ (getList-to-getVec (getVec-to-getList get)) v
     ≡⟨ refl ⟩
-  subst (Vec B) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v)))))
-    ≡⟨ {!!} ⟩
-  subst (Vec B) (sym (get-trafo-2-getlen getlen get (vec-len v))) (subst (Vec B) (cong getlen (length-toList v)) (get (fromList (toList v))))
-    ≡⟨ {!!} ⟩
-  subst (Vec B) (sym (get-trafo-2-getlen getlen get (vec-len v))) (get v)
+  subst (Vec B) p (fromList (toList (get (fromList (toList v)))))
+    ≡⟨ cong (subst (Vec B) p) (fromList-toList (get (fromList (toList v)))) ⟩
+  subst (Vec B) p (subst (Vec B) p' (get (fromList (toList v))))
+    ≡⟨ subst-subst (Vec B) p' p (get (fromList (toList v))) ⟩
+  subst (Vec B) (trans p' p) (get (fromList (toList v)))
+    ≡⟨ cong (subst (Vec B) (trans p' p) ∘ get) (fromList-toList v) ⟩
+  subst (Vec B) (trans p' p) (get (subst (Vec B) (sym (length-toList v)) v))
+    ≡⟨ cong (subst (Vec B) (trans p' p)) (subst-cong (Vec B) getlen get v (sym (length-toList v))) ⟩
+  subst (Vec B) (trans p' p) (subst (Vec B) (cong getlen (sym (length-toList v))) (get v))
+    ≡⟨ subst-subst (Vec B) (cong getlen (sym (length-toList v))) (trans p' p) (get v) ⟩
+  subst (Vec B) (trans (cong getlen (sym (length-toList v))) (trans p' p)) (get v)
+    ≡⟨ cong (flip (subst (Vec B)) (get v)) (proof-irrelevance (trans (cong getlen (sym (length-toList v))) (trans p' p)) p'') ⟩
+  subst (Vec B) p'' (get v)
     ≡⟨ refl ⟩
   getVec-getlen get (sym ∘ (get-trafo-2-getlen getlen get)) v ∎
+    where n' : ℕ
+          n' = length (toList (get (fromList (replicate n tt))))
+          p : length (toList (get (fromList (toList v)))) ≡ n'
+          p = getList-to-getVec-length-property (getVec-to-getList get) v
+          p' : getlen (length (toList v)) ≡ length (toList (get (fromList (toList v))))
+          p' = sym (length-toList (get (fromList (toList v))))
+          p'' : getlen n ≡ n'
+          p'' = sym (get-trafo-2-getlen getlen get (vec-len v))