Why are quotients axiomatic in Lean?

Stream: new members

[Stepan Nesterov]

I'm not really sure where this question would go, but why do quotients in Lean seem to be introduced via an axiom rather than via a straightforward formalization of the classical definition? The latter could go somewhat like this:

import Mathlib.Data.Set.Basic

universe u v
variable {α : Type u} [Setoid α] {β : Type v}

open Setoid

def IsSaturated : Set α → Prop := fun a => ∀ x ∈ a, ∀ y : α, r x y → y ∈ a

def IsConnected : Set α → Prop := fun a => ∀ x ∈ a, ∀ y ∈ a, r x y

def IsEquivalenceClass : Set α → Prop := fun a =>
  Nonempty a ∧ IsSaturated a ∧ IsConnected a

def EquivalenceClass : α → Set α := fun x => {y : α | r x y}

theorem equivalenceclass_isequivalenceclass (x : α) : IsEquivalenceClass (EquivalenceClass x) := by
  constructor
  · use x; exact refl x
  constructor
  · intro y hy z hz; apply Setoid.trans; exact hy; exact hz
  · intro y hy z hz; apply Setoid.trans; apply Setoid.symm; exact hy; exact hz

def MyQuotient : Type u := {a : Set α // IsEquivalenceClass a}

namespace MyQuotient

protected def mk : α → (MyQuotient (α := α)) := fun x => ⟨EquivalenceClass x, equivalenceclass_isequivalenceclass x⟩

theorem sound (x y : α) : r x y → MyQuotient.mk x = MyQuotient.mk y := by
  intro h; apply Subtype.eq; ext z; constructor <;> intro hz <;> apply Setoid.trans
  · apply Setoid.symm; exact h;
  · exact hz;
  · exact h;
  · exact hz;

theorem exists_rep (q : MyQuotient) : ∃ x : α, MyQuotient.mk x = q := by
  obtain ⟨⟨x, h⟩, q.sat, q.conn⟩ := q.property; use x;
  apply Subtype.eq; ext y; constructor <;> intro hy
  · exact q.sat x h y hy
  · exact q.conn x h y hy

theorem exact (x y : α) : MyQuotient.mk x = MyQuotient.mk y → r x y := by
  intro h; rw[Subtype.eq_iff, Set.ext_iff] at h; specialize h x
  change r x x ↔ r y x at h
  apply Setoid.symm; apply h.mp; exact Setoid.refl x

noncomputable def lift (f : α → β) : MyQuotient (α := α) → β :=
  fun q => f (Classical.choose (exists_rep q))

theorem lift_sound (f : α → β) (hf : ∀ x y : α, r x y → f x = f y) : ∀ x : α, lift f (MyQuotient.mk x) = f x := by
  intro x; unfold lift; apply hf;
  have := Classical.choose_spec (exists_rep (MyQuotient.mk x))
  apply exact; exact this

[Aaron Liu]

this doesn't give you good definitional reductions

[Aaron Liu]

see lift is noncomputable

[Aaron Liu]

also in Lean you need quot sound to prove funext

[Riccardo Brasca]

In your theorem sound you use the ext tactic, you need quotient types to prove functional extensionality.

[Aaron Liu]

well the other thing is that Lean could've made funext an axiom and then constructed quotients like this

[Aaron Liu]

but then lift is noncomputable which is sad

[Riccardo Brasca]

Yes, the fact that a lot of proofs about quotients are just rfl is super nice.

[Stepan Nesterov]

In set theory, you don't need choice to construct quotients right?
Is it true that if some object x exists and unique, then I can define it without the axiom of choice?

[Stepan Nesterov]

I used Classical.choice because it's the only way I knew how to use \exists in a function
But maybe it's not logically necessary?

[Aaron Liu]

in Lean a function isn't just exists unique

[Aaron Liu]

but in set theory functions are defined as a relation for which exists unique

[Aaron Liu]

type theory is different from set theory in this way

[Riccardo Brasca]

@Stepan Nesterov the point is docs#funext, that is trivially true in set theory.

[Riccardo Brasca]

And this is proved in Lean using quotients

[Aaron Liu]

unique choice is weaker than choice and is actually provable in set theory and in certain more constructive type theories but in Lean's type theory with propositional erasing unique choice isn't provable without additional axioms like choice

[Stepan Nesterov]

Aaron Liu said:

see lift is noncomputable

I see that Quot.lift is something called an 'opaque def'. Can I think of this as basically an axiom?

[Aaron Liu]

well it's actually not that

[Stepan Nesterov]

Then I don't understand what 'computable' means. If you just defined something by saying 'it's an axiom that there is such a thing', how is that computable?

[Aaron Liu]

as you can see it's a "quotient primitive" which is technically something different

/--
info: Quotient primitive Quot.lift.{u, v} : {α : Sort u} →
  {r : α → α → Prop} → {β : Sort v} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β
-/
#guard_msgs in
#print Quot.lift

[Aaron Liu]

Stepan Nesterov said:

Then I don't understand what 'computable' means. If you just defined something by saying 'it's an axiom that there is such a thing', how is that computable?

computable is unfortunately one of those words that means different things in different contexts and the meanings are related but not quite the same

[Stepan Nesterov]

Aaron Liu said:

as you can see it's a "quotient primitive" which is technically something different

/--
info: Quotient primitive Quot.lift.{u, v} : {α : Sort u} →
  {r : α → α → Prop} → {β : Sort v} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β
-/
#guard_msgs in
#print Quot.lift

Is it different from an axiom? Other than that an axiom is a Prop and this is data

[Aaron Liu]

it computes on Quot.mk

[Aaron Liu]

if it were an axiom then it wouldn't compute on anything

[Riccardo Brasca]

It is different from an axiom also because "being definitionally equal" cannot be an axioms

[Riccardo Brasca]

I mean the following

universe u v

variable  {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β)

example (h : ∀ (a b : α), r a b → f a = f b) (a : α) : Quot.lift f h (Quot.mk r a) = f a := rfl

[Riccardo Brasca]

you cannot assume that Quot.lift f h (Quot.mk r a) = f a, but you cannot assume that those are definitionally equal.

[Aaron Liu]

Stepan Nesterov said:

Aaron Liu said:

as you can see it's a "quotient primitive" which is technically something different

/--
info: Quotient primitive Quot.lift.{u, v} : {α : Sort u} →
  {r : α → α → Prop} → {β : Sort v} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β
-/
#guard_msgs in
#print Quot.lift

Is it different from an axiom? Other than that an axiom is a Prop and this is data

axioms can also be "data"

[Aaron Liu]

for example docs#Classical.choice is data

[Riccardo Brasca]

even better

universe u v

variable  {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β)

example (h : ∀ (a b : α), r a b → f a = f b) : (fun a => Quot.lift f h (Quot.mk r a)) = f := rfl

[Aaron Liu]

well that's just definitional eta

[Aaron Liu]

I guess definitional eta is one of the things that lets you prove funext

[Riccardo Brasca]

Yes, but because the values are definitionally equal

[Riccardo Brasca]

I am almost sure you cannot prove funext without it. Or at least, I once wrote all the various Quot.blah stuff as actual axioms and I wasn't able to prove funext without using the "real" Quot.sound

[Stepan Nesterov]

Riccardo Brasca said:

you cannot assume that Quot.lift f h (Quot.mk r a) = f a, but you cannot assume that those are definitionally equal.

wait what

[Stepan Nesterov]

Which one can you assume?

[Riccardo Brasca]

You can assume Eq (Quot.lift f h (Quot.mk r a)) (f a), because this is just a Prop

[Kevin Buzzard]

@Stepan Nesterov you're absolutely right in that quotients can just be made by brute force; the fact that your lift is noncomputable just means in practice that some proofs are harder if you do things your way.

Another way of thinking about it is this: We are taught that rfl proves goals of the form a=b when a and b are "equal by definition". But in Lean there is an actual definition of what it means to be "equal by definition" and this core part of the story has been thought about super-hard by computer scientists. In Lean, the fact that the triangle commutes in the universal property for quotients is part of core Lean's definition of what it means to be equal by definition, because this is something that one can impose when making the theory of quotients, and in practice this makes people's lives easier. It's analogous to the fact that if you define an inductive type like the naturals, and then use the auto-generated recursor to define a function f from the naturals (by saying that 0 goes to x and n+1 goes to whatever) then the reason that f 0 = x is true by rfl is again part of core Lean's definition of what it means to be equal by definition.

So in short you are totally right that logically one does not need all this quotient axiom stuff if all one wants to do is to build something which represents mathematics in some logically correct way and doesn't care at all about usability. But in practice if you want to make system which is actually usable for doing hard modern mathematics then it takes decades of study, trying to figure out how much you can get away with to make the system fast and usable, without making it inconsistent, and this is why doing computer theorem proving on hard maths took off in the 2020s and not the 1990s.

I went through a lot of the thoughts you're going through now when I was getting to grips with Lean -- asking myself "whyever did they set things up the way they set things up", e.g. "why is 1/0=0", "why is there one definition of "group with group law +" and a different definition of "group with group law *", "why do they use the axiom of choice to prove the law of the excluded middle" etc etc, and basically there are good answers to all of these questions but none of them are anything to do with mathematics, they are all about implementing an efficient system.

[Riccardo Brasca]

The other property is stronger, and there is no way for you to tell Lean "assume a and b are definitionally equal"

[Riccardo Brasca]

@Kevin Buzzard we believe you need them to prove propext and we suspect one can just assume propext and construct them by brute force.

[Riccardo Brasca]

Sorry, funext

[Kevin Buzzard]

At the bottom of the pile there will be some axioms, and it's a very natural question to ask "why those axioms" or "what if we used different axioms" or whatever (e.g. "why is an ext lemma or LEM a theorem not an axiom" (note that set extensionality and LEM are both axioms in ZFC, well, LEM is part of the logic) or "why are quotients an axiom but not a theorem" (quotients can be constructed in ZFC using other more primitive axioms)), but really the answer to these questions is "it is Lean's attempt to make a system which does mathematics efficiently in practice, it is not really of any mathematical relevance".

[Stepan Nesterov]

So basically what you are saying is that existence of quotients is a special type of axiom in that "definitionally equal" in Lean is not just "equal when you unfold all the definitions" but a more complicated relation which includes "left hand side is (Quot.lift f h (Quot.mk r a)) and right hand side is f a"

[Kevin Buzzard]

You literally cannot unfold a definition using Nat.rec in Lean because Nat.rec is an axiom. So saying that "addition is defined by a+0=a and a+Sx=S(a+x)" is really saying "Nat.add is defined in terms of Nat.rec" and when you unfold Nat.add a 0 you literally do not get a, you get Nat.rec a whatever

[Riccardo Brasca]

Exactly, this is the reason (or at least one of the reasons) you don't find Quot.lift in the code.

[Kevin Buzzard]

To make matters worse, it is a theorem that checking definitional equality in Lean is undecidable! Some people working in other theorem provers find this completely abhorrent. rfl is a computer program which provides a very good approximation to checking definitional equality but there are some very short examples kicking around of rfl failing to prove a = b when you can prove that they're definitionally equal (e.g. a = c and c = b can both be proved by rfl). What mathlib is strong evidence for, is that this phenomenon doesn't matter.

[Alfredo Moreira-Rosa]

Riccardo Brasca said:

In your theorem sound you use the ext tactic, you need quotient types to prove functional extensionality.

is ext really using funext ? i though extensionality theorems where different beasts... if you have any pointers about this in the docs, that would be nice

[Alfredo Moreira-Rosa]

Don't bother, i found it : https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Tactic/Ext.html in extcore.

[Snir Broshi]

Riccardo Brasca said:

I am almost sure you cannot prove funext without it. Or at least, I once wrote all the various Quot.blah stuff as actual axioms and I wasn't able to prove funext without using the "real" Quot.sound

An old thread about funext needing quotient defeq:
#new members > Definitional equality with quotient types @ 💬