From b71c0f9559a6c92029e797c3ab3620a51a85c2b5 Mon Sep 17 00:00:00 2001
From: Yishuai Li
Date: Mon, 6 Jan 2020 11:23:07 -0500
Subject: stdlib List: add [remove'] and [count_occ']

---
 doc/changelog/10-standard-library/11350-list.rst |  5 +++++
 theories/Lists/List.v                            | 25 ++++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 doc/changelog/10-standard-library/11350-list.rst

diff --git a/doc/changelog/10-standard-library/11350-list.rst b/doc/changelog/10-standard-library/11350-list.rst
new file mode 100644
index 0000000000..52c2517161
--- /dev/null
+++ b/doc/changelog/10-standard-library/11350-list.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  ``remove'`` and ``count_occ'`` over lists,
+  alternatives to ``remove`` and ``count_occ`` based on ``filter``
+  (`#11350 <https://github.com/coq/coq/pull/11350>`_,
+  by Yishuai Li).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 38723e291f..b3afbd4730 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1391,6 +1391,31 @@ End Fold_Right_Recursor.
       intros f g H l. rewrite filter_map. apply map_ext. assumption.
     Qed.
 
+    (** Remove by filtering *)
+
+    Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
+
+    Definition remove' (x : A) : list A -> list A :=
+      filter (fun y => if eq_dec x y then false else true).
+
+    Lemma remove_alt (x : A) (l : list A) : remove' x l = remove eq_dec x l.
+    Proof with intuition.
+      induction l...
+      simpl. destruct eq_dec; f_equal...
+    Qed.
+
+    (** Counting occurrences by filtering *)
+
+    Definition count_occ' (l : list A) (x : A) : nat :=
+      length (filter (fun y => if eq_dec y x then true else false) l).
+
+    Lemma count_occ_alt (l : list A) (x : A) :
+      count_occ' l x = count_occ eq_dec l x.
+    Proof with intuition.
+      unfold count_occ'. induction l...
+      simpl; destruct eq_dec; simpl...
+    Qed.
+
   End Filtering.
 
 
-- 
cgit v1.2.3