Problem 3: Largest prime factor

This problem proved to be a quick snack for Lean 4, and I was able to solve it with a quick call to the library function Nat.factors.

Revisiting Problem 2: Even Fibonacci numbers

After solving problem 3, I decided to have a closer look at some of the types I found while looking for a solution for problem 2. I realized that I could use very similar code to the one I used for my Stream instance, to construct members of type Stream', Stream'.Seq, and Stream'.WSeq. I realized that Stream'.Seq.corec used the same construction, that I had used for my FibStream, so the following creates a Stream'.Seq ℕ.

def fibSeq : Stream'.Seq ℕ := Stream'.Seq.corec FibStream.next? FibStream.init

This is one instance where I found the source code difficult to understand. It looks like a proof using tactics, but it supposedly produces a function that executes. I will have to revisit this in the future. But at least I understood that it was based on Stream'.corec'. When looking at this function, I realized that I could easily adopt my code to create a Stream' of Fibonacci numbers, since there are indeed an infinite number of them. The only thing I needed to do is to define a next function which unlike the next? function I had used so far doesn’t return an Option.

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

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

  def next? := some ∘ next

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

  def init : FibStream := ⟨0, 1⟩
end FibStream

def fibSeq : Stream'.Seq ℕ := Stream'.Seq.corec FibStream.next? FibStream.init
def fibStream' : Stream' ℕ := Stream'.corec' FibStream.next FibStream.init

On the plus side, there is a filter function defined for this set of types, so I can use this to create a Stream'.WSeq of even Fibonacci numbers.

def evenFibWSeq := Stream'.WSeq.filter (fun x => x % 2 = 0) fibSeq

But there is no takeWhile and no sum, so the gain is limited. And it’s not obvious that using these classes would lead to a better solution for problem 2. So let’s leave it at this for now and look at the next problem.

Problem 4: Largest palindrome product

For problem 2 I decided to stick with a pure functional style and avoid do notation as well as monads. So let’s try do notation for a change.

def maxCompound (factor_min factor_max : ℕ) (filter : ℕ → Bool) : Option ℕ := Id.run do
  let mut result := none

  for i in [factor_min : factor_max + 1] do
    for j in [factor_min : i + 1] do
      let n := i * j
      if filter n
        then match result with
          | none => result := some n
          | some n' => if n > n' then result := some n

  result

This works and gives the correct result, even though it’s rather inefficient. I could improve this by looping from max to min, but I didn’t find an obvious way for doing this. I could use some helper variable, but since I’ve solved this problem, so let’s move on.

Problem 5: Smallest multiple

The key question here turns out to be how to best represent the natural numbers from 1 to 20. I certainly don’t want to type out a literal list with these numbers. Fortunately, Std.Range, which I used for problem 4, is a natural candidate, it even comes with syntactic sugar, so I can use [1 : 21], unfortunately, it seems to only be meant to be used with a monad in a for loop, and doesn’t come with the usual functional features, one might expect. So let’s use a for loop to implement foldl.

def Std.Range.foldl (f : α → ℕ → α) (init : α) (r : Std.Range) : α := Id.run do
  let mut result := init
  
  for i in r do
    result := f result i
  
  return result

With this, the rest is easy.

Problem 6: Sum square difference

Easily solved using the Std.foldl, defined for the previous problem.

Problem 7: 10001st Prime

I’m somewhat surprised that this isn’t implemented in Mathlib, though I guess since it’s focus is on proving stuff, there aren’t many proofs which require the n-th prime. Mathlib has a function Nat.decidablePrime which probably implements a really smart and reasonably fast algorithm, but it’s not quite what I need. In other languages I have solved this by writing a prime generator, which creates a potentially infinite data structure of primes, which I can iterate over. So this means we are back to streams.

Here is a complete implementation of my prime generator:

import Mathlib
import LearnLean.Stream

structure PrimeGenerator where
  known_primes : List ℕ
  candidate : ℕ
deriving Repr

namespace PrimeGenerator
  def init : PrimeGenerator := ⟨[], 2⟩

  instance : Inhabited PrimeGenerator := ⟨init⟩

  def relevant_primes (c : PrimeGenerator) : List ℕ := 
    c.known_primes.takeWhile (·^2 ≤ c.candidate)

  def check_candidate_prime (c : PrimeGenerator) : Bool := 
    ¬ c.relevant_primes.any (· ∣ c.candidate)

  def step (c : PrimeGenerator) : (Option ℕ)  × PrimeGenerator:=
    if c.check_candidate_prime
      then (some c.candidate, ⟨c.known_primes ++ [c.candidate], c.candidate + 1⟩)
      else (none, { c with candidate := c.candidate + 1})

  partial def next (c : PrimeGenerator) : ℕ × PrimeGenerator := 
    match c.step with
    | (none, c') => next c'
    | (some p, c') => (p,c')

  def next? (c : PrimeGenerator) : Option (ℕ × PrimeGenerator) := 
    some (next c)

  instance : Stream PrimeGenerator ℕ := ⟨next?⟩

end PrimeGenerator

One thing I noticed was that, when I tried to use Stream'.Seq.corec and tried to access the 10001nth element, I got a Stack overflow. So it seems the Stream' structures aren’t a good choice for this kind of this kind of programming after all. Which means we need to implement the missing functions for Stream, which I am collecting in the LearnLean.Stream package I’m importing. Here is the implementation for the get? function.

namspace Stream
  def get? (n : Nat) (s : Stream_α) : Option α :=
    let next? := Stream.next? s
    match n with
    | 0 => next?.map (fun (next, _) => next)
    | n + 1 => match next? with
      | none => none
      | some (_, s') => get? n s'
end Stream

One thing to be careful about is that this get? function is 0-based, that means the first prime 2 gets returned by Stream.get? 0 PrimeGenerator.init.

Lean is not just a functional programming language, but also a theorem prover, so I will try to prove something about my code in my next post.

Open Questions

I will start collecting some open questions at the end of my posts, which I will hopefully answer in a future post.

• What does @[…] do? How does it work?
• How do I implement a custom ForIn?
• Is Seq related to Stream'.Seq in any way?
• Is there a canonical way to iterate over the members of a type (where this makes sense)?