Stream: Coq users

Topic: Intuition for setoids?

Patrick Nicodemus (Jun 22 2022 at 05:15):

I have some uncertainty about setoids and their purpose.
I will ask some overlapping questions.
Why do we need setoids?
Why can't we just work with quotient types?
Why does constructive math like setoids?
Why are setoids considered the natural translation of classical (extensional) sets into type theory?

James Wood (Jun 22 2022 at 10:04):

Patrick Nicodemus said:

Why do we need setoids?
Why can't we just work with quotient types?

The usual motivation is that we're working in a theory without quotient types, like CIC or MLTT. In a theory with quotienting, setoids play a much smaller role (but typically still some; you're always going to have some equivalence relations you haven't yet quotiented by, at least).

Patrick Nicodemus said:

Why does constructive math like setoids?

I can't remember exactly where it comes in, but I believe the principle of choice is essential to the construction of quotients in ZFC (something something canonical elements of equivalence classes...). Hopefully someone can clarify this. When we don't have choice, we have to do something explicit in the foundations to allow them to exist. Furthermore, Martin-Löf's formulation of the identity type is quite allergic to proofs of equality between syntactically distinct terms, so well behaved type theories with quotients have typically had to replace it (e.g in cubical type theory).

Patrick Nicodemus said:

Why are setoids considered the natural translation of classical (extensional) sets into type theory?

When we don't have things like quotienting and function extensionality, then Set just isn't good enough for any non-trivial algebra and category theory. For example, without function extensionality, the category of sets doesn't have general coproducts, because the equations we need to prove are between functions, and they don't happen to hold by judgemental equality. Without quotients, you don't get things like real numbers or tensor products. Instead, we take the category of setoids, where there are function setoids satisfying function extensionality and we can take whatever quotients we want.

Ali Caglayan (Jun 22 2022 at 10:08):

For finitary algebraic structures, you don't need choice to construct quotients. For infinitary ones, you will need some form of choice. Typical examples include compelete lattices.

Ali Caglayan (Jun 22 2022 at 10:09):

In general, you cannot make all quotient equalities into judgemental ones since this will break decidability of typechecking.

Ali Caglayan (Jun 22 2022 at 10:10):

However you can get pretty far with decidable quotients.

Patrick Nicodemus (Jun 23 2022 at 12:47):

I've been reading up on this the past couple days and I found a fairly concrete example in Troelstra's book on constructivism and mathematics that helps to illustrate the value of setoids.

Question: Constructively, is it true that $\forall x\in \mathbb{R}, \exists n\in \mathbb{N}, x < n$?

Working with strict equality, we almost certainly cannot prove this theorem constructively, as all functions on $\mathbb{R}$ that we know how to define constructively are continuous, and the only continuous functions $\mathbb{R}\to \mathbb{N}$ are the constant functions.

However if one allows for operations $\mathbb{R}\to \mathbb{N}$ that do not respect equality, and so perhaps send distinct Cauchy sequences to distinct natural numbers even when these distinct Cauchy sequences are equal as real numbers, then the problem can be solved easily: fix any rational $\epsilon$ and for any Cauchy sequence $\{x_n\}$, compute this sequence out to $x_N$ where the precision of the sequence past $N$ is better than $\epsilon$, and return the least natural number greater than $x_n+\epsilon$. This in itself is pretty good justification for setoids in my book - surely I think most mathematicians would be badly turned off from constructive mathematics if you told them it could not be proved that every real was bounded above by a natural number!

Troelstra also points out that the set/setoid distinction and the extensional/intensional distinction is closely related to the constructivity or nonconstructivity of the axiom of choice, which is something that Martin-Lof addresses at length in his paper "100 years of the axiom of choice". For types $A, B$, and $f : A\to B$, if $f$ is surjective then it has a section; this is a theorem of MLTT. So in this sense the axiom of choice is a theorem. However if $A, B$ are setoids and $f$ is a function properly speaking, then surjectivity only suggests that there is an 'operation' $g: B\to A$ which splits $f$, not necessarily respecting the equality. The existence of a proper function $s : B\to A$ with $sf = \operatorname{id}_B$ is much less trivial, matching the conventional wisdom that the Axiom of Choice is a badly nonconstructive axiom (conventional wisdom which is backed up by the theorems of Diaconescu and Goodman-Myhill that the axiom of choice implies LEM).

Patrick Nicodemus (Jun 23 2022 at 12:50):

(deleted)

Gaëtan Gilbert (Jun 23 2022 at 13:02):

Working with strict equality, we almost certainly cannot prove this theorem constructively, as all functions on $\mathbb{R}$ that we know how to define constructively are continuous, and the only continuous functions $\mathbb{R}\to \mathbb{N}$ are the constant functions.

