Hi, does anyone know how to distrust this proof ?

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

what do you mean?

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 ?

I do not know where to use CoInductive Definitions.

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

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?

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

@Théo Zimmermann

Ah, thanks! That's exactly what I missed.

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

@Alexander Gryzlov

Thank you for the information!

Last updated: Jun 16 2024 at 01:42 UTC