MyList.v

Implicit Arguments On.

Require Export PolyList.

Section Listes.

  Variable A:Set.

  Local List:=(list A).

  Inductive item [x:A]: List->nat->Prop :=
      item_hd: (l:List)(item x (cons x l) O)
    | item_tl: (l:List)(n:nat)(y:A)(item x l n)->(item x (cons y l) (S n)).

  Lemma fun_item: (u,v:A)(e:List)(n:nat)(item u e n)->(item v e n)-> u=v.
Proof.
(Induction 1;Intros).
(Inversion_clear H0;Auto).

(Inversion_clear H2;Auto).
Save.

  Lemma list_item: (e:List)(n:nat) {t:A|(item t e n)}+{(t:A)~(item t e n)}.
Realizer Fix item_rec { item_rec/1: List->nat->(sumor A) :=
  [e,n]Cases e n of
     (cons _ l) (S k) => (item_rec l k)
   | (cons h _) _ => (inleft ? h)
   | nil _ => (inright A)
   end}.
Program_all.
(Red; Intros).
Inversion H.

Apply item_hd.

(Apply item_tl; Trivial).

(Red; Intros).
Inversion_clear H.
(Elim n0 with t; Trivial).
Save.

  Inductive trunc: nat->List->List->Prop :=
     trunc_O: (e:List)(trunc O e e)
   | trunc_S: (k:nat)(e,f:List)(x:A)(trunc k e f)
                ->(trunc (S k) (cons x e) f).

  Lemma item_trunc: (n:nat)(e:List)(t:A)(item t e n)
            ->(EX f:List | (trunc (S n) e f)).
Proof.
(Induction n; Intros).
Inversion_clear H.
Exists l.
Apply trunc_S.
Apply trunc_O.

Inversion_clear H0.
(Elim H with l t; Intros).
Exists x.
Apply trunc_S.
Trivial.

Trivial.
Save.

End Listes.

  Hints Resolve item_hd item_tl trunc_O trunc_S : core.

23/12/98, 14:33