agda-stdlib [ new ] notions of finiteness

This PR contains a rough draft of some definitions of constructively well behaved notions of finiteness for setoids, based on this math.se answer. Included are the proofs that the two definitions of subfinitely enumerable are logically equivalent (lemma→ and lemma←). It is a fairly direct transcription, perhaps meaning that we miss out on idiomatic uses of lists rather than Fin.

Clear problems to be resolved before this is merged:

The whole development is in a single file.
[ ] Some of the earlier definitions should be dispersed throughout the library.
[ ] A place should be found in the stdlib hierarchy for a Finite module.
Some of the names are bad/questionable.
[ ] SubFinitelyEnumerable and SubfinitelyEnumerable differ only in case (analogous to the presence/absence of a hyphen in the reference answer).
[ ] lemma→, lemma←
[ ] Maybe inj and srj fields should not have abbreviated names.
[ ] Direct image, _[_], has a name which might cause clashes. I don't use it here, but I thought I'd include it together with the inverse image _[_]⁻¹. These two should be named as a pair.
[ ] Setoid quotient, _/_, might also clash.
General code quality problems:
[ ] Some of the supporting definitions may have duplicates in the library. I didn't check carefully.
[ ] Subset and EquivalenceRelation are conceptually related, but are named and implemented completely differently. We should think carefully about how we want to deal in general with predicates/relations which respect setoid equality.
[ ] Some of the proofs are probably too inlined (particularly extended λ-abstractions).
[ ] The definition of the equivalence relation R is a bit gnarly, with its 5-place iterated Σ-type. I'm following the reference answer here, but maybe it (together with the resulting quotient) could be defined in a more symmetric way, reflecting the symmetry of the pushout construction being performed.
[ ] I'm not making use of any particulars of Fin, so maybe the whole development could/should be generalised to arbitrary cardinalities.

Related PR: #2005 cc @JacquesCarette @Sofia-Insa

Jul 09 '23 22:07 laMudri

Some thoughts (or queries) -

#863 recommends using the name StronglyFinite. Should it be named StronglyFinite or StrictlyFinite?
#2005 recommends creating IsStronglyFinite as the predicate with n as a parameter and StronglyFinite as the Bundled version. Should I still do that?
#2005 and #863 recommend the file should go in Relation.Nullary.Finite.Setoid with a corresponding Propositional module. Should we have the Finite and Enumerable records in Relation.Nullary.Finite.Setoid and the lemmas in Propositional?

More work here (that I will be carrying out)

Closure over sum and product
toList, toVec, toVector functions

I am supposed to take over this and #2005, but I cannot directly push to this branch. How should I proceed ahead with this? Should I create a new PR with @laMudri's code and then work on it with reviews? I think I will start with the checklist mentioned above and ask for help on the way 🙂

cc: @JacquesCarette

Jul 11 '23 19:07 Saransh-cpp

Hi! You must be Jacques' student. I'm happy to give you push access to this branch, in case that's the easiest solution. As for your points:

Yeah, now you mention it, I like StronglyFinite. I think it is indeed the strongest notion of finiteness, while “strict” can mean other things (e.g, I think a “strict setoid” is a setoid whose equivalence relation is propositional equality).
It fits a common pattern to have these unbundled versions, but given that IsStronglyFinite X n = Inverse X (≡.setoid (Fin n)), are we gaining anything by introducing such a definition? Particularly, in view of my last to-do item (if it works out), we just end up with aliases of Inverse, Injection, and Surjection. Perhaps these would be beneficial for the subfinitely enumerable definitions, though. Going the other way, it might be worth creating more bundled definitions, where X too is a field.
Yeah, looking around the previous work, there seems to be a consensus around the Relation.Nullary hierarchy. I don't fully understand why, but it seems plausible. I guess that's where Dec lives. I thought anyway there was promise that these Nullary/Unary/Binary/c hierarchies would be done away with soon.
As for a Propositional module, the earlier definitions would adapt fine to Sets (just precompose with ≡.setoid), but the two subfinitely enumerable definitions would have problems. Both mention the existence of some Apex setoid, so even if you start out with a set and finish with a Fin n, you have to go through setoids. This use of setoids is crucial for the equivalence proofs, because we need quotients to produce the apex in both directions. Probably I would omit the subfinitely enumerable definitions from a Propositional module, because they don't behave as intended.
For the last question, do you mean Properties at the end? Personally, I think modules like Data.List.Relation.Unary.All.Properties are filled with things that aren't properties of All, and instead are just the basic constructions of All (despite being property-like for List). This leaves properties of All (e.g, equations between expressions of All type) with nowhere to go except this really big Properties module. If I can get any sympathy for this view, then I think the equivalences and constructions should go either in the same module as the definitions, or in some sort of Construct module.
The extra work all sounds like worthwhile things to do. I wonder whether toList gives rise to equivalence proofs with alternative definitions of finiteness in terms of lists.
I guess some low-hanging fruit is to provide coercions from stronger notions to weaker notions, if you can think of some reasonable names.

