proofs about for loops

Stream: Is there code for X?

[Scott Morrison]

Does anyone have advice about how to proceed with problems like:

def eval (a : Nat) (B C : Array Nat) : Nat := Id.run do
  let mut r := a
  for b in B, c in C do
    r := r + b * c
  return r

def eval' (a : Nat) (B C : Array Nat) : Nat :=
  B.zip C |>.foldl (init := a) fun r ⟨b, c⟩ => r + b * c

example : eval a B C = eval' a B C := sorry

Presumably we will eventually have a library of lemmas about for loops that transform common idioms into the functional style.

But we don't have that yet, right?

What would you do if faced with this now?

[Damiano Testa]

Did you want eval' to take Int values? And B, C are Nats in eval and Ints in eval'?

[Scott Morrison]

Sorry, copy-paste errors! All just in Nat.

[Damiano Testa]

EDIT: ignore me -- I did not know what for b in B, c in C do meant
Also:

#eval
  let a := 1
  let B : Array Nat := #[1, 1]
  let C : Array Nat := #[1]
  let B' : Array Int := B.map fun x => (Nat.cast x : Int)
  let C' : Array Int := B.map fun x => (Nat.cast x : Int)
  eval a B C = eval' a B' C'

[Damiano Testa]

Should using B twice, instead of B and C be good?

[Damiano Testa]

(Note that I don't know that I'll be able to help with the proof, but I'm trying to understand at least the statement!)

[Damiano Testa]

I tried this a little, but failed. These are my thoughts -- they are certainly a subset of yours, but maybe it helps to see them written down!

• Working with List rather than Array seems better for proofs. In particular, eval' for Lists (i.e. List.foldl) has already some API also for its TR version.
• Even the version where you compare the List.foldl (· + ·) to the sum of a single list is a struggle!

That's all I have... :shrug:

[Scott Morrison]

Here's the prototypical example of "how do I prove things about for loops!?":

set_option autoImplicit true
set_option relaxedAutoImplicit true

example {a : α} {bs : Array β} :
    (Id.run do
      let mut r := a
      for b in bs do r := f r b
      return r) =
      bs.foldl f a :=
  sorry

Suggestions welcome!

[Scott Morrison]

I'm beginning to see how one would do this. We have things like docs#Array.SatisfiesM_foldlM already (heroic work by Mario!), but don't yet have a corresponding Array.SatisfiesM_forIn (not that I'm even sure what that would say!). But I think that would be the first step.

[Patrick Massot]

See the discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Proof.20of.20program

[Scott Morrison]

The key step in @Mario Carneiro's answer there unfortunately doesn't work with today's Std. I wonder if the "with some new lemmas in Std" that he referred to in that message didn't actually make it to Std. :-)

[Mario Carneiro]

@Scott Morrison The new lemmas did make it to Std, but something seems to have broken the base case, List.range' isn't simplifying like it used to. This proof works:

import Std.Data.Range.Lemmas
import Std.Data.List.Lemmas

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

theorem sum_eq (n : Nat) : sum (n + 1) = n*(n+1)/2 := by
  suffices ∀ l i acc r, l + i = n → i * (i + 1) = 2 * acc →
      Id.run (forIn (List.range' (i+1) l) acc fun i r => .yield (r + i)) = r →
      n * (n + 1) = 2 * r by
    rw [sum]
    simp [Std.Range.forIn_eq_forIn_range', Std.Range.numElems_step_1]
    refine (Nat.div_eq_of_eq_mul_right (by decide) ?_).symm
    exact this _ _ _ _ (by rfl) (by rfl) rfl
  intro l i acc r e ih hr
  induction l generalizing i acc
  · simp [← e, ih, ← hr, forIn, Id.run]; simp [List.range']
  · next l IH =>
    rw [Nat.succ_add] at e
    refine IH i.succ _ e ?_ hr
    rw [Nat.mul_add 2, ← ih, ← Nat.add_mul, Nat.mul_comm]

[Mario Carneiro]

the "new lemma" in question is Std.Range.forIn_eq_forIn_range'