28
$\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.

$\endgroup$
9
  • 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 at 2:34
  • 11
    $\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 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 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 at 9:00
  • 4
    $\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 at 12:01

2 Answers 2

12
$\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$
8
  • 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 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 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 at 16:17
  • $\begingroup$ Can you explain some of the abbreviations in your posts (TTobs, MLTT, FUD)? $\endgroup$ Mar 1 at 18:06
  • 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 at 20:49
7
$\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
  • 1
    $\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 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 at 3:21
  • $\begingroup$ @JasonRute Thanks for pointing this out! See my edit. $\endgroup$
    – Couchy
    Mar 2 at 3:39
  • $\begingroup$ @JasonRute It's worth pointing out that Lean breaks definitional equality because of this. $\endgroup$
    – Couchy
    Mar 2 at 3:47
  • 5
    $\begingroup$ Hot damn, I said something quotable! $\endgroup$ Mar 2 at 22:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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