Merge branch feature-delete

Most conflicts stem from varying imports or added functions and a
take-both approach merges them. A notable exception is theorem-2, where
a new result sequence-cong was required. Apart from that, theorem-2
could be taken almost verbatim from feature-delete albeit its type
coming from feature-decsetoid.

Conflicts:
	Bidir.agda
	FinMap.agda
	Generic.agda
	Precond.agda

5 files changed, 199 insertions, 102 deletions

diff --git a/BFF.agda b/BFF.agda
index 88d9244..61eeefd 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -14,6 +14,7 @@ open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary using (DecSetoid ; module DecSetoid)
 
 open import FinMap
+open import Generic using (mapMV)
 import CheckInsert
 import FreeTheorems
 
@@ -34,7 +35,9 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
 
   bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n))
   bff get s v = let s′ = enumerate s
+                    t′ = get s′
                     g  = fromFunc (denumerate s)
-                    h  = assoc (get s′) v
-                    h′ = (flip union g) <$> h
-                in (flip mapV s′ ∘ flip lookupV) <$> h′
+                    g′ = delete-many t′ g
+                    h  = assoc t′ v
+                    h′ = (flip union g′) <$> h
+                in h′ >>= flip mapMV s′ ∘ flip lookupV
diff --git a/Bidir.agda b/Bidir.agda
index 03daf9d..32d0ae7 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -8,7 +8,7 @@ open import Data.Fin using (Fin)
 import Level
 import Category.Monad
 import Category.Functor
-open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
+open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
 open import Data.List using (List)
@@ -25,7 +25,7 @@ import Relation.Binary.EqReasoning as EqR
 
 import FreeTheorems
 open FreeTheorems.VecVec using (get-type ; free-theorem)
-open import Generic using (just-injective ; map-just-injective ; vecIsSetoid)
+open import Generic using (just-injective ; vecIsSetoid ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
 open import FinMap
 import CheckInsert
 open CheckInsert A
@@ -135,31 +135,36 @@ theorem-1 get s = begin
     ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩
   (h′↦r ∘ h↦h′ ∘ just) (restrict (denumerate s) (toList (get (enumerate s))))
     ≡⟨ refl ⟩
-  (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (fromFunc (denumerate s)))
-    ≡⟨ cong (h′↦r ∘ just) (lemma-union-restrict (denumerate s) (toList (get (enumerate s)))) ⟩
+  (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (fromFunc (denumerate s))))
+    ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩
   (h′↦r ∘ just) (fromFunc (denumerate s))
     ≡⟨ refl ⟩
-  just (map (flip lookup (fromFunc (denumerate s))) (enumerate s))
-    ≡⟨ cong just (map-cong (lookup∘tabulate (denumerate s)) (enumerate s)) ⟩
+  mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s)
+    ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-fromFunc-tabulate (denumerate s)) ⟩
+  mapMV (flip lookupVec (tabulate (Maybe.just ∘ denumerate s))) (enumerate s)
+    ≡⟨ mapMV-cong (lookup∘tabulate (Maybe.just ∘ denumerate s)) (enumerate s) ⟩
+  mapMV (Maybe.just ∘ denumerate s) (enumerate s)
+    ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩
   just (map (denumerate s) (enumerate s))
     ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
   just s ∎
     where open ≡-Reasoning
-          h↦h′ = _<$>_ (flip union (fromFunc (denumerate s)))
-          h′↦r = _<$>_ (flip map (enumerate s) ∘ flip lookupVec)
+          h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s))))
+          h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec)
 
-lemma-<$>-just : {A B : Set} {f : A → B} {b : B} {ma : Maybe A} → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
-lemma-<$>-just {ma = just x}  f<$>ma≡just-b = x , refl
-lemma-<$>-just {ma = nothing} ()
 
