Address a "setoid hell"?

[XVilka]

Yesterday I watched the video by Prof Buzzard about Lean and there was a question of how it compares to Coq (obviously), and he replied basically that in Lean it's straightforward to express quotients, while in Coq you get "setoid hell". This specific statement is at 1:04:20 in the video. The question is at 1:00:02 and is probably useful for context.

Sorry, I am a newbie to Coq and never tried Lean (yet), but for him, it was the deal-breaker it seems, so maybe it's possible to address this problem somehow? Note, that his goal is not merely proof something, but to build a substantial corpus of the mathematical foundation, similar to the Metamath and Univalent Foundations, whom he said didn't achieve substantial progress in the past decades, while he did it more efficiently with Lean.

On how quotients are implemented in Lean see their Chapter 11 (Axioms and Computation) of the Theorem Proving in Lean book.

I found a few relevant discussions over the internet:

• https://www.reddit.com/r/Coq/comments/ammiod/quotient_types_with_coq/
• https://perso.crans.org/cohen/work/quotients/ and the paper itself
• https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/

There is some quotients implementation in the Coq-contribs, but not sure how it's useful https://github.com/coq-contribs/rational/tree/master/Quotient

Would be nice to know what the Coq developers themselves think about this.

P.S. His second complain is the Unicode tokens and terms out of the box in Lean, while in Coq you have to either use Unicode.Utf8 library (which is rather limited compared to Lean), or define something less popular by yourself.

[ppedrot]

Quotient types are well known to be tricky in type theory. As far as I know, the only sensible way to allow them is to change the notion of equality to a more extensional one like SetoidTT (which gives you amongst others funext and uip) or CubicalTT (which gives you univalence). In particular, in these systems equality is not defined as an inductive type and proofs of x = x may not reduce to reflexivity.

Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around.

The first thing they do is to axiomatize quotient types, which is somewhat fine and can be done the same in Coq. As any use of axioms, this breaks canonicity, meaning your computations may get stuck on some opaque term. (While slightly cumbersome, axiomatizing quotients already solves 99,9% of the problems of the working mathematician).

Now, were they do evil things that would make decent type theorists shake in terror, they add a definitional reduction rule over the quotient induction principle. We could do the same in the Coq kernel, but there is a very good reason not to do this. Namely, this definitional rule breaks subject reduction, which is a property deemed more important than loss of canonicity.

In Lean, you can write a term t : A where t reduces to u, but u doesn't have type A (or equivalently may not typecheck at all). This is BAD for a flurry of reasons, mark my words. Reinstating it while keeping quotients requires an undecidable type checking algorithm, which is another can of worms you don't want to wander into. The same kind of trouble arises from similar Lean extensions like choice.

To be honest, Coq also fails at SR, but for historical design issues that ought to be fixed at some point. Coinductive types are well-known to break SR due to poor understanding of their consequences at the time they were introduced. See my PR #10764 for more details about why this happens and how to fix it (which would correspond in quotient types to restrictions on the elimination principle to predicates preserving definitional equality).

Everything is not hopeless though. We have been working recently on rewrite rules for Coq, which might provide you with the ability to define quotients that compute and break good properties of CIC in an opt-in and generic way, not relying on hardwired properties in the kernel. Another likely candidate for well-behaved quotients is the extension of Coq to CoqMT, which preserves the good meta-theoretical properties of CIC at the cost of only allowing decidable quotients.

Alternatively, it is possible to embed SetoidTT into Coq + SProp via a syntactic translation, which would allow you to define a new theory atop of Coq and reason inside it, but this currently has quite a few drawbacks, even though we are also working on making this kind of extension more transparent.

TL;DR: Lean support for quotients is FUD. They break an essential metatheoretical property of CIC. Coq people care for this kind of properties, and prefer extending the theory much more slowly at a cost of reduced expressivity (but what use is expressivity of a broken system? You could work in Set theory for that matter).

People that I know have something to say in this thread include @amahboubi, @tabareau and @TheoWinterhalter, so let me ping them.

[jespercockx]

Thanks @ppedrot for the in-depth explanation. I didn't know Lean actually broke subject reduction in this way!

In Agda, you can currently use --cubical mode to define quotients as a higher inductive type, preserving both canonicity and subject reduction. However, in my experience it is currently still a bit cumbersome to work with. In particular, working with interval variables rather than pattern matching on refl can get annoying (or maybe it just takes some time getting used to). I'm very curious if a variant of cubical with UIP (e.g. XTT) will provide a solution.

I have also seen people encoding quotients in Agda using a combination of (strict) Prop and rewrite rules, see e.g. the initiality project. This looks very similar to what happens in Lean in that you postulate quotients and then add the computation rule for the eliminator as a rewrite rule. It seems like this might cause the same problem with subject reduction that @ppedrot describes (the current implementation of rewrite rules in Agda is unsafe in that way).

[SkySkimmer]

@ppedrot what about the reduction rule for quotients breaks SR?

---

You can define the primitives for Lean quotients with a HIT-style private inductive:

Module Export quot. (* simulating Lean namespace with module export kinda works *)

  Section quot.
    Variables (A:Type) (R:A->A->Prop).

    Private Inductive quot := mk : A -> quot.

    Definition quot_lift B (f:A -> B) (q:quot) : (forall a b, R a b -> f a = f b) -> B
      := match q with mk x => fun _ => f x end.

    Definition quot_ind (P:quot -> Prop) (f:forall a, P (mk a)) (q:quot) : P q
      := match q with mk x => f x end.
  End quot.

End quot.

