Getting Into Quotients With Lean (3)

In the previous post, I went over some basic results about partial orders in lean, culminating in a proof that any (definable) subset of a partial order is also a partial order, inheriting the same ordering relation. The textbook I've been following then defines a quasi-order as a set S with a binary relation \le such that for all a, b and c in S:

The main (well, only) result in this section is that a partial order can be recovered by defining a suitable equivalence relation, and taking a quotient over such a relation. In natural language, it proceeds as follows:

Definition: Let \sim be a binary relation on a quasi-order S such that a \sim b if and only if a \le b and b \le a.

Proposition: \sim is an equivalence relation.

Proof: Recall that an equivalence relation is a reflexive, symmetric, and transitive relation.

1. Reflexivity: By reflexivity of the quasi-order, a \le a.
2. Symmetry: By definition of \sim.
3. Transitivity: By transitivity of the quasi-order.

Now consider Q := S/\sim, the quotient of S by \sim. The claim is that Q is a partial order, and the trick is in showing antisymmetry--this will follow due to the usual method of identifying equivalent elements in the quotient. Now, when many people think of quotients, they tend to think of a partition of S into pairwise disjoint yet exhaustive subsets, where each subset is a nonempty set of mutually-related ("equivalent") elements, at least as far as \sim is concerned.

Theorem: Let \rho be any quasi-ordering of a set X. The relation x \sim y, meaning that x \rho y and y > \rho x, is an equivalence relation. If "equivalent" elements are identified, \rho becomes a partial ordering.

In the book's terminology, the \rho relation is just \le, so we've already shown that it's an equivalence relation. It then shows that the quotient is a partial order as follows:

1. Suppose x \le y and x \sim x^*, y \sim y^*.
2. Then x^* \le x \le y \le y^* which implies x^* \le y^*.
3. This shows \le is defined consistently on the quotient.
4. "It follows immediately from this that x \le y and y \le x imply x \sim y (i.e. x = y in the system formed by the subclasses)."

lean

As a note, not every theorem here is used. Some of them are exploratory, and serve no other purpose than to interact with lean's InfoView to see how the tactic state changes, or to convince myself that a certain approach is viable.

class QuasiOrder (S : Type u) extends LE S where
  refl : ∀ a : S, a <= a
  trans : ∀ a b c : S, a <= b -> b <= c -> a <= c

variable {S T : Type}
variable [qos : QuasiOrder S]
variable (a b c : S)

def r : Prop := a <= b ∧ b <= a
infix:50 " ~ " => r

Now we'll get into the proof that ~ is an equivalence relation.

theorem r.def :
  a ~ b <-> a <= b ∧ b <= a := by
    apply Iff.intro
    . intro asm
      rw [r] at asm
      assumption
    . intro asm
      rw [<-r] at asm
      assumption

theorem r.refl :
  a ~ a := by
    rw [r]
    have h : a <= a := QuasiOrder.refl a
    exact ⟨h, h⟩

theorem r.symm :
  a ~ b -> b ~ a := by
    intro asm
    have ⟨l, r⟩ : a <= b ∧ b <= a := asm
    exact ⟨r, l⟩

theorem r.trans :
  a ~ b -> b ~ c -> a ~ c := by
    intro asmab asmbc
    have hab : a <= b ∧ b <= a := asmab
    have hbc : b <= c ∧ c <= b := asmbc
    have l : a <= c := QuasiOrder.trans a b c hab.left hbc.left
    have r : c <= a := QuasiOrder.trans c b a hbc.right hab.right
    exact ⟨l, r⟩

instance eqvr : @Equivalence S r where
  refl := r.refl
  symm := by
    intro a b
    exact r.symm a b
  trans := by
    intro a b c
    exact r.trans a b c

The only thing to note here is that lean will complain if I try instance eqvr : Equivalence r despite the carrier, S, being marked as implicit. The most common error I saw while coding is "typeclass instance problem is stuck, it is often due to metavariables". Explicitly passing in all arguments seems to resolve it, but I do wish I wouldn't have to be this explicit.

instance setoid : Setoid S where
  r := r
  iseqv := eqvr

example : a ≈ b <-> a ~ b := by
  simp [HasEquiv.Equiv, Setoid.r]
  done

@[simp] theorem equiv.def :
  a ≈ b <-> a <= b ∧ b <= a := by
    simp [HasEquiv.Equiv, Setoid.r, r]
    done

A Setoid is what lean calls a type with an associated equivalence relation. It allows the use of ≈ notation, which as you can see is equivalent to the ~ we defined earlier. All of this -- proving that ~ is an equivalence relation and defining the setoid -- is necessary to use lean's Quotient construction.

def Q (inst : QuasiOrder S) := Quotient (@setoid S inst)

notation:max "⟦" e "⟧" => Quotient.mk setoid e

example : Quotient.mk setoid a = ⟦a⟧ := rfl

example : a ≈ b -> ⟦a⟧ = ⟦b⟧ := Quotient.sound

