diff options
| -rw-r--r-- | BFF.agda | 14 | ||||
| -rw-r--r-- | BFFPlug.agda | 18 | ||||
| -rw-r--r-- | Bidir.agda | 49 | ||||
| -rw-r--r-- | Precond.agda | 29 |
4 files changed, 61 insertions, 49 deletions
@@ -14,7 +14,7 @@ open import Function using (id ; _∘_ ; flip) open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) open import FinMap -open import Generic using (mapMV ; ≡-to-Π) +open import Generic using (sequenceV ; ≡-to-Π) import CheckInsert open import GetTypes using (VecVec-to-PartialVecVec) @@ -36,7 +36,7 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV - bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j)) + bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j)) bff G i s v = let s′ = enumerate s t′ = Get.get G s′ g = fromFunc (denumerate s) @@ -44,7 +44,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where t = enumeratel (Get.|gl₁| G i) h = assoc (Get.get G t) v h′ = (flip union (reshape g′ (Get.|gl₁| G i))) <$> h - in h′ >>= flip mapMV t ∘ flip lookupM + in (flip mapV t ∘ flip lookupM) <$> h′ + + sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j)) + sbff G j s v = bff G j s v >>= sequenceV module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where open GetTypes.VecVec public using (Get) @@ -53,5 +56,8 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where open PartialVecBFF A public using (assoc ; enumerate ; denumerate) - bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m) + bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec (Maybe Carrier) m) bff G = PartialVecBFF.bff A (VecVec-to-PartialVecVec G) + + sbff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m) + sbff G = PartialVecBFF.sbff A (VecVec-to-PartialVecVec G) diff --git a/BFFPlug.agda b/BFFPlug.agda index 9f45db1..12ee980 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -13,8 +13,10 @@ open import Relation.Nullary using (yes ; no) open import Function using (flip ; id ; _∘_) open import Function.Equality using (_⟶_ ; _⟨$⟩_) open import Function.LeftInverse using (_RightInverseOf_) +import Category.Monad +open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_) -open import Generic using (≡-to-Π) +open import Generic using (sequenceV ; ≡-to-Π) import BFF import GetTypes import Examples @@ -24,9 +26,9 @@ open GetTypes.PartialVecVec public using (Get) open BFF.PartialVecBFF A public bffsameshape : (G : Get) → {i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i)) -bffsameshape G {i} = bff G i +bffsameshape G {i} = sbff G i -bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec Carrier (Get.|gl₁| G j)) +bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec (Maybe Carrier) (Get.|gl₁| G j)) bffplug G sput {i} {m} s v with sput i m ... | nothing = nothing ... | just j with Get.|gl₂| G j ≟ m @@ -38,16 +40,16 @@ bffplug G sput {i} s v | just j | yes refl with bff G j s v _SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g -bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec Carrier (Get.|gl₁| G (nelteg ⟨$⟩ m))) +bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G (nelteg ⟨$⟩ m))) bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (sym (inv m)) v) module InvExamples where open Examples using (reverse' ; drop' ; sieve' ; tail' ; take') reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m) - reverse-put = bffinv reverse' (≡-to-Π id) (λ _ → refl) + reverse-put s v = bffinv reverse' (≡-to-Π id) (λ _ → refl) s v >>= sequenceV - drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec Carrier (k + m)) + drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m)) drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl) double : ℕ → ℕ @@ -59,10 +61,10 @@ module InvExamples where sieve-inv-len (suc zero) = refl sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x) - sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m)) + sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m)) sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len - tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec Carrier (suc m)) + tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m)) tail-put = bffinv tail' (≡-to-Π id) (λ _ → refl) take-put : (k : ℕ) → {n : ℕ} → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n)) @@ -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 @@ -212,18 +212,27 @@ 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 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 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 +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 j s v) - ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩ - get <$> h′↦r (h↦h′ h) + ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩ + get <$> (just (map just u) >>= sequenceV) + ≡⟨ cong (_<$>_ get ∘ flip _>>=_ sequenceV) (sym p) ⟩ + get <$> (bff G j s v >>= sequenceV) + ≡⟨ cong (_<$>_ get ∘ flip _>>=_ sequenceV ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph ⟩ + get <$> sequenceV (h′↦r (h↦h′ h)) + ≡⟨ lemma-get-sequenceV G (begin⟨ EqSetoid _ ⟩ + sequenceV (h′↦r (h↦h′ h)) + ≡⟨ cong (flip _>>=_ sequenceV ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) (sym ph) ⟩ + (h′↦r <$> (h↦h′ <$> assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) >>= sequenceV) + ≡⟨ cong (flip _>>=_ sequenceV) p ⟩ + sequenceV (map just u) + ≡⟨ lemma-just-sequence u ⟩ + just u ∎) ⟩ + sequenceV (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)) @@ -233,11 +242,11 @@ theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin sequenceV (map just v) ≡⟨ lemma-just-sequence v ⟩ just v ∎) - where open EqR (MaybeSetoid (VecISetoid A.setoid at _)) + 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 diff --git a/Precond.agda b/Precond.agda index 3a48757..45076f3 100644 --- a/Precond.agda +++ b/Precond.agda @@ -25,13 +25,12 @@ 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 Generic using (mapMV ; sequenceV) 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) import BFF import Bidir -open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence) +open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain) import GetTypes open GetTypes.PartialVecVec using (Get ; module Get) open BFF.PartialVecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff ; enumeratel) @@ -63,23 +62,19 @@ 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} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G i s v ≡ just u +assoc-enough : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G i s v ≡ just (map just u) assoc-enough G {i} s v (h , p) = _ , (begin bff G i s v - ≡⟨ cong (flip _>>=_ (flip mapMV t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Get.|gl₁| G i)))) p ⟩ - mapMV (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t - ≡⟨ refl ⟩ - sequenceV (map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t) - ≡⟨ cong (sequenceV ∘ flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ - sequenceV (map (flip lookupM (union h g′)) t) - ≡⟨ cong (sequenceV ∘ flip map t ∘ flip lookupM) (proj₂ wp) ⟩ - sequenceV (map (flip lookupM (fromFunc (proj₁ wp))) t) - ≡⟨ cong sequenceV (map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t) ⟩ - sequenceV (map (Maybe.just ∘ proj₁ wp) t) - ≡⟨ cong sequenceV (map-∘ just (proj₁ wp) t) ⟩ - sequenceV (map Maybe.just (map (proj₁ wp) t)) - ≡⟨ lemma-just-sequence (map (proj₁ wp) t) ⟩ - just (map (proj₁ wp) t) ∎) + ≡⟨ cong (_<$>_ (flip map t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Get.|gl₁| G i)))) p ⟩ + just (map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t) + ≡⟨ cong (Maybe.just ∘ flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ + just (map (flip lookupM (union h g′)) t) + ≡⟨ cong (Maybe.just ∘ flip map t ∘ flip lookupM) (proj₂ wp) ⟩ + just (map (flip lookupM (fromFunc (proj₁ wp))) t) + ≡⟨ cong Maybe.just (map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t) ⟩ + just (map (Maybe.just ∘ proj₁ wp) t) + ≡⟨ cong just (map-∘ just (proj₁ wp) t) ⟩ + just (map Maybe.just (map (proj₁ wp) t)) ∎) where open Get G s′ = enumerate s g = fromFunc (denumerate s) |