Zulip Chat Archive

Stream: new members

Topic: Coinduction


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 08 2019 at 09:10):

you have to import the future, maybe 3 months

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 08 2019 at 09:18):

do you have import meta.coinductive_predicates?

view this post on Zulip Mario Carneiro (Feb 08 2019 at 09:19):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 08 2019 at 09:22):

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

view this post on Zulip 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"}

view this post on Zulip 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

view this post on Zulip Hans-Dieter Hiep (Feb 08 2019 at 09:24):

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

view this post on Zulip 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