Add `filter_reverse`, `head_filter_Some`, `last_filter_Some` lemmas

Added the lemma:

Lemma last_filter_postfix P `{!∀ x : A, Decision (P x)} l x
  last (filter P l) = Some x →
  ∃ l1 l2, l = l1 ++ [x] ++ l2 ∧ Forall (λ z, ¬ (P z)) l2.

(and its counterpart for head)

The lemmas seem useful and general enough to fit in stdpp. The last lemma derives the property Forall (λ z, ¬ (P z)) l2 of the postfix of a split l1 ++ [x] ++ l2 for a list l whenever last (filter P l) = Some x.

theories/list.v

@@ -2028,6 +2028,34 @@ Proof.
   apply list_filter_iff. naive_solver.
 Qed.
 
+Lemma last_filter_postfix `{!EqDecision A} P
+      `{!∀ x : A, Decision (P x)} l x :
+  last (filter P l) = Some x →
+  ∃ l1 l2, l = l1 ++ [x] ++ l2 ∧ Forall (λ z, ¬ (P z)) l2.
+Proof.
+  intros Hl.
+  assert (P x) as HPx.
+  { by eapply elem_of_list_filter, last_Some_elem_of. }
+  pose proof (elem_of_list_split_r l x) as (l1&l2&->&Hinl2).
+  { by eapply elem_of_list_filter, last_Some_elem_of. }
+  exists l1, l2.
+  split; [done|].
+  induction l2 as [|z l2 IHl2]; [done|].
+  apply not_elem_of_cons in Hinl2. destruct Hinl2 as [Hneq Hnin].
+  rewrite filter_app, filter_cons_True, filter_cons, last_app_cons in Hl; [|done].
+  destruct (decide (P z)).
+  + rewrite last_cons_cons in Hl.
+    assert (last (filter P l2) = Some x) as Helemof.
+    { destruct (filter P l2); [by inversion Hl|done]. }
+    apply last_Some_elem_of in Helemof.
+    pose proof (elem_of_list_filter P l2 x) as [Helemof' _].
+    specialize (Helemof' Helemof).
+    by destruct Helemof' as [_ Helemof'].
+  + apply Forall_cons; [done|].
+    eapply IHl2; [|done].
+    by rewrite filter_app, filter_cons_True, last_app_cons.
+Qed.
+
 (** ** Properties of the [prefix] and [suffix] predicates *)
 Global Instance: PartialOrder (@prefix A).
 Proof.