Definitional equality with quotient types

Stream: new members

[Snir Broshi]

While trying to understand the proof of functional extensionality, I ran into this:

theorem wtf (func : Nat → Nat) :
    func 0 = Quot.lift
      (fun f => f 0)
      (fun _f _g h => by rw [h])
      (Quot.mk (fun f g => f = g) func)
  := rfl

I understand why it makes sense for there to be an axiom that lets Quot.lift and Quot.mk cancel each other here, but how come that the two sides here are definitionally equal? Why does this theorem not require using some axiom about quotient types? Especially since almost everything about Quot is some internal magic not exposed to Lean.

[Kyle Miller]

The docstring for docs#Quot.lift explains that this lift/mk cancelation is a reduction that's true definitionally. That's why the two sides are definitionally equal.

[Kyle Miller]

True definitionally means that it's a rule the kernel itself applies.

[Snir Broshi]

Cool, thanks
Do you know why Lean chose this way instead of adding an axiom? Is it to get functional extensionality?
And are Lean's type theory rules (especially about quotient types) documented somewhere? Does it have a name?

[Kyle Miller]

#leantt is Mario's thesis about Lean 3's type theory

[Kyle Miller]

Snir said:

Do you know why Lean chose this way instead of adding an axiom? Is it to get functional extensionality?

No, I'm pretty sure you could prove functional extensionality using an axiom version of this rule.

It's so that the kernel can reduce (compute) functions defined using quotient types.

It doesn't seem so different from how the kernel has reduction rules for recursors of inductive types rather than defining the rules as axioms.

[Snir Broshi]

Kyle Miller said:

No, I'm pretty sure you could prove functional extensionality using an axiom version of this rule.

I can't seem to be able to, unless you allow rw inside lambda expressions.
Here's the original proof of functional extensionality, with all Quot replaced by a new Quot' defined using axioms, and an additional Quot'.lift_mk which is the rule we talked about:

import Mathlib.Tactic.Basic

set_option pp.proofs true

universe u v

axiom Quot' {α : Sort u} (r : α → α → Prop) : Sort u
axiom Quot'.lift {α : Sort u} {r : α → α → Prop} {β : Sort v}
    (f : α → β) (a : ∀ (a b : α), r a b → f a = f b) :
    Quot' r → β
axiom Quot'.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot' r
axiom Quot'.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
axiom Quot'.lift_mk {α : Sort u} {r : α → α → Prop} {β : Sort v}
    (f : α → β) (h : ∀ (a b : α), r a b → f a = f b) (v : α) : Quot'.lift f h (Quot'.mk r v) = f v

theorem funext' {α : Sort*} {β : α → Sort*} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g := by
  let eqv (f g : (x : α) → β x) := ∀ x, f x = g x
  let extfunApp (f : Quot' eqv) (x : α) : β x :=
    Quot'.lift
      (fun (f : ∀ (x : α), β x) => f x)
      (fun _ _ h => h x)
      f
  change extfunApp (Quot'.mk eqv f) = extfunApp (Quot'.mk eqv g)
  exact congrArg extfunApp (Quot'.sound h)

This currently errors in the change tactic, because f and extfunApp (Quot'.mk eqv f) are not definitionally equal anymore. I can't prove f = extfunApp (Quot'.mk eqv f) using rw [Quot'.lift_mk] because it's inside a lambda expression.
Do you know how to proceed?

[Snir Broshi]

Kyle Miller said:

It doesn't seem so different from how the kernel has reduction rules for recursors of inductive types rather than defining the rules as axioms.

I didn't know that was a thing, and I agree, so my question applies to recursors as well. I don't understand why define reductions instead of axioms. Is it for ease-of-use, or do they result in a different type theory?

[Robin Arnez]

It's what allows you to prove 1 + 1 = 2 definitionally. Otherwise you have way fewer definitional equalities. So definitely also ease of use, not sure about type theory implications though

[Kyle Miller]

Snir said:

Do you know how to proceed?

Hmm, maybe you're right, it seems that having this be a definitional rule sort of "smuggles in" some functional extensionality, which quotient types let you leverage into creating the full funext.

[Snir Broshi]

Robin Arnez said:

It's what allows you to prove 1 + 1 = 2 definitionally.

Then I probably don't understand what recursors are, I thought they're all about induction (like nat_rec in Coq), T.casesOn.

[Robin Arnez]

Addition is defined using Nat.rec.

[Snir Broshi]

Robin Arnez said:

Addition is defined using Nat.rec.

How? I tried unfold Nat.add, but that doesn't work, so I copied Nat.add to a new my_add, and unfolding it just computes one step:

def my_add : Nat -> Nat -> Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (my_add a b)

theorem foo : my_add 1 2 = 3 := by
  unfold my_add
  sorry

Where does it use Nat.rec?

[Kyle Miller]

unfold uses unfolding lemmas. Try delta

[Kyle Miller]

You can also do #print my_add.

[Notification Bot]

This topic was moved here from #lean4 > Definitional equality with quotient types by Kyle Miller.

[Snir Broshi]

Robin Arnez said:

Addition is defined using Nat.rec.

So it looks like these two definitions of addition are not equivalent:

def my_add : Nat -> Nat -> Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (my_add a b)

def my_add' a b :=
  match a, b with
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (my_add a b)

I thought the first one was just syntactic sugar for the second one. Why does it need to use a recursor (Nat.brecOn) when it can just be a match statement? And why does Lean define these two very similar syntaxes to be vastly different?

[Kyle Miller]

The second one uses my_add instead of my_add', which is why they don't look equivalent (it's not recursive)

[Kyle Miller]

The first syntax is definitely syntactic sugar for a match.

[Kyle Miller]

Also, be sure to hover over match statements in the Infoview. They're actually functions, and if you #print them you'll see those functions are defined with recursors.

[Snir Broshi]

Oh I think I understand- the recursor is a fixed-point combinator, and the reduction rule for it is like the beta-reduction of the Y combinator, but typed. Thank you all!
I wonder what theories we'd lose if these reductions (for recursors & quotient types) were replaced with axioms about equality, other than functional extensionality which we already seem to have lost.

[Kevin Buzzard]

We'd lose many mathematician users because formalising commutative algebra would become hell

[Aaron Liu]

formalizing anything would become hell

[Aaron Liu]

since by decide would never work