example : ⟦a⟧ = ⟦b⟧ -> a ≈ b := Quotient.exact

example : a ≈ b <-> ⟦a⟧ = ⟦b⟧ := by
  apply Iff.intro
  . exact Quotient.sound
  . exact Quotient.exact

Here we see how to define a quotient over a setoid, and how to lift elements into the quotient. There are also builtin functions for going from the underlying type to the quotient and vice-versa. We also show that equivalent elements are identified in the quotient, which is the primary motivating reason to use quotients in the first place.

As a note, if I try to define Q to be parameterless, lean will yell at me with the good old "typeclass instance problem is stuck" error.

def respectful (f : S -> T) :
  Prop :=
    ∀ a b : S, a ≈ b -> f a = f b
    
def universal1 (g : Q qos -> T) :
  {f : S -> T // respectful f} :=
    let f : S -> T := fun s => g ⟦s⟧
    let prf : respectful f := by
      intro a b asm
      show g ⟦a⟧ = g ⟦b⟧
      have h : ⟦a⟧ = ⟦b⟧ := Quotient.sound asm
      rw [h]
      done
    ⟨f, prf⟩

def universal2 (f : S -> T) (hf : respectful f) :
  Q qos -> T :=
    Quotient.lift f hf

Now we define what it means for a function from our type S to an arbitrary type T to respect the equivalence relation. The other two definitions characterize the universal property of quotients. The first, universal1, says that given any function from the quotient to an arbitrary T, there exists a function from S to T that is respectful -- this function is just composition with quotient-lifting (in lean notation, the function fun a : S => ⟦a⟧). The second definition, universal2, is just the converse: given a respectful function from S to T, we can construct a function from the quotient to T. Notice that universal2 is defined using the builtin Quotient.lift, which lifts a function from the underlying type to one from the quotient.

example (f : S -> T) (hf : respectful f) :
  f = λ a => Quotient.lift f hf ⟦a⟧ := by
    rfl

This is one of the most important parts of how lean implements quotients. When I first saw this proof, I had no idea what was going on -- it says that given any respectful function, it's the same as taking an element, sending it to its equivalence class, then applying the lifted function to that class. But the weird thing, for me, was that it wasn't proved using function extensionality -- it's just "true by definition". I didn't understand what was going on, but now I do: lean's kernel reduces the RHS to the LHS as a computational rule. That is, rfl works because there's special code that lets the kernel reduce functions that are lifted to the quotient to their unlifted form, given a proof that the function is respectful. This computational rule is one component that will let us reason about elements in the quotient.

example (g : Q qos -> T) :
  g = Quotient.lift (fun a : S => g ⟦a⟧) (universal1 g).2 := by
    funext z
    apply Quotient.inductionOn z $ by
      intro a
      rfl

Here's another. In the proof, z is introduced as an arbitrary element in the quotient. The proof uses function extensionality, which says two functions are the same iff they agree at every point. Now, the other component that lets us reason about quotient elements is Quotient.inductionOn: it basically says that to prove something about an arbitrary quotient element, all you have to do is prove the same thing for an equivalence class ⟦a⟧ for arbitrary a : S. As such, we introduce such an arbitrary element a, at which point we can finish the proof by rfl precisely because of the computational rule mentioned earlier.

Now we can turn our attention to showing that the quotient is a bona-fide partial order. Like in the previous post where the same was proved for subsets, we first have to define what it means for elements in the quotient to be ordered -- that is, give an instance for LE (Q qos). Since we only really have access to the underlying ordering on S, we'll have to use that in some way. And because the ordering is binary, and we'll want to lift it to the quotient, a good place to start is Quotient.lift₂, which has the following type:

Quotient.lift₂ :
    (f : α → β → φ)
    (c : (a₁ : α)
      -> (b₁ : β)
      -> (a₂ : α)
      -> (b₂ : β)
      -> a₁ ≈ a₂
      -> b₁ ≈ b₂
      -> f a₁ b₁ = f a₂ b₂
    )
    (q₁ : Quotient s₁)
    (q₂ : Quotient s₂)
    : φ

While the type is intimidating, what it's saying is simple: Given a binary function subject to a certain property, the function can be lifted to act on arbitrary elements of the quotient. The property the function has to fulfill is a generalization of respectfulness to two variables.

So in order to lift the ordering relation to the quotient, we'll need to prove that it's respectful:

theorem le.lifts (a₁ b₁ a₂ b₂ : S) :
  a₁ ≈ a₂ -> b₁ ≈ b₂ -> (a₁ <= b₁) = (a₂ <= b₂) := by
    intro asma asmb
    simp [r] at asma asmb
    apply propext
    apply Iff.intro
    . intro asm1
      have hab1 : a₂ <= b₁ := QuasiOrder.trans a₂ a₁ b₁ asma.right asm1
      have hab2 : a₂ <= b₂ := QuasiOrder.trans a₂ b₁ b₂ hab1 asmb.left
      exact hab2
      done
    . intro asm2
      have hab1 : a₁ <= b₂ := QuasiOrder.trans a₁ a₂ b₂ asma.left asm2
      have hab2 : a₁ <= b₁ := QuasiOrder.trans a₁ b₂ b₁ hab1 asmb.right
      exact hab2
      done

Now, the goal is a little weird: (a₁ <= b₁) = (a₂ <= b₂). It's awkward to say that two inequalities are equal, but luckily lean has an axiom that will help us, that of propositional extensionality. That axiom can be interpreted to say that two objects are equal if and only if they share every property. In code, (P <-> Q) -> P = Q. Thus to show equality of the propositions, we only need to show they imply each other.

With respectfulness proved, we're able to define the ordering relation on the quotient:

def Q.le (q₁ q₂ : Q qos) :
  Prop :=
    Quotient.lift₂ (fun a b : S => a <= b) le.lifts q₁ q₂

instance : LE (Q qos) where
  le := Q.le

It may sound obvious, but every subsequent theorem that works towards showing the quotient is a partial order will be based on the definition given here. In my first attempt I thought I may have to use Quotient.lift and its higher-arity versions to prove as much, but as we will see that is unnecessary.

Earlier I mentioned that to prove something about elements in the quotient, the go-to function is Quotient.inductionOn. Let's look at its type:

Quotient.inductionOn :
    {α : Sort u}
    {s : Setoid α}
    {motive : Quotient s → Prop}
    (q : Quotient s)
    (h : (a : α) → motive (Quotient.mk s a))
    : motive q 

Basically, given a predicate on quotient elements and a proof that it holds of an arbitrary equivalence class, the induction gives that the predicate holds of all quotient elements. There are also the theorems Quotient.inductionOn₂ and Quotient.inductionOn₃, which work on two and three arbitrary elements, respectively.

For reflexivity, if you stub out the proof that Quotient.inductionOn requires with sorry, you can see what type lean is expecting. It will tell you ∀ a : S, ⟦a⟧ <= ⟦a⟧. Now remember that ⟦a⟧ <= ⟦a⟧ was defined above by lifting the ordering relation on S to the quotient. Also remember that the computation rule for Quotient.lift said that lean can reduce Quotient.lift f hf ⟦a⟧ to just f a. However, we didn't use Quotient.lift in the LE (Q qos) instance--we used Quotient.lift₂. Therefore, a reasonable question to ask is whether a similar reduction rule is in place for the binary lift. To find this out, we can proceed as follows: write down the type of the theorem of the reduction rule, but for binary functions instead, and see whether the proof can be finished with rfl and nothing else. If it can, assuming we wrote the correct type, then we'll know we're in a good spot. You can look at the type of Quotient.lift and the type of the theorem that witnesses the reduction, and also the type of Quotient.lift₂. These three types should be enough to figure out the fourth type, that of the theorem:

example
  (f : S -> S -> T)
  (h : ∀ a₁ b₁ a₂ b₂ : S, a₁ ≈ a₂ -> b₁ ≈ b₂ -> f a₁ b₁ = f a₂ b₂) :
    f = fun a b => Quotient.lift₂ f h ⟦a⟧ ⟦b⟧ := by
      rfl

Sure enough, no complaints from lean. Now we can finally combine everything and start proving theorems:

theorem Q.refl (q : Q qos) :
  q <= q :=
    Quotient.inductionOn q QuasiOrder.refl

theorem Q.trans (q₁ q₂ q₃ : Q qos) :
  q₁ <= q₂ -> q₂ <= q₃ -> q₁ <= q₃ :=
    Quotient.inductionOn₃ q₁ q₂ q₃ QuasiOrder.trans

These are so simple that they're essentially self-explanatory. However, the interesting bit is antisymmetry, since that was always going to be proved differently due to our inability to rely on the quasi-order. This will require another builtin, an axiom for quotients that turns lean's quotient types into bonafide mathematical quotients (we already saw this earlier, but it bears repeating since it's so important):

def sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b

The axiom turns equivalences into equalities, which is exactly what we need.

theorem Q.antisymm (q₁ q₂ : Q qos) :
  q₁ <= q₂ -> q₂ <= q₁ -> q₁ = q₂ :=
    Quotient.inductionOn₂ q₁ q₂ $ by
      intro a b asm1 asm2
      exact Quotient.sound ⟨asm1, asm2⟩
      done

And finally:

instance : PartialOrder (Q qos) where
  refl := Q.refl
  antisymm := Q.antisymm
  trans := Q.trans

Notes:

1. Much thanks to Kevin Buzzard and the exercises on quotients in lean which greatly helped me understand how to use them. The link is written for lean 3, but I adapted and went through the exercises in lean 4.
2. Explanation of the universal property: If you consider the comma category of objects under S, the universal property says that the object i := (Q, \hookrightarrow) where \hookrightarrow : a \mapsto \llbracket a \rrbracket is the function sending elements to their equivalence class, is initial. That is, for any object a := (T, f) in the comma category, there's a unique arrow g : i \to a from i to a: