Fintype vs. Finite

Stream: general

[Mirek Olšák]

Can someone explain me why we have the Fintype / Finite distinction? I would find it nice to have a typeclass with explicit canonical enumeration of the elements (without needing choice for it) but none of it is Fintype / Finite -- Finite is just a Prop, and Fintype hides the order in a Multiset. It can become annoying how they support different features.

Fintype often needs DecidableEq, such as Pi.instFintype. So when working with abstract finite types, it can become lengthy to add this assumption everywhere. Ok, I read the description of Finite saying

Definitions should prefer Finite, unless it is important that the definitions
are meant to be computable in the reduction or #eval sense.

so I switch to using Finite everywhere and hoping to not having to care... but

• Finite doesn't have a cardinality measure like Fintype.card. Ok maybe I should use Nat.card
• Then I cannot straightforwardly compare

example {α : Type} [Finite α] (s : Finset α) : s.card ≤ Nat.card α := by exact? -- `exact?` could not close the goal

(I can after some massaging of translating into Set.ncard or to Fintype but it is more steps then should be)

• Fintype has its bundled version FintypeCat, not Finite... maybe I should just use CategoryTheory.Bundled Finite to work with Finite then?

[Andrew Yang]

Yes Nat.card is exactly what you should use. Is there a reason why you need to work with Finset and not Set.Finite?

[Jakub Nowak]

Finset is to Set.Finite kinda like Fintype is to Finite. Although Finset additionally had bundled data. Mixing Finite and Finset is probably not a good idea and you might prefer to use Set.Finite.

[Jakub Nowak]

Or use Fintype and Finset. You can use e.g. variable {α : Type*} [Fintype α] [DecidableEq α] to not have to repeat DecidableEq in every definition.

[Kyle Miller]

Doesn't the doc string for docs#Finite explain the benefit of Finite? It's a Prop, so you avoid the defeq issues Fintype and DecidableEq have.

Something else the docstring explains is that if you need to work with Fintype API then you can add

  have := Fintype.ofFinite α

For example

import Mathlib

example {α : Type} [Finite α] (s : Finset α) :
    s.card ≤ Nat.card α := by
  have := Fintype.ofFinite α
  simpa using Finset.card_le_univ s

Finite was added after Fintype, and there's been inertia switching over.

I would find it nice to have a typeclass with explicit canonical enumeration of the elements

An important part of Fintype is that up to equality there's at most one Fintype instance; having an explicit enumeration would be a different type. That class does exist though: docs#FinEnum

[Mirek Olšák]

Thanks, I will look into FinEnum too.

[Mirek Olšák]

What about the FintypeCat? Is there an intention to turn it into FiniteCat?

[Mirek Olšák]

Sometimes bundled things are better... For example I want a mapping from X to finite types, and otherwise, I would need an universally quantified predicate... (also why I can see Finset useful)

[Kyle Miller]

I vaguely remember in Lean 3 trying to change FintypeCat to use Finite (well, probably finite_cat and finite back then), but the task was bigger than expected and I backed out. I'm curious if there's anyone using FintypeCat to do an actual computation.

I think it would be good to have a FiniteSet type that bundles a Set with a Set.Finite proof, a benefit being that you can use standard set operations on the FiniteSet without needing to construct a Set.Finite proof in parallel.

[Jakub Nowak]

@Kyle Miller Can you explain why people want to switch over to Finite? Tbh, I feel like we don't need Finite. We can just use Fintype and when you're working with type for which you can't create instance of Fintype, only Finite, then you can use open Classical and mark definitions as noncomputable to be able to use Fintype.

[Matt Diamond]

I believe it has something to do with the fact that Fintype instances are data and therefore not automatically equal to each other... this can lead to some annoying instance conflicts

[Kyle Miller]

@Jakub Nowak That often leads to typeclass inference picking up the wrong instances and you getting stuck in frustrating ways.

Let me flip the question: why not Finite everywhere, and leave Fintype for programming or applications of proof by reflection? If we started with Finite, do you think you would be able to convince mathematical users that "open Classical" is a necessary evil?

Consider also that instance search is lighter weight for Finite and more likely to succeed. It doesn't need to look for DecidableEq instances nor do any defeq checks, since it's just a Prop.

[Mirek Olšák]

I would have another Fintype suggestion -- what if Fintype required DecidableEq inside? Are there examples where it is useful to have Fintype without decidable equality?

[Aaron Liu]

well when you do fin_cases of course

[Mirek Olšák]

I mean an example of a type with Fintype instance which doesn't have decidable equality.

[Aaron Liu]

that would be Prop

[Mirek Olšák]

