prove big_sepL_pure

iris/bi/big_op.v

@@ -180,6 +180,39 @@ Section sep_list.
     ⊢ ([∗ list] k↦x ∈ l, Φ k x) ∧ ([∗ list] k↦x ∈ l, Ψ k x).
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
+  Lemma big_sepL_pure_1 (φ : nat → A → Prop) l :
+    ([∗ list] k↦x ∈ l, ⌜φ k x⌝) ⊢@{PROP} ⌜∀ k x, l !! k = Some x → φ k x⌝.
+  Proof.
+    induction l as [|x l IH] using rev_ind.
+    { apply pure_intro=>??. rewrite lookup_nil. done. }
+    rewrite big_sepL_snoc // IH sep_and -pure_and.
+    f_equiv=>-[Hl Hx] k y /lookup_app_Some =>-[Hy|[Hlen Hy]].
+    - by apply Hl.
+    - replace k with (length l) in Hy |- *; last first.
+      { apply lookup_lt_Some in Hy. simpl in Hy. lia. }
+      rewrite Nat.sub_diag /= in Hy. injection Hy as [= ->]. done.
+  Qed.
+  Lemma big_sepL_affinely_pure_2 (φ : nat → A → Prop) l :
+    <affine> ⌜∀ k x, l !! k = Some x → φ k x⌝ ⊢@{PROP} ([∗ list] k↦x ∈ l, <affine> ⌜φ k x⌝).
+  Proof.
+    induction l as [|x l IH] using rev_ind.
+    { rewrite big_sepL_nil. apply affinely_elim_emp. }
+    rewrite big_sepL_snoc // -IH.
+    rewrite -persistent_and_sep_1 -affinely_and -pure_and.
+    f_equiv. f_equiv=>- Hlx. split.
+    - intros k y Hy. apply Hlx. rewrite lookup_app Hy //.
+    - apply Hlx. rewrite lookup_app lookup_ge_None_2 //.
+      rewrite Nat.sub_diag //.
+  Qed.
+  (** The general backwards direction requires [BiAffine] to cover the empty case. *)
+  Lemma big_sepL_pure `{!BiAffine PROP} (φ : nat → A → Prop) l :
+    ([∗ list] k↦x ∈ l, ⌜φ k x⌝) ⊣⊢@{PROP} ⌜∀ k x, l !! k = Some x → φ k x⌝.
+  Proof.
+    apply (anti_symm (⊢)); first by apply big_sepL_pure_1.
+    rewrite -(affine_affinely ⌜_⌝%I).
+    rewrite big_sepL_affinely_pure_2. by setoid_rewrite affinely_elim.
+  Qed.
+
   Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
     <pers> ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, <pers> (Φ k x).
   Proof. apply (big_opL_commute _). Qed.