From 87a476ab9ea56c35d7c22b3b21094fc7c221ec78 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 24 Jul 2023 22:51:27 -0700 Subject: [PATCH] Add proofs of uniqueness preservation for map insert Signed-off-by: Danila Fedorin --- Map.agda | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) diff --git a/Map.agda b/Map.agda index ef2ec18..06aad7c 100644 --- a/Map.agda +++ b/Map.agda @@ -10,10 +10,9 @@ module Map {a b : Level} (A : Set a) (B : Set b) open import Relation.Nullary using (¬_) open import Data.Nat using (ℕ) -open import Data.String using (String; _++_) -open import Data.List using (List; []; _∷_) +open import Data.List using (List; []; _∷_; _++_) open import Data.List.Membership.Propositional using () -open import Data.List.Relation.Unary.All using (All; _∷_) +open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂) open import Data.Unit using (⊤) @@ -33,6 +32,18 @@ data Unique {c} {C : Set c} : List C → Set c where → Unique xs → Unique (x ∷ xs) +Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} → ¬ Data.List.Membership.Propositional._∈_ x xs → Unique xs → Unique (xs ++ (x ∷ [])) +Unique-append {c} {C} {x} {[]} _ _ = push [] empty +Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') = push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs') + where + x'≢x : ¬ x' ≡ x + x'≢x x'≡x = x∉xs (here (sym x'≡x)) + + help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ [])) + help {[]} _ = x'≢x ∷ [] + help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es + + _∈_ : (A × B) → List (A × B) → Set (a ⊔ b) _∈_ p m = Data.List.Membership.Propositional._∈_ p m @@ -72,6 +83,29 @@ insert-keys-∈ f k v ((k' , _) ∷ xs) (there k∈kxs) with (≡-dec-A k k') ... | yes _ = refl ... | no _ = cong (λ xs' → k' ∷ xs') (insert-keys-∈ f k v xs k∈kxs) +insert-keys-∉ : ∀ (f : B → B → B) (k : A) (v : B) (l : List (A × B)) → ¬ (k ∈k l) → (keys l ++ (k ∷ [])) ≡ keys (insert f k v l) +insert-keys-∉ f k v [] _ = refl +insert-keys-∉ f k v ((k' , v') ∷ xs) k∉kl with (≡-dec-A k k') +... | yes k≡k' = absurd (k∉kl (here k≡k')) +... | no _ = cong (λ xs' → k' ∷ xs') (insert-keys-∉ f k v xs (λ k∈kxs → k∉kl (there k∈kxs))) + +∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈k l) +∈k-dec k [] = no (λ ()) +∈k-dec k ((k' , v) ∷ xs) with (≡-dec-A k k') +... | yes k≡k' = yes (here k≡k') +... | no k≢k' with (∈k-dec k xs) +... | yes k∈kxs = yes (there k∈kxs) +... | no k∉kxs = no witness + where + witness : ¬ k ∈k ((k' , v) ∷ xs) + witness (here k≡k') = k≢k' k≡k' + witness (there k∈kxs) = k∉kxs k∈kxs + +insert-preserves-unique : ∀ (f : B → B → B) (k : A) (v : B) (l : List (A × B)) → Unique (keys l) → Unique (keys (insert f k v l)) +insert-preserves-unique f k v l u with (∈k-dec k l) +... | yes k∈kl rewrite insert-keys-∈ f k v l k∈kl = u +... | no k∉kl rewrite sym (insert-keys-∉ f k v l k∉kl) = Unique-append k∉kl u + Map-functional : ∀ (k : A) (v v' : B) (xs : List (A × B)) → Unique (keys ((k , v) ∷ xs)) → Data.List.Membership.Propositional._∈_ (k , v') ((k , v) ∷ xs) → v ≡ v' Map-functional k v v' _ _ (here k,v'≡k,v) = sym (cong proj₂ k,v'≡k,v) Map-functional k v v' xs (push k≢ _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs))