The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Following up on Martijn and Petar's replys, I think one way to look at
this is the following: it is commonly cumbersome to work directly with
tail-recursive definitions, as you experienced in that instance,
because of the way the accumulator changes over the induction step.
One thing to do is to prove that your tail-recursive function is
basically the same thing as the non tail-recursive one, and then use
rewrite's instead of simplifications when you need to.
This is exactly what Martijn's lemma does, it rephrases [sum a (S b)]
as if it had been defined non tail-recursively. This is also what
Petar's lemma does, albeit in a slightlty different way, by relating
the value of [sum a b]  to a "fixed" accumulator, in that case 0,
basically making [sum] a unary function. Indeed you can read his lemma
as:

sum a b = a + sum 0 b

In that second case, you explicitely need the auxiliary non
tail-recursive definition of [sum], ie. [+], whereas in the first case
you don't, but you need one lemma per recursive branch of your
inductive.

Hope this helps,

Stéphane

On Sun, Dec 12, 2010 at 7:17 PM, Martijn Vermaat 
<martijn AT vermaat.name>
 wrote:
>>   Fixpoint sum (a b : nat) : nat :=
>>     match b with
>>     | 0 => a
>>     | S b1 => sum (S a) b1
>>     end.
>>
>>   Lemma sum_zero : forall a : nat, sum 0 a = a.
>
>
> I think the most obvious way is by first proving the following fact:
>
>  Lemma sum_S : forall a b : nat, sum a (S b) = S (sum a b).
>
> From this it is actually quite easy to prove sum_zero.
>
> cheers,
> Martijn
>
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06