Skip to content
Snippets Groups Projects

add some lookup_{union,difference} lemmas

Merged Ralf Jung requested to merge ralf/lookup-union-difference into master
All threads resolved!
Files
2
+ 24
7
@@ -2043,13 +2043,6 @@ Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
Lemma lookup_union_None {A} (m1 m2 : M A) i :
(m1 m2) !! i = None m1 !! i = None m2 !! i = None.
Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
Lemma map_positive_l {A} (m1 m2 : M A) : m1 m2 = m1 = ∅.
Proof.
intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
rewrite lookup_empty, lookup_union_None in Hm; tauto.
Qed.
Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 m1 m2 ∅.
Proof. eauto using map_positive_l. Qed.
Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
m1 ## m2 (m1 m2) !! i = Some x m1 !! i = Some x m2 !! i = Some x.
Proof.
@@ -2062,6 +2055,19 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
m1 ## m2 m2 !! i = Some x (m1 m2) !! i = Some x.
Proof. intro. rewrite lookup_union_Some; intuition. Qed.
Lemma lookup_union_Some_inv_l {A} (m1 m2 : M A) i x :
+1
(m1 m2) !! i = Some x m2 !! i = None m1 !! i = Some x.
Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
Lemma lookup_union_Some_inv_r {A} (m1 m2 : M A) i x :
(m1 m2) !! i = Some x m1 !! i = None m2 !! i = Some x.
Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
Lemma lookup_union_is_Some {A} (m1 m2 : M A) i :
is_Some ((m1 m2) !! i) is_Some (m1 !! i) is_Some (m2 !! i).
Proof.
rewrite <-!not_eq_None_Some, !lookup_union_None.
destruct (m1 !! i); naive_solver.
Qed.
Lemma map_union_comm {A} (m1 m2 : M A) : m1 ## m2 m1 m2 = m2 m1.
Proof.
intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
@@ -2069,6 +2075,14 @@ Proof.
destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
Lemma map_positive_l {A} (m1 m2 : M A) : m1 m2 = m1 = ∅.
Proof.
intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
rewrite lookup_empty, lookup_union_None in Hm; tauto.
Qed.
Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 m1 m2 ∅.
Proof. eauto using map_positive_l. Qed.
Lemma map_subseteq_union {A} (m1 m2 : M A) : m1 m2 m1 m2 = m2.
Proof.
rewrite map_subseteq_spec.
@@ -2525,6 +2539,9 @@ Proof.
unfold difference, map_difference; rewrite lookup_difference_with.
destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
Qed.
Lemma lookup_difference_is_Some {A} (m1 m2 : M A) i :
is_Some ((m1 m2) !! i) is_Some (m1 !! i) m2 !! i = None.
Proof. unfold is_Some. setoid_rewrite lookup_difference_Some. naive_solver. Qed.
Lemma lookup_difference_None {A} (m1 m2 : M A) i :
(m1 m2) !! i = None m1 !! i = None is_Some (m2 !! i).
Proof.
Loading