I am fascinated by Lean 4, because it looks like a great programming language and on top of this it also provides the facilities for proving theorems about code written in this language.

Today, in a typical software engineering project, I would define a custom structure, to represent a concept, i.e. I have a network of interdependent tasks, which need to be run under certain circumstances. Usually there are some requirements on the state of this structure, such that it makes sense based on this concept, i.e. the tasks have lists of upstream and downstream tasks and a tasks needs to be in the downstream list of each of the tasks in its upstream list. These are called “(class) invariants” because each function in the program should preserve these properties, i.e. if all upstream and downstream tasks are consistent, creating or deleting a tasks shouldn’t change that. Many bugs, and I’m tempted to claim all bugs, are caused by some function under some circumstances breaking such an invariant, i.e. I change an upstream dependency for a task, I update the upstream list for itself and add it to the downstream list for the new dependency, but forget to remove it from the downstream list of the old dependency. The best practice solution for this is to write unit tests which run the functions with many different example values and test the invariants after each step. The idea of proving instead, that those invariants are preserved by each function sounds very appealing to me.

I started trying to prove the correctness of the PrimeGenerator from the previous post, but even though I made some progress, it turned out to be too hard for my first proof. So instead I proved the correctness of my Fibonacci generator.

Infinite Sequences

The topic of streams or infinite lazy lists is pretty important for nice solutions for many of the problems of Project Euler. I have discussed Stream', in my previous post, but since then I have discovered that implementations of all its functions aren’t tail recursive, and therefore can quite easily lead to stack overflows. Therefore, as of October 2023, there isn’t a good practical solution available in the Lean 4 libraries, and we will need to come back to this again and again.

A recent Zulip thread discusses that Stream' is inefficient and Pol’tta / Miyahara Kō is working on improving the situation. Here I am going to use my custom implementation of an infinite sequence, which I define like this:

import Std

universe u v

class InfiniteSequence
  (sequence : Type u) (value : outParam (Type v)) 
  : Type (max u v) where
  head : sequence → value
  tail : sequence → sequence

namespace InfiniteSequence
  variable
    {sequence : Type u} {value : Type v} 
    [InfiniteSequence sequence value]

  def drop
    (n : Nat) (s : sequence) 
    : sequence
    :=
    match n with 
    | 0 => s
    | n + 1 => drop n (tail s)

  theorem drop_tail (n : Nat) (s : sequence) 
    : drop n (tail s) = tail (drop n s) := by
    revert s
    induction n
    · case zero =>
      simp only [drop, implies_true]
    · case succ induction_hyp  =>
      simp only [drop]
      intro s
      specialize induction_hyp (tail s)
      exact induction_hyp
  
  def get 
    (n : Nat) (s : sequence) 
    : value
    :=
    head (drop n s)

  def get?
    (n : Nat) (s : sequence) 
    : Option value
    := some (get n s)

  def take (n : Nat) (s : sequence) : List value :=
    let rec go (acc : List value) (n : Nat) (s : sequence) : List value :=
      match n with
      | 0 => acc.reverse
      | n + 1 => go ((head s) :: acc) n (tail s)
    go [] n s

end InfiniteSequence

At college, while studying math, my strength was always my intuition, while my knowledge of theory could be a little bit spotty. And that’s certainly the case here as well, I had never heard to terms “coinductive type” and “corecursion” before I started to learn Lean 4, but it all looks pretty natural and intuitive to me. I am reading up on theory though, for example I’ve been reading Data Types as Quotients of Polynomial Functors, which I found referenced in Mathlib: Quotients of Polynomial Functors. So I felt vindicated in my design choice above when I read “such a type can be expressed naturally in terms of the destructors rather than the constructors”. It’s the destructors head and tail which define the essence of an infinite coinductive sequence. Stream combines them into a single, pair-valued function next?, but this can lead to unnecessary computation, and it’s cleaner to keep them apart.

There is one theorem in this file, which I called drop_tail, which I will come back to later after the discussion of my proof for the Fibonacci numbers.

Fibonacci numbers

import Std
import LearnLean.Sequence

namespace Fibonacci
  structure Lawful
    {sequence : Type}
    (s : sequence)
    [InfiniteSequence sequence Nat]
    : Prop where
      intro ::
      value_0 : InfiniteSequence.get 0 s = 0
      value_1 : InfiniteSequence.get 1 s = 1
      recursion : 
        ∀ i : Nat, 
        (InfiniteSequence.get i s) + (InfiniteSequence.get (i + 1) s)
        = InfiniteSequence.get (i + 2) s

  structure Generator where
    value_pred : Nat
    value : Nat

  namespace Generator
    def head (g : Generator) : Nat := g.value
    def tail (g : Generator) : Generator := ⟨g.value, g.value_pred + g.value⟩

    instance : InfiniteSequence Generator Nat where
      head := head
      tail := tail

  end Generator

