update bff implementation to use delete

In the presence of shape-changing updates, bff needs to shrink one of
the mappings before unifying them. As long the shape does not change,
the union becomes a disjoint union. With this insight we can adapt the
proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately
theorem-2 requires more work and assoc-enough becomes non-trivial due to
the introduction of mapMV.

4 files changed, 48 insertions, 35 deletions

diff --git a/BFF.agda b/BFF.agda
index 0cdb231..f7ddd30 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -14,6 +14,7 @@ open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary.Core using (Decidable ; _≡_)
 
 open import FinMap
+open import Generic using (mapMV)
 import CheckInsert
 import FreeTheorems
 
@@ -33,7 +34,9 @@ module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) 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
-                    g  = fromFunc (denumerate s)
-                    h  = assoc (get s′) v
-                    h′ = (flip union g) <$> h
-                in (flip mapV s′ ∘ flip lookupV) <$> h′
+                    t′ = get s′
+                    g  = partialize (fromFunc (denumerate s))
+                    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 9cc0ca6..c74601a 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -22,7 +22,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨
 
 import FreeTheorems
 open FreeTheorems.VecVec using (get-type ; free-theorem)
-open import Generic using (just-injective ; map-just-injective)
+open import Generic using (just-injective ; map-just-injective ; mapMV ; mapMV-cong ; mapMV-purity)
 open import FinMap
 import CheckInsert
 open CheckInsert Carrier deq
@@ -113,22 +113,28 @@ 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) (fromFunc (denumerate s))
+  (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s)))))
+    ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩
+  (h′↦r ∘ just) (partialize (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 (partialize (fromFunc (denumerate s)))) (enumerate s)
+    ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-partialize-fromFunc (denumerate s)) ⟩
+  mapMV (flip lookupVec (fromFunc (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 h↦h′ = _<$>_ (flip union (fromFunc (denumerate s)))
-          h′↦r = _<$>_ (flip map (enumerate s) ∘ flip lookupVec)
+    where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (partialize (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-union-not-used h h' []        p = refl
 lemma-union-not-used h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong₂ _∷_ (begin
@@ -166,3 +172,4 @@ theorem-2 get v s u p | h , ph = begin
           g    = fromFunc (denumerate s)
           h↦h′ = flip union g
           h′↦r = flip map s′ ∘ flip lookupVec
+-}
diff --git a/FinMap.agda b/FinMap.agda
index 46dbd1c..8cde5a6 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -4,7 +4,7 @@ open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
 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.Properties using (lookup∘tabulate)
 open import Data.List using (List ; [] ; _∷_ ; map ; zip)
 open import Data.Product using (_×_ ; _,_)
@@ -42,8 +42,8 @@ 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 = fromFunc (λ 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))
@@ -110,23 +110,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 (partialize (fromFunc f))) ≡ partialize (fromFunc f)
+lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-partialize-fromFunc f))
+    where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (partialize (fromFunc f)))) (lookupM x (restrict f (toList t))) ≡ just (f x)
+          lemma-inner [] x = begin
+            maybe′ just (lookupM x (partialize (fromFunc f))) (lookupM x empty)
+              ≡⟨ cong (maybe′ just (lookupM x (partialize (fromFunc f)))) (lemma-lookupM-empty x) ⟩
+            lookupM x (partialize (fromFunc f))
+              ≡⟨ cong (lookupM x) (lemma-partialize-fromFunc f) ⟩
+            lookupM x (fromFunc (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) (partialize (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) (partialize (fromFunc f)))) (lookupM x (restrict f (toList (t ∷ ts))))
+              ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f))))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩
+            maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts)))
+              ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (partialize (fromFunc f))) ¬p) ⟩
+            maybe′ just (lookupM x (delete-many ts (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts)))
+              ≡⟨ lemma-inner ts x ⟩
+            just (f x) ∎
diff --git a/Precond.agda b/Precond.agda
index e4699dc..16e452b 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -28,11 +28,13 @@ import Bidir
 
 open BFF.VecBFF Carrier deq using (get-type ; assoc ; enumerate ; denumerate ; bff)
 
+{-
 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′
+-}
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []