[ new ] notions of finiteness #2017

laMudri · 2023-07-09T22:48:45Z

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:

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

Reference: https://math.stackexchange.com/questions/4285348/is-there-a-definition-of-finite-sets-such-that-it-can-be-used-to-constructively/4285367#4285367

Saransh-cpp · 2023-07-11T19:11:46Z

Some thoughts (or queries) -

finite setoid #863 recommends using the name StronglyFinite. Should it be named StronglyFinite or StrictlyFinite?
Upload file Relation.Unary.Enumerable to stdlib #2005 recommends creating IsStronglyFinite as the predicate with n as a parameter and StronglyFinite as the Bundled version. Should I still do that?
Upload file Relation.Unary.Enumerable to stdlib #2005 and finite setoid #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

laMudri · 2023-07-12T10:57:44Z

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.

Saransh-cpp · 2023-07-12T17:25:47Z

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.

JacquesCarette · 2023-07-13T18:56:03Z

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.

JacquesCarette · 2023-07-13T18:57:15Z

src/Function/Bundles.agda

      cong       : to Preserves _≈₁_ ⟶ _≈₂_
      surjective : Surjective to

+    function : Func


This is a very big change (important name, etc). I would not want to try to sneak this in to this PR.

Yeah, I'd be happy to have a separate PR for this. It seemed like a bug-fix, given that all of the surrounding records have a similar definition.

JacquesCarette · 2023-07-13T19:09:55Z

src/Relation/Nullary/Finite/Setoid.agda

+Ω : ∀ p → Setoid (lsuc p) p
+Ω p = record
+  { Carrier = Set p
+  ; _≈_ = λ P Q → (P → Q) × (Q → P)


This function is ⇔. And I just notice a bug: this very same definition is repeated as ⇔ (same name, entirely different file).

In the latter, we also find ⇔-setoid which is Omega.

I think Function.Equivalence is marked for deprecation in v2.0.0; hence, the repetition?

Indeed, I missed that part - well spotted!

Yeah, Function.Equivalence, Function.Injection, &c have been pre-deprecated for a long time (since the inception of Function.Bundles, probably). Both definitions of _⇔_ are unfortunate in that the congruence fields become entirely redundant, which is a (post hoc) justification for this much simpler (P → Q) × (Q → P) type. As for ⇔-setoid, maybe I'm biased by the particular use of it here, but it seems like a terrible name. It's not just some random setoid made out of the notion of equivalence; it's the setoid of propositions.

I agree, but I don't want this to explode any more than it already has!

JacquesCarette · 2023-07-13T19:11:59Z

src/Relation/Nullary/Finite/Setoid.agda

+    }
+  }
+
+Subset : Setoid c ℓ → (p : Level) → Set (c ⊔ ℓ ⊔ lsuc p)


Surely something like these two (Subset and FullSubset) already exist in stdlib elsewhere? Or should, independently.

There is Data.Fin.Subset but the definition is very different.

The names might be quite different.

JacquesCarette · 2023-07-13T19:13:39Z

src/Relation/Nullary/Finite/Setoid.agda

+FullSubset : {X : Setoid c ℓ} → Subset X 0ℓ
+FullSubset = record { to = λ _ → ⊤ }
+
+record EquivalenceRelation (X : Setoid c ℓ) r : Set (c ⊔ ℓ ⊔ lsuc r) where


I'm quite sure that all the definitions from EquivalenceRelation to include-/ do not belong in this file (or even this PR). Some of them likely already exist while others are non-trivial new items that should be in a separate PR.

These are used in lemma→ and lemma←. Should these also go in a different PR?

I think so. It might well turn out that you'll need a preliminary PR or two to set up the groundwork for this one.

JacquesCarette · 2023-07-13T19:14:39Z

src/Relation/Nullary/Finite/Setoid.agda

+  open Setoid X
+  open EquivalenceRelation R
+
+record IsStronglyFinite (X : Setoid c ℓ) (n : ℕ) : Set (c ⊔ ℓ) where


Above these, there should be comments as to the origin of the names (with links).

I could not find an origin for the name StronglyFinite. There are a few references that define finite sets or a notion of finiteness but I could not see any of them using StronglyFinite in particular -

Dependently typed programming with finite sets

Brent's Yorgey's PhD thesis

Towards Certifiable Implementation of Graph Transformation via Relation Categories

Which one should I cite? Or should it be the GitHub comment where StronglyFinite popped up for the first time?

Probably FinitelyEnumerable is closer to what's used out there.

Loking at the references, Dependently typed programming with finite sets introduces "finitely enumerable" for the first time. It classifies the notion of finiteness using some other references -

Intuitionistic frameworks give rise to a rich variety of notions of finiteness that collapse classically. In [8], [5] and [14], the author describe various concepts of finiteness and their interrrelation. According to their classification, this paper focuses on the strongest notion of finiteness, namely, finitely enumerable (listable) sets.

