The Coq mailing list

[Erik Silkensen <eriksilkensen AT gmail.com>]

Thanks, that is informative and I think clears some things up for me.

Is there somewhere I could look in the documentation or online for a simple 
concrete example of this kind of recursion?  I was thinking maybe I could 
work backwards from there to try and understand how it works.  Could someone 
show how to take this code and rewrite it still using Definition or Fixpoint?

Fixpoint f n :=
  match n with
      | 0 => True
      | S m =>
        forall m', m' <= m -> f m'
  end.

On Nov 2, 2013, at 4:00 AM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:

> 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
>>> 
>> 
>