From aad47e05ef1567285aca67b3c8030e36929703b4 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Wed, 26 Feb 2014 12:49:45 +0100 Subject: remove the sequenceV call from bff This allows bff to be more precise with regard to its failure modes, even though we are not yet making use of that projected precision. It allows inserting a default value for entries that could not be recovered in a shape changing update as described in VoigtlaenderHMW13. --- Precond.agda | 29 ++++++++++++----------------- 1 file changed, 12 insertions(+), 17 deletions(-) (limited to 'Precond.agda') 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) -- cgit v1.2.3 From cdaf8389007f1272f05089b75abecf8d6aefb49e Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Wed, 26 Feb 2014 13:57:23 +0100 Subject: weaken assumptions made by theorem-2 and asssoc-enough --- Bidir.agda | 56 ++++++++++++++++++++++++++++---------------------------- Precond.agda | 31 +++++++++++++++++++------------ 2 files changed, 47 insertions(+), 40 deletions(-) (limited to 'Precond.agda') diff --git a/Bidir.agda b/Bidir.agda index adb9800..325d00a 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -26,7 +26,7 @@ import Relation.Binary.EqReasoning as EqR import GetTypes open GetTypes.PartialVecVec using (Get ; module Get) -open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid) +open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective) open import FinMap import CheckInsert open CheckInsert A @@ -212,36 +212,22 @@ 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 (map just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v +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 (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just 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 (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))) +theorem-2 G j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩ + get u + ≡⟨ just-injective (trans (cong (_<$>_ get) (sym p)) + (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph)) ⟩ + get (h′↦r (h↦h′ h)) ≡⟨ refl ⟩ - 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)) - ≡⟨ 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 ∎) + get (map (flip lookupM (h↦h′ h)) t) + ≡⟨ free-theorem (flip lookupM (h↦h′ h)) t ⟩ + map (flip lookupM (h↦h′ h)) (get t) + ≡⟨ lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph) ⟩ + map (flip lookupM h) (get t) + ≈⟨ lemma-2 (get t) v h ph ⟩ + map just v ∎ where open SetoidReasoning open Get G s′ = enumerate s @@ -250,3 +236,17 @@ theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid t = enumeratel (Get.|gl₁| G j) h↦h′ = flip union (reshape g′ (Get.|gl₁| G j)) h′↦r = flip map t ∘ flip lookupM + +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 = drop-just (begin + get <$> just u + ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩ + get <$> sequenceV (map just u) + ≡⟨ lemma-get-sequenceV G (lemma-just-sequence u) ⟩ + sequenceV (get (map just u)) + ≈⟨ sequence-cong (theorem-2 G j s v (map just u) p) ⟩ + sequenceV (map just v) + ≡⟨ lemma-just-sequence v ⟩ + just v ∎) + where open EqR (MaybeSetoid (VecISetoid A.setoid at _)) + open Get G diff --git a/Precond.agda b/Precond.agda index 45076f3..ead2e18 100644 --- a/Precond.agda +++ b/Precond.agda @@ -62,19 +62,26 @@ 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 (map just u) -assoc-enough G {i} s v (h , p) = _ , (begin +assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v ≡ just h) → ∃ λ u → bff G j s v ≡ just u +assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ (flip map t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (|gl₁| j)))) p + where open Get G + g′ = delete-many (get (enumerate s)) (fromFunc (denumerate s)) + t = enumeratel (|gl₁| j) + +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 (enumeratel (Get.|gl₁| G i))) 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 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)) ∎) + ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩ + just (map (flip lookupM (union h (reshape g′ (|gl₁| i)))) t) + ≡⟨ cong just (begin _ + ≡⟨ cong (flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ + map (flip lookupM (union h g′)) t + ≡⟨ cong (flip map t ∘ flip lookupM) (proj₂ wp) ⟩ + map (flip lookupM (fromFunc (proj₁ wp))) t + ≡⟨ map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩ + map (Maybe.just ∘ proj₁ wp) t + ≡⟨ map-∘ just (proj₁ wp) t ⟩ + map Maybe.just (map (proj₁ wp) t) ∎) ⟩ _ ∎) where open Get G s′ = enumerate s g = fromFunc (denumerate s) -- cgit v1.2.3