∀x∈R,∃n∈N,x<n is not a function to nat (because of exists which squashes)
indeed you need axiom of choice to turn such a thing into exists f : real -> nat, forall x, x < f x

James Wood (Jun 23 2022 at 14:38):

It's a general principle of any "reasonable" foundation that (proposition-valued) predicates can ignore quotienting of their arguments. With HoTT-style h-propositions, it's clear how to get this to work: The eliminator for quotients says that you get an element of the unquotiented set, but you have to show that the term you produce respects the equivalence relation the set was quotiented by. It's easy to prove that the equivalence relation is respected when all the terms you could possibly produce are equal (because they're h-props). We can reproduce this style of reasoning in setoids by interpreting $\forall$ as the $\Pi$-setoid and $\exists$ as a $\Sigma$-type together with the equivalence relation which equates everything.

Michael Soegtrop (Jun 23 2022 at 14:52):

I can't quite follow this argument. It is quite easy to find such an n constructively - just one can't find the smallest n which is larger than x. One can compute constructively any real number to arbitrary precision. Let's take precision 1 and compute our Cauchy series for x to precision 1. This results in a rational number x' for which we know that |x-x'|<=1. The rationals are Archimedian, so we can compute a n>x'+1>=x. Where is the issue?

James Wood (Jun 23 2022 at 15:04):

@Michael Soegtrop Wrong thread

James Wood (Jun 23 2022 at 15:11):

Michael Soegtrop said:

One can compute constructively any real number to arbitrary precision.

The difficulty is that this operation doesn't respect equality on real numbers (the same real number, represented by different Cauchy sequences, could produce different approximations). So you don't get an equivalence-preserving function from the setoid $\mathbb R$ to $\mathbb N$ without squashing the $\mathbb N$ (or dropping the equivalence-preserving requirement).

Michael Soegtrop (Jun 23 2022 at 20:04):

But is this the question here? The question is if for any concrete constructive real x there constructively exists an n such that x<n. What does this have to do with equality on reals?

Gaëtan Gilbert (Jun 23 2022 at 20:20):

how do you define constructive real?

Michael Soegtrop (Jun 23 2022 at 20:23):

