Commit d1ecce0a authored by Dan Frumin's avatar Dan Frumin

Swap the direction in the `_flip` big_op lemmas.

parent a4bbc614
......@@ -1516,7 +1516,7 @@ Section list2.
Qed.
Lemma big_sepL2_flip Φ l1 l2 :
([ list] ky1;y2 l1; l2, Φ k y1 y2) ⊣⊢ ([ list] ky1;y2 l2; l1, Φ k y2 y1).
([ 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.
......@@ -1622,7 +1622,7 @@ Section gmap2.
Qed.
Lemma big_sepM2_flip Φ m1 m2 :
([ map] ky1;y2 m1; m2, Φ k y1 y2) ⊣⊢ ([ map] ky1;y2 m2; m1, Φ k y2 y1).
([ 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.
......
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