## Stream: general

### Topic: why is quot an axiom?

#### Kevin Buzzard (Dec 21 2018 at 22:33):

Can't we just do it like this?

import tactic.interactive

-- Lean has the "quotient" function to make equivalence classes.
-- Here I try to figure out why it is needed.

universes u v

namespace xena

-- this doesn't work with Prop but do I care?

variable {β : Type u}
variable (r : β → β → Prop)

-- equiv reln closure of r
inductive requiv {β : Type u} (r : β → β → Prop) : β → β → Prop
| of_r (a b : β) : r a b → requiv a b
| refl (a : β) : requiv a a
| symm ⦃a b : β⦄ : requiv a b → requiv b a
| trans ⦃a b c : β⦄ : requiv a b → requiv b c → requiv a c

definition equiv_class (r : β → β → Prop) (b : β) : set β := {c : β | requiv r b c}

definition quot {β : Type u} (r : β → β → Prop) : Type u :=
{eq_cl : set β // ∃ a : β, equiv_class r a = eq_cl}

namespace quot

definition mk : Π {α : Type u} (r : α → α → Prop), α → quot r :=
λ α r a, ⟨equiv_class r a,a,rfl⟩

theorem ind : ∀ {α : Type u} {r : α → α → Prop} {β : quot r → Prop},
(∀ (a : α), β (mk r a)) → ∀ (q : quot r), β q :=
λ α r β h q,
begin
rcases q with ⟨C,a,Ha⟩,
convert h a,
rw Ha,
end

noncomputable definition lift :
Π {α : Type u} {r : α → α → Prop} {β : Sort v} (f : α → β),
(∀ (a b : α), r a b → f a = f b) → quot r → β :=
λ α r β f h q,begin
apply f,
rcases q with ⟨C,HC⟩,
-- cases HC with a Ha, MEH
let a := classical.some HC,
have Ha : equiv_class r a = C := classical.some_spec HC,
exact a,
end

definition sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b :=
λ α r a b h,begin
unfold mk,
suffices : equiv_class r a = equiv_class r b,
simp [this],
ext,
split,
{ intro Hx,
show requiv r b x,
apply requiv.trans _ Hx,
apply requiv.symm,
apply requiv.of_r,
assumption,
},
{ intro Hx,
show requiv r a x,
apply requiv.trans _ Hx,
apply requiv.of_r,
assumption,
}
end

end quot

end xena


I think I do all the basic theory of quot. I've been teaching quotients (in ZFC) in my class and I was trying to figure out how to explain to mathematicians why all this quot.sound stuff all had to be dealt with via extra axioms, but I've just done it all myself. The two sacrifices I had to make were: (1) it doesn't work for props (but who takes a quotient on proofs of a prop?) and (2) lift (the map which mathematicians think of as a "descent", quite the other direction to the computer science word) is noncomputable. What does quot.sound offer that my set-up doesn't but which I want or need?

#### Kevin Buzzard (Dec 21 2018 at 22:33):

I just make the quotient type as a bunch of equivalence classes.

#### Kevin Buzzard (Dec 21 2018 at 22:34):

A subtype of set β consisting of the equiv classes.

#### Reid Barton (Dec 21 2018 at 22:40):

The differences are that lift is computable, and lift f _ (mk r x) = f x(which it looks like you haven't proved, but I'm sure you can) hold definitionally (this is quot.lift_beta).

#### Kevin Buzzard (Dec 21 2018 at 23:01):

Actually I'm struggling with the theorem about lift:

-- the computation principle
variables (β : Type v) (f : α → β) (a : α)
variable (h : ∀ a b , r a b → f a = f b)
theorem thm : lift f h (mk r a) = f a := begin
rcases (mk r a) with ⟨C,HC⟩, -- HC has nothing to do with a now.
let b := classical.some HC,
have Hb : equiv_class r b = C := classical.some_spec HC,
/-
α : Type u,
r : α → α → Prop,
β : Type v,
f : α → β,
a : α,
h : ∀ (a b : α), r a b → f a = f b,
C : set α,
HC : ∃ (a : α), equiv_class r a = C,
b : α := classical.some HC,
Hb : equiv_class r b = C
⊢ lift f h ⟨C, HC⟩ = f a
-/
show f b = f a,
apply h b a,
-- but I don't know a ∈ C
sorry
end


#### Chris Hughes (Dec 22 2018 at 00:14):

Also, your proof of sound uses quot.sound

#### Kevin Buzzard (Dec 22 2018 at 11:57):

Oh does it? I suppose that's cheating :-)

#### Mario Carneiro (Dec 22 2018 at 12:25):

You use set extensionality in the proof, which is an axiom in ZFC and is derived from propext and quot.sound in lean

#### Kevin Buzzard (Dec 24 2018 at 09:35):

OK so I proved xena.quot.thm. I think definitional equality is overrated, and if I have my maths hat on I'd say the same about computability. I am concerned about Chris' comment though. I am doing this to try and figure out how to explain to mathematicians why Lean wants quotients to be an extra axiom. But set extensionality is implied by function extensionality, right? Would another approach have been to make funext and/or propext axioms and then get quotients using my method? At least if we decide not to care about computability and definitional equality and be 100% mathematician.

#### Mario Carneiro (Dec 24 2018 at 09:53):

yes, that's called zfc

#### Mario Carneiro (Dec 24 2018 at 09:53):

you make set.ext an axiom

#### Mario Carneiro (Dec 24 2018 at 09:53):

and derive funext and the others by constructing everything from sets

#### Mario Carneiro (Dec 24 2018 at 09:54):

if you want to convince yourself, make a copy of set.ext as an actual axiom, and then derive all that and check that you didn't use propext or quot.sound in #print axioms

#### Kevin Buzzard (Feb 15 2019 at 23:58):

I now understand this quotient stuff better. I always understand stuff better with an example, and whilst equivalence classes of continuous non-archimedean valuations on a topological ring might not be the example best suited to everyone, working a lot on this example now I'm back on the perfectoid project has made me see the big picture much better.

Here's something I don't understand going back to the conversation above though. I can see why lift f _ (mk r x) = f x isn't going to be proved by rfl in my set-up above (quotients as equivalence classes), but now I don't understand why it can be proved with rfl if we use Lean's inbuilt quotient. If TPIL is to believed, the whole quot set-up in core is just made by writing down a load of axioms. How can rfl prove the computation law for quot?

#### Mario Carneiro (Feb 16 2019 at 00:00):

because it's an axiom

#### Mario Carneiro (Feb 16 2019 at 00:00):

it's literally baked into lean that this happens

#### Kevin Buzzard (Feb 16 2019 at 00:01):

I don't see the axiom in TPIL

#### Mario Carneiro (Feb 16 2019 at 00:01):

that's why quot has special magic powers you can't achieve even with isomorphic constructions

#### Kevin Buzzard (Feb 16 2019 at 00:01):

but this gives me an idea -- why don't I make the computation law I want to be true by rfl an axiom?

#### Kevin Buzzard (Feb 16 2019 at 00:02):

I can prove it after all, so it's true, so it's safe to make it an axiom, and then I can prove it with rfl?

not necessarily

#### Mario Carneiro (Feb 16 2019 at 00:02):

just because it's true doesn't mean it's a good reduction rule - you've seen that with simp

#### Mario Carneiro (Feb 16 2019 at 00:03):

and I mean axiom in the conventional sense of "a thing that lets you prove things you couldn't before", not the lean sense of "a constant with no computation rules that is called axiom or constant"

#### Kevin Buzzard (Feb 16 2019 at 00:03):

Oh. You mean "it's in the C++ code"?

basically

#### Mario Carneiro (Feb 16 2019 at 00:05):

one of the things I want to experiment with in the fork is user computation rules, which would allow you to install your own computation rules just like you can add your own axioms

#### Johan Commelin (Feb 16 2019 at 05:10):

@Mario Carneiro But in our case of a "fake" quotient, I guess it would be a good reduction rule. Is that true?

#### Mario Carneiro (Feb 16 2019 at 07:26):

It's hard to say. Part of the problem with having computation rules on a type that's not a constant (like quot) is that there are already computation rules, if not very useful ones, and adding a reduction rule on top of that can cause failure of confluence

#### Mario Carneiro (Feb 16 2019 at 07:27):

For a structure, that will be things like a projection on a structure instance computing to the value

Last updated: May 08 2021 at 17:33 UTC