-lemma-union-not-used : {m n : ℕ} {A : Set} (h : FinMapMaybe n A) → (h' : FinMap n A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map just (map (flip lookup (union h h')) is) ≡ map (flip lookupM h) is
+lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
+lemma-<$>-just (just x) f<$>ma≡just-b = x , refl
+lemma-<$>-just nothing  ()
+
+lemma-union-not-used : {m n : ℕ} {A : Set} (h : FinMapMaybe n A) → (h' : FinMapMaybe n A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map (flip lookupM (union h h')) is ≡ map (flip lookupM h) is
 lemma-union-not-used h h' []        p = refl
 lemma-union-not-used h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong₂ _∷_ (begin
-      just (lookup i (union h h'))
-        ≡⟨ cong just (lookup∘tabulate (λ j → maybe′ id (lookup j h') (lookupM j h)) i) ⟩
-      just (maybe′ id (lookup i h') (lookupM i h))
-        ≡⟨ cong just (cong (maybe′ id (lookup i h')) px) ⟩
-      just (maybe′ id (lookup i h') (just x))
+      lookupM i (union h h')
+        ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h') (lookupM j h)) i ⟩
+      maybe′ just (lookupM i h') (lookupM i h)
+        ≡⟨ cong (maybe′ just (lookupM i h')) px ⟩
+      maybe′ just (lookupM i h') (just x)
         ≡⟨ sym px ⟩
       lookupM i h ∎)
   (lemma-union-not-used h h' is' p')
@@ -169,29 +174,73 @@ map-just-≈-injective : {n : ℕ} {x y : Vec Carrier n} → Setoid._≈_ (vecIs
 map-just-≈-injective {x = []}    {y = []}    VecEq.[]-cong              = VecEq.[]-cong
 map-just-≈-injective {x = _ ∷ _} {y = _ ∷ _} (just x≈y VecEq.∷-cong ps) = x≈y VecEq.∷-cong map-just-≈-injective ps
 
+lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma >>= f) ≡ just b → ∃ λ a → ma ≡ just a
+lemma->>=-just (just a) p = a , refl
+lemma->>=-just nothing  ()
+
+lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
+lemma-just-sequence [] = refl
+lemma-just-sequence (x ∷ xs) rewrite lemma-just-sequence xs = refl
+
+lemma-mapM-successful : {A B : Set} {f : A → Maybe B} {n : ℕ} → (v : Vec A n) → {r : Vec B n} → mapMV f v ≡ just r → ∃ λ w → map f v ≡ map just w
+lemma-mapM-successful         []      p = [] , refl
+lemma-mapM-successful {f = f} (x ∷ xs) p with f x | mapMV f xs | inspect (mapMV f) xs
+lemma-mapM-successful         (x ∷ xs) () | nothing | _ | _
+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} {n : ℕ} {v : Vec A n} {r : Vec B n} → mapMV f v ≡ just r → {getlen : ℕ → ℕ} (get : get-type getlen) → get <$> mapMV f v ≡ mapMV f (get v)
+lemma-get-mapMV {f = f} {v = v} p get = 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))
+    ≡⟨ cong (_<$>_ get ∘ sequenceV) pw ⟩
+  get <$> (sequenceV (map just w))
+    ≡⟨ cong (_<$>_ get) (lemma-just-sequence w) ⟩
+  get <$> just w
+    ≡⟨ sym (lemma-just-sequence (get w)) ⟩
+  sequenceV (map just (get w))
+    ≡⟨ cong sequenceV (sym (free-theorem get just w)) ⟩
+  sequenceV (get (map just w))
+    ≡⟨ cong (sequenceV ∘ get) (sym pw) ⟩
+  sequenceV (get (map f v))
+    ≡⟨ cong sequenceV (free-theorem get f v) ⟩
+  sequenceV (map f (get v))
+    ≡⟨ sequence-map f (get v) ⟩
+  mapMV f (get v) ∎
+  where open ≡-Reasoning
+
+sequence-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (vecIsSetoid (MaybeSetoid S) n)} → Setoid._≈_ (vecIsSetoid (MaybeSetoid S) n) m₁ m₂ → Setoid._≈_ (MaybeSetoid (vecIsSetoid S n)) (sequenceV m₁) (sequenceV m₂)
+sequence-cong {S}                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (vecIsSetoid S _))
+sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) with sequenceV xs | sequenceV ys | sequence-cong xs≈ys
+sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | just sxs | just sys | just p = MaybeEq.just (x≈y VecEq.∷-cong p)
+sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (vecIsSetoid S _))
+sequence-cong {S}                                       (nothing VecEq.∷-cong xs≈ys) = Setoid.refl (MaybeSetoid (vecIsSetoid S _))
+
 theorem-2 : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (v : Vec Carrier (getlen m)) → (s u : Vec Carrier m) → bff get s v ≡ just u → Setoid._≈_ (vecIsSetoid A.setoid (getlen m)) (get u) v
-theorem-2 get v s u p with lemma-<$>-just (proj₂ (lemma-<$>-just p))
-theorem-2 get v s u p | h , ph = begin⟨ vecIsSetoid A.setoid _ ⟩
-  get u
-    ≡⟨ just-injective (begin⟨ EqSetoid _ ⟩
-      get <$> (just u)
-        ≡⟨ cong (_<$>_ get) (sym p) ⟩
-      get <$> (bff get s v)
-        ≡⟨ cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
-      get <$> (h′↦r <$> (h↦h′ <$> just h)) ∎) ⟩
-  get (map (flip lookup (h↦h′ h)) s′)
-    ≡⟨ free-theorem get (flip lookup (h↦h′ h)) s′ ⟩
-  map (flip lookup (h↦h′ h)) (get s′)
-     ≈⟨ map-just-≈-injective (begin⟨ vecIsSetoid (MaybeSetoid A.setoid) _ ⟩
-       map just (map (flip lookup (union h g)) (get s′))
-         ≡⟨ lemma-union-not-used h g (get s′) (lemma-assoc-domain (get s′) v h ph) ⟩
-       map (flip lookupM h) (get s′)
-         ≈⟨ lemma-2 (get s′) v h ph ⟩
-       map just v
-         ∎) ⟩
-  v ∎
+theorem-2 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 get v s u p | h′ , ph′ with (lemma-<$>-just (assoc (get (enumerate s)) v) ph′)
+theorem-2 get v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (vecIsSetoid A.setoid _) ⟩
+  get <$> (just u)
+    ≡⟨ cong (_<$>_ get) (sym p) ⟩
+  get <$> (bff get s v)
+    ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
+  get <$> mapMV (flip lookupM (h↦h′ h)) s′
+    ≡⟨ lemma-get-mapMV (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) get ⟩
+  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′))
+    ≡⟨ cong sequenceV (lemma-union-not-used h g′ (get s′) (lemma-assoc-domain (get s′) v h ph)) ⟩
+  sequenceV (map (flip lookupM h) (get s′))
+    ≈⟨ sequence-cong (lemma-2 (get s′) v h ph) ⟩
+  sequenceV (map just v)
+    ≡⟨ lemma-just-sequence v ⟩
+  just v ∎)
     where open SetoidReasoning
           s′   = enumerate s
           g    = fromFunc (denumerate s)
-          h↦h′ = flip union g
-          h′↦r = flip map s′ ∘ flip lookupVec
+          g′   = delete-many (get s′) g
+          h↦h′ = flip union g′
+          h′↦r = flip mapMV s′ ∘ flip lookupM
diff --git a/FinMap.agda b/FinMap.agda
index 1fc2d16..c04c510 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -5,7 +5,7 @@ open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) renaming (setoid to MaybeEq)
 open import Data.Fin using (Fin ; zero ; suc)
 open import Data.Fin.Props using (_≟_)
-open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr) renaming (lookup to lookupVec ; map to mapV)
+open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; toList) renaming (lookup to lookupVec ; map to mapV)
 open import Data.Vec.Equality using ()
 open Data.Vec.Equality.Equality using (_∷-cong_)
 open import Data.Vec.Properties using (lookup∘tabulate)
@@ -37,17 +37,11 @@ fromAscList : {A : Set} {n : ℕ} → List (Fin n × A) → FinMapMaybe n A
 fromAscList []             = empty
 fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs)
 
-FinMap : ℕ → Set → Set
-FinMap n A = Vec A n
+fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A
+fromFunc = mapV just ∘ tabulate
 
-lookup : {A : Set} {n : ℕ} → Fin n → FinMap n A → A
-lookup = lookupVec
-
-fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMap n A
-fromFunc = tabulate
-
-union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMap n  A → FinMap n A
-union m1 m2 = fromFunc (λ f → maybe′ id (lookup f m2) (lookupM f m1))
+union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A
+union m1 m2 = tabulate (λ f → maybe′ just (lookupM f m2) (lookupM f m1))
 
 restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A
 restrict f is = fromAscList (zip is (map f is))
@@ -58,9 +52,6 @@ delete i m = m [ i ]≔ nothing
 delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A
 delete-many = flip (foldr (const _) delete)
 
-partialize : {A : Set} {n : ℕ} → FinMap n A → FinMapMaybe n A
-partialize = mapV just
-
 lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing  → Whatever
 lemma-just≢nothing refl ()
 
@@ -103,9 +94,9 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g →
 lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = refl
 lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc))
 
-lemma-partialize-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → partialize (fromFunc f) ≡ fromFunc (just ∘ f)
-lemma-partialize-fromFunc {zero}  f = refl
-lemma-partialize-fromFunc {suc _} f = cong (_∷_ (just (f zero))) (lemma-partialize-fromFunc (f ∘ suc))
+lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f)
+lemma-fromFunc-tabulate {zero}  f = refl
+lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc))
 
 lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f
 lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p with p refl
