Learning Lean by example

I am interested in Lean for lots of reasons, and one of these reasons is that I am convinced that somehow it can be used to teach university mathematics students about proof in a new way. However I have run into two problems in practice.

First, Lean has a high learning curve, at least if you go about learning it the way I did, which was by trying to do undergraduate maths example sheets in Lean; the main problem is that the questions are in the wrong order, and one is constantly running into things which are easy in maths but hard in Lean (usually because the infrastructure is not yet there).

The second problem is that the resources are not yet there; the existing Lean literature is very good, but doesn’t ever actually get on to doing mathematics, it spends most of the time talking about types and the equation compiler and so on rather than actually working with fields like the real numbers — perhaps this is unsurprising, because the teaching literature tends to stick to core Lean whereas the real numbers are defined in the maths library.

I am going to change this by writing teaching material for mathematicians, but this will take time; I plan on working hard on it this term. I started by going through the material which I have generated whilst learning Lean myself, and some of this I now realise is quite good for beginners. I am just going to post some of this stuff on this blog and tag it “Learning Lean” to see if it’s of any help to anyone.

Here is some code which defines two inductive propositions on natural numbers. The first one is “I am even”. It’s defined like this — 0 is even, and if `n` is even then `n+2` is even; and that’s it. One can really work with this definition; I give some examples in the code below.

The second inductive proposition is “I satisfy the Collatz conjecture” (otherwise known as the 3n+1 problem). Recall that this conjecture says that if you start with any positive integer, and then halve it if it’s even, or multiply it by 3 and add 1 if it’s odd, then eventually you’ll get to 1. It’s cute, but not hard to see, that one can define this as an inductive proposition. I goof around with it a little in the below. I have documented the code; one can just cut and paste it into any Lean session and one doesn’t even need the maths library.

Click here to run the below code with the Lean Web editor (NB I have problems with firefox, but it works in Chrome for me). Or just cut and paste it into a Lean session.

-- Inductive propositions.

-- Example 1: even numbers.

-- inductive definition of "is_even" predicate on the real numbers
inductive is_even : ℕ → Prop 
| even0 : is_even 0 
| evenSS : ∀ n : ℕ, is_even n → is_even (n + 2)

open is_even  

theorem four_is_even : is_even 4 :=
begin
  -- goal now `is_even 4`
  apply evenSS,
  -- goal now `is_even 2`
  apply evenSS,
  -- goal now `is_even 0`
  exact even0  
end

-- can do it with functions too
theorem six_is_even : is_even 6 := evenSS 4 $ evenSS 2 $ evenSS 0 even0

theorem one_is_not_even : ¬ (is_even 1) :=
begin
  intro H,
  -- H : is_even 1
  -- clearly H can not have been proved using either even0 or evenSS
  -- so when we do this
  cases H,
  -- there are no cases left, so the proof is over!
end

-- cases can also be used to pull down higher odd numbers
theorem five_is_not_even : ¬ (is_even 5) :=
begin
  intro H5,
  cases H5 with _ H3, 
  cases H3 with _ H1,
  cases H1,
end

-- example of usage
lemma even_iff_SS_even (n : ℕ) : is_even n ↔ is_even (n + 2) :=
begin
  split,
  { -- easy way
    exact evenSS n,
  },
  -- other way a bit trickier
  intro HSSn,
  cases HSSn with _ Hn,
  assumption
end

-- Example 2: the Collatz conjecture.

/-- collatz n means the collatz conjecture is true for n -/
inductive collatz : ℕ → Prop
| coll0 : collatz 0
| coll1 : collatz 1
| coll_even : ∀ n : ℕ, collatz n → collatz (2 * n)
| coll_odd : ∀ n : ℕ , collatz (6 * n + 4) → collatz (2 * n + 1)

open collatz


theorem coll10 : collatz 10 :=
begin
apply coll_even 5,
apply coll_odd 2,
apply coll_even 8,
apply coll_even 4,
apply coll_even 2,
apply coll_even 1,
apply coll1
end

theorem coll10' : collatz 10 :=
  coll_even 5 $ coll_odd 2 $ coll_even 8 $ coll_even 4 $ coll_even 2 $ coll_even 1 coll1

-- if m is odd then 3m+1 is always even, so we can go from m=2n+1 to 6n+4 and then to 3n+2 in one step.
lemma coll_odd' (n : ℕ) : collatz (3 * n + 2) → collatz (2 * n + 1) :=
begin
  intro H3n2,
  apply coll_odd,
  -- unfortunately applying coll_even will tell us about collatz (2 * (3 * n + 2))
  -- rather than collatz (6 * n + 4), so let's fix this
  rw (show 6 * n + 4 = 2 * (3 * n + 2), by rw [mul_add,←mul_assoc];refl),
  -- with tactic.ring imported from mathlib this line could just be
  --  rw (show 6 * n + 4 = 2 * (3 * n + 2), by ring),

  apply coll_even,
  assumption
end

-- now we can go a bit quicker
theorem coll10'' : collatz 10 :=
begin
  apply coll_even 5,
  apply coll_odd' 2, 
  apply coll_even 4,
  apply coll_even 2,
  apply coll_even 1,
  apply coll1
end

-- Of course one should really be using a home-grown tactic to figure out which
-- of coll_even, coll_odd and coll1 to apply next.

/- this is the Collatz conjecture -/
theorem collatz_conjecture : ∀ n : ℕ, collatz n := sorry
-- Nobody knows how to prove this.