Merge branch feature-get-record into feature-partial-getlen

These two features heavily interconnect. As such it makes sense to
integrate them properly. This non-trivial merge does that work. Compared
to feature-partial-getlen a few definitions moved from FreeTheorems.agda
to GetTypes.agda. Many types changed compared to both branches.

Conflicts:
	BFF.agda
	Bidir.agda
	FreeTheorems.agda
	Precond.agda
        conflict in GetTypes.agda not detected by merge

8 files changed, 212 insertions, 50 deletions

diff --git a/BFF.agda b/BFF.agda
index b26cc92..5bf756d 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -20,10 +20,10 @@ open Injection using (to)
 open import FinMap
 open import Generic using (mapMV ; ≡-to-Π)
 import CheckInsert
-import FreeTheorems
+open import GetTypes using (VecVec-to-PartialVecVec)
 
 module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
-  open FreeTheorems.PartialVecVec public using (get-type)
+  open GetTypes.PartialVecVec public using (Get)
   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
   open CheckInsert A
 
@@ -37,10 +37,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
   denumerate = flip lookupV
 
-  bff : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ EqSetoid ℕ) → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i)))
-  bff gl₁ gl₂ get s v =
-                let s′ = enumerate s
-                    t′ = get s′
+
+  bff : (G : Get) → ({i : Setoid.Carrier (Get.I G)} → Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i) → Vec Carrier ((Get.gl₂ G) ⟨$⟩ i) → Maybe (Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)))
+  bff G s v = let   s′ = enumerate s
+                    t′ = Get.get G s′
                     g  = fromFunc (denumerate s)
                     g′ = delete-many t′ g
                     h  = assoc t′ v
@@ -48,11 +48,11 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
                 in h′ >>= flip mapMV s′ ∘ flip lookupV
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
-  open FreeTheorems.VecVec public using (get-type)
+  open GetTypes.VecVec public using (Get)
   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
   open CheckInsert A
 
   open PartialVecBFF A public using (assoc ; enumerate ; denumerate)
 
-  bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n))
-  bff {getlen} get s v = PartialVecBFF.bff A id↪ (≡-to-Π getlen) get {_} s v
+  bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n))
+  bff G = PartialVecBFF.bff A (VecVec-to-PartialVecVec G)
diff --git a/Bidir.agda b/Bidir.agda
index 7add8fd..cb29420 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -27,8 +27,8 @@ open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ;
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
 
-import FreeTheorems
-open FreeTheorems.PartialVecVec using (get-type ; free-theorem)
+import GetTypes
+open GetTypes.PartialVecVec using (Get ; module Get)
 open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid)
 open import FinMap
 import CheckInsert
@@ -128,13 +128,13 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
   as ∎)
   where open ≡-Reasoning
 
-theorem-1 : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (s : Vec Carrier (to gl₁ ⟨$⟩ i)) → bff gl₁ gl₂ get s (get s) ≡ just s
-theorem-1 gl₁ gl₂ get s = begin
-  bff gl₁ gl₂ get s (get s)
-    ≡⟨ cong (bff gl₁ gl₂ get s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
-  bff gl₁ gl₂ get s (get (map (denumerate s) (enumerate s)))
-    ≡⟨ cong (bff gl₁ gl₂ get s) (free-theorem gl₁ gl₂ get (denumerate s) (enumerate s)) ⟩
-  bff gl₁ gl₂ get s (map (denumerate s) (get (enumerate s)))
+theorem-1 : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (s : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → bff G s (Get.get G s) ≡ just s
+theorem-1 G s = begin
+  bff G s (get s)
+    ≡⟨ cong (bff G s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
+  bff G s (get (map (denumerate s) (enumerate s)))
+    ≡⟨ cong (bff G s) (free-theorem (denumerate s) (enumerate s)) ⟩
+  bff G s (map (denumerate s) (get (enumerate s)))
     ≡⟨ refl ⟩
   (h′↦r ∘ h↦h′) (assoc (get (enumerate s)) (map (denumerate s) (get (enumerate s))))
     ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩
@@ -154,6 +154,7 @@ theorem-1 gl₁ gl₂ get s = begin
     ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
   just s ∎
     where open ≡-Reasoning
+          open Get G
           h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s))))
           h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec)
 