@@ -114,23 +105,24 @@ lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = refl
 lemma-lookupM-delete {i = suc i} {j = zero}  (x ∷ xs) p = refl
 lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc)
 
-lemma-union-restrict : {n : ℕ} {A : Set} → (f : Fin n → A) → (is : List (Fin n)) → union (restrict f is) (fromFunc f) ≡ fromFunc f
-lemma-union-restrict {n} f is = lemma-tabulate-∘ (lemma-inner is)
-    where lemma-inner : (is : List (Fin n)) → (j : Fin n) → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡ f j
-          lemma-inner []       j = begin
-            maybe′ id (lookup j (fromFunc f)) (lookupM j empty)
-              ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-empty j) ⟩
-            maybe′ id (lookup j (fromFunc f)) nothing
-              ≡⟨ refl ⟩
-            lookup j (fromFunc f)
-              ≡⟨ lookup∘tabulate f j ⟩
-            f j ∎
-          lemma-inner (i ∷ is)  j with j ≟ i
-          lemma-inner (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f)))
-                                                    (lemma-lookupM-insert j (f j) (restrict f is))
-          lemma-inner (i ∷ is)  j | no j≢i = begin
-            maybe′ id (lookup j (fromFunc f)) (lookupM j (insert i (f i) (restrict f is)))
-              ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (restrict f is) j≢i)) ⟩
-            maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is))
-              ≡⟨ lemma-inner is j ⟩
-            f j ∎
+lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (fromFunc f)) ≡ fromFunc f
+lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-fromFunc-tabulate f))
+    where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f (toList t))) ≡ just (f x)
+          lemma-inner [] x = begin
+            maybe′ just (lookupM x (fromFunc f)) (lookupM x empty)
+              ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩
+            lookupM x (fromFunc f)
+              ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩
+            lookupM x (tabulate (just ∘ f))
+              ≡⟨ lookup∘tabulate (just ∘ f) x ⟩
+            just (f x) ∎
+          lemma-inner (t ∷ ts) x with x ≟ t
+          lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts)))
+          lemma-inner (t ∷ ts) x | no ¬p = begin
+            maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList (t ∷ ts))))
+              ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩
+            maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList ts)))
+              ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩
+            maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f (toList ts)))
+              ≡⟨ lemma-inner ts x ⟩
+            just (f x) ∎
diff --git a/Generic.agda b/Generic.agda
index f0606ac..f543256 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -8,7 +8,7 @@ open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Product using (_×_ ; _,_)
 open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_)
 open import Data.Vec.Equality using () renaming (module Equality to VecEq)
