How to represent assertions about contents of lists?

Stream: new members

[aron]

I want to represent certain assertions about lists, something like that the list in question contains at least 3 items for which a given predicate is true. Or at most 5 items for which it's true. Or exactly 2 items. Or anything in between.

But I'm struggling to think of how best to represent this sort of thing. As a refinement type containing a pair of list and predicate function, along with a proposition about (List.filter predicate list).length? As an inductive type representing the assertion? Or something else?

[Edward van de Meent]

I suspect the List.filter version will be the simplest way to do this.

[Edward van de Meent]

Particularly since that doesn't need lots of new API

[Daniel Weber]

You could also use docs#List.countP