Coinduction

Stream: new members

[Hans-Dieter Hiep]

I have a basic question about the use of coinduction. Do you think it would be possible to define a coinductive type, that looks like the following?

coinductive ostream (α : Type) : Type
| head : ostream → α
| otail: ostream → option ostream

That is: a stream that can possibly be finite, but it is not yet known when. I could encode it as a stream as follows:

structure gstream (α : Type) : Type :=
(carrier : stream (option α))
(head : carrier 0 ≠ none)
(definite : ∀n, carrier n = none → ∀m ≥ n, carrier m = none)

But dealing with the proof objects here is kind of tedious. Any suggestions?

[Johannes Hölzl]

what you wrote are the destructors of a record, but for coinductive you would need to write down the constructors, like:

coinductive llist (α : Type) : Type
| nil : llist
| cons : α → llist → llist

At least in Isabelle it's called a lazy list, a maybe terminating list. As far as I know, there is no encoding which is nicely reducing in Lean

[Mario Carneiro]

There are plans to support coinductive data types similar to isabelle. This type would fall under the scope, but for now you have to do it "by hand" like you did.

[Mario Carneiro]

Technically, this coinductive type represents a nonempty lazy list, but something like this would work:

coinductive ostream (α : Type) : Type
| mk (head : α) (otail : option ostream) : ostream

[Mario Carneiro]

I'm not sure if we will have special support for "record-like" coinductives with projections, instead of the usual constructor/destructor/corec

[Hans-Dieter Hiep]

Thanks!
Unfortunately, both

coinductive ostream (α : Type) : Type
| mk (head : α) (otail : option ostream) : ostream

and

coinductive nellist (α : Type) : Type
| sing : α → nellist
| cons : α → nellist → nellist

give me an error: vm check failed: is_closure(o) (possibly due to incorrect axioms, or sorry).
Do I need to import anything?

[Mario Carneiro]

you have to import the future, maybe 3 months

[Mario Carneiro]

That's not a great error, though. Are you using 3.4.2? I thought coinductive was removed as a token, so you should get command expected

[Hans-Dieter Hiep]

Yes.

$ lean -v
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
$ lean --make src
/ufs/hdh/projects/lean-abs/src/util.lean:29:0: error: vm check failed: is_closure(o) (possibly due to incorrect axioms, or sorry)

[Mario Carneiro]

weird... when I put

coinductive ostream (α : Type) : Type
| mk (head : α) (otail : option ostream) : ostream

alone in a file I get

test.lean:1:0: error: unknown command 'coinductive'
test.lean:1:12: error: command expected

[Mario Carneiro]

do you have import meta.coinductive_predicates?

[Mario Carneiro]

looks like the old coinductive predicates code fails with that error on a coinductive data type

[Hans-Dieter Hiep]

When you add import data.finmap on top, two errors appear:
the vm check, and invalid introduction rule, ':' expected

[Mario Carneiro]

hm, can't repro, I just get the vm check

[Hans-Dieter Hiep]

OK, perhaps it is because I am using a non-standard mathlib:
mathlib = {git = "https://github.com/leanprover/mathlib", branch = "master", rev = "9615b385615e51359dce12af181d8cfcc386d105"}

[Mario Carneiro]

in any case you aren't going to find an automatic solution right now... this is all just hypothetical syntax at this point, so lean is just finding new and interesting ways to crash

[Hans-Dieter Hiep]

Thanks for answering! Also thanks to @Johannes Hölzl :-)

[Johannes Hölzl]

@Hans-Dieter Hiep oh, you also might want to change the mathlib reference to leanprover-commnuity in the future.