use "module _" to simplify types involving Get records

2 files changed, 98 insertions, 83 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 9b60461..b0469fd 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -214,21 +214,25 @@ lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin
         open Shaped ShapeT
         wp = lemma-<$>-just (sequenceV (content c)) p
 
-lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.I G} {v : Get.SourceContainer G (Maybe A) (Get.gl₁ G i)} {r : Get.SourceContainer G A (Get.gl₁ G i)} → Shaped.sequence (Get.SourceShapeT G) v ≡ just r → Get.get G <$> Shaped.sequence (Get.SourceShapeT G) v ≡ Shaped.sequence (Get.ViewShapeT G) (Get.get G v)
-lemma-get-sequence G {v = v} {r = r} p = begin
-  get <$> Shaped.sequence SourceShapeT v
-    ≡⟨ cong (_<$>_ get ∘ Shaped.sequence SourceShapeT) (lemma-sequence-successful SourceShapeT v p) ⟩
-  get <$> Shaped.sequence SourceShapeT (fmapS just r)
-    ≡⟨ cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩
-  get <$> just r
-    ≡⟨ sym (lemma-just-sequence ViewShapeT (get r)) ⟩
-  Shaped.sequence ViewShapeT (fmapV just (get r))
-    ≡⟨ cong (Shaped.sequence ViewShapeT) (sym (free-theorem just r)) ⟩
-  Shaped.sequence ViewShapeT (get (fmapS just r))
-    ≡⟨ cong (Shaped.sequence ViewShapeT ∘ get) (sym (lemma-sequence-successful SourceShapeT v p)) ⟩
-  Shaped.sequence ViewShapeT (get v) ∎
-  where open ≡-Reasoning
-        open Get G
+module _ (G : Get) where
+  open ≡-Reasoning
+  open Get G
+  open Shaped SourceShapeT using () renaming (sequence to sequenceSource)
+  open Shaped ViewShapeT using () renaming (sequence to sequenceView)
+
+  lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → get <$> sequenceSource v ≡ sequenceView (get v)
+  lemma-get-sequence {v = v} {r = r} p = begin
+    get <$> sequenceSource v
+      ≡⟨ cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩
+    get <$> sequenceSource (fmapS just r)
+      ≡⟨ cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩
+    get <$> just r
+      ≡⟨ sym (lemma-just-sequence ViewShapeT (get r)) ⟩
+    sequenceView (fmapV just (get r))
+      ≡⟨ cong sequenceView (sym (free-theorem just r)) ⟩
+    sequenceView (get (fmapS just r))
+      ≡⟨ cong (sequenceView ∘ get) (sym (lemma-sequence-successful SourceShapeT v p)) ⟩
+    sequenceView (get v) ∎
 
 sequenceV-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂
 sequenceV-cong {S}                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _))
@@ -253,46 +257,51 @@ sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | ju
         open Shaped ShapeT
 sequence-cong ShapeT α (shape≈ , content≈) | .nothing  | .nothing  | nothing = nothing
 
