diff options
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 114 |
1 files changed, 59 insertions, 55 deletions
@@ -31,7 +31,7 @@ open import FinMap import CheckInsert open CheckInsert A import BFF -open BFF.PartialVecBFF A using (assoc ; enumerate ; denumerate ; bff) +open BFF.PartialVecBFF A using (assoc ; enumerate ; enumeratel ; denumerate ; bff) open Setoid using () renaming (_≈_ to _∋_≈_) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) @@ -101,11 +101,11 @@ lemma-2 (i ∷ is) (x ∷ xs) h p with assoc is xs | inspect (assoc is) xs lemma-2 (i ∷ is) (x ∷ xs) h () | nothing | _ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin lookupM i h ∷ map (flip lookupM h) is - ≈⟨ lemma-lookupM-assoc i is x xs h (trans (cong (flip _>>=_ (checkInsert i x)) ir) p) VecEq.∷-cong ISetoid.refl (VecISetoid (MaybeSetoid A.setoid)) ⟩ + ≈⟨ VecEq._∷-cong_ (lemma-lookupM-assoc i is x xs h (trans (cong (flip _>>=_ (checkInsert i x)) ir) p)) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩ just x ∷ map (flip lookupM h) is ≡⟨ cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h h' p is (lemma-assoc-domain is xs h' ir)) ⟩ just x ∷ map (flip lookupM h') is - ≈⟨ Setoid.refl (MaybeSetoid A.setoid) VecEq.∷-cong (lemma-2 is xs h' ir) ⟩ + ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩ just x ∷ map just xs ∎ where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) @@ -125,26 +125,26 @@ 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 s (Get.get G s) ≡ just s -theorem-1 G s = begin - bff G s (get s) - ≡⟨ cong (bff G s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩ - bff G s (get (map (denumerate s) (enumerate s))) - ≡⟨ cong (bff G s) (free-theorem (denumerate s) (enumerate s)) ⟩ - bff G s (map (denumerate s) (get (enumerate 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 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)) ⟩ + bff G i s (get (map (denumerate s) (enumerate s))) + ≡⟨ cong (bff G i s) (free-theorem (denumerate s) (enumerate s)) ⟩ + bff G i s (map (denumerate s) (get (enumerate s))) ≡⟨ refl ⟩ (h′↦r ∘ h↦h′) (assoc (get (enumerate s)) (map (denumerate s) (get (enumerate s)))) ≡⟨ 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)))) (reshape (delete-many (get (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G i))) + ≡⟨ cong (h′↦r ∘ Maybe.just ∘ union (restrict (denumerate s) (toList (get (enumerate s))))) (lemma-reshape-id (delete-many (get (enumerate s)) (fromFunc (denumerate 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 ⟩ - 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 (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)) @@ -152,22 +152,22 @@ theorem-1 G s = begin just s ∎ where open ≡-Reasoning open Get G - h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) - h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) + 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) 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 - 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) +lemma-union-not-used : {m n 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 (reshape h' n))) is ≡ map (flip lookupM h) is +lemma-union-not-used h h' [] p = refl +lemma-union-not-used {n = n} h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong₂ _∷_ (begin + lookupM i (union h (reshape h' n)) + ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j (reshape h' n)) (lookupM j h)) i ⟩ + maybe′ just (lookupM i (reshape h' n)) (lookupM i h) + ≡⟨ cong (maybe′ just (lookupM i (reshape h' n))) px ⟩ + maybe′ just (lookupM i (reshape h' n)) (just x) ≡⟨ sym px ⟩ lookupM i h ∎) (lemma-union-not-used h h' is' p') @@ -178,8 +178,8 @@ 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-just-sequence [] = refl +lemma-just-sequence (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequence xs) 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 @@ -190,19 +190,19 @@ lemma-mapM-successful (x ∷ xs) p | just y | just ys | [ p′ ] with l 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} → (G : Get) → {i : Get.|I| G} {v : Vec A (Get.|gl₁| G i)} {r : Vec B (Get.|gl₁| G i)} → mapMV f v ≡ just r → Get.get G <$> mapMV f v ≡ mapMV f (Get.get G v) -lemma-get-mapMV {f = f} G {v = v} p = let w , pw = lemma-mapM-successful v p in begin +lemma-get-mapMV {f = f} G {v = v} p = 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 just w)) ⟩ - sequenceV (get (map just w)) - ≡⟨ cong (sequenceV ∘ get) (sym pw) ⟩ + ≡⟨ cong (_<$>_ get ∘ sequenceV) (proj₂ wp) ⟩ + get <$> (sequenceV (map just (proj₁ wp))) + ≡⟨ cong (_<$>_ get) (lemma-just-sequence (proj₁ wp)) ⟩ + get <$> just (proj₁ wp) + ≡⟨ sym (lemma-just-sequence (get (proj₁ wp))) ⟩ + sequenceV (map just (get (proj₁ wp))) + ≡⟨ cong sequenceV (sym (free-theorem just (proj₁ wp))) ⟩ + sequenceV (get (map just (proj₁ wp))) + ≡⟨ cong (sequenceV ∘ get) (sym (proj₂ wp)) ⟩ sequenceV (get (map f v)) ≡⟨ cong sequenceV (free-theorem f v) ⟩ sequenceV (map f (get v)) @@ -210,30 +210,33 @@ lemma-get-mapMV {f = f} G {v = v} p = let w , pw = lemma-mapM-successful v p in mapMV f (get v) ∎ where open ≡-Reasoning open Get G + wp = lemma-mapM-successful v p sequence-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₂ sequence-cong {S} VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -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 (VecISetoid S at _)) -sequence-cong {S} (nothing VecEq.∷-cong xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) - -theorem-2 : (G : Get) → {i : Get.|I| G} → (v : Vec Carrier (Get.|gl₂| G i)) → (s u : Vec Carrier (Get.|gl₁| G i)) → bff G s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v -theorem-2 G v s u p with (lemma->>=-just ((flip union (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (Get.get G (enumerate s)) v)) p) -theorem-2 G v s u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate s)) v) ph′) -theorem-2 G v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ +sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequence-cong xs≈ys +sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p) +sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | () +sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | () +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 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⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ get <$> (just u) ≡⟨ cong (_<$>_ get) (sym p) ⟩ - get <$> (bff G s v) + get <$> (bff G j s v) ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩ - get <$> mapMV (flip lookupM (h↦h′ h)) s′ + get <$> mapMV (flip lookupM (h↦h′ h)) t ≡⟨ lemma-get-mapMV G (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) ⟩ - 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) ⟩ + mapMV (flip lookupM (h↦h′ h)) (get t) + ≡⟨ sym (sequence-map (flip lookupM (h↦h′ h)) (get 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 ∎) @@ -242,5 +245,6 @@ theorem-2 G v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (V s′ = enumerate s g = fromFunc (denumerate s) g′ = delete-many (get s′) g - h↦h′ = flip union g′ - h′↦r = flip mapMV s′ ∘ flip lookupM + t = enumeratel (Get.|gl₁| G j) + h↦h′ = flip union (reshape g′ (Get.|gl₁| G j)) + h′↦r = flip mapMV t ∘ flip lookupM |