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. --- Bidir.agda | 49 +++++++++++++++++++++++++++++-------------------- 1 file changed, 29 insertions(+), 20 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index 43d8580..adb9800 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -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 -- 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 'Bidir.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