Oh, I see...

[Violeta Hernández]

As a very quick summary, Fintype is data (it contains an explicit enumeration of all elements of the type), whereas Finite is just a mathematical proposition.

[Mirek Olšák]

Violeta Hernández said:

As a very quick summary, Fintype is data (it contains an explicit enumeration of all elements of the type), whereas Finite is just a mathematical proposition.

I find this exact explanation confusing for the reason I was writing in the original post -- it does not contain an explicit enumeration, as discussed the difference between Fintype and FinEnum

[Aaron Liu]

it does contain an explicit enumeration but you're not allowed to use it unless the result is independent of which enumeration you have

[Mirek Olšák]

That is actually a sensible explanation. Although, you could also say that Finite contains an explicit enumeration but you're not allowed to use it unless the result is a proof...

[Wrenna Robson]

Yes, but that is different.

[Wrenna Robson]

FinEnum is like, "my type is finite and I've picked an ordering for it - this is the ordering".
Fintype is "my type is finite and I've got a representation of it as a finite set - it isn't ordered though"
Finite is "my type is finite, it has some size - I'm not going to tell you what though".

[Wrenna Robson]

If in pen and paper mathematics you would say "let x_i = x_0, x_1, .., x_{n-1} be a finite sequence", then that is FinEnum.
If in pen and paper mathematics you would say "let x_i be elements indexed by this finite set S", then that is FinSet.
If in pen and paper mathematics you would say "Let the set S be finite" then that is Finite.

This isn't perfect but I think it has the right form.

[Mirek Olšák]

