Notes on Lean

Axioms on equalityπŸ”—

The quotient axiom and propositional extensionality postulate equality assuming equivalence. They differ in the nature of the equivalence.

The quotient axiom asserts that ⟦x⟧ = ⟦y⟧ if x β‰ˆ y.

axiom Quot.sound.{u} : βˆ€ {Ξ± : Sort u} {r : Ξ± β†’ Ξ± β†’ Prop} {a b : Ξ±}, r a b β†’ Quot.mk r a = Quot.mk r b#print Quot.sound

example (Ξ± : Sort u) (r : Ξ± β†’ Ξ± β†’ Prop) (x y : Ξ±)
  (h : r x y)
  : Quot.mk r x = Quot.mk r y
:= Quot.sound h

We will show below that the quotient axiom implies function extensionality.

The axiom of propositional extensionality asserts that p = q if p ↔ q.

axiom propext : βˆ€ {a b : Prop}, (a ↔ b) β†’ a = b#print propext

example (p q : Prop)
  (h : p ↔ q)
  : p = q
:= propext h

We will show below that propositional extensionality implies quotient exactness.

Here is a small example illustrating that Lean tracks the axioms that each proof depends on.

lemma t_eq_notf : True = Β¬False
:= propext ⟨λ h ↦ id, Ξ» h ↦ trivial⟩

't_eq_notf' depends on axioms: [propext]#print axioms t_eq_notf

Function extensionalityπŸ”—

Recall that function extensionality is formulated as follows.

theorem funext.{u, v} : βˆ€ {Ξ± : Sort u} {Ξ² : Ξ± β†’ Sort v} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g :=
fun {Ξ±} {Ξ²} {f g} h ↦
  let eqv := fun f g ↦ βˆ€ (x : Ξ±), f x = g x;
  let extfunApp := fun f x ↦ f.liftOn (fun f ↦ f x) fun x_1 x_2 h ↦ h x;
  id (congrArg extfunApp (Quot.sound h))#print funext
'funext' depends on axioms: [Quot.sound]#print axioms funext

example (Ξ± : Sort u) (Ξ² : Ξ± β†’ Sort v) (f g : (x : Ξ±) β†’ Ξ² x)
  (h : βˆ€ x, f x = g x)
  : f = g
:= funext h

The proof of funext is based on defining an equivalence of functions by βˆ€ x, f x = g x, lifting function application on the equivalence classes, and using the quotient axiom together with the quotient reduction.

example (Ξ± : Sort u) (Ξ² : Ξ± β†’ Sort v) (f g : (x : Ξ±) β†’ Ξ² x)
  (h : βˆ€ x, f x = g x)
  : f = g
:=
  -- Definition of a setoid of functions
  let Ξ¦ := (x : Ξ±) β†’ Ξ² x
  let r (φ₁ Ο†β‚‚ : Ξ¦) := βˆ€ x, φ₁ x = Ο†β‚‚ x
  have r_refl (Ο† : Ξ¦) : r Ο† Ο†
    := Ξ» x ↦ rfl
  have r_symm {φ₁ Ο†β‚‚ : Ξ¦} (h : r φ₁ Ο†β‚‚) : r Ο†β‚‚ φ₁
    := Ξ» x ↦ (h x).symm
  have r_trans {φ₁ Ο†β‚‚ φ₃ : Ξ¦} (h1 : r φ₁ Ο†β‚‚) (h2 : r Ο†β‚‚ φ₃)
    : r φ₁ φ₃
    := Ξ» x ↦ calc
      φ₁ x
      _ = Ο†β‚‚ x := h1 x
      _ = φ₃ x := h2 x
  let s : Setoid Φ := ⟨r, ⟨r_refl, r_symm, r_trans⟩⟩
  -- Lift of function application
  let lifted_app (Ο† : Quotient s) (x : Ξ±) :=
    have {φ₁ Ο†β‚‚ : Ξ¦} (h : φ₁ β‰ˆ Ο†β‚‚) : φ₁ x = Ο†β‚‚ x := h x
    Quotient.lift (Ξ» ψ ↦ ψ x) (Ξ» _ _ h ↦ this h) Ο†
  -- Use the quotient axiom
  have : ⟦f⟧ = ⟦g⟧ := Quotient.sound h
  -- Use the quotient reduction
  calc
    f = lifted_app ⟦f⟧ := rfl
    _ = lifted_app ⟦g⟧ := congrArg lifted_app this
    _ = g := rfl

Quotient exactnessπŸ”—

Recall that Quotient.exact is the implication converse to Quotient.sound.

theorem Quotient.exact.{u} : βˆ€ {Ξ± : Sort u} {s : Setoid Ξ±} {a b : Ξ±}, ⟦a⟧ = ⟦b⟧ β†’ a β‰ˆ b :=
fun {Ξ±} {s} {a b} h ↦ Quotient.rel_of_eq✝ h#print Quotient.exact
'Quotient.exact' depends on axioms: [propext]#print axioms Quotient.exact

example (Ξ± : Sort u) (s : Setoid Ξ±) (a₁ aβ‚‚ : Ξ±)
  (h : (⟦aβ‚βŸ§ : Quotient s) = ⟦aβ‚‚βŸ§)
  : a₁ β‰ˆ aβ‚‚
:= Quotient.exact h

The proof of Quotient.exact is based on turning the logical equivalence in the below lemma eqv_iff into equality using propext. In order to use β‰ˆ in calc blocks, we declare a local instance of Trans.

open Setoid in
lemma eqv_iff {Ξ± : Sort u} {s : Setoid Ξ±} {x₁ y₁ xβ‚‚ yβ‚‚ : Ξ±}
  (hx : x₁ β‰ˆ xβ‚‚) (hy: y₁ β‰ˆ yβ‚‚)
  : (x₁ β‰ˆ y₁) ↔ (xβ‚‚ β‰ˆ yβ‚‚)
:=
  let : Trans (Ξ± := Ξ±) (Β· β‰ˆ Β·) (Β· β‰ˆ Β·) (Β· β‰ˆ Β·) := ⟨trans⟩
  have mp := Ξ» h ↦ calc
    xβ‚‚
    _ β‰ˆ x₁ := symm hx
    _ β‰ˆ y₁ := h
    _ β‰ˆ yβ‚‚ := hy
  have mpr := Ξ» h ↦ calc
    x₁
    _ β‰ˆ xβ‚‚ := hx
    _ β‰ˆ yβ‚‚ := h
    _ β‰ˆ y₁ := symm hy
  ⟨mp, mpr⟩

We now prove Quotient.exact by lifting β‰ˆ and using the recursor of =.

example (Ξ± : Sort u) (s : Setoid Ξ±) (a₁ aβ‚‚ : Ξ±)
  (h : (⟦aβ‚βŸ§ : Quotient s) = ⟦aβ‚‚βŸ§)
  : a₁ β‰ˆ aβ‚‚
:=
  let lifted_eqv (q₁ qβ‚‚ : Quotient s) : Prop :=
    Quotient.liftβ‚‚
      (Ξ» x y ↦ x β‰ˆ y)
      (Ξ» _ _ _ _ hx hy ↦ propext (eqv_iff hx hy))
      q₁ qβ‚‚
  let q₁ := ⟦aβ‚βŸ§
  have : lifted_eqv q₁ q₁ :=
    Quotient.ind (motive := Ξ» q ↦ lifted_eqv q q) s.refl q₁
  Eq.rec (motive := Ξ» q _ ↦ lifted_eqv q₁ q) this h