Some Basic Lattice Theory With Lean (2)

In the previous post I went over a very basic introduction to lean, as well as proved a simple proposition about lattice theory. In the same way one might learn a new language by attempting some projecteuler problems, going through a variant of the Ninety-Nine Problems, or even just coding up a new simple project, I endeavored to learn lean by going through a basic, undergraduate level textbook on lattice theory: the aptly-titled Lattice Theory by Garrett Birkhoff. As an actual book for undergraduate math, it's very straightforward -- the definitions are easy to digest, the pace is not too fast, the exercises and theorems understandable, and best of all: it doesn't assume much knowledge out of the gate. But pair it with learning a new theorem prover, when I hadn't used any theorem provers (except pen/pencil and paper) before, and suddenly proofs that would take a few minutes to understand would now take days to formulate and write down. I think trying to document my process could be of interest, and will attempt to do so in this and the next few blog posts.

Unfortunately, most of my incorrect code or experiments aimed at interacting with lean were eventually overwritten, as I learned how to translate mathematical thought into code. So while I can't recreate my original thought process, I do remember when certain abstractions caused more frustration than usual, and I will attempt to write down what was going on in my mind at the time, even if I can't produce the original sequence of refactorings.

Defining a partial order

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

This definition was mostly straightforward, though there was the question of whether to use a typeclass, as depicted here (and what I ultimately went with), or using structure. I also toyed with using different notation for the ordering relation, as the way it's implemented -- by providing an instance of the LE typeclass -- can sometimes lead to funkiness with instance resolution. (An example of such funkiness will show up in the next post in this series.)

instance [PartialOrder S] : LT S where
  lt := fun a b => a <= b ∧ a ≠ b

The textbook writes the following:

If x \ge y but x \neq y, one writes x > y, and says x "is greater than" or "properly includes" y.

At first I had the class definition extending both LE S and LT S, but that made it difficult to use the definition given in the book -- I had to add a new axiom after transitivity to define the difference between strict and non-strict ordering, and using it in proofs was a pain because I needed to appeal to it. With the implementation here, read perhaps as "if S is a partial order, then it has an instance of LT", lean just knows that whenever the strict version is used, it's equivalent to the instance given.

Conveniences

universe u
variable {S : Type u}
variable [pos : PartialOrder S]

def refl {a : S} :
  a <= a :=
    PartialOrder.refl a

def antisymm {a b : S} :
  a <= b -> b <= a -> a = b :=
    PartialOrder.antisymm a b

def trans {a b c : S} :
  a <= b -> b <= c -> a <= c :=
    PartialOrder.trans a b c

The code block at the top lets us use those names without quantifying them -- lean is smart enough to insert them as arguments to definitions that use them, and it makes writing further definitions easier. For example, note in the three definitions above, there's no declaration of [PartialOrder S]. This is because that instance is already in scope, otherwise, almost every subsequent definition and theorem would need to carry that class constraint.

Furthermore, the three rewritten versions of the partial order axioms are for ergonomic reasons -- the elements of type S are given as implicit parameters. In other words, we're relying on lean to infer those arguments based on context, like other arguments or a proof goal's type. If we were to use the axioms directly, we'd use them akin to have hac : a <= c := PartialOrder.trans a b c hab hbc vs the more concise have hac : a <= c := trans hab hbc.

First results

theorem no_el_less_self (a : S) : ¬ a < a := by
  intro asm
  have uhOh : a ≠ a := asm.right
  contradiction

In lean, like in most of logic, negation is defined as implying falsehood: \lnot P := P \to \bot. Then, since the goal is actually a function type, we can introduce the assumption and derive False from it. Here, we destruct the conjunction (remember that the strict ordering is defined in an instance, as a conjunction) to pull out the relevant inequality, and finish the proof with the contradiction tactic.

theorem lt_trans {a b c : S} :
  a < b -> b < c -> a < c := by
    intro asm_ab asm_bc
    have hac : a <= c := trans asm_ab.left asm_bc.left
    suffices hnac : a ≠ c from ⟨hac, hnac⟩
    intro tac
    have hcb : c <= b := by
      rw [<-tac]
      exact asm_ab.left
    have hbc : b = c := antisymm asm_bc.left hcb
    have hnbc : b ≠ c := asm_bc.right
    contradiction

