From a22c0c9252dd903df159fdb0a2cba1f19b6726be Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 17:56:26 -0700 Subject: [PATCH] Prove a property of multi-key lookup Signed-off-by: Danila Fedorin --- Lattice/FiniteMap.agda | 5 +++++ Lattice/Map.agda | 13 +++++++++++++ 2 files changed, 18 insertions(+) diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index aa45fc1..b4213eb 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -30,6 +30,7 @@ open import Lattice.Map ≡-dec-A lB as Map ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ ; ≈-dec to ≈ᵐ-dec ; _[_] to _[_]ᵐ + ; []-∈ to []ᵐ-∈ ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ ; locate to locateᵐ ; keys to keysᵐ @@ -104,6 +105,10 @@ module WithKeys (ks : List A) where _[_] : FiniteMap → List A → List B _[_] (m₁ , _) ks = m₁ [ ks ]ᵐ + []-∈ : ∀ {k : A} {v : B} {ks' : List A} (fm : FiniteMap) → + k ∈ˡ ks' → (k , v) ∈ fm → v ∈ˡ (fm [ ks' ]) + []-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks' + ≈-equiv : IsEquivalence FiniteMap _≈_ ≈-equiv = record { ≈-refl = diff --git a/Lattice/Map.agda b/Lattice/Map.agda index cc7f0ea..8e30306 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -1112,6 +1112,19 @@ _[_] m (k ∷ ks) ... | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ]) ... | no _ = m [ ks ] +[]-∈ : ∀ {k : A} {v : B} {ks : List A} (m : Map) → + (k , v) ∈ m → k ∈ˡ ks → v ∈ˡ (m [ ks ]) +[]-∈ {k} {v} {ks} m k,v∈m (here refl) + with ∈k-dec k (proj₁ m) +... | no k∉km = ⊥-elim (k∉km (forget k,v∈m)) +... | yes k∈km + with (v' , k,v'∈m) ← locate {m = m} k∈km + rewrite Map-functional {m = m} k,v'∈m k,v∈m = here refl +[]-∈ {k} {v} {k' ∷ ks'} m k,v∈m (there k∈ks') + with ∈k-dec k' (proj₁ m) +... | no _ = []-∈ m k,v∈m k∈ks' +... | yes _ = there ([]-∈ m k,v∈m k∈ks') + m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (m₁ m₂ : Map) {k : A} {v₁ v₂ : B} → m₁ ≼ m₂ → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → v₁ ≼₂ v₂ m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