-theorem-2 : (G : Get) → {i : Get.I G} → (j : Get.I G) → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → (v : Get.ViewContainer G Carrier (Get.gl₂ G j)) → (u : Get.SourceContainer G (Maybe Carrier) (Get.gl₁ G j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ Get.fmapV G just v
-theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G i)))) (fromFunc (denumerate (Get.SourceShapeT G) s))) (Shaped.arity (Get.SourceShapeT G) (Get.gl₁ G j)))) <$> (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G j)))) (Shaped.content (Get.ViewShapeT G) v))) p)
-theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G j)))) (Shaped.content (Get.ViewShapeT G) v)) ph′)
-theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = refl , (begin
-  content (get u)
-    ≡⟨ cong content (just-injective (trans (cong (_<$>_ get) (sym p))
-                                           (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩
-  content (get (h′↦r (h↦h′ h)))
-    ≡⟨ refl ⟩
-  content (get (fmapS (flip lookupM (h↦h′ h)) t))
-    ≡⟨ cong content (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
-  content (fmapV (flip lookupM (h↦h′ h)) (get t))
-    ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
-  map (flip lookupM (h↦h′ h)) (content (get t))
-    ≡⟨ lemma-union-not-used h (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))) (content (get t)) (lemma-assoc-domain (content (get t)) (content v) ph) ⟩
-  map (flip lookupM h) (content (get t))
-    ≈⟨ lemma-2 (content (get t)) (content v) h ph ⟩
-  map just (content v)
-    ≡⟨ sym (Shaped.fmap-content ViewShapeT just v) ⟩
-  content (fmapV just v) ∎)
-    where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
-          open Get G
-          open Shaped ViewShapeT using (content)
-          s′   = enumerate SourceShapeT (gl₁ i)
-          g    = fromFunc (denumerate SourceShapeT s)
-          g′   = delete-many (Shaped.content ViewShapeT (get s′)) g
-          t    = enumerate SourceShapeT (gl₁ j)
-          h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j)))
-          h′↦r = (λ f → fmapS f t) ∘ flip lookupM
+module _ (G : Get) where
+  open Get G
+  open Shaped SourceShapeT using () renaming (arity to arityS)
+  open Shaped ViewShapeT using () renaming (content to contentV)
+
+  theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) ViewShapeT (MaybeSetoid A.setoid) at _ ∋ get u ≈ Get.fmapV G just v
+  theorem-2 {i} j s v u p with lemma-<$>-just ((flip union (reshape (delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))) (arityS (gl₁ j)))) <$> assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) p
+  theorem-2 {i} j s v u p | h′ , ph′ with lemma-<$>-just (assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) ph′
+  theorem-2 {i} j s v u p | h′ , ph′ | h , ph = refl , (begin
+    contentV (get u)
+      ≡⟨ cong contentV (just-injective (trans (cong (_<$>_ get) (sym p))
+                                              (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩
+    contentV (get (h′↦r (h↦h′ h)))
+      ≡⟨ refl ⟩
+    contentV (get (fmapS (flip lookupM (h↦h′ h)) t))
+      ≡⟨ cong contentV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
+    contentV (fmapV (flip lookupM (h↦h′ h)) (get t))
+      ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
+    map (flip lookupM (h↦h′ h)) (contentV (get t))
+      ≡⟨ lemma-union-not-used h (reshape g′ (arityS (gl₁ j))) (contentV (get t)) (lemma-assoc-domain (contentV (get t)) (contentV v) ph) ⟩
+    map (flip lookupM h) (contentV (get t))
+      ≈⟨ lemma-2 (contentV (get t)) (contentV v) h ph ⟩
+    map just (contentV v)
+      ≡⟨ sym (Shaped.fmap-content ViewShapeT just v) ⟩
+    contentV (fmapV just v) ∎)
+      where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
+            s′   = enumerate SourceShapeT (gl₁ i)
+            g    = fromFunc (denumerate SourceShapeT s)
+            g′   = delete-many (contentV (get s′)) g
+            t    = enumerate SourceShapeT (gl₁ j)
+            h↦h′ = flip union (reshape g′ (arityS (gl₁ j)))
+            h′↦r = (λ f → fmapS f t) ∘ flip lookupM
+
+module _ (G : Get) where
+  open Get G
 
-theorem-2′ : (G : Get) → {i : Get.I G} → (j : Get.I G) → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → (v : Get.ViewContainer G Carrier (Get.gl₂ G j)) → (u : Get.SourceContainer G Carrier (Get.gl₁ G j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) 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 SourceShapeT u)) ⟩
-  get <$> Shaped.sequence SourceShapeT (fmapS just u)
-    ≡⟨ lemma-get-sequence G (lemma-just-sequence SourceShapeT u) ⟩
-  Shaped.sequence ViewShapeT (get (fmapS just u))
-    ≈⟨ sequence-cong ViewShapeT A.setoid (theorem-2 G j s v (fmapS just u) p) ⟩
-  Shaped.sequence ViewShapeT (fmapV just v)
-    ≡⟨ lemma-just-sequence ViewShapeT v ⟩
-  just v ∎)
-  where open Get G
-        open EqR (MaybeSetoid (ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _))
+  theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _ ∋ get u ≈ v
+  theorem-2′ j s v u p = drop-just (begin
+    get <$> just u
+      ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence SourceShapeT u)) ⟩
+    get <$> Shaped.sequence SourceShapeT (fmapS just u)
+      ≡⟨ lemma-get-sequence G (lemma-just-sequence SourceShapeT u) ⟩
+    Shaped.sequence ViewShapeT (get (fmapS just u))
+      ≈⟨ sequence-cong ViewShapeT A.setoid (theorem-2 G j s v (fmapS just u) p) ⟩
+    Shaped.sequence ViewShapeT (fmapV just v)
+      ≡⟨ lemma-just-sequence ViewShapeT v ⟩
+    just v ∎)
+    where open EqR (MaybeSetoid (ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _))
diff --git a/Precond.agda b/Precond.agda
index e39397c..70f294d 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -25,7 +25,7 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ;
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
-open import Structures using (IsFunctor ; Shaped)
+open import Structures using (IsFunctor ; module Shaped ; Shaped)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
 import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
