The Coq mailing list

[Jean-Baptiste Jeannin <jeannin AT cs.cornell.edu>]

Good evening,

I would like to get a precise, detailed account of the guardedness side 
condition checked by the cofix tactic in Coq. I understand that this side 
condition is only checked when typing "Qed.", and that it essentially is that 
"every corecursive call must be a direct argument to the constructor of the 
coinductive type we are generating" [1], or that it "ensures that the 
hypotheses are only used after the definitions of the functions in their 
conclusions have been unfolded" [4], namely that progress has been made.

However I would like a detailed and precise account of it. I tried looking at 
[2], where it is explained on programs, and translates to proofs using the 
proofs-as-programs correspondence, but I have trouble following; it would be 
helpful to have a concise explanation directly on proofs. The post [3] on 
this list also gives a similar intuitive idea of it, and posts a link to an 
old version of the manual; but the post is 11 years old and the link is dead.

I got interested in this question while reading the recent paper [4], which 
also gives a similar intuitive explanation of the guardedness condition, but 
without the details. I couldn't find the details, please let me know if they 
are available somewhere.

Thank you,
Jean-Baptiste Jeannin

[1] Adam Chlipala, Certified Programming with Dependent Types, Library 
Coinductive chapter, http://adam.chlipala.net/cpdt/html/Coinductive.html
[2] Eduardo Gimenez, Codifying guarded definitions with recursive schemes, 
Types for Proofs and Programs, 1995
[3] https://sympa.inria.fr/sympa/arc/coq-club/2002-04/msg00001.html
[4] Chung-Kil Hur, Georg Neis, Derek Dreyer and Viktor Vafeiadis, The Power 
of Parameterization in Coinductive Proof, POPL 2013