Getting Started With Lean (1)

Lean is possibly the most interesting and exciting language I've ever come across. Like Idris, it's a dependently-typed language, but there are many major differences, both in style and substance. While Idris is based on quantitative type theory (QTT), Lean uses the calculus of inductive constructions (CIC) as its basis.

Lean is also much more heavily oriented towards interactive and automatic theorem proving, whereas Idris is more firmly in the programming camp. In terms of syntax, Idris is (like PureScript) influenced by Haskell and ML syntax in general. Lean, on the other hand, takes great pains to ensure its syntax is easily extensible by the user, since one of its target audiences is mathematicians, who have developed their own notation for their own fields of study.

While Idris can be used to prove mathy theorems, doing so feels like you're often fighting against the type checker.

In addition, one of the most surprising and welcome properties Lean has is that its type system has not been proved unsound. In languages like PureScript, Haskell and even Elm (despite what its front page says), it's pretty easy to subvert the type-checker, either through the FFI (easy in PS), partiality (Haskell's List.head) or allowing non-wellfounded data types (as in the previous link).

As a taste, here are three examples proving the same proposition, one in natural mathematical language, one in Idris, and one in Lean:

Natural language

Definition: A lattice \mathcal L is a set L together with two binary operations on L, called meet (\wedge) and join (\vee), satisfying the following equalities (Note how each is a dual of the other, in the sense that they are the same except by replacing \wedge with \vee and vice-versa):

1. \forall a, b \in L, a \vee (a \wedge b) = a
2. \forall a, b \in L, a \wedge (a \vee b) = a

Proposition: For any a \in L, a \wedge a = a and a \vee a = a.

Proof: We'll prove the first (the second will follow by the duality noted above). We wish to show that a \wedge a = a. Note how the main connective in axiom 2 is a meet, as is the main connective in the proposition. Also note how b is irrelevant in the axioms -- that is, it could be any term at all, and the RHS would still be a. Therefore our goal will be to find a substitution for b that allows us to simplify the term on the LHS, as there is no other rule that allows us to simplify a term other than substitution.

Next, notice how the term in parentheses is a join, the same as in axiom 1. This gives us a hint as to what the substitution should be. Set b in axiom 2 to a \wedge a, for example, and then we have

We can apply axiom 1 on the RHS, deriving the result:

Idris

We'll prove the second part of the proposition.

infix 7 /\ , \/

interface Lattice l where
  (\/) : l -> l -> l
  (/\) : l -> l -> l
  absorb1 : (a, b : l) -> a \/ (a /\ b) = a
  absorb2 : (a, b : l) -> a /\ (a \/ b) = a

idempotencyJ : (a : l) -> Lattice l => a \/ a = a
idempotencyJ a =
  let
    -- lem1 : a /\ (a \/ a) = a
    lem1 = absorb2 a a
    -- lem2 : a \/ (a /\ (a \/ a)) = a
    lem2 = absorb1 a (a \/ a)
  in replace {p = \b => a \/ b = a} lem1 lem2

Note how we define the lattice as an interface, and that we can place all of our assumptions on the LHS of the double arrow =>. The substitution happens in the final line, and we know the proposition is proved because the file is successfully type-checked. We also use replace and explicitly tell the compiler where the subterm we are interested in appears. In general this can be a little tiring to use.

Lean

Here we'll prove both, and change notation slightly -- in VSCode, typing \join and \meet create ⊔ and ⊓ respectively (when editing a lean file, provided the development environment is set up as intended), so I've used those to reduce the cognitive burden of associating different words to create the "correct" characters.

class Lattice (L : Type u) where
  meet : L -> L -> L
  join : L -> L -> L
  absorb₁ : ∀ a b : L, join a (meet a b) = a
  absorb₂ : ∀ a b : L, meet a (join a b) = a

universe u
variable {L : Type u}
variable [Lattice L]

infixl:60 " ⊓ " => Lattice.meet
infixl:60 " ⊔ " => Lattice.join

theorem meet.idempotency (a : L) : a ⊓ a = a := by
  have lem₁ : a ⊔ (a ⊓ a) = a := Lattice.absorb₁ a a
  have lem₂ : a ⊓ (a ⊔ (a ⊓ a)) = a := Lattice.absorb₂ a (a ⊓ a)
  rw [lem₁] at lem₂
  exact lem₂
  done

theorem join.idempotency (a : L) : a ⊔ a = a := by
  have lem₁ : a ⊓ (a ⊔ a) = a := Lattice.absorb₂ a a
  have lem₂ : a ⊔ (a ⊓ (a ⊔ a)) = a := Lattice.absorb₁ a (a ⊔ a)
  rw [lem₁] at lem₂
  exact lem₂
  done

Rewriting the type of the second lemma (rw [lem₁] at lem₂) by substituting in the first lemma "just works". We then finish off the proof by noting that the rewritten type of the second lemma is the same as the goal, and we're done.