Library zoo.common.fin_maps
Require Ltac2.Ltac2.
Require Export stdpp.fin_maps.
Require Export stdpp.fin_map_dom.
Require Import zoo.prelude.
Require Import zoo.common.option.
Require Import zoo.options.
Module doms.
Import Ltac2.
Ltac2 main () :=
Control.enter (fun () ⇒
List.iter (fun (hyp, _, ty) ⇒
lazy_match! ty with
| _ = _ ⇒
try (apply (f_equal dom) in $hyp as ?)
| _ ⇒
()
end
) (Control.hyps ())
).
End doms.
Ltac doms :=
ltac2:(doms.main ()).
Section dom.
Context `{FinMapDom K M D}.
Context {A : Type}.
Implicit Type m : M A.
Lemma elem_ofｰdom₁ m k :
k ∈ dom m →
is_Some (m !! k).
End dom.
Section fmap.
Context `{FinMapDom K M D}.
Context {A : Type}.
Implicit Type m : M A.
Lemma lookupｰfmapｰNone {B} (f : A → B) m k :
(f <$> m) !! k = None ↔
m !! k = None.
End fmap.
Section map_Forall.
Context `{FinMap K M}.
Context {A : Type}.
Implicit Type m : M A.
Lemma map_Forallｰimpl' P1 P2 m :
map_Forall P1 m →
( ∀ k x,
m !! k = Some x →
P1 k x →
P2 k x
) →
map_Forall P2 m.
Lemma map_Forallｰinsert₂' {P m} k x :
P k x →
map_Forall P (delete k m) →
map_Forall P (<[k := x]> m).
Lemma map_Forallｰdeleteｰlookup P m k :
map_Forall P (delete k m) ↔
∀ k' x,
k ≠ k' →
m !! k' = Some x →
P k' x.
Lemma map_Forallｰdeleteｰlookup₁ {P m k} k' x :
map_Forall P (delete k m) →
k ≠ k' →
m !! k' = Some x →
P k' x.
Lemma map_Forallｰdeleteｰlookup₂ P m k :
( ∀ k' x,
k ≠ k' →
m !! k' = Some x →
P k' x
) →
map_Forall P (delete k m).
End map_Forall.
Section map_Forall2.
Context `{FinMapDom K M D}.
Lemma map_Forall2ｰalt {A B R} (m : M A) (𝑚 : M B) :
map_Forall2 R m 𝑚 ↔
dom m ≡ dom 𝑚 ∧
∀ k x 𝑥,
m !! k = Some x →
𝑚 !! k = Some 𝑥 →
R k x 𝑥.
Lemma map_Forall2ｰflip {A B} R (m : M A) (𝑚 : M B) :
map_Forall2 R m 𝑚 ↔
map_Forall2 (λ k x 𝑥, R k 𝑥 x) 𝑚 m.
Lemma map_Forall2ｰlookupｰNoneｰl {A B R} {m : M A} {𝑚 : M B} k :
map_Forall2 R m 𝑚 →
m !! k = None →
𝑚 !! k = None.
Lemma map_Forall2ｰlookupｰNoneｰr {A B R} {m : M A} {𝑚 : M B} k :
map_Forall2 R m 𝑚 →
𝑚 !! k = None →
m !! k = None.
Lemma map_Forall2ｰlookupｰSome {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
map_Forall2 R m 𝑚 →
m !! k = Some x →
𝑚 !! k = Some 𝑥 →
R k x 𝑥.
Lemma map_Forall2ｰlookupｰSomeｰl {A B R} {m : M A} {𝑚 : M B} k x :
map_Forall2 R m 𝑚 →
m !! k = Some x →
∃ 𝑥,
𝑚 !! k = Some 𝑥 ∧
R k x 𝑥.
Lemma map_Forall2ｰlookupｰSomeｰr {A B R} {m : M A} {𝑚 : M B} k 𝑥 :
map_Forall2 R m 𝑚 →
𝑚 !! k = Some 𝑥 →
∃ x,
m !! k = Some x ∧
R k x 𝑥.
Lemma map_Forall2ｰinsertｰl {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
map_Forall2 R m 𝑚 →
𝑚 !! k = Some 𝑥 →
R k x 𝑥 →
map_Forall2 R (<[k := x]> m) 𝑚.
Lemma map_Forall2ｰinsertｰr {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
map_Forall2 R m 𝑚 →
m !! k = Some x →
R k x 𝑥 →
map_Forall2 R m (<[k := 𝑥]> 𝑚).
Lemma map_Forall2ｰfmapｰl {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚 ↔
map_Forall2 R (f <$> m) 𝑚.
Lemma map_Forall2ｰfmapｰl₁ {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚 →
map_Forall2 R (f <$> m) 𝑚.
Lemma map_Forall2ｰfmapｰl₂ {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
map_Forall2 R (f <$> m) 𝑚 →
map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚.
Lemma map_Forall2ｰfmapｰr {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚 ↔
map_Forall2 R m (f <$> 𝑚).
Lemma map_Forall2ｰfmapｰr₁ {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚 →
map_Forall2 R m (f <$> 𝑚).
Lemma map_Forall2ｰfmapｰr₂ {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
map_Forall2 R m (f <$> 𝑚) →
map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚.
End map_Forall2.
Section kmap.
Context `{FinMap K1 M1} `{FinMap K2 M2}.
Context (f : K1 → K2) `{!Inj (=) (=) f}.
Notation kmap := (
kmap (M1 := M1) (M2 := M2)
).
#[local] Lemma NoDupｰfstｰprod_mapｰmap_to_list {A} (m : M1 A) :
NoDup (prod_map f id <$> map_to_list m).*1.
Lemma map_to_listｰkmap {A} (m : M1 A) :
map_to_list (kmap f m) ≡ₚ prod_map f id <$> map_to_list m.
Lemma kmapｰlist_to_map {A} (l : list (K1 × A)) :
NoDup l.*1 →
kmap f (list_to_map l) = list_to_map (prod_map f id <$> l).
End kmap.
Section map۰oflatten.
Context `{FinMap K M}.
Context {A : Type}.
Definition map۰oflatten (m : M (option A)) :=
omap id m.
Lemma lookupｰmap۰oflattenｰNone m k :
m !! k = None →
map۰oflatten m !! k = None.
Lemma lookupｰmap۰oflattenｰSomeｰNone m k :
m !! k = Some None →
map۰oflatten m !! k = None.
Lemma lookupｰmap۰oflattenｰSomeｰSome {m k} a :
m !! k = Some (Some a) →
map۰oflatten m !! k = Some a.
Lemma lookupｰmap۰oflattenｰSomeｰinv m k a :
map۰oflatten m !! k = Some a →
m !! k = Some (Some a).
Lemma map۰oflattenｰempty m :
(∀ k o, m !! k = Some o → o = None) →
map۰oflatten m = ∅.
Lemma map۰oflattenｰunion m1 m2 :
m1 ##ₘ m2 →
map۰oflatten (m1 ∪ m2) = map۰oflatten m1 ∪ map۰oflatten m2.
Lemma map۰oflattenｰinsert {m} k :
m !! k = None →
map۰oflatten (<[k := None]> m) = map۰oflatten m.
Lemma map۰oflattenｰupdate {m} k a :
map۰oflatten (<[k := Some a]> m) = <[k := a]> (map۰oflatten m).
End map۰oflatten.
Require Export stdpp.fin_maps.
Require Export stdpp.fin_map_dom.
Require Import zoo.prelude.
Require Import zoo.common.option.
Require Import zoo.options.
Module doms.
Import Ltac2.
Ltac2 main () :=
Control.enter (fun () ⇒
List.iter (fun (hyp, _, ty) ⇒
lazy_match! ty with
| _ = _ ⇒
try (apply (f_equal dom) in $hyp as ?)
| _ ⇒
()
end
) (Control.hyps ())
).
End doms.
Ltac doms :=
ltac2:(doms.main ()).
Section dom.
Context `{FinMapDom K M D}.
Context {A : Type}.
Implicit Type m : M A.
Lemma elem_ofｰdom₁ m k :
k ∈ dom m →
is_Some (m !! k).
End dom.
Section fmap.
Context `{FinMapDom K M D}.
Context {A : Type}.
Implicit Type m : M A.
Lemma lookupｰfmapｰNone {B} (f : A → B) m k :
(f <$> m) !! k = None ↔
m !! k = None.
End fmap.
Section map_Forall.
Context `{FinMap K M}.
Context {A : Type}.
Implicit Type m : M A.
Lemma map_Forallｰimpl' P1 P2 m :
map_Forall P1 m →
( ∀ k x,
m !! k = Some x →
P1 k x →
P2 k x
) →
map_Forall P2 m.
Lemma map_Forallｰinsert₂' {P m} k x :
P k x →
map_Forall P (delete k m) →
map_Forall P (<[k := x]> m).
Lemma map_Forallｰdeleteｰlookup P m k :
map_Forall P (delete k m) ↔
∀ k' x,
k ≠ k' →
m !! k' = Some x →
P k' x.
Lemma map_Forallｰdeleteｰlookup₁ {P m k} k' x :
map_Forall P (delete k m) →
k ≠ k' →
m !! k' = Some x →
P k' x.
Lemma map_Forallｰdeleteｰlookup₂ P m k :
( ∀ k' x,
k ≠ k' →
m !! k' = Some x →
P k' x
) →
map_Forall P (delete k m).
End map_Forall.
Section map_Forall2.
Context `{FinMapDom K M D}.
Lemma map_Forall2ｰalt {A B R} (m : M A) (𝑚 : M B) :
map_Forall2 R m 𝑚 ↔
dom m ≡ dom 𝑚 ∧
∀ k x 𝑥,
m !! k = Some x →
𝑚 !! k = Some 𝑥 →
R k x 𝑥.
Lemma map_Forall2ｰflip {A B} R (m : M A) (𝑚 : M B) :
map_Forall2 R m 𝑚 ↔
map_Forall2 (λ k x 𝑥, R k 𝑥 x) 𝑚 m.
Lemma map_Forall2ｰlookupｰNoneｰl {A B R} {m : M A} {𝑚 : M B} k :
map_Forall2 R m 𝑚 →
m !! k = None →
𝑚 !! k = None.
Lemma map_Forall2ｰlookupｰNoneｰr {A B R} {m : M A} {𝑚 : M B} k :
map_Forall2 R m 𝑚 →
𝑚 !! k = None →
m !! k = None.
Lemma map_Forall2ｰlookupｰSome {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
map_Forall2 R m 𝑚 →
m !! k = Some x →
𝑚 !! k = Some 𝑥 →
R k x 𝑥.
Lemma map_Forall2ｰlookupｰSomeｰl {A B R} {m : M A} {𝑚 : M B} k x :
map_Forall2 R m 𝑚 →
m !! k = Some x →
∃ 𝑥,
𝑚 !! k = Some 𝑥 ∧
R k x 𝑥.
Lemma map_Forall2ｰlookupｰSomeｰr {A B R} {m : M A} {𝑚 : M B} k 𝑥 :
map_Forall2 R m 𝑚 →
𝑚 !! k = Some 𝑥 →
∃ x,
m !! k = Some x ∧
R k x 𝑥.
Lemma map_Forall2ｰinsertｰl {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
map_Forall2 R m 𝑚 →
𝑚 !! k = Some 𝑥 →
R k x 𝑥 →
map_Forall2 R (<[k := x]> m) 𝑚.
Lemma map_Forall2ｰinsertｰr {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
map_Forall2 R m 𝑚 →
m !! k = Some x →
R k x 𝑥 →
map_Forall2 R m (<[k := 𝑥]> 𝑚).
Lemma map_Forall2ｰfmapｰl {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚 ↔
map_Forall2 R (f <$> m) 𝑚.
Lemma map_Forall2ｰfmapｰl₁ {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚 →
map_Forall2 R (f <$> m) 𝑚.
Lemma map_Forall2ｰfmapｰl₂ {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
map_Forall2 R (f <$> m) 𝑚 →
map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚.
Lemma map_Forall2ｰfmapｰr {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚 ↔
map_Forall2 R m (f <$> 𝑚).
Lemma map_Forall2ｰfmapｰr₁ {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚 →
map_Forall2 R m (f <$> 𝑚).
Lemma map_Forall2ｰfmapｰr₂ {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
map_Forall2 R m (f <$> 𝑚) →
map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚.
End map_Forall2.
Section kmap.
Context `{FinMap K1 M1} `{FinMap K2 M2}.
Context (f : K1 → K2) `{!Inj (=) (=) f}.
Notation kmap := (
kmap (M1 := M1) (M2 := M2)
).
#[local] Lemma NoDupｰfstｰprod_mapｰmap_to_list {A} (m : M1 A) :
NoDup (prod_map f id <$> map_to_list m).*1.
Lemma map_to_listｰkmap {A} (m : M1 A) :
map_to_list (kmap f m) ≡ₚ prod_map f id <$> map_to_list m.
Lemma kmapｰlist_to_map {A} (l : list (K1 × A)) :
NoDup l.*1 →
kmap f (list_to_map l) = list_to_map (prod_map f id <$> l).
End kmap.
Section map۰oflatten.
Context `{FinMap K M}.
Context {A : Type}.
Definition map۰oflatten (m : M (option A)) :=
omap id m.
Lemma lookupｰmap۰oflattenｰNone m k :
m !! k = None →
map۰oflatten m !! k = None.
Lemma lookupｰmap۰oflattenｰSomeｰNone m k :
m !! k = Some None →
map۰oflatten m !! k = None.
Lemma lookupｰmap۰oflattenｰSomeｰSome {m k} a :
m !! k = Some (Some a) →
map۰oflatten m !! k = Some a.
Lemma lookupｰmap۰oflattenｰSomeｰinv m k a :
map۰oflatten m !! k = Some a →
m !! k = Some (Some a).
Lemma map۰oflattenｰempty m :
(∀ k o, m !! k = Some o → o = None) →
map۰oflatten m = ∅.
Lemma map۰oflattenｰunion m1 m2 :
m1 ##ₘ m2 →
map۰oflatten (m1 ∪ m2) = map۰oflatten m1 ∪ map۰oflatten m2.
Lemma map۰oflattenｰinsert {m} k :
m !! k = None →
map۰oflatten (<[k := None]> m) = map۰oflatten m.
Lemma map۰oflattenｰupdate {m} k a :
map۰oflatten (<[k := Some a]> m) = <[k := a]> (map۰oflatten m).
End map۰oflatten.