Transitivity of < is the first result that "has a lot going on". There are two assumptions, each of which is actually a conjunction of two simpler formulas. So there are three variables in scope and (essentially) four assumptions, and the goal is to show two things (joining them in a conjunction, as per the definition of <). The first two lines of the proof are straightforward, but the third uses a tactic that says more-or-less the following:

It suffices to show that a \neq c, since that, combined with the proof that a \le c, is the goal.

Given that lean accepts that tactic (which depends on whether the code to the right of from does, in fact, resolve the overall goal), the goal is changed to show that a != c.

Again, since inequality is defined as the negation of equality, the goal allows us to assume a hypothesis with an aim towards deriving a contradiction. To that end, we introduce the assumption tac : a = c (short for "towards a contradiction"). When defining hcb, we first rewrite its goal (c <= b) by flipping the equality in tac to get something like the following:

But we already know that a <= b, it's in one of the assumptions. With this, we can show that b = c by antisymmetry and b != c by assumption, resulting in a contradiction. Voila!

First difficulties

The first theorem in the book is presented as follows, preceded by an explanation as to why its true:

Theorem 1. Any subset of a partly ordered set is itself partly ordered by the same inclusion relation.

In reality, the theorem is almost blindingly obvious -- taking subsets doesn't result in the structure forgetting it's a partial order, so obviously any subset of a partial order remains a partial order. But in lean, it's not as straightforward. First, there's the problem of what it means to be a subset. With the construction given, a partial order in lean is a type class, one that's instantiated by types -- not sets. So there are a few basic options:

1. Implement enough set theory to be able to talk about subsets -- this exists in lean 3's mathlib, but we're using lean 4, and honestly I feel like this shouldn't have to rely on an external library.
2. Dive into lean's version of subtyping (which I hear is different from the OOP concept, though I can't confirm as I don't know any OOP).
3. An option I just thought of: have an arbitrary type T and a function f : T -> S, as well as a proof that f is injective. In topos theory, this is basically how subsets are handled.

So the tradeoff is that 1 probably requires a lot of scaffolding, all of which I know, but which won't be that fun to implement; and 2 requires figuring out enough of how subtypes work to be able to give an instance to such a subtype that the compiler doesn't yell at me. Since the point is to learn lean, let's go with 2.

Subtypes in lean are akin to definable sets in logic -- they're parameterized by a formula with a free variable, and the syntax is: {x : X // φ x}. You can read this as "the type of x in X such that φ x". Therefore an element of this type is a pair -- an x : X and a proof that φ x.

For our purposes, we don't really care what φ is. Because of this, we only really want to talk about the elements, we don't care about the associated proof -- and therefore, the goals in lean's infoview will sometimes look scary, since lean will try to convince you that it does care about both.

instance PartialOrderSubset {φ : S -> Prop} :
  PartialOrder { a : S // φ a } where
    le := by
      intro ⟨a, _⟩ ⟨b, _⟩
      exact a <= b

    refl := by
      intro ⟨a, _⟩
      exact refl

    antisymm := by
      intro ⟨a, _⟩ ⟨b, _⟩ asm_ab asm_ba
      have : a = b := antisymm asm_ab asm_ba
      simp [this]
      done

    trans := by
      intro a b c hab hbc
      have : a.val <= c.val := trans hab hbc
      exact this

The first thing to notice is that there are four typeclass methods, not three. This is because partial orders are defined as extensions of another typeclass, so we have to provide all those methods at once. The first method is easy enough: the ordering on the subtype is defined by the ordering on the parent S, and nothing else.

The second method, refl, is also fairly easy. Given what we defined for le it stands to reason we only need to show that the first part of a subtype element (the value, as opposed to the property) satisfies reflexivity in the parent. And it does, by appealing to reflexivity on the parent.

Antisymmetry is a bit of a headscratcher. We can reason easily enough about the ordering relation, but how do we deal with equality? We can show equality of the two values, but will we also have to show equality of the two properties? Would we have to appeal to propositional extensionality?

Let's try ignoring the properties and seeing if that suffices. And sure enough, it does (otherwise the done tactic would not be accepted).

Transitivity is not much worse than reflexivity, and the proof proceeds straightforwardly. In the next post, we'll jump in to lean's quotient types which are based on axioms and principles that give it a lot of power.