diff options
Diffstat (limited to 'theories/Lists/List.v')
| -rw-r--r-- | theories/Lists/List.v | 25 |
1 files changed, 25 insertions, 0 deletions
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. |