infinite lists

Stream: lean4

[Adrien Champion]

I'm trying to represent infinite lists, define map zip and such, and reason about all of that. In case you want to know why I included an explanation below.

So basically I started with something like this

inductive Sem.Stream (α : Type u)
| nil : Stream α
| cons : α → (Unit → Stream α) → Stream α

and experimented for a while with this and other designs. After some discussion with @Arthur Paulino (thanks to @Damiano Testa) I wrote this

inductive Sem.Stream (α : Type u)
| nil : Stream α
| cons : α → (Unit → Stream α) → Stream α
deriving Inhabited

so that I can write functions like

partial def Sem.Stream.forever (val : α) : Stream α :=
  cons val (fun () => forever val)

But now I want to prove things about such functions, but I cannot unfold or simp them because they are partial.

@Arthur Paulino told me that I need to look for a different design, but I'm out of ideas. Apparently @Kyle Miller and/or @Anand Rao discussed something similar on the Discord server, which I'm looking for currently.

But if anyone has a clean way to do infinite lists I'm very interested :smiley_cat:

Why?

I'm trying to understand Functional Reactive Programming through this paper:

• http://conal.net/papers/push-pull-frp/push-pull-frp.pdf

I like the approach via denotational semantics so I'm trying to as much of it as I can in Lean. The author use Haskell, so they can represent event streams as a list of (potentially infinite) lists of time/event pairs. Then they go on to prove several things about event streams with temporal-list merging, for instance that it defines a Monoid.

And I want to do that too.

[Leonardo de Moura]

Lean 3 has a stream type which is encoded as Nat -> α
https://github.com/leanprover/lean/blob/72a965986fa5aeae54062e98efb3140b2c4e79fd/library/data/stream.lean
Not sure whether someone has already ported this file to Lean 4.

[Adrien Champion]

Yes, Stream is in Lean 4 and my Sem.Stream implement it

[Adrien Champion]

I was using Stream at first but I failed to prove the properties I wanted because it carries the type of the stream with it, which makes sense

I was trying to erase that type so that I can see streams as a more logically-pure structure where conducting proof is easier/possible

[Leonardo de Moura]

The Stream type in the Lean 4 repo is a different thing. It is a typeclass.

[Adrien Champion]

Oh my bad I misunderstood (did not read properly)

[Adrien Champion]

Oh, this looks pretty interesting, thank you for the link!

[Adrien Champion]

Would there be interest if I was to port this to Lean 4?

[Arthur Paulino]

We're currently using Mathlib4 as a repository of useful data structures for now, so you can place it there and eventually it might be extracted to a separate Std package

[Adrien Champion]

Sounds good I'll do my best then!

[James Gallicchio]

Also worth mentioning that someone is working on building coinductive types in Lean4 (see this topic), but not sure how far that work is yet

[Mario Carneiro]

@Adrien Champion FYI since no one mentioned: your Sem.Stream type consists only of finite lists because it's still an inductive type, so your partial def cannot be made into a proper def because it violates the rules of the logic. For example I can prove that Sem.Stream.forever contains a nil subterm even though I can't unfold it (and even though it plainly doesn't if you look at the definition), because this is true for everything in the Sem.Stream type.

[Adrien Champion]

@Mario Carneiro I do have some understanding of this problem, but thank you for laying it down for me :smiley_cat: I come from SMT-based verification (k-induction, Horn clauses...) and I only started ITPs recently, your feedback helps a lot

@Leonardo de Moura 's pointer looks like a much better approach so I'm definitely dropping my previous, terrible, noob approach

[Mario Carneiro]

Leonardo de Moura said:

Lean 3 has a stream type which is encoded as Nat -> α
https://github.com/leanprover/lean/blob/72a965986fa5aeae54062e98efb3140b2c4e79fd/library/data/stream.lean
Not sure whether someone has already ported this file to Lean 4.

This file was moved to mathlib (data.stream.defs, data.stream.init), and although it has not yet been ported properly you can read it, like everything else, in lean 4 syntax using the mathlib3port repo (Data.Stream.Defs, Data.Stream.Init)

[Mario Carneiro]

for something as simple as data.stream.defs which has no dependencies, it might just work out of the box

[Adrien Champion]

Great to know, thanks, but I'm still porting it as an exercise!

[Mario Carneiro]

there are two files there, and I'm guessing the second one is the more interesting one (and I doubt that one works out of the box since it uses tactic.ext)

[Adrien Champion]

So I ended up porting both files as an exercise, meaning before reading the mathlib contribution guidelines. Now that I have read (enough of) them I don't think I have the time and the energy to actually make the contribution, at least not until there is a formatter.

But maybe this was not for nothing and someone can pick up what I did. Everything compiles fine, it's just a matter of following the guidelines. So here it is:

• https://github.com/AdrienChampion/mathlib4/tree/streams/Mathlib/Data/FStream

[Arthur Paulino]

There is a reformatter script in the lean4 repository, in the scripts directory. AFAIK it's experimental, but you can try

[Adrien Champion]

Thanks, I wasn't aware of this script. I tried it but it mostly fails, I see a lot of "backtrack exceptions" and problems in the output. The bits it does format do not seem to follow mathlib's guidelines at all.

[Adrien Champion]

But maybe I'm just confused about mathlib's contribution guidelines, as most (if not all) of mathlib 4's code I looked at don't follow the guidelines anyway.

[Adrien Champion]

In any case, this discussion would be more suited to #mathlib4 so let me move it there

[Alex J. Best]

What guidelines are you looking at? mathlib for lean 3 has a lot of strict guidelines, but mathlib4 is mostly a testbed and even says "We're not planning to have any review standards in the mathlib4 repo higher than your average wiki during this experimentation phase." in the README

[Mauricio Collares]

Also, if you run the reformat script with lean --run scripts/reformat.lean YourFile.lean, you probably won't get the backtrack exceptions

[Adrien Champion]

Mauricio Collares said:

Also, if you run the reformat script with lean --run scripts/reformat.lean YourFile.lean, you probably won't get the backtrack exceptions

> lean --run script/reformat.lean ~/repos/mathlib4/clean/Mathlib/Data/FStream/Defs.lean | rg "exception"
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception
cannot print: parenthesize: uncaught backtrack exception

[Gabriel Ebner]

You need to run it with lake build && lake env lean --run ~/lean4/script/reformat.lean Mathlib/Data/FStream/Defs.lean

[Adrien Champion]

Alex J. Best said:

What guidelines are you looking at? mathlib for lean 3 has a lot of strict guidelines, but mathlib4 is mostly a testbed and even says "We're not planning to have any review standards in the mathlib4 repo higher than your average wiki during this experimentation phase." in the README

Okay so that's where my confusion was from. I guess I was stressed out at the idea of contributing and jumped straight to mathlib 3 guidelines when I should have paid more attention to the actual readme.

That's my bad, thank you!

[Adrien Champion]

Gabriel Ebner said:

You need to run it with lake build && lake env lean --run ~/lean4/script/reformat.lean Mathlib/Data/FStream/Defs.lean

Right this works better thanks!

[Adrien Champion]

The discussion on porting streams and contributing to mathlib4 continues in **mathlib4>Porting streams (Nat → α)**