Factor out some common properties about lists.

algebra/cmra_big_op.v

@@ -156,11 +156,7 @@ Section list.
   Proof. apply big_opL_forall; apply _. Qed.
   Lemma big_opL_permutation (f : A → M) l1 l2 :
     l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x).
-  Proof.
-    assert (∀ l, imap (λ _ x, f x) l = map f l) as EQ;
-      last by rewrite /big_opL !EQ=>->.
-    intros l; revert f. induction l as [|?? IH]=>// f. rewrite imap_cons IH //.
-  Qed.
+  Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed.
 
   Global Instance big_opL_ne l n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))

base_logic/big_op.v

@@ -137,11 +137,7 @@ Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
 Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P.
 Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
 Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps).
-Proof.
-  intros (Ps1&Ps2&->)%elem_of_list_split.
-  rewrite !big_sep_app /=. rewrite assoc (comm _ _ P) -assoc.
-  by apply sep_mono_r, wand_intro_l.
-Qed.
+Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed.
 
 (** ** Persistence *)
 Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps).
@@ -233,10 +229,8 @@ Section list.
     l !! i = Some x →
     ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ list] k↦y ∈ l, Φ k y)).
   Proof.
-    intros Hli. apply big_sep_elem_of_acc. revert Φ l Hli.
-    induction i as [|? IH]=>Φ [] //= y l; rewrite imap_cons.
-    - intros [=->]. constructor.
-    - intros ?. constructor. by apply (IH (_ ∘ S)).
+    intros Hli. apply big_sep_elem_of_acc, (elem_of_list_lookup_2 _ i).
+    by rewrite list_lookup_imap Hli.
   Qed.
 
   Lemma big_sepL_lookup Φ l i x :

prelude/list.v

@@ -1292,6 +1292,15 @@ Lemma imap_fmap {B C} (f : nat → B → C) (g : A → B) l :
   imap f (g <$> l) = imap (λ n, f n ∘ g) l.
 Proof. unfold imap. generalize 0. induction l; csimpl; auto with f_equal. Qed.
 
+Lemma imap_const {B} (f : A → B) l : imap (const f) l = f <$> l.
+Proof. unfold imap. generalize 0. induction l; csimpl; auto with f_equal. Qed.
+
+Lemma list_lookup_imap {B} (f : nat → A → B) l i : imap f l !! i = f i <$> l !! i.
+Proof.
+  revert f i. induction l as [|x l IH]; intros f [|i]; try done.
+  rewrite imap_cons; simpl. by rewrite IH.
+Qed.
+
 (** ** Properties of the [mask] function *)
 Lemma mask_nil f βs : mask f βs (@nil A) = [].
 Proof. by destruct βs. Qed.
@@ -1401,6 +1410,8 @@ Proof.
   revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto.
   by rewrite Permutation_swap, <-(IH i).
 Qed.
+Lemma elem_of_Permutation l x : x ∈ l → ∃ k, l ≡ₚ x :: k.
+Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed.
 
 (** ** Properties of the [prefix_of] and [suffix_of] predicates *)
 Global Instance: PreOrder (@prefix_of A).