Commit edfdba15 authored by Dan Frumin's avatar Dan Frumin Committed by Robbert

Add `big_sepL2_swap`

parent b6b9d739
......@@ -1475,6 +1475,13 @@ Section list2.
auto using and_mono, laterN_intro.
Qed.
Lemma big_sepL2_flip Φ l1 l2 :
([ list] ky1;y2 l2; l1, Φ k y2 y1) ⊣⊢ ([ list] ky1;y2 l1; l2, Φ k y1 y2).
Proof.
revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2]//=; simplify_eq.
by rewrite IH.
Qed.
Global Instance big_sepL2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([ list] ky1;y2 []; [], Φ k y1 y2).
Proof. simpl; apply _. Qed.
......@@ -1541,6 +1548,14 @@ Section gmap2.
apply big_sepM2_mono. eauto.
Qed.
Lemma big_sepM2_flip Φ m1 m2 :
([ map] ky1;y2 m2; m1, Φ k y2 y1) ⊣⊢ ([ map] ky1;y2 m1; m2, Φ k y1 y2).
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