[8] talks about "Enumerated" sets which I found to be the closest here.

A set A will be said to be enumerated, or simply finite, noted A ε F when there is a list of all its elements. We call such a list an enumeration of A.

I also found https://github.com/agda/agda-finite-prover, which looks somewhat relevant here.

Enumerated is another excellent name.

Spiwack and Coqand unfortunately use rather vague wording in our definition of interest:

Definition
A set A will be said to be enumerated, or simply finite, noted A ε 𝓕 when there
is a list of all its elements. We call such a list an enumeration of A.

I think this means ∃xs : List A. ∀x : A. x ∈ xs, which allows for duplicates in the list. This is equivalent to FinitelyEnumerable from this PR:

Proof
(enumerated → FinitelyEnumerable): Let size be the length of the list xs. The function is given by lookup. This is surjective by the fact that for every x, we have an e : x ∈ xs, and we can take the index of e, which lookup maps to x.
(FinitelyEnumerable → enumerated): The list is given by the tabulation of the surjective function. Given an x : A, it is in the tabulation by surjectivity.

I think this discussion, if anything, motivates the name StronglyFinite. It is stronger than all of these other commonly studied notions of finiteness, and is perhaps the strongest notion we could reasonably call “finiteness”. Definitely, if we had univalence, then any property stronger than “∃ n. it's equivalent to Fin n” precludes the type Fin n for some n. If StronglyFinite is strictly stronger than the other notions of finiteness being discussed, we could ask whether it's worth having in the library at all. I think it is. For example, when people talk about categories whose objects are finite sets, I think they nearly always mean strongly finite sets. Also, I can imagine that strong finiteness is too trivial to mention in pen-and-paper mathematics, because you could just say Fin n instead, but I think people genuinely do want to talk about sets which are strongly finite in Agda.

Anyway, it's important that we get these things right, so thanks for doing the research. I don't have a good enough intuition on the three later (weaker) definitions from the same paper, but hopefully one of them is equivalent to being subfinitely enumerable (if I had to put money on it, I'd go with bounded size, because it seems to have similar properties). I guess it would be good to have all of these list-based definitions in the library too, connected with the appropriate equivalence/inclusion proofs to the definitions already in this PR. It would help get rid of some definitions without proofs.

I certainly very happy to stick to StronglyFinite !

JacquesCarette · 2023-07-13T19:17:27Z

src/Relation/Nullary/Finite/Setoid.agda

+    size : ℕ
+    srj : Surjection (≡.setoid (Fin size)) X
+
+record SubFinitelyEnumerable (X : Setoid c ℓ) c′ ℓ′


The 'source literature' here is silly with its names, and this is copied here.

InjectsIntoFinitelyEnumerable ? And then SurjectionFromFinitelyEnumerable ?

laMudri · 2023-07-13T19:58:27Z

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

Saransh-cpp · 2023-07-13T22:16:57Z

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.

jamesmckinna · 2024-09-05T05:26:57Z

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

JacquesCarette · 2024-12-06T16:06:06Z

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.

laMudri added 3 commits July 9, 2023 22:59

[ new ] notions of finiteness and equivalence proofs

86ed98d

Reference: https://math.stackexchange.com/questions/4285348/is-there-a-definition-of-finite-sets-such-that-it-can-be-used-to-constructively/4285367#4285367

[ minor ] clean up unused parts and names

d26418a

[ minor ] add header and options

8efb395

Saransh-cpp force-pushed the subfinitely-enumerable branch from da6aa3a to 7a7350e Compare July 13, 2023 16:47

JacquesCarette requested changes Jul 13, 2023

View reviewed changes

Saransh-cpp mentioned this pull request Jul 13, 2023

[ new ] notions of finiteness #2022

Closed

Saransh-cpp force-pushed the subfinitely-enumerable branch from 1d7a0f0 to 8efb395 Compare July 13, 2023 22:09

jamesmckinna mentioned this pull request Mar 25, 2024

finite setoid #863

Open

jamesmckinna mentioned this pull request Dec 6, 2024

[ project ] merge PRs #2017 and #2022 #2511

Open

JacquesCarette closed this Dec 6, 2024

[ new ] notions of finiteness #2017

[ new ] notions of finiteness #2017

Uh oh!

Conversation

laMudri commented Jul 9, 2023

Uh oh!

Saransh-cpp commented Jul 11, 2023

Uh oh!

laMudri commented Jul 12, 2023

Uh oh!

Saransh-cpp commented Jul 12, 2023

Uh oh!

JacquesCarette commented Jul 13, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

laMudri commented Jul 13, 2023

Uh oh!

Saransh-cpp commented Jul 13, 2023

Uh oh!

jamesmckinna commented Sep 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JacquesCarette commented Dec 6, 2024

Uh oh!

Uh oh!

jamesmckinna commented Sep 5, 2024 •

edited

Loading