The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

To answer about Function specifically: in short yes Function could
adapt to a type based termination checking. Mainly because Function is
a wrapper upon Fixpoint. It has two goals:

1) Automate (by mean of the graph of the function):
 a) Proof of fixpoint equality
 b) Functional induction
 c) Functional inversion

2) Allow for non structurally decreasing recursive calls, still enjoying 
1)abc.

In particular in case no (wellfounded) relation is given, Function
builds a regular Fixpoint (and then 1)abc). If a new version of
Fixpoint arises with a type-based termination construct, then this
would be compatible with Function almost for free. In particular 1)abc
would be available.

By the way for the record: The description of the Function command is
in the paper below [1] (it was called GenFixpoint at that time). When
a function does not perform recursive calls on "guarded" arguments,
Function uses the so-called Bertot-Baala method also named "converging
iteration" to define the function. This is described in [2] (is there
another ref except Balaa's thesis in french?).

Best regards,
Pierre

[1] Gilles Barthe, Julien Forest, David Pichardie, and Vlad Rusu.
Defining and Reasoning About Recursive Functions: A Practical Tool for
the Coq Proof Assistant.. In Proc of 8th International Symposium on
Functional and Logic Programming (FLOPS'06), volume 3945 of Lecture
Notes in Computer Science, pages 114-129, 2006. Springer-Verlag.

[2] A. Balaa and Y. Bertot. Fix-point equations for well-founded
recursion in type
theory. In M. Aagaard and J. Harrison, editors, Proceedings of TPHOLs'00, 
volume
1689 of Lecture Notes in Computer Science, pages 1-16. Springer-Verlag, 2000.


2014-03-15 0:16 GMT+01:00 Cody Roux 
<cody.roux AT andrew.cmu.edu>:
> Can the Function mechanism mentioned in c) be built on top of sized types?
>
>     Yes of course. Here's something which users should be aware of: the
> functions nat -> nat it is possible to *define* in Coq are the same in CIC
> with recursors, with guard conditions and with size-types (essentially, all
> provably total functions in HOL). The only difference is the *complexity of
> the definition* and the *equational behavior on open terms*, two things that
> are very important in practice.
>