@@ -63,32 +63,38 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
         inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
 
-assoc-enough : (G : Get) → {i : Get.I G} → (j : Get.I G) → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → (v : Get.ViewContainer G Carrier (Get.gl₂ G j)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G j)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u
-assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p
-  where open Get G
-        g′ = delete-many (Shaped.content ViewShapeT (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))
-        t  = enumerate SourceShapeT (gl₁ j)
+module _ (G : Get) where
+  open Get G
+  open Shaped ViewShapeT using () renaming (content to contentV)
 
-assoc-enough′ : (G : Get) → {i : Get.I G} → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → (v : Get.ViewContainer G Carrier (Get.gl₂ G i)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G i)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G i s v ≡ just (Get.fmapS G just u)
-assoc-enough′ G {i} s v (h , p) = _ , (begin
-  bff G i s v
-    ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
-  just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))) t)
-    ≡⟨ cong just (begin _
-        ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
-      fmapS (flip lookupM (union h g′)) t
-        ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩
-      fmapS (flip lookupM (fromFunc (proj₁ wp))) t
-        ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
-      fmapS (Maybe.just ∘ proj₁ wp) t
-        ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just (proj₁ wp) t ⟩
-      fmapS Maybe.just (fmapS (proj₁ wp) t) ∎) ⟩ _ ∎)
-  where open Get G
-        s′ = enumerate SourceShapeT (gl₁ i)
-        g  = fromFunc (denumerate SourceShapeT s)
-        g′ = delete-many (Shaped.content ViewShapeT (get s′)) g
-        t  = enumerate SourceShapeT (gl₁ i)
-        wp = lemma-union-delete-fromFunc (lemma-assoc-domain (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) p)
+  assoc-enough : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → ∃ (λ h → assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u
+  assoc-enough {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p
+    where g′ = delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))
+          t  = enumerate SourceShapeT (gl₁ j)
+
+module _ (G : Get) where
+  open Get G
+  open Shaped ViewShapeT using () renaming (content to contentV)
+
+  assoc-enough′ : {i : I} → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ i)) → ∃ (λ h → assoc (contentV (get (enumerate SourceShapeT (gl₁ i)))) (contentV v) ≡ just h) → ∃ λ u → bff G i s v ≡ just (fmapS just u)
+  assoc-enough′ {i} s v (h , p) = _ , (begin
+    bff G i s v
+      ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
+    just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))) t)
+      ≡⟨ cong just (begin _
+          ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
+        fmapS (flip lookupM (union h g′)) t
+          ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩
+        fmapS (flip lookupM (fromFunc (proj₁ wp))) t
+          ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
+        fmapS (Maybe.just ∘ proj₁ wp) t
+          ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just (proj₁ wp) t ⟩
+        fmapS Maybe.just (fmapS (proj₁ wp) t) ∎) ⟩ _ ∎)
+    where s′ = enumerate SourceShapeT (gl₁ i)
+          g  = fromFunc (denumerate SourceShapeT s)
+          g′ = delete-many (contentV (get s′)) g
+          t  = enumerate SourceShapeT (gl₁ i)
+          wp = lemma-union-delete-fromFunc (lemma-assoc-domain (contentV (get t)) (contentV v) p)
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []