Merge branch feature-omit-sequence into master

Beyond allowing default values during shape updates, this branch simplifies
working with shapes other than Vec.

1 files changed, 40 insertions, 31 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 4d6524e..c9227e9 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -26,7 +26,7 @@ import Relation.Binary.EqReasoning as EqR
 
 import GetTypes
 open GetTypes.PartialVecVec using (Get ; module Get)
-open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid)
+open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective)
 open import FinMap
 import CheckInsert
 open CheckInsert A
@@ -123,7 +123,7 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
   as ∎)
   where open ≡-Reasoning
 
-theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just s
+theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (map just s)
 theorem-1 G {i} s = begin
   bff G i s (get s)
     ≡⟨ cong (bff G i s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
@@ -141,17 +141,17 @@ theorem-1 G {i} s = begin
     ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩
   (h′↦r ∘ just) (fromFunc (denumerate s))
     ≡⟨ refl ⟩
-  mapMV (flip lookupM (fromFunc (denumerate s))) (enumerate s)
-    ≡⟨ mapMV-cong (lemma-lookupM-fromFunc (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 ∎
+  just (map (flip lookupM (fromFunc (denumerate s))) (enumerate s))
+    ≡⟨ cong just (map-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s)) ⟩
+  just (map (Maybe.just ∘ denumerate s) (enumerate s))
+    ≡⟨ cong just (map-∘ just (denumerate s) (enumerate s)) ⟩
+  just (map just (map (denumerate s) (enumerate s)))
+    ≡⟨ cong (Maybe.just ∘ map just) (lemma-map-denumerate-enumerate s) ⟩
+  just (map just s) ∎
     where open ≡-Reasoning
           open Get G
           h↦h′ = _<$>_ (flip union (reshape (delete-many (get (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G i)))
-          h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupM)
+          h′↦r = _<$>_ (flip map (enumerate s) ∘ flip lookupM)
 
 
 lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
@@ -211,32 +211,41 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong
 sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 sequence-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
-theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
-theorem-2 G j s v u p with (lemma->>=-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p)
+theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v
+theorem-2 G j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p)
 theorem-2 G j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) ph′)
-theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin
-  get <$> (just u)
-    ≡⟨ cong (_<$>_ get) (sym p) ⟩
-  get <$> (bff G j s v)
-    ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
-  get <$> h′↦r (h↦h′ h)
+theorem-2 G j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩
+  get u
+    ≡⟨ just-injective (trans (cong (_<$>_ get) (sym p))
+                             (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph)) ⟩
+  get (h′↦r (h↦h′ h))
     ≡⟨ refl ⟩
-  get <$> sequenceV (map (flip lookupM (h↦h′ h)) t)
-    ≡⟨ lemma-get-sequenceV G (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) ⟩
-  sequenceV (get (map (flip lookupM (h↦h′ h)) t))
-    ≡⟨ cong sequenceV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
-  sequenceV (map (flip lookupM (h↦h′ h)) (get t))
-    ≡⟨ cong sequenceV (lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph)) ⟩
-  sequenceV (map (flip lookupM h) (get t))
-    ≈⟨ sequence-cong (lemma-2 (get t) v h ph) ⟩
-  sequenceV (map just v)
-    ≡⟨ lemma-just-sequence v ⟩
-  just v ∎)
-    where open EqR (MaybeSetoid (VecISetoid A.setoid at _))
+  get (map (flip lookupM (h↦h′ h)) t)
+    ≡⟨ free-theorem (flip lookupM (h↦h′ h)) t ⟩
+  map (flip lookupM (h↦h′ h)) (get t)
+    ≡⟨ lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph) ⟩
+  map (flip lookupM h) (get t)
+    ≈⟨ lemma-2 (get t) v h ph ⟩
+  map just v ∎
+    where open SetoidReasoning
           open Get G
           s′   = enumerate s
           g    = fromFunc (denumerate s)
           g′   = delete-many (get s′) g
           t    = enumeratel (Get.|gl₁| G j)
           h↦h′ = flip union (reshape g′ (Get.|gl₁| G j))
-          h′↦r = flip mapMV t ∘ flip lookupM
+          h′↦r = flip map t ∘ flip lookupM
+
+theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (map just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
+theorem-2′ G j s v u p = drop-just (begin
+  get <$> just u
+    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩
+  get <$> sequenceV (map just u)
+    ≡⟨ lemma-get-sequenceV G (lemma-just-sequence u) ⟩
+  sequenceV (get (map just u))
+    ≈⟨ sequence-cong (theorem-2 G j s v (map just u) p) ⟩
+  sequenceV (map just v)
+    ≡⟨ lemma-just-sequence v ⟩
+  just v ∎)
+  where open EqR (MaybeSetoid (VecISetoid A.setoid at _))
+        open Get G