The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi,

> Le 14 sept. 2020 à 22:33, Christian Doczkal <christian.doczkal AT inria.fr> a 
> écrit :
> 
> On 9/14/20 8:16 PM, Gert Smolka wrote:
>> Smiley!  What you are referring to is the guard condition, which was
>> extended over the years but never documented.
> 
> Was it really never documented? I was referring to the slides from Bruno 
> Barras (from some unknown event in 2010, probably some Coq developer 
> meeting) that has a rule for nested fixpoints:
> 
> https://coq.inria.fr/files/adt-2fev10-barras.pdf (Slide 15). 
> 
> But without the explanations, the rules are pretty much indigestible. I 
> guess it's not too surprising that his example is indeed the size function 
> for trees (which relies on the fold_right in the standard library being 
> defined by pulling the function-argument out of the fixpoint):
> 
> Inductive tree := T (A: list tree).
> 
> Fixpoint size (t:tree) :=
>  match t with T A => fold_right (fun t' n => n+size t') 1 A end.
> 
> My question was: what precisely makes the t' from the above 
> lambda-abstraction smaller than t. 

The guard condition allows itself to delta and beta-reduce the body of a 
fixpoint to check for termination.
In doing so, it unfolds the fold_right and substitutes the function inside 
it. In addition,
when guard-checking `(fix F arg { struct arg } := body) A`, the `body` of the 
fixpoint
is guard-checked with the assumption that the size of `arg` is less than or 
equal to the size of
`A` [1]. This is where the magic happens. Now when checking the unfolded 
fold_right the `size t’`
call will have simplified to some `size arg’` where `arg’ < arg <= A < t` 
making the recursive 
call to size legit.

> Funny aside: the conclusion of said talk (10 years ago) was: "Syntactic 
> criteria are dead ».

Maybe it is a good place to mention that their is current work by Jonathan 
Chan and William Bowman 
to implement a sized type checker for Coq [2]. As far as I understand, the 
main current limitation 
is that it cannot handle such nested types without introducing polarities in 
inductive definitions.

[1] 
https://github.com/coq/coq/blob/60960284237b295f8b82e07119e1ba1467b9a1de/kernel/inductive.ml#L1057
[2] https://github.com/coq/coq/pull/12426
— Matthieu