Then you add some axioms. Private inductives can be a bit awkward wrt to what they guarantee, see eg #9609, but it basically works.
(this isn't really a hit because you only have dependent elimination to assumed-proof-irrelevant Prop)

They don't use this directly though, usually they go through the derived notion of

Module Export setoid.
  Class setoid (A:Type) := { r : A -> A -> Prop; iseqv : Equivalence R }.
End setoid.
Definition quotient {A:Type} (r:setoid A) := @quot A (@setoid.r A r).

so there's so typeclass support allowing eg Notation "⟦ a ⟧" := (@quot.mk _ (@setoid.r _ _)).

There's also the difference that they have equality in definitionally proof irrelevant Prop, and Prop is cumulative with everything else. This is unlike us where equality is not yet available in SProp, SProp doesn't have Acc, SProp is not cumulative and anyway the stdlib uses Prop and the Prop equality everywhere. EDIT actually it seems lean doesn't have cumulativity
I don't know how important it is to have irrelevant equalities when working with quotients though (assuming you have quot_ind instead of having to derive it through the regular eliminator at least).

[ppedrot]

Private inductives can be a bit awkward wrt to what they guarantee [...] but it basically works.

Reference needed. I'm confident I can find a SR breakage with private inductive types, I think we actually had an example of that.

[Zimmi48]

Warning: not a technical post

Yesterday I watched the video by Prof Buzzard about Lean and there was a question of how it compares to Coq (obviously), and he replied basically that in Lean it's straightforward to express quotients, while in Coq you get "setoid hell". This specific statement is at 1:04:20 in the video. The question is at 1:00:02 and is probably useful for context.

Sorry, I am a newbie to Coq and never tried Lean (yet), but for him, it was the deal-breaker it seems, so maybe it's possible to address this problem somehow? Note, that his goal is not merely proof something, but to build a substantial corpus of the mathematical foundation, similar to the Metamath and Univalent Foundations, whom he said didn't achieve substantial progress in the past decades, while he did it more efficiently with Lean.

I wonder how much truth vs bulllshit there is in this statement giving the reason why Kevin Buzzard thinks Lean is better than Coq for the project of formalizing mathematics. I have serious doubts that he has given any chance to Coq. Indeed, I have earlier evidence that his initial reason for choosing Lean was not this: https://mathoverflow.net/questions/311071/which-mathematical-definitions-should-be-formalised-in-lean

In this post from just a year ago he says:

15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in.

So this is what convinced him to try out Lean, but do you know what Hales gave as an explanation for this choice at this time? Only this "I thought Lean, because HOL foundations are a bit weak". At this point, he could have given exactly the same justification for using Coq, and Kevin Buzzard would be doing advertisement for Coq instead.

Earlier in another discussion, @mdahas seemed to know that Thomas Hales had decided not to use Coq, not because of some theoretical grounds, but because of basic usability concerns such as the availability of good documentation (it was a long time ago):

If the next Thomas Hales appears, what should he do next? (And if you think that is a ridiculous thing to say that, you didn't asked Thomas Hales the questions I did.)

I am sorry that Coq failed to convince him at the time, but we have made a lot of progress since then.

The thing that is ridiculous is that Thomas Hales is a very famous mathematician who seems to know what he is talking about regarding formalization of mathematics because of his formalization of his proof of the Kepler conjecture. But he did not do this using Lean! And now his project is https://formalabstracts.github.io/, very far from actual large-scale formalization of mathematics. So he hasn't got the same experience doing actual formalization work in Lean as he did earlier and cannot know how much it works at scale (he is also not in the contributors of the mathlib project, which virtually includes every math ever formalized in Lean: https://github.com/leanprover-community/mathlib/graphs/contributors).

So my conclusion is that probably none of the very vocal Lean supporters actually know what they are talking about when they compare Lean to Coq (albeit some other Lean users do know both systems). Of course, I would be very happy to be proved wrong.

Sorry for hijacking this technical issue with such a rant, I am just fed up with this "mastermind public relation campaign" as Pierre-Marie put it.

[gares]

Kevin Buzzard thinks Lean is better than Coq for the project of formalizing mathematics. I have serious doubts that he has given any chance to Coq

I asked him this question in person at ITP. He was an invited speaker and, in that occasion, he did not compare Coq to Lean, but rather say that what we prove with these tools is not very convincing for a mathematician... His answer to my question was that, to him, Coq, Lean, ... look roughly the same, but colleagues like Hales were using Lean, so he tried it too.
Well, I guess that answer was less sexy than some bold claim, but I also imagine you get less pressure to say something strong when you are asked a question at breakfast by a person you don't know ;-)

I've also asked the same questions to others, and other than the social aspect the reason was ergonomics (UI, installation, doc). In a way, especially when you are approaching a new system, these things are way more important than, well, features. So, I guess we've still quite some work ahead...

[mattam82]

@SkySkimmer if quot_lift doesn’t guard at all on the fact that the function is equivariant for related terms to produce its output that’s probably where the devil lies.

[mattam82]

I would add that math-comp didn’t seem to do too bad with their encoding of effective quotients in pure CIC.

[SkySkimmer]

@SkySkimmer if quot_lift doesn’t guard at all on the fact that the function is equivariant for related terms to produce its output that’s probably where the devil lies.

It may be inconsistent with the r a b -> mk a = mk b axiom but I don't see how it could impact SR.

[andres-erbsen]

@ppedrot, could you please explain what reduction behavior of Lean's quotients is problematic? Here is the file I was experimenting with, in case that is helpful... (I'm mostly asking out of mathematical curiosity, though).

prelude
import init.data.quot init.logic

inductive notquot {A : Type} (R : A -> A -> Prop) : Type
| mk (_ : A) : notquot

-- this succeeds due to the built-in primitive reduction rules for eliminators of inductive types
def notquot_ind_beta {A R} {B : notquot R → Prop} (f : ∀ a, B (notquot.mk R a)) (a : A)
  : (notquot.rec f (notquot.mk R a) : B (notquot.mk R a)) = f a
  := rfl

-- quot.lift reduces the same way as the the eliminator of the inductive type above
-- it is restricted to non-dependent Proper continuations
-- this is similar to what is achieved to careful use of Private Inductive in coq,
-- and in my eye the most surprising thing here, so is this where the problem lies?
def lift_beta {A} {R : A → A → Prop} {B} (f : A → B) (pf : ∀ a b, R a b → f a = f b) (a : A)
  : (quot.lift f pf (quot.mk R a)   : B                 ) = f a
  := rfl

-- note that quot.ind reduces because of judgemental proof irrelevance
-- it is restricted to continuations constructing propositions
def ind_beta {A R} {B : quot R → Prop} (p : ∀ a, B (quot.mk R a)) (a : A)
  : (quot.ind p (quot.mk R a) : B (quot.mk R a)) = p a
  := rfl

-- on the other hand, quot.sound does not have special reduction behavior
def T := quot (λ x y : nat, x=x)
def collapse_mk_T (x y : nat) : (quot.mk _ x : T) = quot.mk _ y := quot.sound rfl
def zer : T := quot.mk _ 0
def one : T := quot.mk _ 1
def one_zer : one = zer := collapse_mk_T _ _
def zer_one : zer = one := collapse_mk_T _ _
inductive vec (t : Type) : T -> Type
| nil : vec (quot.mk _ 0)
| cons n (x:t) (xs : vec (quot.mk _ n)) : vec (quot.mk _ (nat.succ n))
def a := vec.nil nat
def b := @eq.rec T zer (vec nat) (vec.nil nat) one zer_one
def c := @eq.rec T one (vec nat) b zer one_zer
#check (rfl : a = c)
-- 80:1: ⁇ : a = c
-- 
-- 80:9: invalid type ascription, term has type
--   ?m_2 = ?m_2
-- but is expected to have type
--   a = c

-- EDIT to add:
#check (rfl : @eq.rec nat 0 (λ _, nat) _ 0 rfl = 0) --yes
#check (rfl : @eq.rec nat 0 (λ _, nat) _ 0 sorry = 0) --yes
#check (rfl : @eq.rec nat 0 (λ _, nat) _ 1 sorry = 0) --no
#check (rfl : quot.mk (λ x y, x=x) 0 = quot.mk (λ x y, x=x) 1))--no
#check (collapse_mk_T _ _ : quot.mk (λ x y, x=x) 0 = quot.mk (λ x y, x=x) 1)--yes

[ppedrot]

@andres-erbsen the issue is described in Section 3.1 of this document summarizing the Lean type system.

[SkySkimmer]

That doesn't mention any quotient related issues.

[ppedrot]

Look at the end of Section 3.1.1. Quotients of propositions create non-transitivity of algorithmic conversion, which in turn breaks SR.

[SkySkimmer]

ok Gaëtan Gilbert

…

On 12/10/2019 11:53, Pierre-Marie Pédrot wrote: Look at the end of Section 3.1.1. Quotients of propositions create non-transitivity of algorithmic conversion, which in turn breaks SR. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#10871>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AASZB3GV3LBJGFG2VGKLWDTQOGNAZANCNFSM4I7HDOPQ>.

[andres-erbsen]

Thanks for the pointer! I transcribed the example (to the best of my ability) and observed a different weird behavior than described in the paper.

constant P : Prop
constant R : P -> P -> Prop
constant A : Type
constant f : P -> A
constant H : ∀ x y, R x y -> f x = f y
constant q : @quot P R
constant h : P

#check (@quot P R : Prop)    -- yes
#check (quot.lift f H q : A) -- yes
#check (rfl :               q =                quot.mk R h       ) -- yes
#check (rfl : quot.lift f H q = quot.lift f H (quot.mk R h)      ) -- no (3.1.1 says this should go through)
#check (rfl :                   quot.lift f H (quot.mk R h) = f h) -- yes
#check (rfl : quot.lift f H q =                               f h) -- no