loop invariants

Stream: lean4

[Leonard Wiechmann]

how would i be able to use the fact that for _ in [:n] runs for exactly n iterations?
for example, say i have a struct (i: Nat, h: (P i)), and in each iteration, i derive the next instance of the struct (with i.succ and (P i.succ)).
at the end of the loop, i have (n, (P n)), but how can i get a proof of i = n?
i guess another way of asking that question is, how can i do induction with for loops?

def foo (n: Nat) := Id.run do
  let mut i := 0
  for _ in [:n] do
    i := i + 1
  -- how to derive `Eq i n`?

[Mario Carneiro]

you can't, at least not inside the do block itself

[Mario Carneiro]

you can prove after the fact that i = n at that point however

[Mario Carneiro]

If you want this kind of reasoning inside the program itself you will have to write it in a different way

[Leonard Wiechmann]

hmm, i suspected that it might not be possible. break & continue could mess things up.
by "proving after the fact" i assume you mean outside of the system?

[Mario Carneiro]

no, I mean in a theorem after the def

[Mario Carneiro]

You can reason about do blocks, you just can't make use of that reasoning inside the definition of the do block itself because do blocks are simply typed

[Leonard Wiechmann]

oh, that sounds really interesting!
would that work for

def foo (n: Nat) := Id.run do
  let mut i := 0
  for _ in [:n] do
    i := i + 1
  return 4

or would i have to return i?
i don't even know how i'd formulate the theorem's type if i isn't returned. :thinking:

[Sebastian Ullrich]

You can only state theorems about the pure value of a term, which i in your code above does not participate in

[Mario Carneiro]

your definition is equivalent to def foo (n : Nat) := 4 (and you can prove this). Maybe give a slightly less trivial example where you want a loop invariant?

[Mario Carneiro]

if you returned i then the definition would be provably equivalent to def foo (n : Nat) := n so that's one way to express that the loop did in fact run n times

[Leonard Wiechmann]

provably equivalent to def foo (n : Nat) := n

ok, that makes sense.
i was messing with an iterative fibonacci function. but i guess that's not possible because "do blocks are simply typed".

[Mario Carneiro]

could you write some pseudocode of what you want?

[Mario Carneiro]

something like this?

def fib (n : Nat) := Id.run do
  let mut a := 0
  let mut b := 1
  for _ in [:n] do
    (a, b) := (b, a + b)
  return a

[Leonard Wiechmann]

something like this.
where termination is proved using acc.

    let mut i: {Nat // ⋅ <= n}         := <0, Nat.zero_le n>
    let mut a: {Nat // ⋅ = fib i}      := fib i
    let mut b: {Nat // ⋅ = fib i.succ} := fib i.succ
    while h: i < n do
        (i, a, b) := (
            <i + 1, Nat.succ_le_of_lt h>
            b,
            a + b)
    let h: (i = n) := Nat.eq_of_le_not_lt i.prop h
    return h.rewrite a

(this would define fib_iter: Pi (n: Nat) -> {Nat // ⋅ = fib n})

[Leonard Wiechmann]

though i guess your example with an external proof could be cool too.

[Mario Carneiro]

when I want to write a dependently typed program (i.e. the actual execution relies on proofs), I use local tail recursion:

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

def fib' (n : Nat) :=
  let rec go
    (i : {i // i ≤ n})
    (a : {a // a = fib i})
    (b : {b // b = fib (i + 1)}) :
    {x // x = fib n} :=
  if h : i < n then
    go ⟨i + 1, h⟩ b ⟨a + b, by rw [a.2, b.2]; rfl⟩
  else
    have : i = n := Nat.le_antisymm i.2 (Nat.ge_of_not_lt h)
    by rw [← this]; exact a
  go ⟨0, Nat.zero_le _⟩ ⟨0, rfl⟩ ⟨1, rfl⟩
termination_by go => n - i

[Mario Carneiro]

but it is generally preferable to keep the proof separate from the program if it's not necessary for the type correctness of the program (as it is in this case)

[Leonard Wiechmann]

i see, that's really cool!
and i definitely see why you'd want the proof separate :D

[Leonard Wiechmann]

if i wanted to do an external proof, i'd probably use brec, right? (to get fib i = fib' i for the previous two i)
i'm not too familiar with using lean "practically".

[Mario Carneiro]

you usually don't need to use brec directly, since you can write recursive theorems the same way as recursive functions

[Leonard Wiechmann]

oh, that makes sense!

[Leonard Wiechmann]

def fib3 (n : Nat) := Id.run do
  let mut a := 0
  let mut b := 1
  for _ in [:n] do
    (a, b) := (b, a + b)
  return a


def fib3_eq_fib: ∀ n: Nat, fib3 n = fib n
| 0 => by rfl
| 1 => by rfl
| n+2 => by
  have h: (fib3 n + fib3 (n+1)) = fib3 (n+2) := sorry
  rw [← h]
  rw [(fib3_eq_fib n), (fib3_eq_fib (n+1))]
  rfl

so far i have this, but i don't know how to reason about the fib3 terms.

[Mario Carneiro]

The for loop is not optimized for reasoning. You can do it but the terms are pretty bad

[Leonard Wiechmann]

i see, so it's theoretically possible but not practical?

[Mario Carneiro]

the requisite lemmas don't exist yet

[Mario Carneiro]

not that that's ever stopped me

theorem fib3_eq_fib : fib3 n = fib n := by
  let rec go : ∀ fuel i, fuel + i = n →
    Std.Range.forIn.loop (m := Id)
      (fun _ r => ForInStep.yield ⟨r.2, r.1 + r.2⟩)
      fuel i n 1 (MProd.mk (fib i) (fib (i+1))) =
    ⟨fib n, fib (n+1)⟩
  | 0, i, eq => by simp at eq; simp [Std.Range.forIn.loop, eq]
  | fuel+1, i, eq => by
    rw [Std.Range.forIn.loop]; split <;> rename_i h
    · rw [Nat.le_antisymm (by simp_arith [← eq]) h]; rfl
    · have := go fuel (i+1) (by rw [Nat.add_right_comm] at eq; exact eq)
      rw [fib] at this; simp [this]
  have := go n 0 rfl
  simp [fib] at this; simp [fib3, Id.run, forIn, Std.Range.forIn]; rw [this]