Prove that restrict needs the key in both maps

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-08-04 00:07:10 -07:00
parent 56147cfc82
commit 66dfe14207

View File

@ -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))