From d392b7a63cee8a772ad756c2ca5f3c757827f4c0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Jul 2019 19:38:05 +0200
Subject: [PATCH] Add lemma `big_sepL2_reverse`.

---
 theories/bi/big_op.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 66915c353..bd7fb0fd7 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -400,6 +400,17 @@ Section sep_list2.
     by f_equiv; f_equiv=> k [??].
   Qed.
 
+  Lemma big_sepL2_reverse_2 (Φ : A → B → PROP) l1 l2 :
+    ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2) ⊢ ([∗ list] y1;y2 ∈ reverse l1;reverse l2, Φ y1 y2).
+  Proof.
+    revert l2. induction l1 as [|x1 l1 IH]; intros [|x2 l2]; simpl; auto using False_elim.
+    rewrite !reverse_cons (comm bi_sep) IH.
+    by rewrite (big_sepL2_app _ _ [x1] _ [x2]) big_sepL2_singleton wand_elim_l.
+  Qed.
+  Lemma big_sepL2_reverse (Φ : A → B → PROP) l1 l2 :
+    ([∗ list] y1;y2 ∈ reverse l1;reverse l2, Φ y1 y2) ⊣⊢ ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2).
+  Proof. apply (anti_symm _); by rewrite big_sepL2_reverse_2 ?reverse_involutive. Qed.
+
   Lemma big_sepL2_sep Φ Ψ l1 l2 :
     ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2)
     ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
-- 
GitLab