The Coq mailing list

[anabelcesar <anabelcesar AT gmail.com>]

Thanks a lot, Julien.

Cesar

2009/3/30 Julien Forest <forest AT ensiie.fr>

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.