Generalize lemma `big_sepL2_app_inv` and use that to prove `big_sepL2_snoc`.

iris/bi/big_op.v

@@ -416,32 +416,36 @@ Section sep_list2.
     by rewrite IH -assoc.
   Qed.
   Lemma big_sepL2_app_inv Φ l1 l2 l1' l2' :
-    length l1 = length l1' →
+    length l1 = length l1' ∨ length l2 = length l2' →
     ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2) -∗
     ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) ∗
     ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k)%nat y1 y2).
   Proof.
-    revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] //= ?; simplify_eq.
+    revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] /= Hlen.
     - by rewrite left_id.
-    - by rewrite -assoc IH.
+    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length Hlen /= app_length.
+      apply pure_elim'; lia.
+    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length -Hlen /= app_length.
+      apply pure_elim'; lia.
+    - by rewrite -assoc IH; last lia.
+  Qed.
+  Lemma big_sepL2_app_same_length Φ l1 l2 l1' l2' :
+    length l1 = length l1' ∨ length l2 = length l2' →
+    ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2) ⊣⊢
+    ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) ∗
+    ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k)%nat y1 y2).
+  Proof.
+    intros. apply (anti_symm _).
+    - by apply big_sepL2_app_inv.
+    - apply wand_elim_l'. apply big_sepL2_app.
   Qed.
 
   Lemma big_sepL2_snoc Φ x1 x2 l1 l2 :
-    ([∗ list] k↦y1;y2 ∈ (l1 ++ [x1]);(l2 ++ [x2]), Φ k y1 y2) ⊣⊢
-    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ Φ (length l1) x1 x2.
-  Proof.
-    apply (anti_symm (⊢)); last first.
-    - apply wand_elim_l'. rewrite big_sepL2_app. apply wand_mono; last done.
-      rewrite big_sepL2_singleton Nat.add_0_r. done.
-    - rewrite big_sepL2_app_inv_l. apply exist_elim=>l2l. apply exist_elim=>l2r.
-      apply pure_elim_l=>Hl2.
-      apply (pure_elim (length [x1] = length l2r)).
-      { rewrite !big_sepL2_length sep_elim_r. done. }
-      simpl. destruct l2r as [? l2r|]; first done.
-      destruct l2r as [|]; last done. intros _.
-      apply app_inj_tail in Hl2 as [-> ->].
-      apply sep_mono_r.
-      rewrite big_sepL2_singleton Nat.add_0_r. done.
+    ([∗ list] k↦y1;y2 ∈ l1 ++ [x1]; l2 ++ [x2], Φ k y1 y2) ⊣⊢
+    ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) ∗ Φ (length l1) x1 x2.
+  Proof.
+    rewrite big_sepL2_app_same_length; last by auto.
+    by rewrite big_sepL2_singleton Nat.add_0_r.
   Qed.
 
   (** The lemmas [big_sepL2_mono], [big_sepL2_ne] and [big_sepL2_proper] are more