From 66dfe14207040fe8043ce913c8050e3a444ec82a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 4 Aug 2023 00:07:10 -0700 Subject: [PATCH] Prove that restrict needs the key in both maps Signed-off-by: Danila Fedorin --- Map.agda | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Map.agda b/Map.agda index 77c9b07..1bdce79 100644 --- a/Map.agda +++ b/Map.agda @@ -329,6 +329,22 @@ private module ImplInsert (f : B → B → B) where Unique (keys l₂) → Unique (keys (intersect l₁ l₂)) intersect-preserves-Unique {l₁} u = restrict-preserves-Unique (updates-preserve-Unique {l₁} u) + restrict-needs-both : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} → + (k , v) ∈ restrict l₁ l₂ → (k ∈k l₁ × (k , v) ∈ l₂) + restrict-needs-both {k} {v} {l₁} {[]} () + restrict-needs-both {k} {v} {l₁} {(k' , v') ∷ xs} k,v∈l₁l₂ + with ∈k-dec k' l₁ | k,v∈l₁l₂ + ... | yes k'∈kl₁ | here k,v≡k',v' + rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v' = + (k'∈kl₁ , here refl) + ... | yes _ | there k,v∈l₁xs = + let (k∈kl₁ , k,v∈xs) = restrict-needs-both k,v∈l₁xs + in (k∈kl₁ , there k,v∈xs) + ... | no k'∉kl₁ | k,v∈l₁xs = + let (k∈kl₁ , k,v∈xs) = restrict-needs-both k,v∈l₁xs + in (k∈kl₁ , there k,v∈xs) + + Map : Set (a ⊔ b) Map = Σ (List (A × B)) (λ l → Unique (keys l))