Problem 2: Even Fibonacci numbers

Fibonacci numbers are a common toy problem which is used in many programming tutorials, since naive implementations can go horribly wrong. Mathlib of course contains an implementation, which avoids all these pitfalls, and an even faster implementation. I didn’t use either for this problem for multiple reasons. First, when I started this problem I didn’t know about the Mathlib4 docs, so I wasn’t even able to find them. Second, since I want to learn Lean 4, it’s a reasonable exercise to implement it myself. And third, I don’t actually want a function which gives me the n-th Fibonacci number, I want a function which gives me all the Fibonacci numbers up to the n-th. This means, when I have computed the (n-1)-th number, I should keep all the work I have done so far to compute the next number, rather than starting fresh.

Infinite lists

In Haskell I would have used an infinite list for this purpose, but since Lean 4 uses eager, rather than lazy evaluation, it wasn’t completely obvious how to do this.

I found a thread in the Zulip archive which discusses the idea of an Iterable, which in turn references ForIn. Unfortunately all that the Lean manual had to say on this topic was “TODO: describe forIn“. With the help of the Mathlib 4 docs, I found the documentation and source code of a couple of interesting types and classes. ForIn seem to be tightly linked to monads, which I didn’t want to use for now. The description and name of LazyList seemed promising, but it wasn’t obvious to me how to implement one representing Fibonacci numbers. Then I found Stream, but also Stream' and Stream'.Seq, which at first I confused with Seq. I finally decided to go with Stream, for one, it seemed reasonable to use a class from the base language, but also, because I understood how to implement my Fibonacci numbers with it.

structure FibStream : Type where
  x₁ : ℕ
  x₂ : ℕ
deriving Repr

namespace FibStream
  def next? (s : FibStream) : Option (ℕ × FibStream) :=
    match s with
    | ⟨x₁, x₂⟩ => 
      let x₃ := x₁ + x₂
      some (x₃, ⟨x₂, x₃⟩)

  instance : Stream FibStream ℕ where
    next? := next?

  def init : FibStream := ⟨0, 1⟩

end FibStream

The idea behind FibStream, like any other Stream, is, that it encapsulates all the data necessary to compute the next Fibonacci number. The next? function uses this information to actually compute the next Fibonacci number, and also the FibStream data necessary for the Fibonacci number after that. The result is wrapped in an Option, because while the stream of Fibonacci numbers never ends, other streams can terminate by returning none. The constant init is just the data required for the very first Fibonacci number.

The drawback of using Stream was that very few useful functions are implemented for it. The first function I was missing was take. While there is a List.take, there is no corresponding Stream.take. It was straight forward to implement this just for my FibStream, but I decided to try and implement this for all Streams. First, so I could learn how to do this, and second, so I could reuse this for other problems.

Installing Mathlib and import

After I got lake working by rebooting my computer, I remembered seeing a tutorial on how to install Mathlib using lake, but it took me quite a while to find it again on the Lean website: creating a Lean project. After that import Mathlib worked flawlessly.

However, when I tried to put some code in another file called Stream.lean I couldn’t get import to work. It turned out that I had made a mistake when setting up my project. I used lake new learn-lean math to create my project folder learn-lean, so lake assumed that the folder which contains my .lean files is called LearnLean, while I used the name MyProject. I decided to rename my folder, though I probably could also have edited the following entry in lakefile.lean:

lean_lib «LearnLean» {
  -- add any library configuration options here
}

I was finally able to import LearnLean.Stream. Unfortunately, when I changed Stream.lean, it didn’t affect the version that was imported. I finally found the solution in the YouTube video Quick Tour of the Lean 4 Visual Studio Code extension. I can execute a command in VS Code by pressing Ctrl+Shift+P and searching for Lean 4: Refresh File Dependencies. This refreshes all changes in the files I import.

Custom Stream functions

With that out of the way I was finally able to implement my custom Stream functions. Here are a few of them:

namespace Stream
  variable {Stream_α : Type} {α : Type} [Stream Stream_α α] 
  
  def take (n : Nat) (s : Stream_α) : List α :=
    match n with
    | 0   => []
    | n+1 => 
      let next? := Stream.next? s
      match next? with
      | none => []
      | some (next, s') => next :: take n s'

  structure Filter (Stream_α : Type) [Stream Stream_α α] where
    stream : Stream_α
    filter_by : α → Bool
    

  partial def Filter.next? (s : Filter Stream_α) : Option (α × Filter Stream_α) :=
    let next? := Stream.next? s.stream
    match next? with
    | none => none
    | some (next, s') =>
      let next_filtered : Filter Stream_α := { stream := s', filter_by := s.filter_by : Filter Stream_α }
      if s.filter_by next then
        some (next, next_filtered)
      else
        Filter.next? next_filtered

  def filter (p : α → Bool) (s : Stream_α) : Filter Stream_α :=
    { stream := s, filter_by := p }

  instance : Stream (Filter Stream_α) α where
    next? := Filter.next?
end

I created a new structure Stream.Filter which hold both the original stream, as well as the filter function, since both are needed to produce the next element in the filtered stream. Stream.Filter.next? is also declared partial, since there is no guarantee, that Stream will ever produce an object which passes the filter.

With these and a few similar functions I was able to complete problem 2.