end Fibonacci

def Fibonacci : Fibonacci.Generator := ⟨1, 0⟩

The first thing of note is that I used a custom structure in my definition of a Fibonacci sequence, alternatively I could have used a a logical conjunction ∧, but And is also nothing but a structure.

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

And since I have three conditions, this would result in a nested structure using the nondescript labels left and right. The only potential downside I can think of is that I can’t directly use any theorem which applies to And for my Definition, but this doesn’t seem that relevant. The intro :: provides a custom name for the constructor, which would otherwise be named mk, I do this so it matches the name of the constructor of And.

The Generator which constructs the Fibonacci numbers should hopefully be self-explanatory, and in any case I will proof that the resulting InfiniteSequence matches the Definition next.

Proof Fibonacci.isLawful

After this introduction, here is my proof that my implementation of the Fibonacci numbers is correct.

namespace Fibonacci
  theorem isLawful 
    : Lawful Fibonacci := by
    apply Lawful.intro
    · case value_0 => decide
    · case value_1 => decide

    · case recursion =>
      intro i
      simp only [
        InfiniteSequence.get,
        InfiniteSequence.drop, 
        InfiniteSequence.drop_tail,
        Nat.add
      ]

      simp only [
        InfiniteSequence.tail, Generator.tail,
        InfiniteSequence.head, Generator.head
      ]

end Fibonacci

A certainly learnt a lot about proofs in Lean from Mathematics in Lean and the chapter in Functional Programming in Lean. But there is a lot I had to figure out by trial and error, so here is my current mental model of proofs in Lean 4 using the tactics mode.

First, the basics, there are hypotheses, which are assumed to be true, and goals, which I try to show to be true. The initial hypotheses is everything between the name of the theorem (isLawful) and the :, in this case there are no initial hypothesis. After that comes the initial goal (Lawful Fibonacci) and after the := starts the proof with by in order to enter the tactics mode. In VSCode the right hand panel shows the current hypotheses and goals, marked by ⊢, like this:

⊢ Lawful Fibonacci

In tactics mode it is possible to work from the goal backwards, just like it is possible to work from the hypotheses forward. The first tactic I’m using here, called apply, is for working backwards from the goal. Based on the name I tried to use it to work forward from the hypothesis, but I realized that if I want to apply a theorem to some hypotheses I can simply apply it like a function (this can be done directly outside tactics mode, while inside tactics mode it needs to be used with have). The apply tactic answers the inverse question: what hypotheses would be needed, such that applying this theorem would result in my goal? And the goal is then replaced with the answers to this question. I am using this tactic with the constructor Lawful.intro, and since the constructor requires the three statements I labeled value_0, value_1, and recursion these become the three new goals. Now I can address each of these goals individually.

case value_0
⊢ InfiniteSequence.get 0 Fibonacci = 0

case value_1
⊢ InfiniteSequence.get 1 Fibonacci = 1

case recursion
⊢ ∀ (i : Nat),
  InfiniteSequence.get i Fibonacci + InfiniteSequence.get (i + 1) Fibonacci 
  = InfiniteSequence.get (i + 2) Fibonacci

The first two goals are easy to decide for Lean, by just computing the value and comparing it with the required answer, this is why I can complete them using the decide tactic.

The third and last goal contains a quantifier ∀ (i : Nat), in a natural language proof, I would handle this with a statement like “let’s assume i is a natural number”, the same purpose is served here by the intro tactic. It removes the quantifier from the goal and introduces the corresponding hypothesis.

i : Nat
⊢ InfiniteSequence.get i Fibonacci + InfiniteSequence.get (i + 1) Fibonacci 
  = InfiniteSequence.get (i + 2) Fibonacci

The simp tactic can be used to work forward from hypothesis, as well as working backwards from the goals, like I do here. Unlike apply it is able to work on individual parts of any statement. By default it uses all definitions and theorems marked by @[simp] and tries to make progress using them. In this case I specify my own functions InfiniteSequence.get, InfiniteSequence.drop, and the theorem InfiniteSequence.drop_tail, since none of them is marked with @[simp], I also specify Nat.add, since I know that this is the only other definition that’s required, so I can use the parameter only, so simp doesn’t waste time trying unnecessary definitions and theorems.

i : Nat
⊢ InfiniteSequence.head (InfiniteSequence.drop i Fibonacci) 
    + InfiniteSequence.head (InfiniteSequence.tail (InfiniteSequence.drop i Fibonacci)) 
  = InfiniteSequence.head (InfiniteSequence.tail (InfiniteSequence.tail (
    InfiniteSequence.drop i Fibonacci)))

