The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

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. 

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

Best,
Christian