## Stream: new members

### Topic: Coinduction

#### Hans-Dieter Hiep (Feb 08 2019 at 08:34):

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 (Feb 08 2019 at 08:57):

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 (Feb 08 2019 at 08:58):

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 (Feb 08 2019 at 09:00):

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 (Feb 08 2019 at 09:01):

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 (Feb 08 2019 at 09:07):

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 (Feb 08 2019 at 09:10):

you have to import the future, maybe 3 months

#### Mario Carneiro (Feb 08 2019 at 09:11):

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 (Feb 08 2019 at 09:14):

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 (Feb 08 2019 at 09:17):

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 (Feb 08 2019 at 09:18):

do you have import meta.coinductive_predicates?

#### Mario Carneiro (Feb 08 2019 at 09:19):

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

#### Hans-Dieter Hiep (Feb 08 2019 at 09:20):

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

#### Mario Carneiro (Feb 08 2019 at 09:22):

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

#### Hans-Dieter Hiep (Feb 08 2019 at 09:23):

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 (Feb 08 2019 at 09:23):

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 (Feb 08 2019 at 09:24):

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

#### Johannes Hölzl (Feb 08 2019 at 13:09):

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

Last updated: May 12 2021 at 23:13 UTC