The Coq mailing list

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

To rebound on Julien's reply, just a more general remark : it is
almost always harder to reason about tail-recursive functions because
you need to manually introduce the adequate invariant on the
accumulator  (in that case, the function F) in your induction
principles.

For instance, to prove your lemma, you could have proven the following
(more general) result by induction on n, by adding a property on F :
Lemma for_aa : forall (n nf : nat) (F : nat -> Set),
  (forall m, m < nf -> F m = unit) ->
  forall m, m <= n+nf -> iterated_unit_ext F n m = unit.

A good way to proceed is Julien's : start by writing a lemma showing
that your function is equal to the non tail-recursive version you
could have written. Then use this lemma to rewrite instead of using
conversion.
I just wanted to emphasize that you can use Julien's solution in many
cases since it is more general that it may look.

--
Stephane L.

On Mon, Mar 30, 2009 at 1:59 PM, Julien Forest 
<forest AT ensiie.fr>
 wrote:
> On Mon, 30 Mar 2009 13:26:51 +0200
> anabelcesar 
>Â <anabelcesar AT gmail.com>
>  wrote:
>
>> Dear Coq users,
>>
>> I am working with families of sets F:nat -> Set and I need to
>> extend them using a particular set as the first set of the family.
>> In the example below, I use "unit".
>>
>> Then, If we iterate the construction n times, the n first sets should be
>> unit
>> (and in particular the set n in the family). But I do not know how to prove
>> this
>> (probably easy) Lemma.
>>
>> Any help is appreciated.
>>
>> Cesar
>>
>>
>> -----------------------------------------------------------------
>> Section Function_extension.
>>
>> Variable F:nat-> Set.
>>
>>
>> Definition unit_ext: nat -> Set:=
>> fun n : nat => match n with
>>                | 0 => unit
>>                | S n0 => F n0
>>                end.
>> End Function_extension.
>>
>> Fixpoint iterated_unit_ext ( F:nat-> Set)(n:nat){struct n}:=
>>  match n with
>>                | 0 => unit_ext F
>>                | S n => iterated_unit_ext (unit_ext F) n
>>                end.
>>
>> Lemma aa:forall (n:nat) (F:nat -> Set), iterated_unit_ext  F  n n  = unit.
>> Proof.
>>
>> ------------------------------------------------------------------
> Hi,
> the trick is to prove first that:
> Lemma lem1 : forall n m F, iterated_unit_ext F (S n) m = unit_ext 
> (iterated_unit_ext F n) m.
>
> .......
>
> Section Function_extension.
>
> Variable F:nat-> Set.
>
>
> Definition unit_ext: nat -> Set:=
> fun n : nat => match n with
>               | 0 => unit
>               | S n0 => F n0
>               end.
> End Function_extension.
>
> Fixpoint iterated_unit_ext ( F:nat-> Set)(n:nat){struct n}:=
>  match n with
>    | 0 => unit_ext F
>    | S n => iterated_unit_ext (unit_ext F) n
>  end.
>
>
> Lemma lem1 : forall n m F, iterated_unit_ext F (S n) m = unit_ext
> (iterated_unit_ext F n) m. Proof.
> induction n as [|n].
> simpl;reflexivity.
> simpl.
> intros.
> rewrite <- IHn. simpl;reflexivity.
> Qed.
>
> Lemma aa:forall (n:nat) (F:nat -> Set), iterated_unit_ext  F  n n  = unit.
> Proof.
>  induction n as [|n].
>  simpl. reflexivity.
>  intros.
>  rewrite lem2.
>  simpl.
>  auto.
> Qed.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



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