-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[WIP] added basic machinery for defining coinductive types #71
[WIP] added basic machinery for defining coinductive types #71
Conversation
4fe227b
to
a588f9e
Compare
I took the example from It defines a possibly infinite tree as:
It can be constructed using
The parameter |
data/coinductive.lean
Outdated
-/ | ||
import data.pfun | ||
|
||
import data.stream |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This import is not needed, right?
data/coinductive.lean
Outdated
apply n_ih, | ||
end | ||
|
||
abbreviation path' (β : α → Type v) := list (Σ i, β i) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
AFAIK, the abbreviation
command is not intended for general usage. Its only purpose is to define id_rhs
. The difference compared to def
is that it sets a special reducibility hint for the kernel type-checker.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the note! I thought I read a comment from Leo about abbreviation
removing the need to ever use reducible
but I can't find it anymore. In any case, this definition works even without reducible
so I'll just make it plain.
data/coinductive.lean
Outdated
variables {β} | ||
protected def corec (i : X) : cofix β := | ||
{ approx := s_corec f i | ||
, consistent := P_corec _ _ } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I won't complain about coding style. https://github.com/leanprover/mathlib/blob/master/docs/style.md
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the naming is good but the spacing probably needs work. The proofs I think need a lot of work. A lot are far too long. I'll be addressing both as I whip the package into shape
def mk_tree : ℕ → l_two_tree ℕ :=
l_two_tree.corec $ λ z n mk_tree, This seems to work pretty nicely in practice. Is it possible to change the internal |
91dac62
to
17dfb6e
Compare
I have a few ideas on how to do that. I think ultimately, the best will be to have a different keyword than I can address your example with an ad hoc contraption as follows:
Notice that |
I should add: thanks for asking this question, I could really use that kind of device in my pipes library and I was about to dive head first in an implementation of unbounded recursion to handle my problem. What you asked about is much better. |
By changing
to
I managed to write a corecursor that accommodates arbitrary (non-null) number of nested constructors:
It has one new quirk: the necessity of calling |
Here are a few ideas for where this project might go:
|
Looking at how I enabled nested constructors, I'm wondering if we could have a more relaxed guardedness criterion than Coq and allow code like this:
Basically, one of the branches is not guarded (according to Coq) but the list argument decreases until we use a constructor of stream. |
My motivating example for this feature is a Lean port of the Haskell pipes library for composing streaming programs: https://hackage.haskell.org/package/pipes. As an aside, it is also beautifully documented. Mine is https://github.com/cipher1024/lean-pipes. I started developing it again to see how far the current feature set takes me. This package finally enabled me to write the I'm now exploring how I need to adapt bisimulation for practical proofs of equality. |
90db5b4
to
07094ee
Compare
2f0beae
to
22e671c
Compare
07094ee
to
f6c67b7
Compare
6c317ff
to
a351325
Compare
…ion.approximation and cofix
…tree` constructors arbitrarily deep
representation of coinductive types. Not meant for manipulating individual coinductive types
a351325
to
1bbbced
Compare
@cipher1024 What is the status of this? Is this still WIP, or dead? Should we close this PR? |
I have moved this development to |
Fare well |
No description provided.