Proving correctness of a simple for-loop

Stream: new members

[Federico Lebrón]

Hi! Quite new to Lean4 here. I'm trying to prove the correctness of the following code, using the new monadic local-imperative features:

def elementExists (l: List Int) (q : Int) : Id Bool := do
  for y in l do
    if y = q then
      return true
  return false

The proof I have so far goes:

import Std.Data.HashSet.Lemmas
import Std.Tactic.Do
open Std Do
namespace List
@[simp]
theorem Zipper.pref_mk {α} {l : List α} {rpref suff h} :
    (List.Zipper.mk rpref suff h : List.Zipper l).pref = rpref.reverse := rfl
end List

theorem elementExists_spec (l : List Int) (q : Int)  :
    ⦃⌜True⌝⦄ elementExists l q ⦃⇓r => r = true ↔ List.contains l q ⦄ := by
  mvcgen [elementExists]
  case inv =>
    exact (fun (⟨ret, _⟩, traversalState) =>
      (ret = none ∧ ¬List.contains traversalState.pref q) ∨
      (ret = some true ∧ List.contains traversalState.pref q), ())
  { simp_all }

  {
    intro
    split
    {
      simp
      left
      simp_all
      expose_names
      rewrite [heq.symm]
      simp
      constructor
      {
        intro hnot
        cases h with
        | inl ha => {
          cases ha with | intro a b => exact b hnot
        }
        | inr hb => {
          sorry
        }
      }
      {
        intro q
        exact h_2 q.symm
      }
    }
    {
      simp_all
    }
  }

  all_goals simp_all

If I understand correctly, at the point I'm using sorry, I have to prove something like this:

heq : ⟨none, PUnit.unit⟩ = b'
hnot : q ∈ rpref
hb : b.fst = some true ∧ q ∈ rpref
⊢ False

And I suppose (though it's not clear to me where I would verify this) that b' is the state of have-I-early-returned after the loop body, while b is the state before the loop body. Thus the reason we'd reach False is "You can't have already-early-exited, and later not-have-early exited".

How can I express this fact in Lean? Namely, what connects the behavior of my code (where early exits prevent future not-having-early-exited states) to this proof? I have a feeling my loop invariant may be too weak, and that's where I should introduce this relation between code and proof.

Also I welcome any stylistic critiques, I basically banged on this to make something work... is it "unseemly" to leave things as simp_all? For expository purposes how do folks go about saying "OK simp_all, I know you could close this goal, but how would _I_ close it?"? This expose_names I gather is not preferred, how should I have introduced these unpronounceable names that were generated by mvcgen? Lastly, where would I have found documentation about Std.Do and mvcgen?

Thanks!

[Markus Himmel]

You can adjust the loop invariant to specifically include that after doing an early return you won't traverse the list any further:

import Std.Data.HashSet.Lemmas
import Std.Tactic.Do
open Std Do
namespace List
@[simp]
theorem Zipper.pref_mk {α} {l : List α} {rpref suff h} :
    (List.Zipper.mk rpref suff h : List.Zipper l).pref = rpref.reverse := rfl
end List

def elementExists (l: List Int) (q : Int) : Id Bool := do
  for y in l do
    if y = q then
      return true
  return false

theorem elementExists_spec (l : List Int) (q : Int)  :
    ⦃⌜True⌝⦄ elementExists l q ⦃⇓r => r = true ↔ List.contains l q ⦄ := by
  mvcgen [elementExists]
  case inv =>
    exact (fun (⟨ret, _⟩, traversalState) =>
      (ret = none ∧ ¬List.contains traversalState.pref q) ∨
      (ret = some true ∧ List.contains traversalState.pref q ∧ traversalState.pref = l), ())
  { simp_all }

  {
    intro
    split
    {
      simp
      left
      simp_all
      expose_names
      rewrite [heq.symm]
      simp [Ne.symm h_2]
    }
    {
      simp_all
    }
  }

  all_goals simp_all

Maybe future versions of mvcgen will do this automatically for you.

In fact, with this modification, the whole proof can be automated away:

theorem elementExists_spec (l : List Int) (q : Int)  :
    ⦃⌜True⌝⦄ elementExists l q ⦃⇓r => r = true ↔ List.contains l q ⦄ := by
  mvcgen [elementExists]
  case inv =>
    exact (fun (⟨ret, _⟩, traversalState) =>
      (ret = none ∧ ¬List.contains traversalState.pref q) ∨
      (ret = some true ∧ List.contains traversalState.pref q ∧ traversalState.pref = l), ())
  all_goals (simp_all <;> grind)

Federico Lebrón said:

Lastly, where would I have found documentation about Std.Do and mvcgen?

Right now, there is none, that's why the current version is just a preview :)

Federico Lebrón said:

is it "unseemly" to leave things as simp_all?

As long as it closes the goal: not at all, the whole point is to free you from having to think about all of the details.

Federico Lebrón said:

For expository purposes how do folks go about saying "OK simp_all, I know you could close this goal, but how would _I_ close it?"?

You can use simp_all? to see which lemmas from the library it used.

Federico Lebrón said:

This expose_names I gather is not preferred, how should I have introduced these unpronounceable names that were generated by mvcgen?

You can use next for this:

  next hl hxq =>
    simp [hxq, hl]
    -- Possibly more tactics

[Federico Lebrón]

Ah, thank you Markus! I had not thought of expressing this as you have, "If at the moment you evaluate the invariant, ret = some true, then we also have traversalState.pref = l, meaning we fast-forwarded through the rest of the loop." Do I understand those semantics correctly? Those aren't quite the semantics of a regular while-loop early exit (i.e. we never actually _traversed_ the whole of l, and if we had been incrementing an integer i on each iteration, we'd find i < List.length l, not =). Where did your idea of doing this come from, and how does Lean manage to prove this is true when we add this speeding-through-the-while-loop condition to the invariant? It must be using something specifically about zippers and their iteration, right?

