GhaS Shee (Jun 01 2021 at 15:10): 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.
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: Oct 13 2024 at 01:02 UTC