[stdlib] filter_length

[haansn08]

Adds filter_length: length (filter l) <= length l.

[andres-erbsen]

Thank you for the contribution. I left some suggestions inline.

[andres-erbsen]

@coqbot run ci

[JasonGross]

Do we also want something like length (filter f l) + length (filter (fun x => negb (f x)) l) = length l?

[andres-erbsen]

I agree that accepting a mere inequality as "the" lemma for length of filter seems dissatisfying in some way, but I don't see where I'd want a lemma where the implied length is expressed in terms of filter itself or using essentially a reimplementation of it such as sum (map Nat.of_bool . ). Thus, I am inclined to stick with the proposed version.

[andres-erbsen]

@coqbot run full ci

[haansn08]

Maybe we rename the lemma filter_length_le and an equality condition filter_length_iff: length (filter l) = length l <-> forallb l?

[olaure01]

Do we also want something like length (filter f l) + length (filter (fun x => negb (f x)) l) = length l?

For this, I would probably go through partition by adding something like:

Lemma partition_filter A f (l : list A) : partition f l = (filter f l, filter (fun x => negb (f x)) l).

(then you can use partition_length).

[haansn08]

@olaure01 Done. I also split up filter_length_iff as you suggested.

[andres-erbsen]

Just naming suggestions.

[andres-erbsen]

Ok, looks good. Please add a changelog entry.

[haansn08]

@andres-erbsen Ok, changelog entry added and commits squashed.

[andres-erbsen]

@coqbot run full ci

I intend to merge if CI passes

[andres-erbsen]

@coqbot merge now

[coqbot-app]

@andres-erbsen: You cannot merge this PR because:

• No milestone has been set.

[andres-erbsen]

@coqbot merge now