Add "Complete" predicate for lists that contain every element of a type

[MatthewDaggitt]

Useful for when creating list based notions of finite sets.

Waiting until after v1.6 to include CHANGELOG entry

[gallais]

We may want to bite the bullet and formalise the various notions of finiteness
discussed in this paper: https://dl.acm.org/doi/abs/10.1145/2808098.2808102

In which case we should maybe think about a naming scheme that is less specific
to this one notion?

[JacquesCarette]

I agree that formalising all of those is a good idea, and has implications for naming.

[MatthewDaggitt]

We may want to bite the bullet and formalise the various notions of finiteness
discussed in this paper: https://dl.acm.org/doi/abs/10.1145/2808098.2808102

In which case we should maybe think about a naming scheme that is less specific
to this one notion?

I agree. This is the notion of All from the paper. Unfortunately the name All is already taken so I think Complete isn't that bad of an alternative. Other suggestions are welcome though?

Note that this isn't a notion of finiteness, e.g. Listable, which is a dependent product of a list and this property. I'd imagine that definition would go in the Relation.Nullary hierarchy somewhere?

[TOTBWF]

Perhaps Enumeration?

[gallais]

I guess I would expect Enumeration to be a conjunction of Complete and Minimal
where Minimal xs = ∀ x → (p q : x ∈ xs) → p ≡ q

[MatthewDaggitt]

I guess I would expect Enumeration to be a conjunction of Complete and Minimal
where Minimal xs = ∀ x → (p q : x ∈ xs) → p ≡ q

I think you mean the existing Unique predicate instead of Minimal? The problem with Minimal is that it only works over propositional equality (unless you define the notion of equality over membership proofs). In my case I really do need finite sets over some Setoid as the true underlying type may be infinite, and it's only when quotienting by my notion of equality that it becomes finite.

[gallais]

I think you mean the existing Unique predicate instead of Minimal?

I guess these two are distinct formalisation of the same idea.

The problem with Minimal is that it only works over propositional equality (unless you define the notion of equality over membership proofs).

Right it does assume uniqueness of setoid-equality proofs when I guess you could have a weaker form
of minimality by only insisting that the two membership proofs are pointing at the same index,
irrespective of what the stored equivalence proof is.

[MatthewDaggitt]

Okay, so I think the conversation has got a little sidetracked. I agree that it would be desirable to add the notions of finiteness in that paper to the library.

The definition of Complete is exactly the equivalent to the All definition in the paper, and so I think this is a good first step in doing so. Obviously we can't use the name All again, so unless anyone has any objections to the name Complete in the next couple of days I propose to merge this in?

[andreasabel]

Great initiative!

I think Enumeration is the term that would make this structure easier discoverable. "Complete" is less specific. Enumeration is a mathematically correct term for this (https://en.wikipedia.org/wiki/Enumeration), as it does not necessitate a unique enumeration. Maybe a unique enumeration could then simply be called UniqueEnumeration.

FWIW, I implemented a simple version of Enumeration at https://github.com/andreasabel/agda-scope/blob/aad6e9e7a87406f3f26e05caf802b407fe96ee2c/micro/Library.agda#L80-L117

[MatthewDaggitt]

I'm happy to rename this to Enumerates to mimic your development @andreasabel.