-open import Function using (_∘_)
+open import Function using (_∘_ ; id)
 open import Level using () renaming (zero to ℓ₀)
 open import Relation.Binary using (Setoid ; module Setoid)
 open import Relation.Binary.Core using (_≡_ ; refl)
@@ -18,23 +18,13 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ;
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
 
-∷-injective : {A : Set} {n : ℕ} {x y : A} {xs ys : Vec A n} →
-              (x ∷V xs) ≡ (y ∷V ys) → x ≡ y × xs ≡ ys
-∷-injective refl = refl , refl
-
 just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y
 just-injective refl = refl
 
 length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
-length-replicate zero       = refl
+length-replicate zero    = refl
 length-replicate (suc n) = cong suc (length-replicate n)
 
-map-just-injective : {A : Set} {n : ℕ} {xs ys : Vec A n} →
-                     map Maybe.just xs ≡ map Maybe.just ys → xs ≡ ys
-map-just-injective {xs = []V}      {ys = []V}       p  = refl
-map-just-injective {xs = x ∷V xs′} {ys = y ∷V ys′}  p with ∷-injective p
-map-just-injective {xs = x ∷V xs′} {ys = .x ∷V ys′} p | refl , p′ = cong (_∷V_ x) (map-just-injective p′)
-
 mapMV : {A B : Set} {n : ℕ} → (A → Maybe B) → Vec A n → Maybe (Vec B n)
 mapMV f []V = just []V
 mapMV f (x ∷V xs) = (f x) >>= (λ y → (_∷V_ y) <$> (mapMV f xs))
@@ -57,6 +47,15 @@ maybeEq-to-≡ : {A : Set} {a b : Maybe A} → Setoid._≈_ (MaybeEq (PropEq A))
 maybeEq-to-≡ (just refl) = refl
 maybeEq-to-≡ nothing     = refl
 
+sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n)
+sequenceV = mapMV id
+
+sequence-map : {A B : Set} {n : ℕ} → (f : A → Maybe B) → sequenceV {n = n} ∘ map f ≗ mapMV f
+sequence-map f []V = refl
+sequence-map f (x ∷V xs) with f x
+sequence-map f (x ∷V xs) | just y = cong (_<$>_ (_∷V_ y)) (sequence-map f xs)
+sequence-map f (x ∷V xs) | nothing = refl
+
 subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) →
              f ∘ subst T p ≗ subst T (cong g p) ∘ f
 subst-cong T f refl _ = refl
