diff options
| -rw-r--r-- | Bidir.agda | 123 | ||||
| -rw-r--r-- | Precond.agda | 58 |
2 files changed, 98 insertions, 83 deletions
@@ -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 [] |