Lazy lists

Stream: lean4

[Andrew Yang]

What is the canonical way to get lazy lists?
Here's an example that I need: Suppose I have a l : List Nat, and some (decidable but slow) predicate P : Nat -> Nat -> Bool. I have a lean proof that P a b is satisfied for some a b in l, and a paper proof that a must be one of the first 10 elements of l. How can I find any such a b? If I had lazy list I could write ((l ×ˢ l).filter P).head sorry which will only call P $10|L|$ times at most, but I have the impression that this is $|L|^2$ in lean.

[Henrik Böving]

You could just call List.find? instead of filter

[Andrew Yang]

Thanks! I see. But I guess this is my bad in simplifying my example too much.
In my actual application I have such a function

def List.differences (l : List (List Nat)) : List Nat :=
  (l.map fun li ↦ (li ×ˢ li).filterMap fun (i, j) ↦
    if i < j then .some (j - i) else .none).flatten

And I want a performant implementation of l.differences.dedup.length == 1 if I know that each element will appear at most 10 times and that each (l[i]).Nodup.

[Andrew Yang]

But side question: how does List.find? avoid the problem?
Does (l ×ˢ l).find? P not evaluate l ×ˢ l first?

[Henrik Böving]

Sure but it won't evaluated P that many times, if you also want to avoid that you could use a double for loop instead.

[Andrew Yang]

Using for loops for the application above, I now have

import Mathlib.Data.List.Defs

def List.differences (l : List (List Nat)) : List Nat :=
  (l.map fun li ↦ (li ×ˢ li).filterMap fun (i, j) ↦
    if i < j then .some (j - i) else .none).flatten

def List.differencesDedupLengthLEOne?
    (l : List (List Nat)) : Bool := Id.run do
  let mut thing := 0
  let mut flag := false
  for li in l do
    for i in li do
      for j in li do
        if i >= j then continue
        if not flag then
          flag := true
          thing := j - i
        else if j - i == thing then
          continue
        else
          return false
  return true

theorem foo (l : List (List Nat)) :
    l.differences.dedup.length <= 1 ↔ l.differencesDedupLengthLEOne? := sorry

Is this the intended way? I'll be sad if I am forced to do imperative programming in a FP language, and I have no idea how hard the last sorry will be.

[Henrik Böving]

In principle you could also use hand rolled recursion if it's the imperative part that annoys you. I guess the upcoming work on iterators might also help.

[Andrew Yang]

I guess I can tolerate the imperative part, but I've just tried to induction l; simp [differencesDedupLengthLEOne?] on the sorry and the goal state exploded into 400+ lines and I don't know where to start.

[Bhavik Mehta]

I use MLList for this purpose, but I don't know how canonical it is

[Shreyas Srinivas]

Mathlib once had a lazy list definition

[Andrew Yang]

And it is being replaced with MLList it seems? I'll look into that too. Thanks!
But my first impression is that it is also not suited for proving things...

[Kim Morrison]

MLList isn't intended for proof (at all).

[Shreyas Srinivas]

Strictly speaking I don't see the utility of laziness in proofs

[Shreyas Srinivas]

Lean's thunks come with special support to make them work as thunks should( as I learnt a few months ago), but beyond that lazy lists that use thunks are just lists with extra steps to unfold them.

[Andrew Yang]

By “suited for proving” I mean to write an algorithm with lazy lists and verify in lean that it actually does the right thing.

[Shreyas Srinivas]

In that case, unless you are feeling adventurous, I suggest avoiding monadic code. It's not impossible to prove things inside the Id monad, it's just more tedious and less well documented.

[Shreyas Srinivas]

I started a speculative (potentially fruitless or even wildly wrong) discussion related to this on discord. Feel free to check it out and contribute

[Niels Voss]

I think it might actually be impossible to prove things about MLList, at least without native_decide. It's behavior is defined by an unsafe non positive inductive type

[James Sully]

Henrik Böving said:

upcoming work on iterators

That sounds exciting!