Do you think one could use an invariant more similar to how one proves it in a C-style loop?

int i;
for (i = 0; i < n; ++i) {
  if (l[i] == q) return true;
}
return false;

Where the invariant would be:

• ret = true if and only if q exists in l[0 .. i - 1].
• i <= n.

The guard being i < n, so the negation of the guard, and the invariant, imply the postcondition. Do you think Lean and mvcgen could prove this automatically as well?

I tried doing this, btw, after I saw your blog post from a few days ago, so double thank you :)

[Federico Lebrón]

A simple translation is:

def foo (l: List Int) (q : Int) : Id Bool := do
  let mut i : Nat := 0
  let n : Nat := l.length
  while i < n do
    if l[i]! = q then
      return true
    i := i + 1
  return false

The automatically generated invariant by:

theorem elementExists_spec (l : List Int) (q : Int)  :
    ⦃⌜True⌝⦄ foo l q ⦃⇓r => r = true ↔ List.contains l q ⦄ := by
  mvcgen [foo]

is:

wp⟦forIn Lean.Loop.mk ⟨none, 0⟩ fun x r ↦
      if r.snd < l.length then
        if l[r.snd]! = q then pure (ForInStep.done ⟨some true, r.snd⟩)
        else do
          pure PUnit.unit
          pure PUnit.unit
          pure (ForInStep.yield ⟨none, r.snd + 1⟩)
      else pure (ForInStep.done ⟨none, r.snd⟩)⟧
  (fun a ↦
    wp⟦match a.fst with
        | none => do
          pure PUnit.unit
          pure false
        | some a => pure a⟧
      ⇓ r => r = true ↔ l.contains q = true,
    (⇓ r => r = true ↔ l.contains q = true).snd)

With some basic manipulation:

  intro _true
  simp
  dsimp [wp]
  dsimp [PredTrans.pure]
  apply Iff.intro
  {
    intro h
    dsimp [Id.run] at h

we get to:

l : List Int
q : Int
_true : ⌜True⌝
h : (match
    (forIn Lean.Loop.mk ⟨none, 0⟩ fun x r ↦
        if r.snd < l.length then
          if l[r.snd]?.getD 0 = q then pure (ForInStep.done ⟨some true, r.snd⟩)
          else pure (ForInStep.yield ⟨none, r.snd + 1⟩)
        else pure (ForInStep.done ⟨none, r.snd⟩)).fst with
  | none => pure false
  | some a => pure a) =
  true
⊢ q ∈ l

But it's not clear to me how to use h. Since this is the Id monad it should be easy to get rid of the monad at least, and this goal is "Prove that if the program returned True, then q is in l`.

Is there a way to introduce my own invariants, instead of using mvcgen? I haven't worked with weakest precondition much, while I'm more used to using induction with the i-based invariant :)

[Markus Himmel]

Proving things about while loops is not possible at the moment. The reason for this is that while is implemented as a partial function and therefore opaque to the Lean kernel. It is likely that this restriction can be lifted in the future so that you can prove things about while loops as long as you also provide a termination proof.

You can make progress using a for loop over a range:

import Std.Tactic.Do
open Std Do

def foo (l: List Int) (q : Int) : Id Bool := do
  let n : Nat := l.length
  for h : i in [0:n] do
    if l[i] = q then
      return true
  return false

theorem elementExists_spec (l : List Int) (q : Int)  :
    ⦃⌜True⌝⦄ foo l q ⦃⇓r => r = true ↔ List.contains l q ⦄ := by
  mvcgen [foo]
  case inv =>
    exact (fun (⟨ret, _⟩, traversalState) =>
      -- Think of `traversalState.rpref.length` as `i`
      (ret = none ∧ ¬(l.take traversalState.rpref.length).contains q) ∨
      (ret = some true ∧ l.contains q ∧ traversalState.rpref.length = l.length), ())
  all_goals simp_all

So far there is no "first class" support for for loops over ranges however; mvcgen basically transforms the loop into a loop over the list [0, 1, ..., n - 1], and from there the proofs are similar to the original version except that you now have the additional indexing indirection. I expect that proofs about for loops over ranges will be a bit nicer in the released version.

[Marcelo Fornet]

I had not thought of expressing this as you have, "If at the moment you evaluate the invariant, ret = some true, then we also have traversalState.pref = l, meaning we fast-forwarded through the rest of the loop."

I'm also confused about this.

Similar paragraph on https://markushimmel.de/blog/my-first-verified-imperative-program/

The third line is a fairly literal translation of the first case described in prose above, and the fourth line is a translation of the second case, with the slightly technical condition l = traversalState.pref thrown in, which asserts that if we have taken the early return, we will not traverse the list any further.

What is happening in that case, given l = traversalState.pref is not necessarily True at the point of the early return.