Lean with project Euler

Stream: new members

[Markus Schmaus]

Hi all,

I recently discovered Lean and was intrigued by the idea of a functional programming language, which is also a theorem prover.

I decided to learn some Lean 4 and solve some problems from project Euler using it, like I did for a couple of other languages before. I started writing up my experiences in a couple of posts. Here is the first one: Learning Lean 4 as a programming language – Project Euler.

[Markus Schmaus]

I published the second post in the series: Learning Lean 4 as a programming language 2 – Infinite lists

[Alex J. Best]

Did you think about proving any of your answers correct in Lean? Using some reasonable formalization of the statement. I'd be curious how hard / awkward that was and I think we as a community could learn from that

[Markus Schmaus]

For problem 7 I have written a prime sieve and I have been working on proving it to be correct.

[Markus Schmaus]

Here is the next post: Learning Lean 4 as a programming language 3 – Weak sequences. This still only covers some coding and no proofs, yet. The prime number stuffed turned out to be a too hard for my first proof, but I was able to proof my Fibonacci code to be correct. I still have to write this up, which will be my next post.

[Kevin Buzzard]

Re your open questions: you could just ask them here in another thread in #new members or #lean4 (they are sufficiently non-elementary that I should think #lean4 will be fine). Regarding iterating over members of a type -- how would you iterate over the real numbers? What hypotheses do you have on your type? Might it be infinite, for example?

[Markus Schmaus]

The list of types for which this makes sense probably isn't that long. All uncountable infinite types, like the reals, are out for obvious reasons. It obviously makes sense for Nat, Nat.Primes, and the instances of the Finite. For Int and Rat it's possible though not obvious in which order.

[Ioannis Konstantoulas]

Writing provable code for Euler problems is an interesting exercise, but can be tricky. For instance, for problem 5 in your link, a solution is

import Std.Data.Nat.Gcd

def minMul (n : Nat) : Nat :=
  List.iota n |>.foldl Nat.lcm 1

#eval minMul 10
#eval minMul 20

But proving this solves your problem can be tricky, depending on what you assume!

[Markus Schmaus]

I was rather busy the last days, but I finally found the time to complete my first post, that includes proofs: Learning Lean 4 as a programming language 4 – Proofs

[Patrick Massot]

Thanks for writing this! I don't have time to read all of it now, but I'd like to already point out you have very unusual code formatting. Could you add frequent warnings telling your readers they won't be able to contribute to any existing Lean 4 project if they follow your formatting style?

[Markus Schmaus]

Is there a style guide for code formatting?

[Jireh Loreaux]

#style

[Jireh Loreaux]

from a quick glance at your code, I would say the major takeaways are:

1. we don't indent everything in a namespace or section
2. : and := are appended the ends of preceding lines, not on their own or at the front.
3. for continuing declaration statements, we indent 4 spaces, and then the start of the proof reverts back to a 2-space indent.
4. arguments to declarations don't get their own lines.

But there are probably more things to be gleaned from the style guide too.

[Jireh Loreaux]

e.g., to make a snippet of your code adhere to the style guide, it would look like this:

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⟩


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

[Alex J. Best]

The reason specialize doesn't auto close the goal is that most people would write

exact induction_hyp (tail s)

In place of

specialize induction_hyp (tail s)
exact induction_hyp

[Jireh Loreaux]

and additionally, if my memory serves, the specialize tactic was written for purely pedagogical purposes

[Patrick Massot]

It can be useful in some corner cases, notably where followed by a rw at.

[Markus Schmaus]

@Jireh Loreaux a couple of these lines seem long to me. Specifically

  recursion : ∀ i : Nat,
    (InfiniteSequence.get i s) + (InfiniteSequence.get (i + 1) s) = InfiniteSequence.get (i + 2) s

and

    simp only [InfiniteSequence.get, InfiniteSequence.drop, InfiniteSequence.drop_tail, Nat.add]

as they get cut off by the Zulip code display. Is there a style guide conform way to wrap them?

[Jireh Loreaux]

Mathlib has a 100 character limit, and that's what I used above. You could break them earlier.

[Gareth Ma]

Hi, I just saw this. I have also done some PE in Lean before, though not for optimised speed. You can find it here.

[Gareth Ma]

As Ioannis said above, writing a program is easy, it's pretty much just Haskell. Proving it indeed solves your problem will be quite interesting, especially for code written imperatively using Monads, even with for loops.