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

1 files changed, 88 insertions, 39 deletions

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