Commit 78c857b9 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ci/ralf/map-dom-inv' into 'master'

some map lemmas

See merge request iris/stdpp!234
parents dd04c27a de42bc79
......@@ -163,6 +163,41 @@ Proof.
- by rewrite dom_empty.
- simpl. by rewrite dom_insert, IH.
Qed.
Lemma dom_singleton_inv {A} (m : M A) i :
dom D m {[i]} x, m = {[i := x]}.
Proof.
intros Hdom. assert (is_Some (m !! i)) as [x ?].
{ apply (elem_of_dom (D:=D)); set_solver. }
exists x. apply map_eq; intros j.
destruct (decide (i = j)); simplify_map_eq; [done|].
apply not_elem_of_dom. set_solver.
Qed.
Lemma dom_union_inv `{!RelDecision (@{D})} {A} (m : M A) (X1 X2 : D) :
X1 ## X2
dom D m X1 X2
m1 m2, m = m1 m2 m1 ## m2 dom D m1 X1 dom D m2 X2.
Proof.
intros.
exists (filter (λ '(k,x), k X1) m), (filter (λ '(k,x), k X1) m).
assert (filter (λ '(k, _), k X1) m ## filter (λ '(k, _), k X1) m).
{ apply map_disjoint_filter. }
split_and!; [|done| |].
- apply map_eq; intros i. apply option_eq; intros x.
rewrite lookup_union_Some, !map_filter_lookup_Some by done.
destruct (decide (i X1)); naive_solver.
- apply dom_filter; intros i; split; [|naive_solver].
intros. assert (is_Some (m !! i)) as [x ?] by (apply (elem_of_dom (D:=D)); set_solver).
naive_solver.
- apply dom_filter; intros i; split.
+ intros. assert (is_Some (m !! i)) as [x ?] by (apply (elem_of_dom (D:=D)); set_solver).
naive_solver.
+ intros (x&?&?). apply dec_stable; intros ?.
assert (m !! i = None) by (apply not_elem_of_dom; set_solver).
naive_solver.
Qed.
(** If [D] has Leibniz equality, we can show an even stronger result. This is a
common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
(and thus also [gset K], the usual domain) but the value type [A] does not. *)
......@@ -207,6 +242,14 @@ Section leibniz.
Lemma dom_list_to_map_L {A} (l : list (K * A)) :
dom D (list_to_map l : M A) = list_to_set l.*1.
Proof. unfold_leibniz. apply dom_list_to_map. Qed.
Lemma dom_singleton_inv_L {A} (m : M A) i :
dom D m = {[i]} x, m = {[i := x]}.
Proof. unfold_leibniz. apply dom_singleton_inv. Qed.
Lemma dom_union_inv_L `{!RelDecision (@{D})} {A} (m : M A) (X1 X2 : D) :
X1 ## X2
dom D m = X1 X2
m1 m2, m = m1 m2 m1 ## m2 dom D m1 = X1 dom D m2 = X2.
Proof. unfold_leibniz. apply dom_union_inv. Qed.
End leibniz.
(** * Set solver instances *)
......
......@@ -296,6 +296,8 @@ Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
Proof.
intros [_ []]. rewrite map_subseteq_spec. intros ??. by rewrite lookup_empty.
Qed.
Lemma map_empty_subseteq {A} (m : M A) : m.
Proof. apply map_subseteq_spec. intros k v []%lookup_empty_Some. Qed.
Lemma map_subset_alt {A} (m1 m2 : M A) :
m1 m2 m1 m2 i, m1 !! i = None is_Some (m2 !! i).
......@@ -1475,6 +1477,9 @@ Section merge.
Context {A} (f : option A option A option A) `{!DiagNone f}.
Implicit Types m : M A.
(** These instances can in many cases not be applied automatically due to Coq
unification bug #6294. Hence there are many explicit derived instances for
specific operations such as union or difference in the rest of this file. *)
Global Instance: LeftId (=) None f LeftId (=) ( : M A) (merge f).
Proof.
intros ??. apply map_eq. intros.
......@@ -2104,6 +2109,20 @@ Qed.
Lemma delete_union {A} (m1 m2 : M A) i :
delete i (m1 m2) = delete i m1 delete i m2.
Proof. apply delete_union_with. Qed.
Lemma union_delete_insert {A} (m1 m2 : M A) i x :
m1 !! i = Some x
delete i m1 <[i:=x]> m2 = m1 m2.
Proof.
intros. rewrite <-insert_union_r by apply lookup_delete.
by rewrite insert_union_l, insert_delete, insert_id by done.
Qed.
Lemma union_insert_delete {A} (m1 m2 : M A) i x :
m1 !! i = None m2 !! i = Some x
<[i:=x]> m1 delete i m2 = m1 m2.
Proof.
intros. rewrite <-insert_union_l by apply lookup_delete.
by rewrite insert_union_r, insert_delete, insert_id by done.
Qed.
Lemma map_Forall_union_1_1 {A} (m1 m2 : M A) P :
map_Forall P (m1 m2) map_Forall P m1.
Proof. intros HP i x ?. apply HP, lookup_union_Some_raw; auto. Qed.
......@@ -2371,6 +2390,25 @@ Proof.
apply map_empty; intros i. rewrite lookup_difference_None.
destruct (m !! i); eauto.
Qed.
Global Instance map_difference_right_id {A} : RightId (=) (:M A) () := _.
Lemma map_difference_empty {A} (m : M A) : m = m.
Proof. by rewrite (right_id _ _). Qed.
Lemma delete_difference {A} (m1 m2 : M A) i x :
delete i (m1 m2) = m1 <[i:=x]> m2.
Proof.
apply map_eq. intros j. apply option_eq. intros y.
rewrite lookup_delete_Some, !lookup_difference_Some, lookup_insert_None.
naive_solver.
Qed.
Lemma difference_delete {A} (m1 m2 : M A) i x :
m1 !! i = Some x
m1 delete i m2 = <[i:=x]> (m1 m2).
Proof.
intros. apply map_eq. intros j. apply option_eq. intros y.
rewrite lookup_insert_Some, !lookup_difference_Some, lookup_delete_None.
destruct (decide (i = j)); naive_solver.
Qed.
End theorems.
(** ** The seq operation *)
......
......@@ -779,6 +779,8 @@ Section set.
intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition].
destruct (decide (x X)); intuition.
Qed.
Lemma union_difference_singleton x Y : x Y Y {[x]} Y {[x]}.
Proof. intros ?. apply union_difference. set_solver. Qed.
Lemma difference_union X Y : X Y Y X Y.
Proof.
intros x. rewrite !elem_of_union; rewrite elem_of_difference.
......@@ -800,6 +802,8 @@ Section set.
Context `{!LeibnizEquiv C}.
Lemma union_difference_L X Y : X Y Y = X Y X.
Proof. unfold_leibniz. apply union_difference. Qed.
Lemma union_difference_singleton_L x Y : x Y Y = {[x]} Y {[x]}.
Proof. unfold_leibniz. apply union_difference_singleton. Qed.
Lemma difference_union_L X Y : X Y Y = X Y.
Proof. unfold_leibniz. apply difference_union. Qed.
Lemma non_empty_difference_L X Y : X Y Y X .
......
Supports Markdown
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