From 066861f9cdde4ded6c5442508bef1a27576c68d7 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 17 Dec 2013 08:22:12 +0100
Subject: 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.
---
 BFF.agda     | 11 +++++++----
 Bidir.agda   | 23 +++++++++++++++--------
 FinMap.agda  | 47 ++++++++++++++++++++++++-----------------------
 Precond.agda |  2 ++
 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 []
-- 
cgit v1.2.3


From 88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 17 Dec 2013 08:49:24 +0100
Subject: refactor to get rid of FinMap without Maybe entirely

The union was the only user of this type and now it uses only partial
mappings. So drop remaining uses of FinMap and make everything work with
FinMapMaybe instead.
---
 BFF.agda     |  2 +-
 Bidir.agda   | 12 ++++++------
 FinMap.agda  | 49 ++++++++++++++++++++-----------------------------
 Precond.agda |  2 +-
 4 files changed, 28 insertions(+), 37 deletions(-)

diff --git a/BFF.agda b/BFF.agda
index f7ddd30..896350a 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -35,7 +35,7 @@ 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
                     t′ = get s′
-                    g  = partialize (fromFunc (denumerate s))
+                    g  = fromFunc (denumerate s)
                     g′ = delete-many t′ g
                     h  = assoc t′ v
                     h′ = (flip union g′) <$> h
diff --git a/Bidir.agda b/Bidir.agda
index c74601a..1e65bab 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -113,20 +113,20 @@ 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)))) (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate 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) (partialize (fromFunc (denumerate s)))
+  (h′↦r ∘ just) (fromFunc (denumerate s))
     ≡⟨ refl ⟩
-  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 (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 h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s)))))
+    where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s))))
           h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec)
 
 
diff --git a/FinMap.agda b/FinMap.agda
index 8cde5a6..c125c47 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -33,17 +33,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
-
-lookup : {A : Set} {n : ℕ} → Fin n → FinMap n A → A
-lookup = lookupVec
-
-fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMap n A
-fromFunc = tabulate
+fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A
+fromFunc = mapV just ∘ tabulate
 
 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))
+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))
@@ -54,9 +48,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 ()
 
@@ -99,9 +90,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
@@ -110,24 +101,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-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-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 (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))
+            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) (partialize (fromFunc f))))) (lemma-lookupM-insert x (f x) (restrict f (toList ts)))
+          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) (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)))
+            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/Precond.agda b/Precond.agda
index 16e452b..40ffd79 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -20,7 +20,7 @@ open import Function using (flip ; _∘_)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
-open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty)
+open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty)
 import CheckInsert
 open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
-- 
cgit v1.2.3


From 2d7db0d8c48c41ecef78ef9f18253632a80f4710 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Fri, 24 Jan 2014 13:30:39 +0100
Subject: prove theorem-2 in the presence of delete

The biggest piece of this puzzle was establishing
  get <$> mapMV f v == mapMV f (get v)
provided that the result of mapMV is just something.
lemma-union-not-used lost a "map just", but could be retained in
structure.
---
 Bidir.agda   | 110 +++++++++++++++++++++++++++++++++++++++++------------------
 Generic.agda |  13 +++++--
 2 files changed, 87 insertions(+), 36 deletions(-)

diff --git a/Bidir.agda b/Bidir.agda
index 1e65bab..eef8bff 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 ; mapMV ; mapMV-cong ; mapMV-purity)
+open import Generic using (just-injective ; map-just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
 open import FinMap
 import CheckInsert
 open CheckInsert Carrier deq
@@ -130,46 +130,88 @@ theorem-1 get s = begin
           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-<$>-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' : 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 : {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')
 
+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-mapMV-just : {A B : Set} {n : ℕ} {f : A → Maybe B} {s : Vec A n} {v : Vec B n} → mapMV f s ≡ just v → All (λ x → ∃ λ y → f x ≡ just y) (toList s)
+lemma-mapMV-just         {s = []}     p = Data.List.All.[]
+lemma-mapMV-just {f = f} {s = x ∷ xs} p with f x | inspect f x
+lemma-mapMV-just         {s = x ∷ xs} () | nothing | _
+lemma-mapMV-just {f = f} {s = x ∷ xs} p  | just y  | [ py ] with mapMV f xs | inspect (mapMV f) xs
+lemma-mapMV-just         {s = x ∷ xs} () | just y  | [ py ] | nothing | _
+lemma-mapMV-just         {s = x ∷ xs} p  | just y  | [ py ] | just ys | [ pys ] = (y , py) Data.List.All.∷ (lemma-mapMV-just pys)
+
+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) ∎
+
 theorem-2 : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (v : Vec Carrier (getlen m)) → (s u : Vec Carrier m) → bff get s v ≡ just u → 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
-  get u
-    ≡⟨ just-injective (begin
-      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
-       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 = just-injective (begin
+  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′))
+    ≡⟨ cong sequenceV (lemma-2 (get s′) v h ph) ⟩
+  sequenceV (map just v)
+    ≡⟨ lemma-just-sequence v ⟩
+  just v ∎)
     where 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/Generic.agda b/Generic.agda
index 11b9594..2ef374c 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -7,7 +7,7 @@ open import Data.Maybe using (Maybe ; just ; nothing)
 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 Function using (_∘_)
+open import Function using (_∘_ ; id)
 import Level
 open import Relation.Binary.Core using (_≡_ ; refl)
 open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans)
@@ -23,7 +23,7 @@ just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x
 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} →
@@ -46,6 +46,15 @@ mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → map
 mapMV-purity f []V = refl
 mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = 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
-- 
cgit v1.2.3


