From 066861f9cdde4ded6c5442508bef1a27576c68d7 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 17 Dec 2013 08:22:12 +0100 Subject: update bff implementation to use delete In the presence of shape-changing updates, bff needs to shrink one of the mappings before unifying them. As long the shape does not change, the union becomes a disjoint union. With this insight we can adapt the proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately theorem-2 requires more work and assoc-enough becomes non-trivial due to the introduction of mapMV. --- BFF.agda | 11 +++++++---- Bidir.agda | 23 +++++++++++++++-------- FinMap.agda | 47 ++++++++++++++++++++++++----------------------- Precond.agda | 2 ++ 4 files changed, 48 insertions(+), 35 deletions(-) diff --git a/BFF.agda b/BFF.agda index 0cdb231..f7ddd30 100644 --- a/BFF.agda +++ b/BFF.agda @@ -14,6 +14,7 @@ open import Function using (id ; _∘_ ; flip) open import Relation.Binary.Core using (Decidable ; _≡_) open import FinMap +open import Generic using (mapMV) import CheckInsert import FreeTheorems @@ -33,7 +34,9 @@ module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) bff get s v = let s′ = enumerate s - g = fromFunc (denumerate s) - h = assoc (get s′) v - h′ = (flip union g) <$> h - in (flip mapV s′ ∘ flip lookupV) <$> h′ + t′ = get s′ + g = partialize (fromFunc (denumerate s)) + g′ = delete-many t′ g + h = assoc t′ v + h′ = (flip union g′) <$> h + in h′ >>= flip mapMV s′ ∘ flip lookupV diff --git a/Bidir.agda b/Bidir.agda index 9cc0ca6..c74601a 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -22,7 +22,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨ import FreeTheorems open FreeTheorems.VecVec using (get-type ; free-theorem) -open import Generic using (just-injective ; map-just-injective) +open import Generic using (just-injective ; map-just-injective ; mapMV ; mapMV-cong ; mapMV-purity) open import FinMap import CheckInsert open CheckInsert Carrier deq @@ -113,22 +113,28 @@ theorem-1 get s = begin ≡⟨ 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)))) (fromFunc (denumerate s))) - ≡⟨ cong (h′↦r ∘ just) (lemma-union-restrict (denumerate s) (toList (get (enumerate s)))) ⟩ - (h′↦r ∘ just) (fromFunc (denumerate s)) + (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s))))) + ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩ + (h′↦r ∘ just) (partialize (fromFunc (denumerate s))) ≡⟨ refl ⟩ - just (map (flip lookup (fromFunc (denumerate s))) (enumerate s)) - ≡⟨ cong just (map-cong (lookup∘tabulate (denumerate s)) (enumerate s)) ⟩ + mapMV (flip lookupVec (partialize (fromFunc (denumerate s)))) (enumerate s) + ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-partialize-fromFunc (denumerate s)) ⟩ + mapMV (flip lookupVec (fromFunc (Maybe.just ∘ denumerate s))) (enumerate s) + ≡⟨ mapMV-cong (lookup∘tabulate (Maybe.just ∘ 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 ∎ - where h↦h′ = _<$>_ (flip union (fromFunc (denumerate s))) - h′↦r = _<$>_ (flip map (enumerate s) ∘ flip lookupVec) + where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s))))) + h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) + lemma-<$>-just : {A B : Set} {f : A → B} {b : B} {ma : Maybe A} → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a lemma-<$>-just {ma = just x} f<$>ma≡just-b = x , refl lemma-<$>-just {ma = nothing} () +{- lemma-union-not-used : {m n : ℕ} {A : Set} (h : FinMapMaybe n A) → (h' : FinMap n A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map just (map (flip lookup (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 @@ -166,3 +172,4 @@ theorem-2 get v s u p | h , ph = begin g = fromFunc (denumerate s) h↦h′ = flip union g h′↦r = flip map s′ ∘ flip lookupVec +-} diff --git a/FinMap.agda b/FinMap.agda index 46dbd1c..8cde5a6 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -4,7 +4,7 @@ open import Data.Nat using (ℕ ; zero ; suc) open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) open import Data.Fin using (Fin ; zero ; suc) open import Data.Fin.Props using (_≟_) -open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr) renaming (lookup to lookupVec ; map to mapV) +open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; toList) renaming (lookup to lookupVec ; map to mapV) open import Data.Vec.Properties using (lookup∘tabulate) open import Data.List using (List ; [] ; _∷_ ; map ; zip) open import Data.Product using (_×_ ; _,_) @@ -42,8 +42,8 @@ lookup = lookupVec fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMap n A fromFunc = tabulate -union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMap n A → FinMap n A -union m1 m2 = fromFunc (λ f → maybe′ id (lookup f m2) (lookupM f m1)) +union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A +union m1 m2 = fromFunc (λ f → maybe′ just (lookupM f m2) (lookupM f m1)) restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A restrict f is = fromAscList (zip is (map f is)) @@ -110,23 +110,24 @@ lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = refl lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = refl lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc) -lemma-union-restrict : {n : ℕ} {A : Set} → (f : Fin n → A) → (is : List (Fin n)) → union (restrict f is) (fromFunc f) ≡ fromFunc f -lemma-union-restrict {n} f is = lemma-tabulate-∘ (lemma-inner is) - where lemma-inner : (is : List (Fin n)) → (j : Fin n) → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡ f j - lemma-inner [] j = begin - maybe′ id (lookup j (fromFunc f)) (lookupM j empty) - ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-empty j) ⟩ - maybe′ id (lookup j (fromFunc f)) nothing - ≡⟨ refl ⟩ - lookup j (fromFunc f) - ≡⟨ lookup∘tabulate f j ⟩ - f j ∎ - lemma-inner (i ∷ is) j with j ≟ i - lemma-inner (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) - (lemma-lookupM-insert j (f j) (restrict f is)) - lemma-inner (i ∷ is) j | no j≢i = begin - maybe′ id (lookup j (fromFunc f)) (lookupM j (insert i (f i) (restrict f is))) - ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (restrict f is) j≢i)) ⟩ - maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) - ≡⟨ lemma-inner is j ⟩ - f j ∎ +lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (partialize (fromFunc f))) ≡ partialize (fromFunc f) +lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-partialize-fromFunc f)) + where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (partialize (fromFunc f)))) (lookupM x (restrict f (toList t))) ≡ just (f x) + lemma-inner [] x = begin + maybe′ just (lookupM x (partialize (fromFunc f))) (lookupM x empty) + ≡⟨ cong (maybe′ just (lookupM x (partialize (fromFunc f)))) (lemma-lookupM-empty x) ⟩ + lookupM x (partialize (fromFunc f)) + ≡⟨ cong (lookupM x) (lemma-partialize-fromFunc f) ⟩ + lookupM x (fromFunc (just ∘ f)) + ≡⟨ lookup∘tabulate (just ∘ f) x ⟩ + just (f x) ∎ + lemma-inner (t ∷ ts) x with x ≟ t + lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (partialize (fromFunc f))))) (lemma-lookupM-insert x (f x) (restrict f (toList ts))) + lemma-inner (t ∷ ts) x | no ¬p = begin + maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList (t ∷ ts)))) + ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f))))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩ + maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts))) + ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (partialize (fromFunc f))) ¬p) ⟩ + maybe′ just (lookupM x (delete-many ts (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts))) + ≡⟨ lemma-inner ts x ⟩ + just (f x) ∎ diff --git a/Precond.agda b/Precond.agda index e4699dc..16e452b 100644 --- a/Precond.agda +++ b/Precond.agda @@ -28,11 +28,13 @@ import Bidir open BFF.VecBFF Carrier deq using (get-type ; assoc ; enumerate ; denumerate ; bff) +{- assoc-enough : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (s : Vec Carrier m) → (v : Vec Carrier (getlen m)) → ∃ (λ h → assoc (get (enumerate s)) v ≡ just h) → ∃ λ u → bff get s v ≡ just u assoc-enough get s v (h , p) = u , cong (_<$>_ (flip map s′ ∘ flip lookup) ∘ (_<$>_ (flip union g))) p where s′ = enumerate s g = fromFunc (denumerate s) u = map (flip lookup (union h g)) s′ +-} data All-different {A : Set} : List A → Set where different-[] : All-different [] -- cgit v1.2.3