From 88a712fa98780a2288c31f7d38f1235b4f36dd45 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 25 Jul 2023 18:22:24 -0700 Subject: [PATCH] Implement the more powerful Map-functional theorem Signed-off-by: Danila Fedorin --- Map.agda | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/Map.agda b/Map.agda index 44493ce..adf1fe4 100644 --- a/Map.agda +++ b/Map.agda @@ -1,4 +1,4 @@ -open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; cong) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.Core using (Rel) open import Relation.Nullary using (Dec; yes; no) @@ -105,13 +105,10 @@ private module ImplInsert (f : B → B → B) where merge-preserves-unique [] l₂ u₂ = u₂ merge-preserves-unique ((k₁ , v₁) ∷ xs₁) l₂ u₂ = insert-preserves-unique k₁ v₁ (merge xs₁ l₂) (merge-preserves-unique xs₁ l₂ u₂) --- Map-functional : ∀ (k : A) (v v' : B) (xs : List (A × B)) → Unique (keys ((k , v) ∷ xs)) → MemProp._∈_ (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)) --- where --- unique-not-in : ∀ (xs : List (A × B)) (v' : B) → ¬ (All (λ k' → ¬ k ≡ k') (keys xs) × (k , v') ∈ xs) --- unique-not-in ((k' , _) ∷ xs) v' (k≢k' ∷ _ , here k',≡x) = k≢k' (cong proj₁ k',≡x) --- unique-not-in (_ ∷ xs) v' (_ ∷ rest , there k,v'∈xs) = unique-not-in xs v' (rest , k,v'∈xs) +private + unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)} → ¬ (All (λ k' → ¬ k ≡ k') (keys l) × MemProp._∈_ (k , v) l) + unique-not-in {l = (k' , _) ∷ xs} (k≢k' ∷ _ , here k',≡x) = k≢k' (cong proj₁ k',≡x) + unique-not-in {l = _ ∷ xs} (_ ∷ rest , there k,v'∈xs) = unique-not-in (rest , k,v'∈xs) module _ (f : B → B → B) where open ImplInsert f renaming @@ -134,3 +131,9 @@ module _ (_≈_ : B → B → Set b) where lift : Map → Map → Set (a ⊔ b) lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁ + +Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v' +Map-functional (here k,v≡x) (here k,v'≡x) = cong proj₂ (trans k,v≡x (sym k,v'≡x)) +Map-functional {m = (_ , push k≢xs _)} (here k,v≡x) (there k,v'∈xs) rewrite sym k,v≡x = absurd (unique-not-in (k≢xs , k,v'∈xs)) +Map-functional {m = (_ , push k≢xs _)} (there k,v∈xs) (here k,v'≡x) rewrite sym k,v'≡x = absurd (unique-not-in (k≢xs , k,v∈xs)) +Map-functional {m = (_ ∷ xs , push _ uxs)} (there k,v∈xs) (there k,v'∈xs) = Map-functional {m = (xs , uxs)} k,v∈xs k,v'∈xs