@@ -191,9 +192,8 @@ lemma-mapM-successful         (x ∷ xs) () | just y | nothing | _
 lemma-mapM-successful         (x ∷ xs) p  | just y | just ys | [ p′ ] with lemma-mapM-successful xs p′
 lemma-mapM-successful         (x ∷ xs) p  | just y | just ys | [ p′ ] | w , pw = y ∷ w , cong (_∷_ (just y)) pw
 
-
-lemma-get-mapMV : {A B : Set} {f : A → Maybe B} {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → {i : Setoid.Carrier I} {v : Vec A (to gl₁ ⟨$⟩ i)} {r : Vec B (to gl₁ ⟨$⟩ i)} → mapMV f v ≡ just r → (get : get-type gl₁ gl₂) → get <$> mapMV f v ≡ mapMV f (get v)
-lemma-get-mapMV {f = f} gl₁ gl₂ {v = v} p get = let w , pw = lemma-mapM-successful v p in begin
+lemma-get-mapMV : {A B : Set} {f : A → Maybe B} → (G : Get) → {i : Setoid.Carrier (Get.I G)} {v : Vec A (to (Get.gl₁ G) ⟨$⟩ i)} {r : Vec B (to (Get.gl₁ G) ⟨$⟩ i)} → mapMV f v ≡ just r → Get.get G <$> mapMV f v ≡ mapMV f (Get.get G v)
+lemma-get-mapMV {f = f} G {v = v} p = let w , pw = lemma-mapM-successful v p in begin
   get <$> mapMV f v
     ≡⟨ cong (_<$>_ get) (sym (sequence-map f v)) ⟩
   get <$> (sequenceV (map f v))
@@ -203,15 +203,16 @@ lemma-get-mapMV {f = f} gl₁ gl₂ {v = v} p get = let w , pw = lemma-mapM-succ
   get <$> just w
     ≡⟨ sym (lemma-just-sequence (get w)) ⟩
   sequenceV (map just (get w))
-    ≡⟨ cong sequenceV (sym (free-theorem gl₁ gl₂ get just w)) ⟩
+    ≡⟨ cong sequenceV (sym (free-theorem just w)) ⟩
   sequenceV (get (map just w))
     ≡⟨ cong (sequenceV ∘ get) (sym pw) ⟩
   sequenceV (get (map f v))
-    ≡⟨ cong sequenceV (free-theorem gl₁ gl₂ get f v) ⟩
+    ≡⟨ cong sequenceV (free-theorem f v) ⟩
   sequenceV (map f (get v))
     ≡⟨ sequence-map f (get v) ⟩
   mapMV f (get v) ∎
   where open ≡-Reasoning
+        open Get G
 
 sequence-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂
 sequence-cong {S}                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _))
@@ -220,16 +221,16 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecE
 sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 sequence-cong {S}                                       (nothing VecEq.∷-cong xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
-theorem-2 : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (v : Vec Carrier (gl₂ ⟨$⟩ i)) → (s u : Vec Carrier (to gl₁ ⟨$⟩ i)) → bff gl₁ gl₂ get s v ≡ just u → VecISetoid A.setoid at _ ∋ get u ≈ v
-theorem-2 gl₁ gl₂ get v s u p with (lemma->>=-just ((flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (get (enumerate s)) v)) p)
-theorem-2 gl₁ gl₂ get v s u p | h′ , ph′ with (lemma-<$>-just (assoc (get (enumerate s)) v) ph′)
-theorem-2 gl₁ gl₂ get v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩
+theorem-2 : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (v : Vec Carrier (Get.gl₂ G ⟨$⟩ i)) → (s u : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → bff G s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
+theorem-2 G v s u p with (lemma->>=-just ((flip union (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (Get.get G (enumerate s)) v)) p)
+theorem-2 G v s u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate s)) v) ph′)
+theorem-2 G v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩
   get <$> (just u)
     ≡⟨ cong (_<$>_ get) (sym p) ⟩