Thanks, I think I understand it now. Although, I would say that pen & paper cannot distinguish Finite & Fintype because in standard mathematics, you get unique choice by default (there might be an official name I don't remember). If you say "there exists unique x", you just take it without hesitation (without any worry about axiom of choice). Finite says "There exists unique representation of the type as a finite set", and Fintype is the order-less finite set.

As far as I understand, Lean doesn't really care about choice / unique choice distinction but it distinguishes "having something" and "knowing it uniquely exists" for calculation purposes.

[Ruben Van de Velde]

Wrenna Robson said:

If in pen and paper mathematics you would say "let x_i = x_0, x_1, .., x_{n-1} be a finite sequence", then that is FinEnum.
If in pen and paper mathematics you would say "let x_i be elements indexed by this finite set S", then that is FinSet.
If in pen and paper mathematics you would say "Let the set S be finite" then that is Finite.

This isn't perfect but I think it has the right form.

Though I think I've quite often seen the first phrasing where the order was completely irrelevant.

[Jakub Nowak]

Wrenna Robson said:

If in pen and paper mathematics you would say "let x_i = x_0, x_1, .., x_{n-1} be a finite sequence", then that is FinEnum.
If in pen and paper mathematics you would say "let x_i be elements indexed by this finite set S", then that is FinSet.
If in pen and paper mathematics you would say "Let the set S be finite" then that is Finite.

This isn't perfect but I think it has the right form.

I think this just makes things more confusing. For me, when looking from the mathematics perspective, all three are equivalent. I think, the differentiation of FinEnum /Fintype/Finite just doesn't exists in mathematics.
EDIT: Well, nvm about FinEnum, if you have an ordering, you can make a statement about this particular ordering, that would depend on the ordering chosen. Although, I can't find a difference between Fintype and Finite from mathematics perspective. In some sense, there's no difference in Lean either, because one can convert between the two noncomputably. So I guess the problem is that there's no "computable" in mathematics?

[Kyle Miller]

Yeah @Mirek Olšák, standard mathematics doesn't distinguish between constructions and unique existence. In ZF foundations, there's no computational content to it. It's easy to forget that whenever you write an expression with $f(x)$ in it, since functions aren't primitive, implicitly you are introducing a universal quantifier (that's to say, if you have an expression $P(f(x))$, it stands for $\forall y\in Y, (x,y)\in f\to P(y)$). It's not evaluating the function exactly — you don't have "the" element.

So, I'd push back a bit on standard mathematics letting you "just take [the element] without hesitation". Certainly there's no hesitation in doing the above sort of transformation, but it does make you wonder what it means to just take the element. Similarly, when you suggested that Finite contains an explicit enumeration @Mirek Olšák, I would counter that it only stands for the mere evidence that if you do the above sort of $\forall$ transformation then the quantification will find an explicit enumeration, rather than Finite containing the enumeration itself.

In Lean, constructions are a native concept, and that's a big enough difference that (in my opinion) it's hard to truly compare what "axiom of (unique) choice" means between each system. As you said, with constructions you can actually "have something" instead of only knowing it exists. I'd also counter that standard mathematics does (or at least could) distinguish between Finite and Fintype, but there's usually not much point to; $\operatorname{Fintype}(S)$ would be the set of pairs $(n,e)$ where $n\in\mathbb{N}$ and $e$ is an element of the quotient of the set of bijections $\{0,\dots,n-1\}\to S$ by the action of the symmetric group on $\{0,\dots,n-1\}$. If you define a function $\operatorname{Fintype}(S)\to T$ you'll need to make use of the universal property of the quotient if you want access to a specific bijection in your definition, or otherwise choose a fixed representative from the equivalence class by some means.

In standard mathematics, you don't need to invoke the axiom of choice to get a witness from an existential. That's because of the above sort of transformation: the rule of inference involved when you "take" a witness is that to prove $(\exists x, P(x))\to Q$ it suffices to prove $\forall x, P(x) \to Q$. The same goes for Lean.

The axiom of choice in Lean only applies when you want to use witnesses to existentials as if they are actual constructions (granted, that's a lot of power, and it's strong enough to prove the ZFC-style axiom of choice; basically that if you have a forall-exists, you can deduce exists-forall by assembling all the witnesses using a function). In simpler cases, Classical.choice is sort of a way to say "let's apply a ZF-style function", one that was defined by proving existence of an output value, rather than actually invoking ZFC choice. I wouldn't be surprised if a lot of noncomputable functions in Lean are using Classical.choice this way, in the sense that from within proofs Classical.choice could be eliminated if you expanded all the definitions.

I think my point here (not directed to you Mirek, I'm writing primarily to make sense of all this) is that, first, just because a Lean function uses Classical.choice doesn't mean you would need to invoke ZFC choice in standard mathematics, and, second, you can in principle avoid constructions and native Lean functions and use ZF-style functions (subsets of $A\times B$) instead — it would be horrible without some elaborator to do it, but in any case I think it's worth recognizing that the Lean type A -> B is conventionally used to model the set of all ZF functions (which is justifiable using Classical.choice), especially when you're thinking about the role of choice in each logical system.

[Martin Dvořák]

Kyle Miller said:

if you have an expression $P(f(x))$, it stands for $\forall y\in Y, (x,y)\in f\to P(y)$

It seems you just made me realize something about set theory that I never realized before! Given that ZF is defined as a theory in FOL, I simply assumed that $P(f(x))$ was a call of a function symbol inside a call of a relation symbol (in the first-order sense). I was wrong! What really goes on is that $P$ and $f$ are just members of the universe (because they both are sets) and you cannot "call" any functions in set theory!

Please let me know if I got it wrong again.

[Aaron Liu]

yeah ZF in the presentation I usually see it has no function symbols

[Aaron Liu]

you can convert the axioms of union, pairing, replacement, etc. into function symbols

[Kyle Miller]

@Martin Dvořák I thought I'd mention that another valid translation to eliminate the definition of function application is $\exists y\in Y, (x,y)\in f\land P(y)$. (The forall version is to skolemization as this one is to herbrandization.)

[François G. Dorais]

Jakub Nowak said:

In some sense, there's no difference in Lean either, because one can convert between the two noncomputably. So I guess the problem is that there's no "computable" in mathematics?

Yes, that's the underlying issue... except that there is no actual _problem_ ! There is just a distinction and, as is typical, this distinction is useful to some but not to others.

[Mirek Olšák]

The problem is that whenever there is a distinction of two almost identical concepts, an annoyance arises from each of these concepts supporting a bit different features, and conversion is annoying.

[Mirek Olšák]

On the other hand, the distinction between unique choice, and choice is a bit awkwardly missing. I would find it sometimes more philosophically satisfying to know I am using only unique choice in definitions, so that the values will not depend on particular values of the choice function.

[Mirek Olšák]

And to all the ZFC discussion, I would add that ZFC models functions by uniqueness.

• small functions are defined as binary relations with unique y for each x
• the axiom of replacement conditions the class function used the same way -- for each x there must be at most one y

[Jakub Nowak]

Maybe, instead of having to make this distinction manually it would make sense to have this distinction be part of the language? Isn't Finite just noncomputable instance of Fintype? And it could work like, in computable function argument [Fintype s] will refer to computable instance, but in noncomputable function, it would refer to noncomputable instance. And we would need syntax like e.g. [noncomputable Fintype s] to refer to noncomputable instance in computable function.

[Kyle Miller]

Jakub Nowak said:

Isn't Finite just noncomputable instance of Fintype?

No it's not — Finite is a proposition, so instances of it are definitionally equal. #general > Fintype vs. Finite @ 💬

[Jakub Nowak]

Kyle Miller said:

That often leads to typeclass inference picking up the wrong instances and you getting stuck in frustrating ways.

Fintype has unique instance up to quotient, so I don't thing there are better or worse instances in this case?

Kyle Miller said:

Let me flip the question: why not Finite everywhere, and leave Fintype for programming or applications of proof by reflection? If we started with Finite, do you think you would be able to convince mathematical users that "open Classical" is a necessary evil?

Not sure what's your point? What's evil in "open Classical"? If we switch to Finite everywhere, then you would need to use classical logic whenever you want to get the elements.

[Kyle Miller]

Yes, I am saying what I'm saying while aware that Fintype is a subsingleton type. Even though Fintype is a subsingleton, two instances of Fintype T might not be definitionally equal. This means that expressions fail to unify. This problem is painfully well-known to people who use Fintype frequently, and it's why we have tactics like convert to try to get around it. This tactic inserts rewrites to unify two terms that are only propositionally equal.

If Lean were an "extensional" system — where if terms are propositionally equal then they're definitionally equal — then theoretically the problem goes away, but that comes with its own problems.

[Kyle Miller]

Jakub Nowak said:

If we switch to Finite everywhere, then you would need to use classical logic whenever you want to get the elements.

That's partly true (in proofs you can use obtain to get a particular enumeration without classical logic), but even if it took classical logic, would that be something mathematicians would care about? Mathlib is largely focused on formalizing (classical) mathematics. (Classical's in parentheses because mathematicians think "classical" means math from the Greeks, or sometimes even from just a few decades ago.)

[Kyle Miller]

Mirek Olšák said:

On the other hand, the distinction between unique choice, and choice is a bit awkwardly missing.

I've thought about that too. It would be possible to create a linter that determines whether or not a defined Lean function is "mathematical", by which I mean something like your suggestion, though I'm struggling to define it concisely.

Recall that what noncomputable means is that the Lean compiler failed to find a way to create some C code that computes the same thing, in some sense. It fails if any noncomputable functions are used in computationally relevant way. (In mathematics, values and types are relevant, but proofs are not. Possibly propositions aren't relevant either.)

I'm imagining @[nonmathematical] would mean that the "mathematics" compiler wasn't able to construct a defining equation that makes use of only "mathematical" functions; it would fail if nonmathematical functions are used in a mathematically relevant way.

So, for example, Classical.choice would be marked nonmathematical. There could be a unique choice function that the linter recognizes as mathematical:

noncomputable
def Subsingleton.choice (α : Sort _) [Subsingleton α] [Nonempty α] : α :=
  Classical.choice ‹Nonempty α›

The "mathematical compiler" could have a rule where it attempts to upgrade Classical.choice to Subsingleton.choice by synthesizing a Subsingleton instance, rather than outright fail.

I think the basic algorithm would be to check that every constant in the definition is not marked nonmathematical, ignoring those constants that appear inside of proofs.

Possibly there are some transformations you'd want it to do to avoid some false negatives. Here's a contrived example, but there are real cases of this out there:

def f (n : Nat) : {n : Nat // n < 10} :=
  have inst := Classical.choose
  ⟨n % 10, ... a proof that uses `inst` for some reason ...⟩

You could avoid flagging it nonmathematical by realizing inst is only used in proofs. A simple way to deal with this is to zeta and beta reduce everything before doing the check.

[Riccardo Brasca]

Speaking of unique choice, I am working in a project where I want to avoid choice but I added unique choice, and so far even tactics like ring usually don't create problems

[Aaron Liu]

but what about docs#Setoid.piQuotientEquiv

[Mirek Olšák]

Yes, some nonmathematical like this makes sense. Regarding the example of building an instance outside of a proof but only using it in a proof, it could be dealt with by also tracing parts of the local context as nonmathematical

[Mirek Olšák]

Perhaps it could be called ambiguous instead

[Wrenna Robson]

I do find the definitions of these things and the distinctions useful from my perspective, a semi-mathematical one

[Wrenna Robson]

It's just good moral hygiene to make sure you aren't e.g. arbitrarily assuming an order for no reason

[Wrenna Robson]

I think that learning to use Lean to formalise maths has made me a better mathematician

[Kyle Miller]

Mirek Olšák said:

Perhaps it could be called ambiguous instead

Or @[arbitrary] to signify an arbitrary choice is made.

I'd actually like to see this exist. There are some arbitrary functions in mathlib, like docs#Subspace.dualLift, where it would be nice to know that it's arbitrary and that anything using it in a relevant way is also arbitrary. Right now it's arbitrariness is recorded only in the docstring.

[Wrenna Robson]

What is an example of a noncomputable function that does not arise from an arbitrary choice, out of interest?

[Henrik Böving]

the lean annotation noncomputable or the computer science idea of noncomputable?

[TongKe Xue]

Does either of:

halts : TuringMachine -> bool
not_halts: TuringMachine -> bool

satisfy the requirement via proof of the Halting problem ?

Wrenna Robson said:

What is an example of a noncomputable function that does not arise from an arbitrary choice, out of interest?

[Mirek Olšák]

Wrenna Robson said:

What is an example of a noncomputable function that does not arise from an arbitrary choice, out of interest?

For example Nat.card, deriv, or tsum (although analysis is a bit tricky, sometimes the dummy values are taken by choice). In general any function which splits on a non-computable proposition would satisfy the criteria, so one of the most fundamental non-computable non-arbitrary functions is Classical.propDecidable.

[Wrenna Robson]

Henrik Böving said:

the lean annotation noncomputable or the computer science idea of noncomputable?

The former!

[Mirek Olšák]

And besides splitting on a Prop value, also functions that extract the unique data from a propositions, such as the Fintype.ofFinite discussed here, or Equiv.ofBijective

[Henrik Böving]

Wrenna Robson said:

Henrik Böving said:

the lean annotation noncomputable or the computer science idea of noncomputable?

The former!

Any function that calls a recursor that is not False.rec, any function that makes the compiler error for various reasons etc. noncomputable has no meaning in the theory world.

[Aaron Liu]

I think tensor products are still noncomputable because they used to take too long to compile

[Jakub Nowak]

Kyle Miller said:

No it's not — Finite is a proposition, so instances of it are definitionally equal. #general > Fintype vs. Finite @ 💬

Can't we have all noncomputable Subsingletons (instances of) be definitionally equal?

[Aaron Liu]

not if you can get data out

[Jakub Nowak]

How can you get data out of noncomputable definition?

[Kyle Miller]

noncomputable is for the compiler, and it does not have meaning for the elaborator or the kernel.

[Aaron Liu]

noncomputable def k : Nat := 1

-- k : Nat
-- this is data
#check k

[Kyle Miller]

In fact, #reduce k shows 1

[Jakub Nowak]

Ah, I see. I thought that noncomputable vs computable is like a difference between exists and sigma pair.

[Kyle Miller]

Even if it were @Jakub Nowak, it's still problematic. Using a Type instance like Fintype along with the Classical instance leads to "diamonds" very easily. Imagine on one hand having the Classical instance for the Cartesian product, and on the other having the instance that combines the Classical instances for each factor. These are not definitionally equal.

[Kyle Miller]

(Incidentally @Mirek Olšák, this diamond issue is a reason having Fintype carry a DecidableEq instance can be problematic, at least if Fintype can provide DecidableEq instances. You have to make sure both the DecidableEq and Fintype hierarchies agree on the DecidableEq instances. For what it's worth, people have pointed out before that Fintype is in a strange spot constructively, since it's not sufficient on its own for getting an element of Trunc ((n : Nat) × (α ≃ Fin n)), without the additional decidable equality. All it can do is give you Trunc ((n : Nat) × {f : Fin n → α // Function.Bijective f}). I suppose Fintype just captures the least you need to represent the universe as a List, and it's reasonable for definitions to require DecidableEq separately if they need it to be the "real" Fintype. As far as I'm aware, Fintype is not designed specifically to make a Fintype Prop instance — it's just convenient that it works out.)

[Mirek Olšák]

If Fintype was simply extending DecidableEq, it should work out fine, no? I thought such class extensions are reasonably immune to diamonds...

[Kyle Miller]

It doesn't make it immune, but it helps. (That said, DecidableEq isn't a structure, it's a pi type, and Lean doesn't allow extending non-structures.)

[Mirek Olšák]

By the way, I didn't know about Trunc but it made me realize that the standard choice axiom could be split into the unique and mathematical part as

axiom uniqueChoice.{u} {α : Type u} : Nonempty α → Trunc α
axiom mathChoice.{u} {α : Type u} : Trunc α → α

[Mirek Olšák]

And with extending non-structures, you also reminded me how I was pondering about the difference between WellFounded and IsWellFounded. What I could detect

1. WellFounded has the argument α implicit, IsWellFounded explicit.
2. WellFounded supports any Sort, IsWellFounded only Type.
3. WellFounded is not a structure, so it cannot be extended (it is "only" an inductive type with a single constructor), IsWellFounded is a class.

If it is enough differences to have it separated is still not clear to me...