diff options
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 119 |
1 files changed, 59 insertions, 60 deletions
@@ -18,9 +18,8 @@ open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) -open import Relation.Binary.Core using (refl ; _≡_) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) -open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; inspect ; [_] ; module ≡-Reasoning) open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid) import Relation.Binary.EqReasoning as EqR @@ -38,10 +37,10 @@ open Setoid using () renaming (_≈_ to _∋_≈_) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f is) -lemma-1 f [] = refl +lemma-1 f [] = P.refl lemma-1 f (i ∷ is′) = begin (assoc is′ (map f is′) >>= checkInsert i (f i)) - ≡⟨ cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩ + ≡⟨ P.cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩ checkInsert i (f i) (restrict f is′) ≡⟨ lemma-checkInsert-restrict f i is′ ⟩ just (restrict f (i ∷ is′)) ∎ @@ -49,15 +48,15 @@ lemma-1 f (i ∷ is′) = begin lemma-lookupM-checkInserted : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert i x h ≡ just h' → MaybeSetoid A.setoid ∋ lookupM i h' ≈ just x lemma-lookupM-checkInserted i x h p with checkInsert i x h | insertionresult i x h -lemma-lookupM-checkInserted i x h refl | ._ | same x' x≈x' pl = begin +lemma-lookupM-checkInserted i x h P.refl | ._ | same x' x≈x' pl = begin lookupM i h ≡⟨ pl ⟩ just x' ≈⟨ MaybeEq.just (Setoid.sym A.setoid x≈x') ⟩ just x ∎ where open EqR (MaybeSetoid A.setoid) -lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lookup∘update i h (just x)) -lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _ +lemma-lookupM-checkInserted i x h P.refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lookup∘update i h (just x)) +lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _ _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe m A) → Set _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is) @@ -67,8 +66,8 @@ lemma-assoc-domain [] [] ph = Data.List.All.[] lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs' lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ] lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h' -lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph') -lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_ +lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph') +lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_ (x' , lookup∘update i' h' (just x')) (Data.List.All.map (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡) @@ -76,9 +75,9 @@ lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ c lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _ lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js -lemma-map-lookupM-assoc i x h ph [] pj = refl -lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = cong₂ _∷_ - (trans (lemma-lookupM-checkInsert j i h pl x ph) (sym pl)) +lemma-map-lookupM-assoc i x h ph [] pj = P.refl +lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = P.cong₂ _∷_ + (P.trans (lemma-lookupM-checkInsert j i h pl x ph) (P.sym pl)) (lemma-map-lookupM-assoc i x h ph js pj) lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) at _ ∋ map (flip lookupM h) is ≈ map just v @@ -89,7 +88,7 @@ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin lookupM i h ∷ map (flip lookupM h) is ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩ just x ∷ map (flip lookupM h) is - ≡⟨ cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩ + ≡⟨ P.cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩ just x ∷ map (flip lookupM h') is ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩ just x ∷ map just xs ∎ @@ -100,7 +99,7 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin fmap (denumerate ShapeT c) (fill s (allFin (arity s))) ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩ fill s (map (flip lookupVec (content c)) (allFin (arity s))) - ≡⟨ cong (fill s) (map-lookup-allFin (content c)) ⟩ + ≡⟨ P.cong (fill s) (map-lookup-allFin (content c)) ⟩ fill s (content c) ≡⟨ content-fill c ⟩ c ∎ @@ -111,29 +110,29 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin theorem-1 : (G : Get) → {i : Get.I G} → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s) theorem-1 G {i} s = begin bff G i s (get s) - ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩ + ≡⟨ P.cong (bff G i s ∘ get) (P.sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩ bff G i s (get (fmapS f t)) - ≡⟨ cong (bff G i s) (free-theorem f t) ⟩ + ≡⟨ P.cong (bff G i s) (free-theorem f t) ⟩ bff G i s (fmapV f (get t)) - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT (fmapV f (get t))))) - ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩ + ≡⟨ P.cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩ h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (map f (Shaped.content ViewShapeT (get t))))) - ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩ + ≡⟨ P.cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩ (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (Shaped.content ViewShapeT (get t))) - ≡⟨ cong just (begin + ≡⟨ P.cong just (begin h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) (reshape g′ (Shaped.arity SourceShapeT (gl₁ i)))) - ≡⟨ cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩ + ≡⟨ P.cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩ h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) g′) - ≡⟨ cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩ + ≡⟨ P.cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩ h′↦r (fromFunc f) - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ fmapS (flip lookupM (fromFunc f)) t ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc f) t ⟩ fmapS (Maybe.just ∘ f) t ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just f t ⟩ fmapS just (fmapS f t) - ≡⟨ cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩ + ≡⟨ P.cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩ fmapS just s ∎) ⟩ _ ∎ where open ≡-Reasoning open Get G @@ -145,7 +144,7 @@ theorem-1 G {i} s = begin 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 (just x) f<$>ma≡just-b = x , P.refl lemma-<$>-just nothing () lemma-union-not-used : {n : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → (i : Fin n) → ∃ (λ x → lookupM i h ≡ just x) → lookupM i (union h h′) ≡ lookupM i h @@ -153,60 +152,60 @@ lemma-union-not-used h h′ i (x , px) = begin 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 ⟩ + ≡⟨ P.cong (maybe′ just (lookupM i h′)) px ⟩ maybe′ just (lookupM i h′) (just x) - ≡⟨ sym px ⟩ + ≡⟨ P.sym px ⟩ lookupM i h ∎ where open ≡-Reasoning 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 (just a) p = a , P.refl lemma->>=-just nothing () lemma-just-sequenceV : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v -lemma-just-sequenceV [] = refl -lemma-just-sequenceV (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs) +lemma-just-sequenceV [] = P.refl +lemma-just-sequenceV (x ∷ xs) = P.cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs) lemma-just-sequence : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C A s) → Shaped.sequence ShapeT (Shaped.fmap ShapeT just c) ≡ just c lemma-just-sequence ShapeT {s = s} c = begin fill s <$> sequenceV (content (fmap just c)) - ≡⟨ cong (_<$>_ (fill s) ∘ sequenceV) (fmap-content just c) ⟩ + ≡⟨ P.cong (_<$>_ (fill s) ∘ sequenceV) (fmap-content just c) ⟩ fill s <$> sequenceV (map just (content c)) - ≡⟨ cong (_<$>_ (fill s)) (lemma-just-sequenceV (content c)) ⟩ + ≡⟨ P.cong (_<$>_ (fill s)) (lemma-just-sequenceV (content c)) ⟩ fill s <$> just (content c) - ≡⟨ cong just (content-fill c) ⟩ + ≡⟨ P.cong just (content-fill c) ⟩ just c ∎ where open ≡-Reasoning open Shaped ShapeT lemma-sequenceV-successful : {A : Set} {n : ℕ} → (v : Vec (Maybe A) n) → {r : Vec A n} → sequenceV v ≡ just r → v ≡ map just r -lemma-sequenceV-successful [] {r = []} p = refl +lemma-sequenceV-successful [] {r = []} p = P.refl lemma-sequenceV-successful (just x ∷ xs) p with sequenceV xs | inspect sequenceV xs lemma-sequenceV-successful (just x ∷ xs) () | nothing | _ -lemma-sequenceV-successful (just x ∷ xs) {r = .x ∷ .ys} refl | just ys | [ p′ ] = cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′) +lemma-sequenceV-successful (just x ∷ xs) {r = .x ∷ .ys} P.refl | just ys | [ p′ ] = P.cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′) lemma-sequenceV-successful (nothing ∷ xs) () lemma-sequence-successful : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C (Maybe A) s) → {r : C A s} → Shaped.sequence ShapeT c ≡ just r → c ≡ Shaped.fmap ShapeT just r -lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin +lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (P.sym (begin fill s <$> (map just <$> (content <$> just r)) - ≡⟨ cong (_<$>_ (fill s) ∘ _<$>_ (map just)) (begin + ≡⟨ P.cong (_<$>_ (fill s) ∘ _<$>_ (map just)) (begin content <$> just r - ≡⟨ cong (_<$>_ content) (sym p) ⟩ + ≡⟨ P.cong (_<$>_ content) (P.sym p) ⟩ content <$> (fill s <$> sequenceV (content c)) - ≡⟨ sym (Functor.composition MaybeFunctor content (fill s) (sequenceV (content c))) ⟩ + ≡⟨ P.sym (Functor.composition MaybeFunctor content (fill s) (sequenceV (content c))) ⟩ content ∘ fill s <$> sequenceV (content c) ≡⟨ Functor.cong MaybeFunctor (fill-content s) (sequenceV (content c)) ⟩ id <$> sequenceV (content c) ≡⟨ Functor.identity MaybeFunctor (sequenceV (content c)) ⟩ sequenceV (content c) - ≡⟨ cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩ + ≡⟨ P.cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩ sequenceV (map just (proj₁ wp)) ≡⟨ lemma-just-sequenceV (proj₁ wp) ⟩ just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)) ∎) ⟩ fill s <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p))) - ≡⟨ cong (_<$>_ (fill s) ∘ just) (sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩ + ≡⟨ P.cong (_<$>_ (fill s) ∘ just) (P.sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩ fill s <$> just (content c) - ≡⟨ cong just (content-fill c) ⟩ + ≡⟨ P.cong just (content-fill c) ⟩ just c ∎)) where open ≡-Reasoning open Shaped ShapeT @@ -221,15 +220,15 @@ module _ (G : Get) where 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) ⟩ + ≡⟨ P.cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩ get <$> sequenceSource (fmapS just r) - ≡⟨ cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩ + ≡⟨ P.cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩ get <$> just r - ≡⟨ sym (lemma-just-sequence ViewShapeT (get r)) ⟩ + ≡⟨ P.sym (lemma-just-sequence ViewShapeT (get r)) ⟩ sequenceView (fmapV just (get r)) - ≡⟨ cong sequenceView (sym (free-theorem just r)) ⟩ + ≡⟨ P.cong sequenceView (P.sym (free-theorem just r)) ⟩ sequenceView (get (fmapS just r)) - ≡⟨ cong (sequenceView ∘ get) (sym (lemma-sequence-successful SourceShapeT v p)) ⟩ + ≡⟨ P.cong (sequenceView ∘ get) (P.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₂ @@ -241,15 +240,15 @@ sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-con sequenceV-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 _)) sequenceV-cong {S} (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (EqSetoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (EqSetoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y +sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (P.setoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (P.setoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y sequence-cong ShapeT α {x = x} {y = y} (shape≈ , content≈) with sequenceV (Shaped.content ShapeT x) | sequenceV (Shaped.content ShapeT y) | sequenceV-cong content≈ -sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (refl , (begin +sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (P.refl , (begin content (fill s x) ≡⟨ fill-content s x ⟩ x ≈⟨ x≈y ⟩ y - ≡⟨ sym (fill-content s y) ⟩ + ≡⟨ P.sym (fill-content s y) ⟩ content (fill s y) ∎)) where open EqR (VecISetoid α at _) open Shaped ShapeT @@ -260,17 +259,17 @@ module _ (G : Get) where 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 : 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 (P.setoid _) 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 + theorem-2 {i} j s v u p | h′ , ph′ | h , ph = P.refl , (begin contentV (get u) - ≡⟨ cong contentV (just-injective (trans (cong (_<$>_ get) (sym p)) - (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩ + ≡⟨ P.cong contentV (just-injective (P.trans (P.cong (_<$>_ get) (P.sym p)) + (P.cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩ contentV (get (h′↦r (h↦h′ h))) - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ contentV (get (fmapS (flip lookupM (h↦h′ h)) t)) - ≡⟨ cong contentV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩ + ≡⟨ P.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)) @@ -278,7 +277,7 @@ module _ (G : Get) where 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) ⟩ + ≡⟨ P.sym (Shaped.fmap-content ViewShapeT just v) ⟩ contentV (fmapV just v) ∎) where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) s′ = enumerate SourceShapeT (gl₁ i) @@ -291,10 +290,10 @@ module _ (G : Get) where module _ (G : Get) where open Get G - 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′ : {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 (P.setoid _) 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)) ⟩ + ≡⟨ P.cong (_<$>_ get) (P.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)) @@ -302,4 +301,4 @@ module _ (G : Get) where Shaped.sequence ViewShapeT (fmapV just v) ≡⟨ lemma-just-sequence ViewShapeT v ⟩ just v ∎) - where open EqR (MaybeSetoid (ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _)) + where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _)) |