Here I use the theorem InfiniteSequence.drop_tail, which is necessary because I implemented InfiniteSequence.drop using tail recursion, this performs better from a computational perspective, but makes proofs a little bit more tricky. Which is probably why all the functions in Stream' are implemented without tail recursion, and why in other places within Lean and Mathlib, there is a reference implementation without tail recursion which is marked with @[implemented_by …], pointing to a faster version using tail recursion for practical use for the compiler. As it is I also need to make a second call to simp for InfiniteSequence.tail, Generator.tail, InfiniteSequence.head, and Generator.head. If I try to combine them, simp doesn’t find the correct place to apply this theorem. But after that second invocation I am done, as simp is able to completely fulfill the goal.

Proof InfiniteSequence.drop_tail

The code for InfiniteSequence above already contains the proof for InfiniteSequence.drop_tail, but now that we looked at the proof for Fibonacci numbers I will look at this more closely here.

namespace InfiniteSequence
  theorem drop_tail (n : Nat) (s : sequence) 
    : drop n (tail s) = tail (drop n s) := by
    revert s
    induction n
    · case zero =>
      simp only [drop, implies_true]
    · case succ induction_hyp  =>
      simp only [drop]
      intro s
      specialize induction_hyp (tail s)
      exact induction_hyp

end InfiniteSequence

Unlike with isLawful, there are two explicit hypotheses here, (n : Nat) and (s : sequence), as well as three more implicit hypotheses {sequence : Type u}, {value : Type v}, and [InfiniteSequence sequence value].

sequence : Type u
value : Type v
inst✝ : InfiniteSequence sequence value
n : Nat
s : sequence
⊢ drop n (tail s) = tail (drop n s)

The first thing I do here is the opposite of what I did for isLawful. While I used intro in that case to move a quantified variable to the hypothesis, I use revert here to move s from the hypothesis into the goal.

sequence : Type u
value : Type v
inst✝ : InfiniteSequence sequence value
n : Nat
⊢ ∀ (s : sequence), drop n (tail s) = tail (drop n s)

I do this, such that when I use induction tactics next, the induction hypothesis is for all s and not just for a specific s.

case zero
sequence : Type u
value : Type v
inst✝ : InfiniteSequence sequence value
⊢ ∀ (s : sequence), drop Nat.zero (tail s) = tail (drop Nat.zero s)

case succ
sequence : Type u
value : Type v
inst✝ : InfiniteSequence sequence value
n✝ : Nat
n_ih✝ : ∀ (s : sequence), drop n✝ (tail s) = tail (drop n✝ s)
⊢ ∀ (s : sequence), drop (Nat.succ n✝) (tail s) = tail (drop (Nat.succ n✝) s)

The initial “zero” case can be easily proved using drop and implies_true, which leaves the induction step “succ“. We replace drop with its definition and move s to the hypothesis. Now I benefit from using revert earlier, since my induction hypothesis states that the statement is true for all s, so it’s also true for tail s, which I fix for the quantifier using the specialize tactic.

sequence : Type u
value : Type v
inst✝ : InfiniteSequence sequence value
n✝ : Nat
s : sequence
induction_hyp : drop n✝ (tail (tail s)) = tail (drop n✝ (tail s))
⊢ drop n✝ (tail (tail s)) = tail (drop n✝ (tail s))

Now I have a hypothesis which is exactly the goal, but unlike the simp tactic, the specialize tactic doesn’t automatically fulfill this goal, so I have to call the exact tactic in order to complete this proof.

Thoughts on Proofs

From what I know today I would classify both proofs to be rather easy. It was quite a journey to get here, but most of this was about learning how to use Lean 4 for proving theorems, not about proving these theorems specifically.

I still find proofs hard to read, mostly because I find it hard to predict how each tactic influences the tactic state. In terms of documentation the Tactics chapter in the Lean Reference Manual is useful, but it’s rather brief and doesn’t link to the source code, so a lot of my understanding is based on trial and error. Paper-Proof is something I’ve seen mentioned, but I haven’t tried it. But in the end understanding a proof might not be that important. If I don’t understand the source code of a function, I don’t know what that function does, but if I don’t understand the source code of a proof, I still know exactly what it does: it proves the theorem which it is attached to.

The question I’m trying to answer for myself with this project is: how useful are proofs for programming? I certainly see the potential, but what have I learnt so far? The definition of Lawful is maybe somewhat easier to read and understand than the definition of Generator, but in any case, the fact that there are two different expressions of Fibonacci numbers, which I then show to be equivalent, certainly raises the confidence, that both of them are correct. However, in the case of my prime number generator, the proof turned out to be too much for me, so for proofs to be useful for me, proofs must become easier and faster for me to complete.

Answers

• What does @[…] do? How does it work?
  I still don’t have a complete understanding of this syntax, but Significant changes from Lean 3 explains @[implemented_by …], which I mentioned in this post, as well as @[extern …]. As I also mentioned above, the simp tactic by default uses theorems and definitions which are marked with @[simp] and there is another tactic called aesop which uses those marked with @[aesop].