Proofs about for loops

Stream: lean4

[Tyler Josephson ⚛️]

I can sum up the first n natural numbers using a variety of functions:

def sumNumbers : Nat → Nat
  | 0 => 0
  | (n+1) => n + 1 + sumNumbers n

def sumNumbersFor (n : Nat) : IO Nat := do
  let mut sum := 0
  for i in [0:n+1] do
    sum := sum + i
  return sum

theorem sumNumbers_equiv_sumNumbersFor (n : Nat) :
  sumNumbers n = sumNumbersFor n := by
  sorry -- type mismatch

How might I show these two functions are injective? There's a type mismatch in my theorem statement, so I can't even get started.

[Yaël Dillies]

Are you sure sumNumbersFor needs to be in IO?

[Yaël Dillies]

def sumNumbersFor (n : Nat) : Id Nat := do
  let mut sum := 0
  for i in [0:n+1] do
    sum := sum + i
  return sum

works

[Damiano Testa]

Or even using Nat and starting with Id.run do.

[Eric Wieser]

Arguably you often want to live in CoreM so that you can respond to interruptions:

import Lean

open Lean
def sumNumbersFor (n : Nat) : CoreM Nat := do
  let mut sum := 0
  for i in [0:n+1] do
    checkSystem "sumNumbersFor"  -- or IO.checkCanceled
    sum := sum + i
  return sum

#eval sumNumbersFor 3000000

the checkSystem means that if you comment out the #eval line, lean stops running the computation in the background

[Eric Wieser]

Otherwise every time you edit the file, you spawn more and more long-running processes that compute the sum, all of which only exit when they're done

[Eric Wieser]

(unfortunately, you can't prove much about this version)

[Jannis Limperg]

Is the issue (which perhaps deserves its own thread) that when #eval is elaborated, it starts a long-running computation that is not cancelled when elaboration is cancelled? Afair #eval uses the interpreter, so this should be fairly easy to fix.

[Bhavik Mehta]

Here's a start for you - I don't know if the first two theorems are in batteries but I suspect they could be, since the case where a for loop does computation without quitting early isn't rare.

import Batteries.Data.Range.Lemmas

def sumNumbersFor (n : Nat) : Nat := Id.run <| do
  let mut sum := 0
  for i in [0:n+1] do
    sum := sum + i
  return sum

universe u v w

theorem List.forIn_yield {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type w} {β : Type u}
    {l : List α} {f : β → α → β} {b : β} :
    (forIn l b fun i r => pure (ForInStep.yield (f r i)) : m β) =
      pure (l.foldl f b) := by
  induction l generalizing b with
  | nil => rfl
  | cons x xs ih =>
      rw [List.forIn_cons, List.foldl_cons, pure_bind]
      exact ih

theorem List.Id_forIn_yield {α : Type w} {β : Type u}
    {l : List α} {f : β → α → β} {b : β} :
    (forIn l b (fun i r => ForInStep.yield (f r i)) : Id β) = l.foldl f b :=
  List.forIn_yield

theorem sumNumbersFor_eq (n : Nat) : sumNumbersFor n = (List.range (n + 1)).foldl (· + ·) 0 := by
  rw [sumNumbersFor]
  dsimp
  rw [Std.Range.forIn_eq_forIn_range', Std.Range.numElems_step_1, Nat.sub_zero]
  dsimp
  rw [List.Id_forIn_yield, Id.run, ←List.range_eq_range']

If you import mathlib, you could then say that this is equal to a List.sum or a Finset.sum, and then use the formula in mathlib for the sum. Alternatively you could just use induction on n to get the formula directly

[Eric Wieser]

Jannis Limperg said:

Is the issue (which perhaps deserves its own thread) that when #eval is elaborated, it starts a long-running computation that is not cancelled when elaboration is cancelled? Afair #eval uses the interpreter, so this should be fairly easy to fix.

I think the only cancellation method available is cooperative, and requires the task to call IO.checkCancelled? At any rate, the interpreter is out of the picture if the function in question is compiled.

[Frédéric Dupuis]

While there are ways to do this as was shown in previous messages, at the moment proving statements about monadic code is very difficult. You'll have a much easier time by sticking to a more functional coding style, such as using things like List.foldl and friends instead of for loops. The main difficulty is that for loops have the possibility of breaking out of the loop in the middle, and this possibility has to be taken into account in proofs (all this ForInStep.yield stuff in Bhavik's example) even in the case where early breaks are obviously not happening in your code.

[Tyler Josephson ⚛️]

This is really helpful, thanks!

In general, it seems like if I wanted to some property of sumNumbersFor (for this case, I'm thinking of Gauss's summation formula), I could either 1) rewrite it in functional style, prove injectivity with the new function, then prove the property of the new function, 2) prove the property of sumNumbersFor directly, or 3) give up on the imperative style, and only write programs in the functional style. And it seems like for both 1) and 2), the proofs will be rather difficult. If I'm concerned about execution efficiency, I can write a tail recursive version of my functional-style function, and follow the methods described in FPIL to prove their equivalence.

Furthermore, I'd generally think that the proofs are what give me confidence that my code is correct, so in most cases, the best practice would be to write in functional style, and validate with proofs. The application I have in mind involves translating software that's always been written in imperative style, so translating for loops in Python into for loops in Lean would be an easier first step compared to refactoring in a functional style, but the resulting Lean code will be hard to write proofs about, so the refactor into a functional style first will probably make more sense. The only other reason to write with for loops in Lean would potentially be efficiency of code execution, but if this does become important enough, it's great to know that proving such connections is possible, in principle.

[Bhavik Mehta]

Frédéric Dupuis said:

While there are ways to do this as was shown in previous messages, at the moment proving statements about monadic code is very difficult. You'll have a much easier time by sticking to a more functional coding style, such as using things like List.foldl and friends instead of for loops. The main difficulty is that for loops have the possibility of breaking out of the loop in the middle, and this possibility has to be taken into account in proofs (all this ForInStep.yield stuff in Bhavik's example) even in the case where early breaks are obviously not happening in your code.

Agreed - I've made a few proofs like this and the first step is almost always to turn it into a functional version rather than an imperative version. So if you can get away with doing that from the start, it's definitely better. The approach I gave above works purely because you're in the case that an early break isn't happening - it can be adapted if it does happen, but it's not as short.