Stream: Coq users

Topic: How to use cofix.


view this post on Zulip GhaS Shee (Jun 01 2021 at 15:10):

Hi, does anyone know how to distrust this proof ?

Lemma foo : bar.
Proof.
  cofix foo.
  assumption .
Qed.

view this post on Zulip Gaëtan Gilbert (Jun 01 2021 at 15:19):

what do you mean?

view this post on Zulip GhaS Shee (Jun 01 2021 at 15:44):

I do not know where to use CoInductive Definitions exactly in the Coq system.
However, Coinductive Nat and Coinductive le definition might lead to
forall a b : Nat , le a b by the proving procedure.
What's the problem here ?

view this post on Zulip Gaëtan Gilbert (Jun 01 2021 at 16:02):

I do not know where to use CoInductive Definitions.

if you don't need them, don't use them

view this post on Zulip GhaS Shee (Jun 01 2021 at 16:07):

Then, how do you get 'I do not need coinductive definitions' ?
I think coinduction is quite useful in a recursive proof.
The problem seems it allows us to use coinduction without any restriction.
Does anyone know about the history of the specification?
Why coq allows us to do the proof?

view this post on Zulip Théo Zimmermann (Jun 01 2021 at 16:37):

There are restrictions on how you can use coinduction. Qed will check these. You can read more about this in the coinductive chapter of the reference manual: https://coq.inria.fr/refman/language/core/coinductive.html#top-level-definitions-of-co-recursive-functions

view this post on Zulip GhaS Shee (Jun 01 2021 at 16:57):

@Théo Zimmermann
Ah, thanks! That's exactly what I missed.

view this post on Zulip Alexander Gryzlov (Jun 01 2021 at 17:37):

it's probably better to use paco for bigger coinductive proofs, as it will explicitly show you the guards in the goal

view this post on Zulip GhaS Shee (Jun 02 2021 at 05:56):

@Alexander Gryzlov
Thank you for the information!


Last updated: Jan 31 2023 at 12:01 UTC