## Stream: Coq users

### Topic: How to use cofix.

#### 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.
``````

#### Gaëtan Gilbert (Jun 01 2021 at 15:19):

what do you mean?

#### 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 ?

#### 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

#### 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?

#### 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

#### GhaS Shee (Jun 01 2021 at 16:57):

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

#### 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

#### GhaS Shee (Jun 02 2021 at 05:56):

@Alexander Gryzlov
Thank you for the information!

Last updated: Jun 16 2024 at 01:42 UTC