Commit 011805b3 authored by Alix Trieu's avatar Alix Trieu Committed by Robbert

Additional lemmas about map_imap

parent 1b3d161d
......@@ -35,6 +35,20 @@ Proof.
destruct 1 as [?[Eq _]%map_filter_lookup_Some]. by eexists.
Qed.
Lemma dom_imap_subseteq {A B} (f: K A option B) (m: M A) :
dom D (map_imap f m) dom D m.
Proof.
intros k. rewrite 2!elem_of_dom, map_lookup_imap.
destruct 1 as [?[?[Eq _]]%bind_Some]. by eexists.
Qed.
Lemma dom_imap {A B} (f: K A option B) (m: M A) X :
( i, i X x, m !! i = Some x is_Some (f i x))
dom D (map_imap f m) X.
Proof.
intros HX k. rewrite elem_of_dom, HX, map_lookup_imap.
unfold is_Some. setoid_rewrite bind_Some. naive_solver.
Qed.
Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x i dom D m.
Proof. rewrite elem_of_dom; eauto. Qed.
Lemma not_elem_of_dom {A} (m : M A) i : i dom D m m !! i = None.
......@@ -167,6 +181,10 @@ Section leibniz.
Proof. unfold_leibniz; apply dom_difference. Qed.
Lemma dom_fmap_L {A B} (f : A B) (m : M A) : dom D (f <$> m) = dom D m.
Proof. unfold_leibniz; apply dom_fmap. Qed.
Lemma dom_imap_L {A B} (f: K A option B) (m: M A) X :
( i, i X x, m !! i = Some x is_Some (f i x))
dom D (map_imap f m) = X.
Proof. unfold_leibniz; apply dom_imap. Qed.
End leibniz.
(** * Set solver instances *)
......
......@@ -944,6 +944,16 @@ Proof.
by rewrite map_lookup_imap.
Qed.
Lemma map_imap_delete {A B} (f : K A option B) (m : M A) (i : K) :
map_imap f (delete i m) = delete i (map_imap f m).
Proof.
apply map_eq. intros k. rewrite map_lookup_imap.
destruct (decide (k = i)) as [->|Hk_not_i].
- by rewrite !lookup_delete.
- rewrite !lookup_delete_ne by done.
by rewrite map_lookup_imap.
Qed.
Lemma map_imap_ext {A1 A2 B} (f1 : K A1 option B)
(f2 : K A2 option B) (m1 : M A1) (m2 : M A2) :
( k, f1 k <$> (m1 !! k) = f2 k <$> (m2 !! k))
......@@ -953,6 +963,17 @@ Proof.
specialize (HExt i). destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Lemma map_imap_compose {A1 A2 B} (f1 : K A1 option B)
(f2 : K A2 option A1) (m : M A2) :
map_imap f1 (map_imap f2 m) = map_imap (λ k x, f2 k x = f1 k) m.
Proof.
apply map_eq. intros i. rewrite !map_lookup_imap. by destruct (m !! i).
Qed.
Lemma map_imap_empty {A B} (f : K A option B) :
map_imap f =@{M B} .
Proof. unfold map_imap. by rewrite map_to_list_empty. Qed.
(** ** Properties of the size operation *)
Lemma map_size_empty {A} : size ( : M A) = 0.
Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment