Stream: Coq users

Topic: Unfolding cofixpoints


view this post on Zulip maxv (Jul 20 2023 at 10:00):

Here is another question about cofixpoints. Say I want to prove a goal that involves a subexpression (cofix f ... := ...) (...) and I want to unfold it once, rewriting the goal so as to substitute the argument into the body of f. How would I do that? My first guess was cbv cofix but that doesn't do anything.

view this post on Zulip Karl Palmskog (Jul 20 2023 at 10:28):

I'd recommend following tutorial/examples on coinduction, there are a few in Coq'Art

view this post on Zulip Li-yao (Jul 20 2023 at 16:15):

Do I have to recourse to wrapping it in an artificial case expression to force evaluation?
Yes. To ensure termination, cofix only reduces under an eliminator (match or primitive projection for coinductive records). You can prove a lemma to eta expand terms of coinductive types (in cpdt there is a chapter on coinduction, where the relevant construct is called "frob"). Or you can phrase your propositions so that all occurrences of coinductive type end up under eliminators in the first place.

view this post on Zulip Pierre Castéran (Jul 21 2023 at 13:46):

Karl Palmskog said:

I'd recommend following tutorial/examples on coinduction, there are a few in Coq'Art

A text on unfolding cofixpoints is available in section 13.4 of this chapter.


Last updated: Jun 13 2024 at 19:02 UTC