Porting `stream`s (`Nat → α`)

Stream: mathlib4

[Adrien Champion]

Original discussion in #lean4 > infinite lists.

I ported the stream type from mathlib/data/stream/defs.lean and mathlib/data/stream/init.lean which encodes streams as functions over discrete time (Nat → α).

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

If deemed worth it, I would be interested in contributing this code to mathlib4. I wrote it as an exercise: naming the stream type FStream might not have been a good idea, and commits (all two of them) do not follow lean's commit conventions, but that's easily fixed.

[Marcus Rossel]

Not sure about this, but I'm guessing this will be covered by synport. Are you aware of the general porting strategy for mathlib4?

[Adrien Champion]

Well in the original discussion @Mario Carneiro pointed to the ported version of these files

• https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Data/Stream/Defs.lean
• https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Data/Stream/Init.lean

I was then told that they would most likely not work right away, or at least the Initfile, because of the dependency on tactic.ext. The port itself was initially more of an exercise than anything for me, so I did not investigate much.

All I can say is that I was using the ported Init.lean and went back to the Lean 3 version when I ran into a few theorems/proofs that did not make sense. I don't remember precisely what the problem was but I can re-discover it if you want more details (I vaguely remember notation clashes or something like that but I'm not sure)

[Adrien Champion]

Marcus Rossel said:

Not sure about this, but I'm guessing this will be covered by synport. Are you aware of the general porting strategy for mathlib4?

To address your question no, I was not aware of this page. Thank you for mentioning it I'll read this asap

[Adrien Champion]

Also, my version includes Lean-4-ifying some aspects that (I assume) synport would not cover. (Slightly) more documentation is one aspect, but I'm thinking more of defining functions in the appropriate namespace for accessibility and val.fun args notation. For instance the original version has appendStream : List -> stream a -> stream a which I changed to List.appendStream, and added FStream.prependList.

[Adrien Champion]

Admittedly there are few situations like that in the port

[Mario Carneiro]

I think we should try not to make any naming changes for things that already exist, because this makes downstream porting a lot harder. If your innovations are possible to do in lean 3 as well as lean 4, it seems better to submit them first to mathlib and then port it to mathlib4.

[Mario Carneiro]

Perhaps we should also back-port the new name, since stream is taken

[Adrien Champion]

I understand. Sadly, I have virtually no experience with Lean 3 and not enough time to get into it for the sake of this (very minor) contribution :/

[Adrien Champion]

Thank you all for the feedback though!