Jul 12 '23 10:07 laMudri

Hi, yes! Thanks for the detailed discussion and the invite to the repository! I've started working on this locally.

It fits a common pattern to have these unbundled versions, but given that IsStronglyFinite X n = Inverse X (≡.setoid (Fin n)), are we gaining anything by introducing such a definition? Particularly, in view of my last to-do item (if it works out), we just end up with aliases of Inverse, Injection, and Surjection. Perhaps these would be beneficial for the subfinitely enumerable definitions, though. Going the other way, it might be worth creating more bundled definitions, where X too is a field.

I don't really have an opinion here. I'll leave this up to you and other maintainers 🙂

I thought anyway there was promise that these Nullary/Unary/Binary/c hierarchies would be done away with soon.

Oh, I see. A lot of API changes before 2.0.0

As for a Propositional module, the earlier definitions would adapt fine to Sets (just precompose with ≡.setoid), but the two subfinitely enumerable definitions would have problems. Both mention the existence of some Apex setoid, so even if you start out with a set and finish with a Fin n, you have to go through setoids. This use of setoids is crucial for the equivalence proofs, because we need quotients to produce the apex in both directions. Probably I would omit the subfinitely enumerable definitions from a Propositional module, because they don't behave as intended.

What exactly is supposed to in the Propositional module? Is it supposed to have a different version of StronglyFinite which takes a Set instead of a Setoid? I'm not very sure I understood this very well.

For the last question, do you mean Properties at the end?

Yes, my bad, I meant Properties. I can maybe start working on them in the Properties and see how it goes with the reviews.

Jul 12 '23 17:07 Saransh-cpp

Re IsStronglyFinite: we actually gain quite a lot of type inference by making it a 1-constructor data (less sure about 1-field record ?). The extra indirection makes operating over it a bit more annoying. I think the original suggestion was to make these uniform with respect to the other algebraic structures in Agda.
Not a big fan of Nullary either, but that is how 2.0 is being done, so we go along.
Propositional is short for PropositionalEquality and is the version that hard-wires ≡.setoid.

I will also comment on the current code regarding a number of other items.

Jul 13 '23 18:07 JacquesCarette

Re IsStronglyFinite: we actually gain quite a lot of type inference by making it a 1-constructor data (less sure about 1-field record ?). The extra indirection makes operating over it a bit more annoying. I think the original suggestion was to make these uniform with respect to the other algebraic structures in Agda.

In this case, ≡.setoid (Fin _) is already definitionally injective (see the snippet below), so there is no gain when it comes to unification.

open import Data.Fin
open import Relation.Binary.PropositionalEquality as ≡

test : ∀ n → ≡.setoid (Fin n) ≡ ≡.setoid (Fin _)
test n = refl

Jul 13 '23 19:07 laMudri

I think it would be better to keep this PR intact and create small subset PRs. I have created #2022 to add the relevant finiteness records by picking up the first commit.

Jul 13 '23 22:07 Saransh-cpp

I think it was right to turn #2022 back to DRAFT, but probably a mistake on my part to leave comments there, rather than a more substantial review of the material here, esp. eg the discussion of Apex etc.

Related and/or candidate for deprecation in the course of this programme: Data.List.Relation.Unary.Enumerates.Setoid.IsEnumeration

Sep 05 '24 05:09 jamesmckinna

We're also closing this one, for now, in favour of project issue #2511 as it's been hanging idle for too long and still requires a lot of work.

Dec 06 '24 16:12 JacquesCarette