-  get <$> (bff gl₁ gl₂ get s v)
+  get <$> (bff G s v)
     ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
   get <$> mapMV (flip lookupM (h↦h′ h)) s′
-    ≡⟨ lemma-get-mapMV gl₁ gl₂ (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) get ⟩
+    ≡⟨ lemma-get-mapMV G (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) ⟩
   mapMV (flip lookupM (h↦h′ h)) (get s′)
     ≡⟨ sym (sequence-map (flip lookupM (h↦h′ h)) (get s′)) ⟩
   sequenceV (map (flip lookupM (h↦h′ h)) (get s′))
@@ -240,6 +241,7 @@ theorem-2 gl₁ gl₂ get v s u p | h′ , ph′ | h , ph = drop-just (begin⟨
     ≡⟨ lemma-just-sequence v ⟩
   just v ∎)
     where open SetoidReasoning
+          open Get G
           s′   = enumerate s
           g    = fromFunc (denumerate s)
           g′   = delete-many (get s′) g
diff --git a/Everything.agda b/Everything.agda
new file mode 100644
index 0000000..7399254
--- /dev/null
+++ b/Everything.agda
@@ -0,0 +1,12 @@
+-- The sole purpose of this module is to ease compilation of everything.
+module Everything where
+
+import Generic
+import FinMap
+import CheckInsert
+import GetTypes
+import FreeTheorems
+import BFF
+import Bidir
+import LiftGet
+import Precond
diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index c22a68d..2181163 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -13,31 +13,40 @@ open Injection using (to)
 
 open import Generic using (≡-to-Π)
 
+import GetTypes
+
 module ListList where
   get-type : Set₁
   get-type = {A : Set} → List A → List A
 
+  open GetTypes.ListList public
+
   postulate
     free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
 
+  assume-get : get-type → Get
+  assume-get get = record { get = get; free-theorem = free-theorem get }
+
 module VecVec where
   get-type : (ℕ → ℕ) → Set₁
   get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
 
-  free-theorem-type : Set₁
-  free-theorem-type = {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+  open GetTypes.VecVec public
 
   postulate
-    free-theorem : free-theorem-type
+    free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+
+  assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
+  assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }
 
 module PartialVecVec where
   get-type : {I : Setoid ℓ₀ ℓ₀} → (I ↪ (EqSetoid ℕ)) → (I ⟶ (EqSetoid ℕ)) → Set₁
   get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
 
+  open GetTypes.PartialVecVec public
+
   postulate
     free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
 
-  open VecVec using () renaming (free-theorem-type to VecVec-free-theorem-type)
-
-  VecVec-free-theorem : VecVec-free-theorem-type
-  VecVec-free-theorem {getlen} get = free-theorem Function.Injection.id (≡-to-Π getlen) get
+  assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → Get
+  assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get }
diff --git a/GetTypes.agda b/GetTypes.agda
new file mode 100644
index 0000000..a52ec24
--- /dev/null
+++ b/GetTypes.agda
@@ -0,0 +1,45 @@
+module GetTypes where
+
+open import Level using () renaming (zero to ℓ₀)
+open import Data.Nat using (ℕ)
+open import Data.List using (List ; map)
+open import Data.Vec using (Vec) renaming (map to mapV)
+open import Function using (_∘_)
+open import Function.Equality using (_⟶_ ; _⟨$⟩_)
+open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
+open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
+open import Relation.Binary using (Setoid)
+open Injection using (to)
+
+open import Generic using (≡-to-Π)
+
+module ListList where
+  record Get : Set₁ where
+    field
+      get : {A : Set} → List A → List A
+      free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+
+module VecVec where
+  record Get : Set₁ where
+    field
+      getlen : ℕ → ℕ
+      get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+      free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+
+module PartialVecVec where
+  record Get : Set₁ where
+    field
+      I : Setoid ℓ₀ ℓ₀
+      gl₁ : I ↪ EqSetoid ℕ
+      gl₂ : I ⟶ EqSetoid ℕ
+      get : {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
+      free-theorem : {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
+
+VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
+VecVec-to-PartialVecVec G = record
+  { I = EqSetoid ℕ
+  ; gl₁ = id↪
+  ; gl₂ = ≡-to-Π getlen
+  ; get = get
+  ; free-theorem = free-theorem
+  } where open VecVec.Get G
diff --git a/LiftGet.agda b/LiftGet.agda
index 31a632e..f064bf8 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -2,23 +2,51 @@ 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_)
+open import Data.Vec using (Vec ; toList ; fromList) renaming ([] to []V ; _∷_ to _∷V_ ; map to mapV)
 open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
 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 ; trans ; proof-irrelevance)
