The Coq mailing list

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