diff options
| -rw-r--r-- | doc/changelog/10-standard-library/11350-list.rst | 5 | ||||
| -rw-r--r-- | theories/Lists/List.v | 25 |
2 files changed, 30 insertions, 0 deletions
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 74335da2f1..2e8af3ecb9 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1630,6 +1630,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. |