What exactly is setoid hell?

Question

One of the only arguments I've heard about why Lean is better than Coq is that you can construct quotients of built-in structures by default. (In Coq, you apparently have to use Setoids instead of Sets, or so I've heard, hence the title).

However, I am still having a hard time seeing why this supposed problem is actually such a problem.

Could someone elaborate on this for me?

I would like to see some sort of minimal working example, where a theorem with a nice short proof in Lean has a much more verbose, less elegant proof in Coq.

---

Edit: I'm grateful this question sparked a bunch of really interesting discussion, the main reason I have not accepted an answer is because none of them have satistifed:

I would like to see some sort of minimal working example

Answer 1

Setoid hell means that you are doing by hand the work of a compiler.

A setoid is just a type equipped with an equivalence relation. One can then define functions between setoids as functions between the underlying types respecting the equivalence. Similarly, you can endow other type formers with a setoid structure. Long story short, this construction constitutes a syntactic model of TTobs, a type theory with many nice properties. TTobs contains MLTT and also features quotient types, so working from within it allows to define stuff in the standard mathematical way.

Now, such a syntactic model can be seen as a compilation from TTobs into (some variant of) Coq. Like any compilation process, it is both systematic and tedious. Everytime the user writes a function, for instance, she has to provide a proof of respectfulness by hand, when it should actually be inferable. In addition to being annoying it is also error-prone when done manually.

This is not as tedious as writing the X86 assembly code corresponding to the compilation of a Coq program after extraction and OCaml compilation, but it is still a PITA. Who would do it knowing it can be done by a computer faster, in a safer way and with a high-level abstraction as a bonus?

Answer 2

Disclaimer: I know very little about Lean, so I would be happy to be proved wrong.

There is no escape from setoid hell. Lean simply gives a different way of doing the same thing one does in Coq.

In Lean, given a type $X$ with a relation $\sim$, we obtain a new type $\tilde X = X/\sim$ such that if $x\sim y$ then $[x] = [y]$. In Coq, $\tilde X$ is not allowed to be a type because we can no longer decide whether two elements of $\tilde X$ are equal (there is a way around this if your relation is decidable, say using SSReflect, and Lean probably has similar functionality).

In Lean, if you want to define a function $f : \tilde X\to Y$ (or a proposition on $\tilde X$), you need to use quot.lift which requires you to prove that whenever $x \sim y$ then $f([x]) = f([y])$. In Coq, you simply define a function $f : X\to Y$, then prove a congruence lemma f_eq saying that $x\sim y$ implies $f(x) = f(y)$.

Now the difference is that in Lean, given $x\sim y$ and $f : \tilde X\to Y$, you can rewrite $f([x])$ to $f([y])$ automatically using elimination for equality, whereas in Coq, you have to invoke the congruence lemma f_eq.

So in summary, Lean keeps track of the congruence rule in the definition of $f$, whereas in Coq you have to keep track of $f$ and f_eq.

I don't actually know exactly what setoid hell refers to, but if it refers to keeping track of congruence rules within the term then I suppose you could say Lean avoids this, but the amount of work you need to do is the same.

I am nethertheless going to quote Jacques Carette

Setoid hell arises not because some coherences must be proven. It arises when you're forced to prove these coherences again and again when defining functions that can't possibly "go wrong". So Setoid hell is actually caused by a failure to provide proper abstraction mechanisms.

---

As Jason Rute points out, this means that in Coq, if we want to prove nested equalities of the form $f(g(x)) = f(g(y))$ given $x\sim y$, we would need to first apply g_eq, then apply f_eq, which can be cumbersome. However, Coq supports generalized rewriting, where $f$ and $g$ can be declared as Parametric Morphism's (given $\sim$ is declared a Parametric Relation) which allows directly rewriting in this setting.

Answer 3

The main difference between setoids and quotients occurs when defining new functions in terms of existing functions, such as f(x) = g(h(x)). With setoids you will need to prove a lemma that f respects the equivalence relation using a trivial proof with the lemmas that g and h respect the equivalence relation. Coq has the solve_proper tactic to solve such trivial goals, but you still need to state the lemma and invoke this tactic.

With quotients, you do not need to do that: if g and h operate on the quotient type, then f also operates on the quotient type, which means that f automatically respects the equivalence relation by type checking. With quotients, you only need to prove a lemma when you define a function by actually opening up the quotient and peeking at a representative.

Answer 4

One can pack the compatibility proofs with the functions so that composition is proper for free, but then we're using a different function space:

Record setoid := { carrier :> Type; equiv : relation carrier }.
Record setoid_morphism A B :=
  { f : A -> B;
    f_eq : Proper (equiv A ==> equiv B) f }.

Definition compose {A B C} (g : setoid_morphism B C) (f : setoid_morphism A B) : setoid_morphism A C. ... Qed

From the usability point of view, this precludes using standard fun x => and applications to construct functions as one must always use the packed combinators on setoids, interaction with pattern-matching is also complicated by this. One also has to be careful to only use setoid_morphisms everywhere, which can become tedious. Still, many libraries have used that style effectively. This provides also the ability to peek inside the quotient and build functions that do not respect it (for example if you have a quotient type of real numbers and want to print them to strings). The Lean choice of rather biting the bullet and allowing quotients to be modelled by eq makes it feel much simpler I guess.