-open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
+open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance ; module ≡-Reasoning)
+open import Relation.Binary.HeterogeneousEquality using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-subst-removable) renaming (refl to het-refl ; sym to het-sym ; cong to het-cong ; reflexive to het-reflexive)
 
 import FreeTheorems
 open import Generic using (length-replicate ; subst-cong ; subst-fromList ; subst-subst ; toList-fromList ; toList-subst)
-open FreeTheorems.ListList using (get-type ; free-theorem)
-open FreeTheorems.VecVec using () renaming (get-type to getV-type)
+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)
 
 getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
 getVec-to-getList get = toList ∘ get ∘ fromList
 
+fromList∘map : {α β : Set} → (f : α → β) → (l : List α) → fromList (map f l) ≡ subst (Vec β) (sym (length-map f l)) (mapV f (fromList l))
+fromList∘map f []       = refl
+fromList∘map f (x ∷ xs) rewrite fromList∘map f xs = trans (subst-cong (Vec _) (_∷V_ (f x)) (sym (length-map f xs)) (mapV f (fromList xs)))
+                                                          (cong (flip (subst (Vec _)) (f x ∷V mapV f (fromList xs))) (proof-irrelevance (cong suc (sym (length-map f xs)))
+                                                                                                                                        (sym (cong suc (length-map f xs)))))
+
+toList∘map : {α β : Set} {n : ℕ} → (f : α → β) → (v : Vec α n) → toList (mapV f v) ≡ map f (toList v)
+toList∘map f []V       = refl
+toList∘map f (x ∷V xs) = cong (_∷_ (f x)) (toList∘map f xs)
+
+GetV-to-GetL : GetV → GetL
+GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theorem = ft }
+  where open GetV getrecord
+        open ≡-Reasoning
+        ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs)))
+        ft f xs = begin
+          toList (get (fromList (map f xs)))
+            ≡⟨ cong (toList ∘ get) (fromList∘map f xs) ⟩
+          toList (get (subst (Vec _) (sym (length-map f xs)) (mapV f (fromList xs))))
+            ≡⟨ cong toList (subst-cong (Vec _) get (sym (length-map f xs)) (mapV f (fromList xs))) ⟩
+          toList (subst (Vec _) (cong getlen (sym (length-map f xs))) (get (mapV f (fromList xs))))
+            ≡⟨ toList-subst (get (mapV f (fromList xs))) (cong getlen (sym (length-map f xs))) ⟩
+          toList (get (mapV f (fromList xs)))
+            ≡⟨ cong toList (free-theorem f (fromList xs)) ⟩
+          toList (mapV f (get (fromList xs)))
+            ≡⟨ toList∘map f (get (fromList xs)) ⟩
+          map f (toList (get (fromList xs))) ∎
+
 getList-to-getlen : get-type → ℕ → ℕ
 getList-to-getlen get = length ∘ get ∘ flip replicate tt
 
@@ -31,10 +59,11 @@ getList-length get l = begin
   length (get l)
     ≡⟨ sym (length-map (const tt) (get l)) ⟩
   length (map (const tt) (get l))
