Upload file `Relation.Unary.Enumerable` to stdlib

[Sofia-Insa]

Upload file Relation.Unary.Enumerable to stdlib with one record IsEnumerable

changes declared in CHANGELOG.md

[jamesmckinna]

So I think of Unary, Binary as qualifiers to Relation as defining unary etc. predicates on a given set.

Here you've defined a property of sets in general.

So, somewhat unfortunately (I continue to find it a very awkward naming convention), I think I am right in saying that such properties belong instead under Relation.Nullary. (Along the analogy with Decidable... and indeed, an Enumerable of size 2 had better be equivalent to such a thing?)

Can one of the 'true' experts please confirm this?

Likewise, I think the preferred naming of the concept would/should be simply Enumerable (On the linguistic model/analogy that the compound P A be read as "A is/has property P... so we wouldn't typically want to say/write "A is IsEnumerable" for example)

[Taneb]

I don't qualify as a "true" expert if @jamesmckinna doesn't, but I agree: this should go under Relation.Nullary.

Also, this seems to be only finitely enumerable. Maybe Finite would be a better name for it? Although I'd like to see an actual Enumerable as well.

[jamesmckinna]

Alternatively/additionally, you might wish to factor out as an IsP/HasP record the property of being 'of size n', with Enumerable then being the 'bundled' form which packages the size n and the 'of size n' property...?

[jamesmckinna]

And as for Finite vs. `Enumerable', I'd be inclined to agree with @Taneb , were the many intuitionistically distinct notions of 'finite'ness not already a minefield.

Suggest instead, somewhat reluctantly given the verboseness: FinitelyEnumerable (groan)

[JacquesCarette]

Just to be clear, I've asked @Sofia-Insa to "port" some things from a library of mine to stdlib. That library was developed with a slightly different context in mind, which is what is creating some of these issues. All of which do need to be fixed. [I'm mostly saying this so that the blame goes to me.]

On tightening imports: absolutely. What made it to this PR was already better than the starting point...

I completely despise Relation.Nullary. Awful naming scheme. However, I currently have nothing better to offer, and agree that that is where current conventions say this should go.

I also agree that IsEnumerable should be the predicate with n as a parameter and Enumerable should be the Bundled version.

I don't like Finite for the name as there are too many constructive definitions of Finite which end up being different. #863 calls this StronglyFinite. I kind of prefer that over FinitelyEnumerable ? Not strongly (ha!) though. There are relevant discussions in #1881 and #1770.

I agree about having more properties (and I already have some of these, so they'd be incoming as well). I think it's better to first settle on the many issues brought up here, then submit a new PR with additional properties.

[jamesmckinna]

I think @gallais 's suggested additions would make this a 'better' PR, and now that you (@Sofia-Insa) have cut your teeth on some smaller PRs, working up to a slightly bigger one seems like a worthwhile progression?

Regarding closure properties (but I think there may also be prior work on the (Near)Semiring structure on Set? Can't remember where/when/who though?)

• [ ] closure under Sum should be straightforward
• [ ] closure under Product: row order or column order? I guess the former makes more sense for the generalisation to dependent product?

Regarding naming (for all authors/reviewers to consider), some alternative suggestions spring to mind, but these can all (?) be fixed put at the end, once the module contents stabilise:

• [ ] should enumerate be called toList for uniformity/consistency with other aspects of the library?
• [ ] ditto. enumerated: toList∈?
• [ ] regarding the *Finite designations, I guess I'd be OK with StronglyFinite, except that I don't personally find Strongly an especially helpful qualifier, as it's not entirely clear to me what the (linear?) ordering by 'strength' of these things is supposed to be...

[Taneb]

I'd be a lot happier with StronglyFinite if we also had a WeaklyFinite with the appropriate implication

[gallais]

Also: should this be generalised to an arbitrary setoid? The use of _↔_ forces propositional equality but A could have a more interesting structure than that!

[jamesmckinna]

Also (though this is perhaps marginal?):

• [ ] toList or toVec, given that the size is statically known?
• [ ] if generalised to Setoid, do we end up needing to proliferate the number, and types, of enumerations in the presence of eg DecSetoid to ensure no duplications in the enumeration?

[gallais]

Can we not prove the no duplication just from the bijection assumption?

[JacquesCarette]

Yes, we should absolutely generalize this to an arbitrary setoid. And indeed, the bijection is enough to prove no duplication.

Note that since Fin n has decidable equality, setoid A will automatically have a DecSetoid structure.

The discussion does bring to mind a philosophical question of stdlib development: should it be allowed to be small-step incremental, or only big complete chunks are wanted? [Personally, given the current slow growth, I would vote for small-step; once we get to a dozen PR/day (I think Lean gets even more), obviously that can be revisited.]

[gallais]

I am not sure I agree. It is common to get definitions subtly wrong and we often only discover that when trying to prove results. In which case adding a single definition means that we may need to make backwards incompatible changes in the future to patch the issue. Which will be a pain.

E.g. the fact we want a Setoid arises when we start thinking of proving that if A and B are finite then so is A -> B.

[JacquesCarette]

That's an excellent point. Ok, I have to agree, as I've witnessed "subtly wrong" sufficiently many times. Sigh.

[JacquesCarette]

I've converted this PR to Draft, so that it can be augmented to be more full-featured regarding (at least) finite enumerability.

[jamesmckinna]

Thanks @JacquesCarette and due apologies to @Sofia-Insa for getting caught up in a longer-running, but important, debate about library design, and with it, the role and size of PRs

My own thinking, for what it's worth, is that I (could be persuaded to) prefer 'small' PRs when there is an 'easy'/label:low-hanging-fruit issue at stake.

But a lot of label:addition PRs represent ... well, choices where things may, indeed, be "subtly wrong", so I hope that everyone can entertain the debate in a constructive fashion. And that involves both the mathematics, as here, and its implementation in type theory...

[jamesmckinna]

Apologies for not understanding bijections between Sets and DecSetoids... my brain too full of other stuff to have thought things through properly. But then, all the more so: flatten to a List, or to a (Functional) Vec?

[gallais]

But then, all the more so: flatten to a List, or to a (Functional) Vec?

Probably every single one of them using the toList, toVec, (toFresh?) naming scheme you suggested earlier.

[MatthewDaggitt]

Sorry, I've missed most of this conversation. I agree with all the conclusions, i.e. Relation.Nullary, extending it to Setoid, and in this case when introducing new definitions they should have at least a small selection of proofs about them to show the definition is reasonable.

[jamesmckinna]

What are the current plans for this PR @Sofia-Insa , @JacquesCarette ? (Besides: rebasing to fix the CHANGELOG merge conflicts with the up-to-date v2.0 release version?)

[JacquesCarette]

Another one that I should take over. I most definitely want to continue pushing on this.

[MatthewDaggitt]

@JacquesCarette any chance you plan to pick this up in the next couple of weeks? Otherwise, I'll post a link to this discussion in the original issue and then close this as there's not very much code here.

[JacquesCarette]

Next couple of weeks? Unfortunately not so likely, sorry.