why is quot an axiom?

Stream: general

[Kevin Buzzard]

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,
  -- ask about better way
  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]

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

[Kevin Buzzard]

A subtype of set β consisting of the equiv classes.

[Reid Barton]

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]

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]

Also, your proof of sound uses quot.sound

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

yes, that's called zfc

[Mario Carneiro]

you make set.ext an axiom

[Mario Carneiro]

and derive funext and the others by constructing everything from sets

[Mario Carneiro]

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]

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]

because it's an axiom

[Mario Carneiro]

it's literally baked into lean that this happens

[Kevin Buzzard]

I don't see the axiom in TPIL

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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?

[Mario Carneiro]

not necessarily

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

basically

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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