Tests for `big_sepL2`.

tests/proofmode.ref

@@ -88,6 +88,32 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P
   
+1 subgoal
+  
+  PROP : sbi
+  x1, x2 : nat
+  l1, l2 : list nat
+  P : PROP
+  ============================
+  "HP" : P
+  _ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
+  _ : <affine> ⌜x1 = x2⌝
+      ∗ ([∗ list] y1;y2 ∈ l1;(l2 ++ l2), <affine> ⌜y1 = y2⌝)
+  --------------------------------------∗
+  P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
+  
+1 subgoal
+  
+  PROP : sbi
+  Φ : nat → nat → PROP
+  x1, x2 : nat
+  l1, l2 : list nat
+  ============================
+  _ : Φ x1 x2
+  _ : [∗ list] y1;y2 ∈ l1;l2, Φ y1 y2
+  --------------------------------------∗
+  <absorb> Φ x1 x2
+  
 1 subgoal
   
   PROP : sbi

tests/proofmode.v

@@ -486,11 +486,28 @@ Proof.
 Qed.
 
 Lemma test_big_sepL_simpl x (l : list nat) P :
-  P -∗
+   P -∗
   ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
   ([∗ list] y ∈ x :: l, <affine> ⌜ y = y ⌝) -∗
   P.
 Proof. iIntros "HP ?? /=". Show. done. Qed.
+
+Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
+  P -∗
+  ([∗ list] k↦y1;y2 ∈ []; l2, <affine> ⌜ y1 = y2 ⌝) -∗
+  ([∗ list] y1;y2 ∈ x1 :: l1; (x2 :: l2) ++ l2, <affine> ⌜ y1 = y2 ⌝) -∗
+  P ∨ ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, True).
+Proof. iIntros "HP ?? /=". Show. by iLeft. Qed.
+
+Lemma test_big_sepL2_iDestruct (Φ : nat → nat → PROP) x1 x2 (l1 l2 : list nat) :
+  ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, Φ y1 y2) -∗
+  <absorb> Φ x1 x2.
+Proof. iIntros "[??]". Show. iFrame. Qed.
+
+Lemma test_big_sepL2_iFrame (Φ : nat → nat → PROP) (l1 l2 : list nat) P :
+  Φ 0 10 -∗ ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2) -∗
+  ([∗ list] y1;y2 ∈ (0 :: l1);(10 :: l2), Φ y1 y2).
+Proof. iIntros "$ ?". iFrame. Qed.
 End tests.
 
 (** Test specifically if certain things print correctly. *)