-    ≡⟨ cong length (sym (free-theorem get (const tt) l)) ⟩
+    ≡⟨ cong length (sym (free-theoremL get (const tt) l)) ⟩
   length (get (map (const tt) l))
     ≡⟨ cong (length ∘ get) (replicate-length l) ⟩
   length (get (replicate (length l) tt)) ∎
+  where open ≡-Reasoning
 
 length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ n
 length-toList []V = refl
@@ -47,6 +76,7 @@ getList-to-getVec-length-property get {_} {m} v = begin
     length (get (replicate (length (toList v)) tt))
       ≡⟨ cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
     length (get (replicate m tt)) ∎
+    where open ≡-Reasoning
 
 getList-to-getVec : get-type → ∃ λ (getlen : ℕ → ℕ) → (getV-type getlen)
 getList-to-getVec get = getlen , get'
@@ -55,6 +85,54 @@ 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)))
 
+ind-cong : {I : Set} → (X Y : I → Set) → (f : {i : I} → X i → Y i) → {i j : I} → (i ≡ j) → {x : X i} → {y : X j} → x ≅ y → f x ≅ f y
+ind-cong X Y f refl het-refl = het-refl
+
+private
+  module GetV-Implementation (getrecord : GetL) where
+
+    open GetL getrecord
+
+    getlen = length ∘ get ∘ flip replicate tt
+
+
+    length-property : {C : Set} {m : ℕ} → (s : Vec C m) → length (get (toList s)) ≡ getlen m
+    length-property {m = m} s = begin
+      length (get (toList s))
+        ≡⟨ sym (length-map (const tt) (get (toList s))) ⟩
+      length (map (const tt) (get (toList s)))
+        ≡⟨ cong length (sym (free-theorem (const tt) (toList s))) ⟩
+      length (get (map (const tt) (toList s)))
+        ≡⟨ cong (length ∘ get) (replicate-length (toList s)) ⟩
+      length (get (replicate (length (toList s)) tt))
+        ≡⟨ cong getlen (length-toList s) ⟩
+      getlen m ∎
+      where open ≡-Reasoning
+
+    getV : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
+    getV s = subst (Vec _) (length-property s) (fromList (get (toList s)))
+
+    ft : {α β : Set} (f : α → β) {n : ℕ} (v : Vec α n) → getV (mapV f v) ≡ mapV f (getV v)
+    ft f v = ≅-to-≡ (begin
+      subst (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v))))
+        ≅⟨ ≡-subst-removable (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v)))) ⟩
+      fromList (get (toList (mapV f v)))
+        ≅⟨ het-cong (fromList ∘ get) (het-reflexive (toList∘map f v)) ⟩
+      fromList (get (map f (toList v)))
+        ≅⟨ het-cong fromList (het-reflexive (free-theorem f (toList v))) ⟩
+      fromList (map f (get (toList v)))
+        ≡⟨ fromList∘map f (get (toList v)) ⟩
+      subst (Vec _) (sym (length-map f (get (toList v)))) (mapV f (fromList (get (toList v))))
+        ≅⟨ ≡-subst-removable (Vec _) (sym (length-map f (get (toList v)))) (mapV f (fromList (get (toList v)))) ⟩
+      mapV f (fromList (get (toList v)))
+        ≅⟨ ind-cong (Vec _) (Vec _) (mapV f) (length-property v) (het-sym (≡-subst-removable (Vec _) (length-property v) (fromList (get (toList v))))) ⟩
+      mapV f (subst (Vec _) (length-property v) (fromList (get (toList v)))) ∎)
+      where open ≅-Reasoning
+
+GetL-to-GetV : GetL → GetV
+GetL-to-GetV getrecord = record { getlen = getlen; get = getV; free-theorem = ft }
+  where open GetV-Implementation getrecord
+
 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)
@@ -66,7 +144,8 @@ get-commut-1 get {A} l = begin
   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))
