The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

On Wed, 14 Feb 2007, Hugo Herbelin wrote:

>  - new command Function to generate fixpoints with arbitrary well-
>    foundedness termination evidence and associated "functional"
>    induction scheme, fixpoint equation, and support for inversion
>    (by P. Courtieu and J. Forest and by Y. Bertot)

http://coq.inria.fr/V8.1/refman/Reference-Manual004.html#@default87

Function ident binder1...bindern  {wf term1 ident0} : type0 := term0

About this new feature, I would like to add that the CoLoR library 
(http://color.loria.fr) provides many useful results for proving the 
well-foundedness of relations:

- either directly: see the CoLoR directories Util/Multiset (well-foundedness 
of the multiset extension of a well-founded relation) and Util/Relation 
(lexicographic combination of well-founded relations [Lexico.v], union of 
well-founded relations [Union.v], well-foundedness of a relation modulo 
another one [SN.v], well-foundedness of an iterate [SN.v], etc.)

- or by defining your ordering as the rewrite relation generated by a set of 
rewrite rules (see for instance Term/WithArity/ATrs.v) and using the numerous 
termination criteria formalized in CoLoR (polynomial interpretations, RPO, 
dependency pairs, etc.)

NB. In CoLoR, relations are oriented from left to right: SN R is equivalent to 
Acc (transp R) (see Util/Relation/AccUtil.v for conversion lemmas).

You can freely download the CoLoR library on http://color.loria.fr/.