Proof of program

Stream: lean4

[Patrick Massot]

Very locally I'm interested in proving programs. But I have no idea how to get started. Say I want to complete:

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 := sorry

How do I even get started? I can guess induction n, but then what?

[Eric Wieser]

That's false, right? sum n = n there.

[Patrick Massot]

Fixed. I changed my mind half-way through and ended up in an inconsistent state, sorry.

[Kevin Buzzard]

I would get rid of the division, by multiplying both sides by 2 before you state anything but I can't say anything else coherent about this question

[Eric Wieser]

I think the crux of the question is maybe "how do I prove things about docs4#Std.Range.forIn", which I think I've seen threads about before

[Eric Wieser]

See for instance this message by Mario

[Patrick Massot]

Yes, that's one crux. The other one is let mut

[Kevin Buzzard]

Your real question is how to relate sum(n+1) to sum(n) (unless there's another way?) but yeah this suddenly looks terrifying :-)

[Eric Wieser]

I don't think the let mut is a crux; if you rw [sum] to start the proof you see that it desugars immediately

[Eric Wieser]

Running simp then gets you to

Id.run (forIn { start := 0, stop := n + 1, step := 1 } 0 fun i r => ForInStep.yield (r + i)) = ...

which looks in the realm of "basic missing API for forIn"

[Siddhartha Gadgil]

What I would do is define the function differently, as a recursive definition. Then a proof should be easier.

[Patrick Massot]

I specifically don't want to write in an openly functional way.

[Patrick Massot]

The question is: can you write a program normally and still prove it is correct?

[Siddhartha Gadgil]

There is a paper of @Sebastian Ullrich and @Leonardo de Moura about proving things in Monads. One of them can probably explain (to me using mutable variables is not the normal way :smile: ).

[Eric Wieser]

mutable variables (and likely even monads) are irrelevant here, consider

def sum := Id.run do
  let mut r := 0
  r := r + 2
  r := r + 3
  return r

theorem sum_eq : sum = 5 := rfl -- no problem

The problem here is Std.Range.forIn not having API

[Patrick Massot]

Siddhartha, are sure this paper exists? I know about the great https://leanprover.github.io/papers/do.pdf which is mostly about writing normal programs in a functional programming language. It has a short section about proofs, but only devoted to translating between do notation and openly functional style, not directly about proving programs. Is there another paper?

[Siddhartha Gadgil]

Patrick Massot said:

Siddhartha, are sure this paper exists? I know about the great https://leanprover.github.io/papers/do.pdf which is mostly about writing normal programs in a functional programming language. It has a short section about proofs, but only devoted to translating between do notation and openly functional style, not directly about proving programs. Is there another paper?

I meant that paper. I had wrongly assumed that it had such proofs.

[Kyle Miller]

@Patrick Massot I proved a few forIn lemmas to make some progress here.

All that's left is this theorem about natural numbers, and it's sort of gross because the loop is summing upwards rather than downwards:

theorem main :
    acc + start + (start + 1 + n) * (start + n) / 2 - (start + 1) * start / 2 =
    acc + (start + 1 + n) * (start + n) / 2 - start * (start - 1) / 2 := by
  sorry

The code:

import Mathlib.Tactic

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

section forIn_thms

theorem forIn_range_done1 [Monad m] {f : Nat → β → m (ForInStep β)}
    {fuel start stop step : Nat} (h : stop ≤ start) :
    Std.Range.forIn.loop f fuel start stop step b = pure b := by
  cases fuel <;> simp [Std.Range.forIn.loop, h]

theorem forIn_range_fuel_boost1 [Monad m] (f : Nat → β → m (ForInStep β))
    (fuel start stop n : Nat) (b : β) (hf : stop ≤ start + fuel) :
    Std.Range.forIn.loop f fuel start stop 1 b =
      Std.Range.forIn.loop f (fuel + n) start stop 1 b :=
  match fuel with
  | 0 => by
    simp at hf
    simp [forIn_range_done1 hf]
  | fuel + 1 => by
    rw [Nat.add_assoc, Nat.add_comm 1, ← Nat.add_assoc]
    simp [Std.Range.forIn.loop]
    congr! 5 with _ h' s b'
    simp at h'
    have hf' : stop ≤ start + 1 + fuel := by rwa [Nat.add_assoc, Nat.add_comm 1]
    exact forIn_range_fuel_boost1 f fuel (start + 1) stop n b' hf'

theorem forIn_range_1_aux [Monad m] (f : Nat → β → m (ForInStep β))
  (fuel start stop : Nat) (h : stop ≤ start + fuel) :
  Std.Range.forIn.loop f fuel start stop 1 b =
    if start < stop then
      f start b >>= fun r =>
      match r with
      | ForInStep.done b  => pure b
      | ForInStep.yield b => Std.Range.forIn.loop f (fuel - 1) (start + 1) stop 1 b
    else
      pure b := by
  split
  next h' =>
    cases fuel
    · simp at h
      have := trans h h'
      exact False.elim <| Nat.lt_le_antisymm h' h
    next fuel =>
      rw [Std.Range.forIn.loop]
      have : ¬ start ≥ stop := by simp [h']
      simp [this]
      rfl
  next h' =>
    simp at h'
    cases fuel
    · rw [Std.Range.forIn.loop]
      simp [h']
    next fuel =>
      rw [Std.Range.forIn.loop]
      simp [h']

theorem forIn_range_1 [Monad m] (f : Nat → β → m (ForInStep β)) :
    forIn [start:stop] b f =
      if start < stop then
        f start b >>= fun r =>
        match r with
        | ForInStep.done b  => pure b
        | ForInStep.yield b => forIn [start+1 : stop] b f
      else
        pure b := by
  simp [forIn, Std.Range.forIn]
  split
  next h =>
    rw [forIn_range_1_aux]
    simp [h]
    have : stop - 1 + 1 = stop := by cases stop <;> simp at h <;> simp
    congr! 4
    · rw [forIn_range_fuel_boost1 f (stop - 1) (start + 1) stop 1]
      · simp [this]
      · rw [Nat.add_assoc, Nat.add_comm 1, this]
        simp
    · simp
  next h =>
    simp at h
    simp [forIn_range_done1, h]

theorem forIn_range' [Monad m] (f : Nat → β → m (ForInStep β))
    (h : start < stop) :
    forIn [start:stop] b f =
      f start b >>= fun r =>
      match r with
      | ForInStep.done b  => pure b
      | ForInStep.yield b => forIn [start+1 : stop] b f := by
  rw [forIn_range_1]
  simp [h]

end forIn_thms

theorem main :
    acc + start + (start + 1 + n) * (start + n) / 2 - (start + 1) * start / 2 =
    acc + (start + 1 + n) * (start + n) / 2 - start * (start - 1) / 2 := by
  sorry

theorem sum_eq_aux (n start acc : Nat) :
    Id.run (forIn [start : start + n] acc fun i r ↦ ForInStep.yield (r + i)) =
      acc + (start + n) * (start + n - 1) / 2 - start * (start - 1) / 2 :=
  match n with
  | 0 => by
    rw [forIn_range_1]
    simp
    rfl
  | n + 1 => by
    rw [forIn_range']
    case h => simp
    simp
    rw [add_comm n, ← add_assoc]
    rw [sum_eq_aux n (start + 1)]
    simp only [ge_iff_le, Nat.succ_add_sub_one, add_le_iff_nonpos_left, nonpos_iff_eq_zero, add_tsub_cancel_right]
    apply main

theorem sum_eq (n : Nat) : sum (n + 1) = n*(n+1)/2 := by
  rw [sum]
  simp
  have := sum_eq_aux (n + 1) 0 0
  simp at this
  rw [this, Nat.mul_comm]

[Kyle Miller]

The mathlib congr! tactic is pretty good at descending into equalities between monad expressions, ifs, and lambdas, and this is used a couple of times here.

[Patrick Massot]

Thanks a lot Kyle!

[Henrik Böving]

I think generally speaking a theorem of the form

for x in [0:n] do
  action

is eqiuvalent to

action
for x in [1:n]
  action

and

for x in [0:n+1]
  action

is equivalent to

for x in [0:n]
   action
action

unfolded to the forIn definition of Std.Range could ease these proofs a lot.

[Henrik Böving]

Hm, actually that theorem doesnt hold if action as a break /o\

[Kyle Miller]

@Henrik Böving Are you suggesting something that's different from, for example, forIn_range'?

[Kyle Miller]

Most of the complexity is from reasoning about the fuel after you unfold the forIn definition.

[Kyle Miller]

Regarding inducting on the stop, I was thinking about how to formulate that, but you need a version of forIn that catches when there's a break to make it easy to state (I guess like Python's for ... else ... loops)

[Kevin Buzzard]

Wow so this is crazy complicated compared to the inductive def of sum. Even the statements are kinda awful. If you multiply both sides by 2 then main is just ring, you've moved the division difficulties elsewhere (but they're not hard to solve here I guess).

[Patrick Massot]

Kevin, this really isn't about Nat division this time. I simply tried to get a program that does something small but non-zero. In my real example there is no Nat division.

[Kyle Miller]

@Kevin Buzzard If Lean has the ability to write imperative programs like this, then I think we should be able to prove things about them. This is a pretty standard program to compute triangle numbers, and you shouldn't have to change the program just because it's not mathematically the most convenient.

That goal isn't hard to prove, though it's not the most fun. Here's something without thinking too hard:

theorem key' (n : Int) : 2 ∣ n * (n + 1) := by
  rw [Int.dvd_iff_emod_eq_zero, ← Int.even_iff]
  apply Int.even_mul_succ_self

theorem key (n : Nat) : (n + 1) * (n + 2) / 2 = n * (n + 1) / 2 + n + 1 := by
  qify [key' n]
  rw [Int.cast_div]
  simp
  ring
  apply key'
  norm_num

theorem key'' (a b c d : Nat) : a + (b + c) - (d + c) = a + b - d := by
  induction c
  · rfl
  simp [Nat.add_succ, *]

theorem main :
    acc + start + (start + 1 + n) * (start + n) / 2 - (start + 1) * start / 2 =
    acc + (start + 1 + n) * (start + n) / 2 - start * (start - 1) / 2 := by
  cases start
  · simp
  next start =>
    simp [Nat.succ_eq_add_one]
    have := key start
    rw [mul_comm] at this
    simp [this]
    rw [add_assoc _ start]
    rw [add_assoc acc, add_comm (start + 1)]
    simp [key'']
    ring_nf
    trivial

[Kyle Miller]

I'm sure the proofs of sum_eq, sum_eq_aux, and main could be improved, but they're not so long that it suggests that it's practically impossible to prove things about for

[Eric Wieser]

Eric Wieser said:

See for instance this message by Mario

One suggestion in this thread was to redefine forIn to avoid a fuel argument, because then we get useful equation lemmas

[Eric Wieser]

(with the speculation being that it only exists in the first place because termination_by didn't exist yet)

[Mario Carneiro]

I did write some API for dealing with these loops, including a bind-like operator docs4#ForInStep.bind like Kyle suggested, but I was mainly aiming for for loops over lists, not Range.

[Mario Carneiro]

see docs4#List.forIn_eq_bindList

[Patrick Massot]

It looks like this is again relating forIn with functional stuff, but surely this isn't how we hope that proofs of programs in Lean 4 will look like, right? I guess we want tactics generating goals where the local context is the same as what you see inside the loop while programming, without seeing any forIn or monadic stuff, right? I'm aware this is a very vague specification, but does it make some sense?

[Mario Carneiro]

Sure, that is definitely on the agenda (we have been holding some meetings at CMU on this topic). It's a major endeavor though, and not likely to seamlessly interact with do notation as it currently exists (which was quite clearly not written with proving in mind). The approach Std is taking is much more pragmatic and similar to where other such goals pop up in mathlib: break everything down into functional stuff and have lemmas for everything

[Sebastian Ullrich]

The proofs in the do paper were based on forM plus exception monads, not forIn (because they use a different implementation of do notation) https://kha.github.io/do-supplement/For.lean.html

[Shreyas Srinivas]

Mario Carneiro said:

Sure, that is definitely on the agenda (we have been holding some meetings at CMU on this topic). It's a major endeavor though, and not likely to seamlessly interact with do notation as it currently exists (which was quite clearly not written with proving in mind). The approach Std is taking is much more pragmatic and similar to where other such goals pop up in mathlib: break everything down into functional stuff and have lemmas for everything

How do we get this for our programs?

[Mario Carneiro]

what do you mean?

[Shreyas Srinivas]

How do we automatically convert our imperative programs to functional versions?

[Kyle Miller]

I think Std's approach is that there is a team of volunteers that do it (unless you're asking what they're talking about at the meetings)

[Shreyas Srinivas]

delete previous message okay so it is done by hand. I am curious to know what the solutions are, as discussed in these meetings of course.

[Mario Carneiro]

the meetings are about the kind of thing Patrick was talking about: having a fancy proof context which works with the imperative program, in a style similar to dafny. One thing I can say is that it would almost certainly be an alternative to the do notation, not a proof about it

[Mario Carneiro]

It is still very much in the design stage though, if you want to prove things about do notation programs you have to do it the old fashioned way

[Jeremy Avigad]

The idea is to modify the "do unchained" approach and devise syntax so that there are places to write loop invariants and proofs. Ideally, the proofs can be filled in automatically, making Lean look more like Dafny or Why3 or F* in that sense. But users will also be able to write interactive proofs by hand.

There is a toy proof-of-concept example here: https://github.com/avigad/verification_demo/blob/main/Demo/Demo.lean#L94-L103.

[Mario Carneiro]

With some new theorems in Std, the proof is now down to this:

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, Id.run]
  · 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]

You can probably golf it some more using mathlib stuff

[Patrick Massot]

Great! Could you also do the forIn' versions?

[Shreyas Srinivas]

I am interested in working towards a solution to this problem because this will make algorithmic verification so much less painful than it is (even in the isabelle world).

[Shreyas Srinivas]

my initial idea was to replace all the loops with folds, because they seem like a general way to represent what loops seem to be doing (fold on a list that carries the relevant program state).

[Shreyas Srinivas]

I don't have a proof that it works in all cases. The idea is based on how forM_ and mapM_ work in haskell

[Jannis Limperg]

forIn, which the for syntax sugar boils down to, is just a monadic fold. It's a slight generalisation of foldlM that also allows early exit.

[Shreyas Srinivas]

The lean version is. But foldl doesn't need to be defined monadically

[Jannis Limperg]

In that case I don't understand the idea. Do you intend to convert the monadic folds to non-monadic ones?

[Shreyas Srinivas]

Jannis Limperg said:

In that case I don't understand the idea. Do you intend to convert the monadic folds to non-monadic ones?

It was an initial idea. I essentially rewrote my own list so that Lean doesn't use some Lean.Internal.coeM and I wrote my fold operation on it. Now I am trying to write an induction rule on this version of fold

[Mario Carneiro]

I essentially rewrote my own list

Don't reinvent List, it will multiply your work 10x. There is a reason String and Array both use List for the model instead of reimplementing it, it has a huge API, convenient recursion principles and a lot of lemmas.