diff --git a/Precond.agda b/Precond.agda
index 9bae83b..19329b5 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -3,36 +3,90 @@ open import Relation.Binary.Core using (Decidable ; _≡_)
 module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
 
 open import Data.Nat using (ℕ)
-open import Data.Fin using (Fin)
+open import Data.Fin using (Fin ; zero ; suc)
+open import Data.Fin.Props using (_≟_)
 open import Data.List using (List ; [] ; _∷_)
 import Level
 import Category.Monad
 import Category.Functor
-open import Data.Maybe using (nothing ; just)
+open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
-open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
+open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList ; tabulate)
+open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘)
+import Data.List.All
 open import Data.List.Any using (here ; there)
 open Data.List.Any.Membership-≡ using (_∉_)
 open import Data.Maybe using (just)
-open import Data.Product using (∃ ; _,_)
-open import Function using (flip ; _∘_)
+open import Data.Product using (∃ ; _,_ ; proj₂)
+open import Function using (flip ; _∘_ ; id)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
+open import Relation.Nullary using (yes ; no)
 
-open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty)
+open import Generic using (mapMV ; sequenceV ; sequence-map)
+open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete)
 import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
-import Bidir
+open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
 
 open BFF.VecBFF (decSetoid deq) using (get-type ; 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
+lemma-lookup-map-just (suc f) (x ∷ xs) = lemma-lookup-map-just f xs
+
+lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma)
+lemma-maybe-just a (just x) = refl
+lemma-maybe-just a nothing = refl
+
+lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Vec A n} → (toList is) in-domain-of h → ∃ λ v → union h (delete-many is (map just g)) ≡ map just v
+lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin
+  union h (map just g)
+    ≡⟨ lemma-tabulate-∘ (λ f → begin
+      maybe′ just (lookup f (map just g)) (lookup f h)
+        ≡⟨ cong (flip (maybe′ just) (lookup f h)) (lemma-lookup-map-just f g) ⟩
+      maybe′ just (just (lookup f g)) (lookup f h)
+        ≡⟨ lemma-maybe-just (lookup f g) (lookup f h) ⟩
+      just (maybe′ id (lookup f g) (lookup f h)) ∎) ⟩
+  tabulate (λ f → just (maybe′ id (lookup f g) (lookup f h)))
+    ≡⟨ tabulate-∘ just (λ f → maybe′ id (lookup f g) (lookup f h)) ⟩
+  map just (tabulate (λ f → maybe′ id (lookup f g) (lookup f h))) ∎)
+lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Data.List.All.∷ ps) = _ , (begin
+  union h (delete i (delete-many is (map just g)))
+    ≡⟨ lemma-tabulate-∘ inner ⟩
+  union h (delete-many is (map just g))
+    ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩
+  map just _ ∎)
+  where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (map just g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (map just g))) (lookup f h)
+        inner f with f ≟ i
+        inner .i | yes refl = begin
+          maybe′ just (lookupM i (delete i (delete-many is (map just g)))) (lookup i h)
+            ≡⟨ cong (maybe′ just _) px ⟩
+          just x
+            ≡⟨ cong (maybe′ just _) (sym px) ⟩
+          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 : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (s : Vec Carrier m) → (v : Vec Carrier (getlen m)) → ∃ (λ h → assoc (get (enumerate s)) v ≡ just h) → ∃ λ u → bff get s v ≡ just u
-assoc-enough get s v (h , p) = u , cong (_<$>_ (flip map s′ ∘ flip lookup) ∘ (_<$>_ (flip union g))) p
-    where s′ = enumerate s
-          g  = fromFunc (denumerate s)
-          u  = map (flip lookup (union h g)) s′
+assoc-enough get s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin
+  bff get 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′) ⟩
+  sequenceV (map (flip lookupM (union h g′)) s′)
+    ≡⟨ cong (sequenceV ∘ flip map s′ ∘ flip lookupM) pw ⟩
+  sequenceV (map (flip lookupM (map just w)) s′)
+    ≡⟨ cong sequenceV (map-cong (λ f → lemma-lookup-map-just f w) s′) ⟩
+  sequenceV (map (Maybe.just ∘ flip lookup w) s′)
+    ≡⟨ cong sequenceV (map-∘ just (flip lookup w) s′) ⟩
+  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
+        g  = fromFunc (denumerate s)
+        g′ = delete-many (get s′) g
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []