Skip to content
Snippets Groups Projects
Commit 6688588a authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/lookup-union-difference' into 'master'

add some lookup_{union,difference} lemmas

See merge request iris/stdpp!315
parents 28ed75d0 90b61523
No related branches found
No related tags found
No related merge requests found
...@@ -155,6 +155,8 @@ API-breaking change is listed. ...@@ -155,6 +155,8 @@ API-breaking change is listed.
does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems) does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
- Add `get_head` tactic to determine the syntactic head of a function - Add `get_head` tactic to determine the syntactic head of a function
application term. application term.
- Add map lookup lemmas: `lookup_union_is_Some`, `lookup_difference_is_Some`,
`lookup_union_Some_l_inv`, `lookup_union_Some_r_inv`.
The following `sed` script should perform most of the renaming The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
...@@ -2043,13 +2043,6 @@ Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed. ...@@ -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 : Lemma lookup_union_None {A} (m1 m2 : M A) i :
(m1 m2) !! i = None m1 !! i = None m2 !! i = None. (m1 m2) !! i = None m1 !! i = None m2 !! i = None.
Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed. 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 : 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. m1 ## m2 (m1 m2) !! i = Some x m1 !! i = Some x m2 !! i = Some x.
Proof. Proof.
...@@ -2062,6 +2055,19 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed. ...@@ -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 : Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
m1 ## m2 m2 !! i = Some x (m1 m2) !! i = Some x. m1 ## m2 m2 !! i = Some x (m1 m2) !! i = Some x.
Proof. intro. rewrite lookup_union_Some; intuition. Qed. Proof. intro. rewrite lookup_union_Some; intuition. Qed.
Lemma lookup_union_Some_inv_l {A} (m1 m2 : M A) i x :
(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. Lemma map_union_comm {A} (m1 m2 : M A) : m1 ## m2 m1 m2 = m2 m1.
Proof. Proof.
intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))). intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
...@@ -2069,6 +2075,14 @@ Proof. ...@@ -2069,6 +2075,14 @@ Proof.
destruct (m1 !! i), (m2 !! i); compute; naive_solver. destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed. 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. Lemma map_subseteq_union {A} (m1 m2 : M A) : m1 m2 m1 m2 = m2.
Proof. Proof.
rewrite map_subseteq_spec. rewrite map_subseteq_spec.
...@@ -2525,6 +2539,9 @@ Proof. ...@@ -2525,6 +2539,9 @@ Proof.
unfold difference, map_difference; rewrite lookup_difference_with. unfold difference, map_difference; rewrite lookup_difference_with.
destruct (m1 !! i), (m2 !! i); compute; intuition congruence. destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
Qed. 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 : Lemma lookup_difference_None {A} (m1 m2 : M A) i :
(m1 m2) !! i = None m1 !! i = None is_Some (m2 !! i). (m1 m2) !! i = None m1 !! i = None is_Some (m2 !! i).
Proof. Proof.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment