Commit a92bf1dd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add lemma `big_sepL_sepL2_diag` and `big_sepM_sepM2_diag`.

parent d920fcd4
...@@ -686,6 +686,11 @@ Section sep_list2. ...@@ -686,6 +686,11 @@ Section sep_list2.
Proof. rewrite big_sepL2_alt. apply _. Qed. Proof. rewrite big_sepL2_alt. apply _. Qed.
End sep_list2. End sep_list2.
Lemma big_sepL_sepL2_diag {A} (Φ : nat A A PROP) (l : list A) :
([ list] ky l, Φ k y y) -
([ list] ky1;y2 l;l, Φ k y1 y2).
Proof. revert Φ. induction l as [|x l IH]=> Φ /=; [done|]. by rewrite -IH. Qed.
Lemma big_sepL2_ne_2 {A B : ofe} Lemma big_sepL2_ne_2 {A B : ofe}
(Φ Ψ : nat A B PROP) l1 l2 l1' l2' n : (Φ Ψ : nat A B PROP) l1 l2 l1' l2' n :
l1 {n} l1' l2 {n} l2' l1 {n} l1' l2 {n} l2'
...@@ -1573,6 +1578,15 @@ Section map2. ...@@ -1573,6 +1578,15 @@ Section map2.
Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed. Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
End map2. End map2.
Lemma big_sepM_sepM2_diag `{Countable K} {A} (Φ : K A A PROP) (m : gmap K A) :
([ map] ky m, Φ k y y) -
([ map] ky1;y2 m;m, Φ k y1 y2).
Proof.
revert Φ. induction m as [|x k l ? IH] using map_ind=> Φ /=.
{ by rewrite big_sepM_empty big_sepM2_empty. }
by rewrite big_sepM_insert // big_sepM2_insert // -IH.
Qed.
Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe) Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe)
(Φ Ψ : K A B PROP) m1 m2 m1' m2' n : (Φ Ψ : K A B PROP) m1 m2 m1' m2' n :
m1 {n} m1' m2 {n} m2' m1 {n} m1' m2 {n} m2'
......
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