From d2521627834713a651be0ac22aab0a1cd78df920 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 27 Jan 2014 09:02:45 +0100
Subject: prove assoc-enough in the presence of delete

The old definition of bff had a single failure mode - assoc - and its
proof was a single cong. Now we need to show that the other failure mode
- mapM (flip lookupM ...) - is eliminated by the success of the former
resulting in a larger proof.
---
 Precond.agda | 84 ++++++++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 71 insertions(+), 13 deletions(-)

diff --git a/Precond.agda b/Precond.agda
index 40ffd79..90027b4 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -3,38 +3,96 @@ 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₁ ; proj₂)
+open import Function using (flip ; _∘_ ; id)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
+open import Relation.Nullary using (yes ; no)
 
-open import FinMap using (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 Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
-import Bidir
+open import Bidir Carrier deq using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
 
 open BFF.VecBFF Carrier 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
+
+fromMaybe : {A : Set} → A → Maybe A → A
+fromMaybe a ma = maybe′ id a ma
+
+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 (fromMaybe (lookup f g) (lookup f h)) ∎) ⟩
+  tabulate (λ f → just (fromMaybe (lookup f g) (lookup f h)))
+    ≡⟨ tabulate-∘ just (λ f → fromMaybe (lookup f g) (lookup f h)) ⟩
+  map just (tabulate (λ f → fromMaybe (lookup f g) (lookup f h))) ∎)
+lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (p Data.List.All.∷ ps) = _ , (begin
+  union h (delete i (delete-many is (map just g)))
+    ≡⟨ lemma-tabulate-∘ (λ f → (begin
+      maybe′ just (lookupM f (delete i (delete-many is (map just g)))) (lookup f h)
+        ≡⟨ inner f ⟩
+      maybe′ just (lookupM f (delete-many is (map just g))) (lookup f h) ∎)) ⟩
+  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 _) (proj₂ p) ⟩
+          just (proj₁ p)
+            ≡⟨ cong (maybe′ just _) (sym (proj₂ p)) ⟩
+          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 []
-- 
cgit v1.2.3


From 71025b5f1d0a11b0cf373192210b293a77d45c04 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 27 Jan 2014 09:31:56 +0100
Subject: cleanup unused functions and useless steps

---
 Bidir.agda   | 10 +---------
 Generic.agda | 10 ----------
 Precond.agda | 26 ++++++++++----------------
 3 files changed, 11 insertions(+), 35 deletions(-)

diff --git a/Bidir.agda b/Bidir.agda
index eef8bff..05ee066 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 ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
+open import Generic using (just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
 open import FinMap
 import CheckInsert
 open CheckInsert Carrier deq
@@ -150,14 +150,6 @@ lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma
 lemma->>=-just (just a) p = a , refl
 lemma->>=-just nothing  ()
 
-lemma-mapMV-just : {A B : Set} {n : ℕ} {f : A → Maybe B} {s : Vec A n} {v : Vec B n} → mapMV f s ≡ just v → All (λ x → ∃ λ y → f x ≡ just y) (toList s)
-lemma-mapMV-just         {s = []}     p = Data.List.All.[]
-lemma-mapMV-just {f = f} {s = x ∷ xs} p with f x | inspect f x
-lemma-mapMV-just         {s = x ∷ xs} () | nothing | _
-lemma-mapMV-just {f = f} {s = x ∷ xs} p  | just y  | [ py ] with mapMV f xs | inspect (mapMV f) xs
-lemma-mapMV-just         {s = x ∷ xs} () | just y  | [ py ] | nothing | _
-lemma-mapMV-just         {s = x ∷ xs} p  | just y  | [ py ] | just ys | [ pys ] = (y , py) Data.List.All.∷ (lemma-mapMV-just pys)
-
 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
diff --git a/Generic.agda b/Generic.agda
index 2ef374c..4e55c21 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -15,10 +15,6 @@ 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
 
@@ -26,12 +22,6 @@ length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) 
 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))
diff --git a/Precond.agda b/Precond.agda
index 90027b4..6aba291 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -18,7 +18,7 @@ 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 (∃ ; _,_ ; proj₁ ; proj₂)
+open import Data.Product using (∃ ; _,_ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
@@ -37,9 +37,6 @@ lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup
 lemma-lookup-map-just zero    (x ∷ xs) = refl
 lemma-lookup-map-just (suc f) (x ∷ xs) = lemma-lookup-map-just f xs
 
-fromMaybe : {A : Set} → A → Maybe A → A
-fromMaybe a ma = maybe′ id a ma
-
 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
@@ -52,16 +49,13 @@ lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin
         ≡⟨ 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 (fromMaybe (lookup f g) (lookup f h)) ∎) ⟩
-  tabulate (λ f → just (fromMaybe (lookup f g) (lookup f h)))
-    ≡⟨ tabulate-∘ just (λ f → fromMaybe (lookup f g) (lookup f h)) ⟩
-  map just (tabulate (λ f → fromMaybe (lookup f g) (lookup f h))) ∎)
-lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (p Data.List.All.∷ ps) = _ , (begin
+      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-∘ (λ f → (begin
-      maybe′ just (lookupM f (delete i (delete-many is (map just g)))) (lookup f h)
-        ≡⟨ inner f ⟩
-      maybe′ just (lookupM f (delete-many is (map just g))) (lookup f h) ∎)) ⟩
+    ≡⟨ lemma-tabulate-∘ inner ⟩
   union h (delete-many is (map just g))
     ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩
   map just _ ∎)
@@ -69,9 +63,9 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (p Data.List
         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 _) (proj₂ p) ⟩
-          just (proj₁ p)
-            ≡⟨ cong (maybe′ just _) (sym (proj₂ p)) ⟩
+            ≡⟨ 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)
 
-- 
cgit v1.2.3