Commit d7d70ff1 authored by Dan Frumin's avatar Dan Frumin

Add `big_sepM2_flip` and rename `big_sepL2_swap` to `.._flip`.

parent 76251904
......@@ -1515,7 +1515,7 @@ Section list2.
auto using and_mono, laterN_intro.
Qed.
Lemma big_sepL2_swap Φ l1 l2 :
Lemma big_sepL2_flip Φ l1 l2 :
([ list] ky1;y2 l1; l2, Φ k y1 y2) ⊣⊢ ([ list] ky1;y2 l2; l1, Φ k y2 y1).
Proof.
revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2]//=; simplify_eq.
......@@ -1621,6 +1621,14 @@ Section gmap2.
apply big_sepM2_mono. eauto.
Qed.
Lemma big_sepM2_flip Φ m1 m2 :
([ map] ky1;y2 m1; m2, Φ k y1 y2) ⊣⊢ ([ map] ky1;y2 m2; m1, Φ k y2 y1).
Proof.
rewrite /big_sepM2. apply and_proper; [apply pure_proper; naive_solver |].
rewrite -map_zip_with_flip map_zip_with_map_zip big_sepM_fmap.
apply big_sepM_proper. by intros k [b a].
Qed.
Global Instance big_sepM2_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([ map] kx1;x2 ;, Φ k x1 x2).
Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. 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