The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 20/03/2012 07:08, Andrej Bauer a écrit :
> How does Coq detect a structurally decreasing argument in a fixpoint?
> Is this described somewhere?
> 
> Pointers to relevant literature would be greately appreciated! (This
> is about an undergraduate student project.)

I don't know if it qualifies as "literature", but the commit message
introducing it is quite explicit:

> If a fixpoint is not written with an explicit { struct ... }, then 
> all arguments are tried successively (from left to right) until one is 
> found that satisfies the structural decreasing condition.
> 
> When the system accepts a fixpoint, it now prints which decreasing argument 
> was used, e.g:
> 
>  plus is recursively defined (decreasing on 1st argument)
> 
> The search is quite brute-force, and may need to be optimized for huge 
> mutual
> fixpoints (?). Anyway, writing explicit {struct} is always a possible 
> fallback.
> 
> N.B. in the standard library, only 4 functions have an decreasing argument 
> different from the one that would be automatically infered: 
>   List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind
> And compiling with as few explicit struct as possible would add about 15s 
> in compilation time for the whole standard library. 

From revision 9961 in trunk, by letouzey:

  https://gforge.inria.fr/scm/viewvc.php?view=rev&root=coq&revision=9961


Cheers,

-- 
Stéphane