41
$\begingroup$

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

$\endgroup$
10
  • 1
    $\begingroup$ I found this fascinating issue which talks about why Coq doesn't support quotients, but it does not address my question: github.com/coq/coq/issues/10871 $\endgroup$ Mar 1, 2022 at 2:34
  • 13
    $\begingroup$ I am starting to be a bit annoyed by this rumour, but let me restate the truth here: the fact that Coq cannot have Lean-style quotients is pure FUD. You can definitely add them via private inductive types and axiomatize the rest in SProp. Obviously you get as a result the same kind of issues. The only real argument is that Coq libraries do not rely on this structure since it's not part of the stdlib, so you're bound to reinvent the wheel. $\endgroup$ Mar 1, 2022 at 8:15
  • 3
    $\begingroup$ @Pierre-MariePédrot so the only difference is actually that Lean decided to include this in the standard library by default, but Coq didn't and so you have to build it yourself? $\endgroup$ Mar 1, 2022 at 23:05
  • 4
    $\begingroup$ @setholopolus Yes. Don't get me wrong, this is a very important difference, because that means everybody relies on the same definition in Lean. This gives more code sharing and an easier time for people that do not understand how to reimplement them. $\endgroup$ Mar 2, 2022 at 9:00
  • 8
    $\begingroup$ This rumour was started by an ignorant comment I made in my 2019 MS talk that will not die and which I have repeatedly apologised for. However one thing I am unclear on is whether trickery in Coq can make the commutativity of the diagram coming from quotient.lift be definitionally true (lift f (quotient.mk x) = f x := rfl). I should say that I do not place too much weight on definitional equality any more, so am not sure of the importance of this question, but I don't know the answer to it anyway. $\endgroup$ Mar 4, 2022 at 12:01

3 Answers 3

19
$\begingroup$

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?

$\endgroup$
9
  • 2
    $\begingroup$ I wonder given the OP’s request for a practical example and your comment where your feel the situation is poorly understood, that your answer could be improved by two or three examples: (1) A Coq proof going through setoid hell. (2) (If you wish) a Lean proof of the same thing avoiding setoid hell. (3) A Coq proof avoiding setoid hell similar to Lean, by using private inductive types. $\endgroup$
    – Jason Rute
    Mar 1, 2022 at 12:05
  • 3
    $\begingroup$ I don't think the addresses the problem apart from repeating what the OP probably already knows. If it is systematic, why can't tactics work? It's these questions that is the crux. $\endgroup$
    – Trebor
    Mar 1, 2022 at 12:10
  • $\begingroup$ There is no simple example, because it's a matter of scalability. You don't appreciate scalability until you hit large-ish examples. (Said otherwise, tediousness is not an objective criterion.) $\endgroup$ Mar 1, 2022 at 16:17
  • 2
    $\begingroup$ Many constructions in algebra are natural with quotients, such as tensor products of modules. Any construction can be simulated without quotients, but you have to carry around the equivalence relation somewhere. If a language makes this bookkeeping easy then perhaps it doesn't matter, but from experience of developing mathematics most seem to agree that the Setoid approach does not make it convenient to carry the equivalence relation data around. Quotients are the ideal because the constructed type automatically satisfies the relation. $\endgroup$ Mar 1, 2022 at 20:49
  • 3
    $\begingroup$ I would add: I'm not sure it's possible to appreciate how bad things get without examples involving families of types (indexed by setoids). I've seen people claim that working with setoids is not so bad, but the corresponding examples usually end up being those where we have simple types replaced by setoids. I think families of setoids indexed by setoids are also where you would start seeing gaps in what tactics are able to help with (because even defining what a family is is complicated, despite being completely rote). $\endgroup$
    – Dan Doel
    Jan 19, 2023 at 16:25
14
$\begingroup$

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.

$\endgroup$
8
  • 2
    $\begingroup$ Does your analysis change much for functions $f,g:\tilde{X}\to \tilde{X}$? In this latter case, if $f(x)$ is buried in, say $g(f(x))$, with quotients you can simply rewrite (or maybe even defeq in some cases) to show $g(f([[x]]))=g(f([[y]]))$. But for setoids, you would need to apply congruence rules for both $f$ and $g$, to get $g(f(x))\sim g(f(y))$ and you would have to do it at every step of a possibly long set of equivalences, right? Of course, that doesn’t preclude the possibility of having good automation or abstraction mechanisms to do this for you as mention by others. $\endgroup$
    – Jason Rute
    Mar 2, 2022 at 3:01
  • $\begingroup$ I guess I’m suggesting by lifting equivalence to equality, it seems you can avoid a large amount of bookkeeping in situations like this since equality already has good tooling via rewriting, simplification, and definitional equality. With quotients it seems you only need congruence when going from $X$ to $\tilde{X}$. But for setoids, you need it for any time you work with functions on $\tilde{X}$. $\endgroup$
    – Jason Rute
    Mar 2, 2022 at 3:21
  • $\begingroup$ @JasonRute Thanks for pointing this out! See my edit. $\endgroup$
    – Couchy
    Mar 2, 2022 at 3:39
  • 1
    $\begingroup$ I think it’s also worth pointing out that for Lean users that example isn’t a big deal at all (as the rest of that discussion you linked to shows). And to avoid any misconceptions, let me also remark that Lean is proven to be consistent. $\endgroup$
    – Jason Rute
    Mar 2, 2022 at 4:16
  • 10
    $\begingroup$ Hot damn, I said something quotable! $\endgroup$ Mar 2, 2022 at 22:16
7
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.