+    where open ≡-Reasoning
+          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)
@@ -84,6 +163,7 @@ get-trafo-1 get {B} l = begin
   get (toList (fromList l))
     ≡⟨ cong get (toList-fromList l) ⟩
   get l ∎
+  where open ≡-Reasoning
 
 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
 vec-len {_} {n} _ = n
@@ -98,6 +178,7 @@ fromList-toList {A} (x ∷V xs) = begin
   subst (Vec A) (cong suc (sym (length-toList xs))) (x ∷V xs)
     ≡⟨ 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) ∎
+  where open ≡-Reasoning
 
 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 {B} v = begin
@@ -108,6 +189,7 @@ get-commut-2 getlen get {B} v = begin
   toList (get (subst (Vec B) (sym (length-toList v)) v))
     ≡⟨ cong (toList ∘ get) (sym (fromList-toList v)) ⟩
   toList (get (fromList (toList v))) ∎
+  where open ≡-Reasoning
 
 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
@@ -118,6 +200,7 @@ get-trafo-2-getlen getlen get n = begin
   vec-len (get (fromList (replicate n tt)))
     ≡⟨ cong getlen (length-replicate n) ⟩
   getlen n ∎
+  where open ≡-Reasoning
 
 get-trafo-2-get : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ subst (Vec B) (sym (get-trafo-2-getlen getlen get n)) ∘ get
 get-trafo-2-get getlen get {B} {n} v = begin
@@ -136,7 +219,8 @@ get-trafo-2-get getlen get {B} {n} v = begin
   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) ∎
-    where n' : ℕ
+    where open ≡-Reasoning
+          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
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..5dfe960
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,8 @@
+AGDA ?= agda
+AGDALIB ?= /usr/share/agda-stdlib
+
+all:Everything.agdai
+clean:
+	rm -f *.agdai
+Everything.agdai:$(wildcard *.agda)
+	$(AGDA) -i. -i$(AGDALIB) Everything.agda
diff --git a/Precond.agda b/Precond.agda
index a6f2871..787f010 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -34,8 +34,9 @@ import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
 open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
-
-open BFF.PartialVecBFF (decSetoid deq) using (get-type ; assoc ; enumerate ; denumerate ; bff)
+import GetTypes
+open GetTypes.PartialVecVec using (Get ; module Get)
+open BFF.PartialVecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
 
 lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup f (map Maybe.just v) ≡ Maybe.just (lookup f v)
 lemma-lookup-map-just zero    (x ∷ xs) = refl
@@ -73,9 +74,9 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Da
           maybe′ just (lookupM i (delete-many is (map just g))) (lookup i h) ∎
         inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i)
 
-assoc-enough : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (s : Vec Carrier (to gl₁ ⟨$⟩ i)) → (v : Vec Carrier (gl₂ ⟨$⟩ i)) → ∃ (λ h → assoc (get (enumerate s)) v ≡ just h) → ∃ λ u → bff gl₁ gl₂ get s v ≡ just u
-assoc-enough gl₁ gl₂ get s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin
-  bff gl₁ gl₂ get s v
+assoc-enough : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (s : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → (v : Vec Carrier (Get.gl₂ G ⟨$⟩ i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u
+assoc-enough G s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin
+  bff G s v
     ≡⟨ cong (flip _>>=_ (flip mapMV s′ ∘ flip lookupM) ∘ _<$>_ (flip union g′)) p ⟩
   mapMV (flip lookupM (union h g′)) s′
     ≡⟨ sym (sequence-map (flip lookupM (union h g′)) s′) ⟩
@@ -88,7 +89,8 @@ assoc-enough gl₁ gl₂ get s v (h , p) = let w , pw = lemma-union-delete-fromF
   sequenceV (map Maybe.just (map (flip lookup w) s′))
     ≡⟨ lemma-just-sequence (map (flip lookup w) s′) ⟩
   just (map (flip lookup w) s′) ∎)
-  where s′ = enumerate s
+  where open Get G
+        s′ = enumerate s
         g  = fromFunc (denumerate s)
         g′ = delete-many (get s′) g