From bc138d87f0378654f9aed42ce3a111a928bcd522 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 13:57:29 -0800 Subject: [PATCH] Prove things about key-based access in map Signed-off-by: Danila Fedorin --- Lattice/Map.agda | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/Lattice/Map.agda b/Lattice/Map.agda index 405a7d3..2c7daaf 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -1086,3 +1086,29 @@ module _ {l} {L : Set l} with refl ← Map-functional {m = f' l₂} k,v∈f'l₂ k,v₂∈f'l₂ with refl ← Map-functional {m = f l₂} k,v'∈fl₂ k,v₂∈fl₂ = (v₁ ⊔₂ v , (v'≈v'' , k,v₁v₂∈f'l₁f'l₂)) + + +_[_] : Map → List A → List B +_[_] m [] = [] +_[_] m (k ∷ ks) + with ∈k-dec k (proj₁ m) +... | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ]) +... | no _ = m [ 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₂ + with k,v₁v₂∈m₁m₂ ← ⊔-combines {m₁ = m₁} {m₂ = m₂} k,v₁∈m₁ k,v₂∈m₂ + with (v' , (v₁v₂≈v' , k,v'∈m₂)) ← (proj₁ m₁≼m₂) _ _ k,v₁v₂∈m₁m₂ + with refl ← Map-functional {m = m₂} k,v₂∈m₂ k,v'∈m₂ + = v₁v₂≈v' + +m₁≼m₂⇒k∈km₁⇒k∈km₂ : ∀ (m₁ m₂ : Map) {k : A} → + m₁ ≼ m₂ → k ∈k m₁ → k ∈k m₂ +m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ = + let + k∈km₁m₂ = union-preserves-∈k₁ {l₁ = proj₁ m₁} {l₂ = proj₁ m₂} k∈km₁ + (v , k,v∈m₁m₂) = locate {m = m₁ ⊔ m₂} k∈km₁m₂ + (v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂ + in + forget k,v'∈m₂