Well as defined in the Coq standard library (https://github.com/coq/coq/blob/3ed332aeac665d034b5f9045ccffcd83ea03d962/theories/Reals/Cauchy/ConstructiveCauchyReals.v#L66)

Michael Soegtrop (Jun 23 2022 at 20:24):

I guess I should just go and try prove it in Coq - the easiest way to understand it.

Gaëtan Gilbert (Jun 23 2022 at 20:24):

those are cauchy sequences not reals

Michael Soegtrop (Jun 23 2022 at 20:25):

Sorry, I got the wrong line, I updated the link.

Gaëtan Gilbert (Jun 23 2022 at 20:27):

what I said was actually meant for the new link so my point stands

Michael Soegtrop (Jun 23 2022 at 20:28):

Not sure what exactly you mean. As I said I will just try and prove ∀x∈R,∃n∈N,x<n - then I will see.

Michael Soegtrop (Jun 23 2022 at 20:29):

(with CReal from above as real).

Gaëtan Gilbert (Jun 23 2022 at 20:29):

I mean you can prove exists x y : R, x <= y <= x /\ x <> y

Gaëtan Gilbert (Jun 23 2022 at 20:30):

where <= is CRealLe and <> is the negation of Coq.Init.Logic.eq

Raul (Jun 23 2022 at 20:41):

Okay, is trickier than it seems.
It's not possible as long as you can't tell how close you're to the upper number.
Interesting to learn (and sry for the mistake).

But in which sense would be a help to have a construction that gives you a solution and does not respect equality.
The same reason why with equality it doesn't work would make non-constructive to work with the values of the function.
Isn't it like you lose the point of constructiveness?

Guillaume Melquiond (Jun 24 2022 at 05:07):

Patrick Nicodemus said:

Working with strict equality, we almost certainly cannot prove this theorem constructively, as all functions on $\mathbb{R}$ that we know how to define constructively are continuous, and the only continuous functions $\mathbb{R}\to \mathbb{N}$ are the constant functions.

This reasoning is a bit flawed. As mentioned by Michael, it is easy to constructively build a function f: R -> N such that forall x, x < f x. And this function is indeed continuous. But you should keep in mind what continuous actually means here. As James mentioned, either f is not setoid-preserving or N is squashed. In the former case, the input topology is not Hausdorff's, while in the latter case, the output topology is trivial. Thus, in both cases, the notion of continuity is utterly pointless, and does not say much about the constantness of function f.

Michael Soegtrop (Jun 24 2022 at 08:11):

@Gaëtan Gilbert : sorry, I still can't follow you. Are you saying more or less "yes, with CReal for R you can prove ∀x∈R,∃n∈N,x<n , but CReals are no real numbers, because you could prove things which should be contradicting like exists x y : R, x <= y <= x /\ x <> y"?
Can you share you intuition how one would prove that? I don't see that and would even think that I can prove False assuming that.

Gaëtan Gilbert (Jun 24 2022 at 08:11):

CReals are no real numbers

yes
they are unquotiented cauchy sequences

Michael Soegtrop (Jun 24 2022 at 08:15):

Well but isn't this what one usually means by "constructive real"?
Are you sure you can prove exists x y : R, x <= y <= x /\ x <> y? How?

Michael Soegtrop (Jun 24 2022 at 08:17):

Maybe I got the initial statement of @Patrick Nicodemus wrong. I assumed that "Constructively, is it true" implies that we are talking about constructive reals.

Guillaume Melquiond (Jun 24 2022 at 08:19):

Michael Soegtrop said:

Well but isn't this what one usually means by "constructive real"?
Are you sure you can prove exists x y : R, x <= y <= x /\ x <> y? How?

Sure. Take two equivalent but not equal Cauchy sequences (e.g., the constant sequence zero and any non-constant sequence converging to zero).

Michael Soegtrop (Jun 24 2022 at 08:22):

@Guillaume Melquiond : ah yes, silly me - interesting. I need to ponder over what this implies for a while.

Michael Soegtrop (Jun 24 2022 at 08:24):

But this is true for the Coq rationals as well. So stating on that basis that constructive reals are not reals is not quite valid, since one can state on the same basis that Coq rationals are not rationals.

Guillaume Melquiond (Jun 24 2022 at 08:27):

Not quite. If you take Coq's Qc set, you can prove that x <= y <= x -> x = y. That is because the canonicity of a representant in the quotient set is now decidable (while this is not true for Cauchy sequences).

Michael Soegtrop (Jun 24 2022 at 08:28):

I am talking about the standard library Q: Record Q : Set := Qmake { Qnum : Z; Qden : positive }..

Guillaume Melquiond (Jun 24 2022 at 08:30):

But Qc is also a standard library.

Michael Soegtrop (Jun 24 2022 at 08:34):

Ah OK - I thought it was mathcomp.
Anyway I think we can conclude that there exists a definition of rationals in the Coq standard library which defines something which are not rationals if one applies @Gaëtan Gilbert's argument.

Guillaume Melquiond (Jun 24 2022 at 08:36):

Yes. Q should never have been defined as a synonymous for Z * positive. Those are not rational numbers, whichever way you look at them.

Michael Soegtrop (Jun 24 2022 at 08:41):

I see what you mean and for Q I follow your argument, although I can't say I ever had any issues with QArith Q.

Michael Soegtrop (Jun 24 2022 at 08:41):

For reals I am not sure if constructive reals in the sense of "unquotiented Cauchy sequences" are not the better model for real numbers. Maybe that has to do with the fact that I am physicist and have a bit more mechanical and less abstract view of the world.

Paolo Giarrusso (Jun 24 2022 at 23:31):

On your last point, would the right solution be to use the setoid over unquotiented Cauchy sequences?

James Wood (Jun 27 2022 at 08:28):

Guillaume Melquiond said:

Yes. Q should never have been defined as a synonymous for Z * positive. Those are not rational numbers, whichever way you look at them.

I guess, to clarify, the point here is that the set Z * positive has no more to do with ℚ than the set nat * nat has to do with ℤ. Only the setoid deserves to be called Q. That said, the setoid of rational numbers is probably the only codified use of the set Z * positive, so the naming is harmless in practice.

Guillaume Melquiond (Jun 27 2022 at 09:02):

My point is that Coq's Q is not the setoid. The actual setoid is named Qc in the standard library. Q is really just the cartesian product.

Paolo Giarrusso (Jun 27 2022 at 11:35):

Isn't Qc the actual quotient? If a setoid is a pair of a set and an equivalence, calling Q a setoid is as improper as calling the set Z a ring — it’s an abuse of notation that calls for canonical structures (even if Coq does not let you write Z : ring directly, IIUC).

Guillaume Melquiond (Jun 27 2022 at 11:52):

Paolo Giarrusso said:

Isn't Qc the actual quotient?

Right, my mistake. And since Qeq is declared as a global instance, Q can indeed be considered a setoid.

Last updated: Apr 19 2024 at 17:02 UTC