Proving something about forIn

Stream: new members

[Yongyi Chen]

I'm challenging myself to prove that doNothing is the identity function, where

import Mathlib

def doNothing (as : Array α) := Id.run do
  let mut r := #[]
  for a in as do r := r.push a
  return r

What I attempted:

import Mathlib

def doNothing (as : Array α) := Id.run do
  let mut r := #[]
  for a in as do r := r.push a
  return r

theorem pop_concat_last_eq (as : Array α) (h : as.size > 0) : as.pop ++ #[as.data.getLast (List.length_pos.mp h)] = as := by
  apply Array.ext'
  simp
  exact List.dropLast_append_getLast (List.length_pos.mp h)

theorem doNothing_eq_id (as : Array α) : doNothing as = as := by
  induction' h : as.size with n ih generalizing as
  . rw [List.length_eq_zero] at h
    have : as = #[] := by apply Array.ext' h
    subst this
    trivial
  . let bs := as.pop
    let b := as.data.getLast (List.length_pos.mp (Nat.lt_of_sub_eq_succ h))
    have : bs ++ #[b] = as := by exact pop_concat_last_eq as (Nat.lt_of_sub_eq_succ h)
    rw [← this]
    replace ih : doNothing bs = bs := ih bs (by simp only [Array.size_pop, ge_iff_le, Nat.succ_sub_succ_eq_sub, nonpos_iff_eq_zero, tsub_zero, h])
    dsimp [doNothing, Id.run, forIn]
    sorry

I'm hitting a brick wall here. Not sure if this is the right approach.

[Kevin Buzzard]

These "how to prove that a completely basic program has no bugs" questions remind me of the Lean chat in summer 2017 when it was mostly "how to prove that a completely basic maths question (such as 2+2<500.678) is true" and there was no norm_num.

[Joachim Breitner]

I’d say that doing proofs over monadic code like this will be very painful, without suitable tactics and program logics. I expect there is a way to push this through, but I don’t expect it to be practical.

If you start your proof with unfold doNothing you’ll see that it ’s defined using a function called forIn:

α: Type u_1
as: Array α
⊢ Id.run
    (let r := #[];
    do
    let r ←
      forIn as r fun a r =>
          let r := r;
          let r := Array.push r a;
          do
          pure PUnit.unit
          pure (ForInStep.yield r)
    let r : Array α := r
    pure r) =
  as

So I expect you’ll need to define a helper lemma about that forIn, prove that by induction, and then use it outside.

[Joachim Breitner]

Practically speaking, if you want to verify basic programs, write them in a pure functional style, e.g. using recursion.

[Yongyi Chen]

So it looks like it's not just me, and we don't have (yet) the tools to do this. Thanks!

[Tomas Skrivan]

It is definitely possible but not that straightforward as one would hope. Here is version for List. For Array I have to think about it a bit more.

def doNothing (as : List α) := Id.run do
  let mut r := []
  for a in as do r := r.concat a
  return r

@[simp]
theorem forIn_concat_append (as as' : List α)
  : (forIn (m:=Id) as as' fun a' r => ForInStep.yield (List.concat r a')) = as'.append as :=
by
  revert as'
  induction as
  case nil =>
    simp
  case cons a' as h =>
    simp[List.concat,h]
    intro as'
    induction as'
    case nil =>
      simp[List.concat]
    case cons a'' as' h' =>
      simp[h',List.concat,List.append]

example (a : List α)
  : doNothing a = a :=
by
  simp[doNothing,Id.run]

I think having some induction principle for lists or arrays that is peeling off elements from the right would be helpful.

[Tomas Skrivan]

I think for arrays it would be helpful to prove this simp theorem analogous to List.forIn_cons

@[simp] theorem Array.forIn_cons [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β)
    : forIn (Array.mk (a::as)) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn (Array.mk as) b f := sorry

[Tomas Skrivan]

@Yongyi Chen btw it would be helpful if your example code would be self contained and work with the View in Lean 4 playground button in the top right corner of every code block

[Yongyi Chen]

Oh, I'll add in the necessary imports!

[Tomas Skrivan]

Unfortunately with more complicated code you want to maintain an invariant inside of the for loop. Then it gets hard and there is not much tooling for that right now.

[Yongyi Chen]

Yeah, going through the code and showing invariants is how a proof in a typical CS class would go.

[Mario Carneiro]

Every time this exercise comes up we find a few more lemmas for Std. I was able to reduce the proof to this:

import Std.Data.Array.Lemmas

--- for std
theorem Array.forIn_eq_data_forIn [Monad m]
    (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
    forIn as b f = forIn as.data b f := sorry -- proof omitted
@[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
    arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)

def doNothing (as : Array α) := Id.run do
  let mut r := #[]
  for a in as do r := r.push a
  return r

theorem doNothing_eq_id (as : Array α) : doNothing as = as := by
  simp [doNothing, Array.forIn_eq_data_forIn]
  let f a r : Id (ForInStep (Array α)) := ForInStep.yield (Array.push r a)
  have H l r : forIn l r f = r ++ (l : List α) := by induction l generalizing r <;> simp [*]
  apply Array.ext'; rw [H]; simp [Id.run]

[Mario Carneiro]

added in 282e3a1

[Mario Carneiro]

Tomas Skrivan said:

Unfortunately with more complicated code you want to maintain an invariant inside of the for loop. Then it gets hard and there is not much tooling for that right now.

There is always an invariant when proving things about loops of any kind, and this one is no exception. It is the inductive hypothesis, and in this case I have written it as saying that forIn l r f = r ++ (l : List α), that is, the effect of the loop is to append as to the initial value r

[Jun Yoshida]

I have struggled with such problems several times, too. IMO, it is convenient to relate @forIn m ρ α _ β loop with ρ.foldlM (m:=StateT (ForInStep β) m) (e.g. in the case ρ=List α or Array α) or its combination with a "proof attacher" like List.pmap. If ρ.foldlM has a good induction principle, then we can just use it. I believe that Std.Range also admits such a good foldM.

[Jun Yoshida]

From this point of view, it may be worth having some analogue of Haskell's MonoFoldable class.