From d2521627834713a651be0ac22aab0a1cd78df920 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 27 Jan 2014 09:02:45 +0100 Subject: prove assoc-enough in the presence of delete The old definition of bff had a single failure mode - assoc - and its proof was a single cong. Now we need to show that the other failure mode - mapM (flip lookupM ...) - is eliminated by the success of the former resulting in a larger proof. --- Precond.agda | 84 ++++++++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 71 insertions(+), 13 deletions(-) diff --git a/Precond.agda b/Precond.agda index 40ffd79..90027b4 100644 --- a/Precond.agda +++ b/Precond.agda @@ -3,38 +3,96 @@ open import Relation.Binary.Core using (Decidable ; _≡_) module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where open import Data.Nat using (ℕ) -open import Data.Fin using (Fin) +open import Data.Fin using (Fin ; zero ; suc) +open import Data.Fin.Props using (_≟_) open import Data.List using (List ; [] ; _∷_) import Level import Category.Monad import Category.Functor -open import Data.Maybe using (nothing ; just) +open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) -open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList) +open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList ; tabulate) +open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘) +import Data.List.All open import Data.List.Any using (here ; there) open Data.List.Any.Membership-≡ using (_∉_) open import Data.Maybe using (just) -open import Data.Product using (∃ ; _,_) -open import Function using (flip ; _∘_) +open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) +open import Function using (flip ; _∘_ ; id) open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) +open import Relation.Nullary using (yes ; no) -open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) +open import Generic using (mapMV ; sequenceV ; sequence-map) +open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete) import CheckInsert open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF -import Bidir +open import Bidir Carrier deq using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence) open BFF.VecBFF Carrier deq using (get-type ; assoc ; enumerate ; denumerate ; bff) -{- +lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup f (map Maybe.just v) ≡ Maybe.just (lookup f v) +lemma-lookup-map-just zero (x ∷ xs) = refl +lemma-lookup-map-just (suc f) (x ∷ xs) = lemma-lookup-map-just f xs + +fromMaybe : {A : Set} → A → Maybe A → A +fromMaybe a ma = maybe′ id a ma + +lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma) +lemma-maybe-just a (just x) = refl +lemma-maybe-just a nothing = refl + +lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Vec A n} → (toList is) in-domain-of h → ∃ λ v → union h (delete-many is (map just g)) ≡ map just v +lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin + union h (map just g) + ≡⟨ lemma-tabulate-∘ (λ f → begin + maybe′ just (lookup f (map just g)) (lookup f h) + ≡⟨ cong (flip (maybe′ just) (lookup f h)) (lemma-lookup-map-just f g) ⟩ + maybe′ just (just (lookup f g)) (lookup f h) + ≡⟨ lemma-maybe-just (lookup f g) (lookup f h) ⟩ + just (fromMaybe (lookup f g) (lookup f h)) ∎) ⟩ + tabulate (λ f → just (fromMaybe (lookup f g) (lookup f h))) + ≡⟨ tabulate-∘ just (λ f → fromMaybe (lookup f g) (lookup f h)) ⟩ + map just (tabulate (λ f → fromMaybe (lookup f g) (lookup f h))) ∎) +lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (p Data.List.All.∷ ps) = _ , (begin + union h (delete i (delete-many is (map just g))) + ≡⟨ lemma-tabulate-∘ (λ f → (begin + maybe′ just (lookupM f (delete i (delete-many is (map just g)))) (lookup f h) + ≡⟨ inner f ⟩ + maybe′ just (lookupM f (delete-many is (map just g))) (lookup f h) ∎)) ⟩ + union h (delete-many is (map just g)) + ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩ + map just _ ∎) + where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (map just g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (map just g))) (lookup f h) + inner f with f ≟ i + inner .i | yes refl = begin + maybe′ just (lookupM i (delete i (delete-many is (map just g)))) (lookup i h) + ≡⟨ cong (maybe′ just _) (proj₂ p) ⟩ + just (proj₁ p) + ≡⟨ cong (maybe′ just _) (sym (proj₂ p)) ⟩ + maybe′ just (lookupM i (delete-many is (map just g))) (lookup i h) ∎ + inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i) + 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′ --} +assoc-enough get s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin + bff get s v + ≡⟨ cong (flip _>>=_ (flip mapMV s′ ∘ flip lookupM) ∘ _<$>_ (flip union g′)) p ⟩ + mapMV (flip lookupM (union h g′)) s′ + ≡⟨ sym (sequence-map (flip lookupM (union h g′)) s′) ⟩ + sequenceV (map (flip lookupM (union h g′)) s′) + ≡⟨ cong (sequenceV ∘ flip map s′ ∘ flip lookupM) pw ⟩ + sequenceV (map (flip lookupM (map just w)) s′) + ≡⟨ cong sequenceV (map-cong (λ f → lemma-lookup-map-just f w) s′) ⟩ + sequenceV (map (Maybe.just ∘ flip lookup w) s′) + ≡⟨ cong sequenceV (map-∘ just (flip lookup w) s′) ⟩ + sequenceV (map Maybe.just (map (flip lookup w) s′)) + ≡⟨ lemma-just-sequence (map (flip lookup w) s′) ⟩ + just (map (flip lookup w) s′) ∎) + where s′ = enumerate s + g = fromFunc (denumerate s) + g′ = delete-many (get s′) g data All-different {A : Set} : List A → Set where different-[] : All-different [] -- cgit v1.2.3