The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 2 Nov 2013 03:09:56 -0400,
Erik Silkensen 
<eriksilkensen AT gmail.com>
 a écrit :

> Hi Chris, 
> 
> Thanks for such a quick reply and for the pointer to
> well_founded_induction lt_wf.  Does this mean I should be using the
> Fix tactic?  Or Function or Program Fixpoint?  I think I’m getting
> stuck on how syntactically it should look for this basic example.

AFAIK, Fix is not a tactic of the Standard Library. The tactic is 'fix'
which also is a keyword of the language. There is a 'Fix' function
somewhere.

For "Function"/"Program Fixpoint", they do not extend what you can do
with "Definition" or "Fixpoint". I never use them and would not
recommend their use until you really understand how it works, and are
able to do without it (that is simply my point of view, others,
including yourself, might think differently).
In fact even Fixpoint can be defined with Definition
("Fixpoint f <args> := t." is almost the same as
 "Definition f := fix f <args>" := t.", there is a slight difference
 though, but they are both extensionnaly equal, and whenever you can
 define one, you also can define the other).

So simply use the Definition or Fixpoint keyword.

> Thanks again,
> 
> -Erik
> 
> On Nov 2, 2013, at 2:27 AM, Chris Dams 
> <chris.dams.nl AT gmail.com>
> wrote:
> 
> > Dear Eric,
> > 
> > Well, well-founded recursion is exactly what can help you define
> > such a function. Try typing the following into coq.
> > 
> > Require Import Arith.
> > Check well_founded_induction lt_wf.
> > 
> > The type of "well_founded_induction lt_wf" is basically what you
> > seem to want.
> > 
> > Good luck!
> > Chris
> > 
>