Stream: Coq users

Topic: Intuition for setoids?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Jun 22 2022 at 10:10):

However you can get pretty far with decidable quotients.

view this post on Zulip 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 xR,nN,x<n\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 R\mathbb{R} that we know how to define constructively are continuous, and the only continuous functions RN\mathbb{R}\to \mathbb{N} are the constant functions.

However if one allows for operations RN\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 {xn}\{x_n\}, compute this sequence out to xNx_N where the precision of the sequence past NN is better than ϵ\epsilon, and return the least natural number greater than xn+ϵ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,BA, B, and f:ABf : A\to B, if ff 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,BA, B are setoids and ff is a function properly speaking, then surjectivity only suggests that there is an 'operation' g:BAg: B\to A which splits ff, not necessarily respecting the equality. The existence of a proper function s:BAs : B\to A with sf=idBsf = \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).

view this post on Zulip Patrick Nicodemus (Jun 23 2022 at 12:50):

(deleted)

view this post on Zulip 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 R\mathbb{R} that we know how to define constructively are continuous, and the only continuous functions RN\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

view this post on Zulip 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.

view this post on Zulip 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 R\mathbb R to N\mathbb N without squashing the N\mathbb N (or dropping the equivalence-preserving requirement).

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jun 23 2022 at 20:20):

how do you define constructive real?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jun 23 2022 at 20:24):

those are cauchy sequences not reals

view this post on Zulip Michael Soegtrop (Jun 23 2022 at 20:25):

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

view this post on Zulip Gaëtan Gilbert (Jun 23 2022 at 20:27):

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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jun 23 2022 at 20:29):

(with CReal from above as real).

view this post on Zulip Gaëtan Gilbert (Jun 23 2022 at 20:29):

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

view this post on Zulip Gaëtan Gilbert (Jun 23 2022 at 20:30):

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

view this post on Zulip Raul (Jun 23 2022 at 20:41):

(deleted)

view this post on Zulip 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 R\mathbb{R} that we know how to define constructively are continuous, and the only continuous functions RN\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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jun 24 2022 at 08:11):

CReals are no real numbers

yes
they are unquotiented cauchy sequences

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Michael Soegtrop (Jun 24 2022 at 08:28):

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

view this post on Zulip Guillaume Melquiond (Jun 24 2022 at 08:30):

But Qc is also a standard library.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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: Feb 01 2023 at 11:04 UTC