MyList.v


Require Le.
Require Gt.
Require Export PolyList.
Require Export PolyListSyntax.

Section Listes.

  Variable A:Set.

  Local List:=(list A).


  Inductive In [x:A]: List->Prop :=
    In_hd: (l:List)(
In x (cons ? x l))
  | In_tl: (y:A)(l:List) (In x l) -> (In x (cons ? y l)).

  Hint In_hd In_tl.


  Lemma In_app: (x:A)(l1,l2:List)
                      (
In x l1^l2)->(In x l1)\/(In x l2).
(Induction l1; Simpl; Intros;Auto).

(Inversion_clear H0; Auto).
(Elim H with l2; Auto).
Save.


  Definition incl: List->List->Prop :=
              [l1,l2](x:A)(
In x l1)->(In x l2).

  Hint Unfold incl.


  Lemma incl_app_sym: (l1,l2:List)(incl l1^l2 l2^l1).
(Red; Intros).
(Elim In_app with x l1 l2; Intros; Auto).
(Elim l2; Simpl; Auto).

(Elim H0; Simpl; Auto).
Save.


  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).
(Induction 1;Intros).
(Inversion_clear H0;Auto).

(Inversion_clear H2;Auto).
Save.


  Fixpoint nth_def [d:A; l:List]: nat->A :=
    [n:nat]Cases l n of
         nil _ => d
       | (cons x _) O => x
       | (cons _ tl) (S k) => (
nth_def d tl k)
       end.

  Lemma nth_sound: (x:A)(l:List)(n:nat)(item x l n)->(d:A)(nth_def d l n)=x.
(Induction 1;Simpl;Auto).
Save.

  Lemma inv_nth_nl: (x:A)(n:nat)~(item x (nil ?) n).
(Unfold not ;Intros).
Inversion_clear H.
Save.

  Lemma inv_nth_cs: (x,y:A)(l:List)(n:nat)(item x (cons ? y l) (S n))
                          ->(item x l n).
Intros.
(Inversion_clear H;Auto).
Save.

  Inductive insert [x:A]: nat->List->List->Prop :=
      insert_hd: (l:List)(
insert x O l (cons ? x l))
    | insert_tl: (n:nat)(l,il:List)(y:A)(insert x n l il)
                    ->(insert x (S n) (cons ? y l) (cons ? y il)).


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

  Hint trunc_O trunc_S.


  Lemma item_trunc: (n:nat)(e:List)(t:A)(item t e n)
            ->(Ex [f:List](trunc (S n) e f)).
(Induction n;Intros).
Inversion_clear H.
(Exists l;Auto).

Inversion_clear H0.
(Elim H with l t ;Intros;Auto).
(Exists x;Auto).
Save.


  Lemma ins_le: (k:nat)(f,g:List)(d,x:A)(insert x k f g)->(n:nat)(le k n)
         ->(nth_def d f n)=(nth_def d g (S n)).
(Induction 1;Auto).
(Destruct n0;Intros).
Inversion_clear H2.

Simpl.
Auto.
Save.

  Lemma ins_gt: (k:nat)(f,g:List)(d,x:A)(insert x k f g)->(n:nat)(gt k n)
              ->(nth_def d f n)=(nth_def d g n).
(Induction 1;Auto).
Intros.
Inversion_clear H0.

(Destruct n0;Intros).
Auto.

(Simpl;Auto).
Save.

  Lemma ins_eq: (k:nat)(f,g:List)(d,x:A)
             (
insert x k f g)->(nth_def d g k)=x.
(Induction 1;Simpl;Auto).
Save.




  Lemma list_item: (e:List)(n:nat) {t:A|(item t e n)}+{(t:A)~(item t e n)}.
Realizer [e:List]<nat->(sumor A)>Match e with
     [_:nat](inright A)
     [h:A][f:List][itemf:nat->(sumor A)][n:nat]<sumor A>Case n of
          (inleft A h)
          [k:nat]<sumor A>Case (itemf k) of
                [u:A](inleft A u)
                (inright A)
                end
          end
     end.
Program_all.
(Red; Intros).
Inversion_clear H.

Apply item_hd.

(Apply item_tl; Auto).

(Red; Intros).
Inversion_clear H.
(Elim n1 with t; Auto).
Save.


  Definition list_disjoint: List->List->Prop :=
      [l1,l2](x:A)(
In x l1)->(In x l2)->False.




  Inductive first_item [x:A]: List->nat->Prop :=
    fit_hd: (l:List)(
first_item x (cons ? x l) O)
  | fit_tl: (l:List)(y:A)(n:nat) (first_item x l n) -> ~x=y
                                      -> (first_item x (cons ? y l) (S n)).

  Hint fit_hd fit_tl.

  Lemma first_item_is_item: (x:A)(l:List)(n:nat)(first_item x l n)
                                  ->(item x l n).
(Induction 1; Intros).
Apply item_hd.

(Apply item_tl; Trivial).
Save.

  Lemma first_item_unique: (x:A)(l:List)(n:nat)(first_item x l n)
                                           -> (m:nat)(first_item x l m) -> m=n.
(Induction 1; Intros; Auto).
Inversion_clear H0;Auto.

(Elim H2; Auto).

Generalize H2 .
(Inversion_clear H3; Intros).
(Elim H3; Auto).

(Elim H1 with n1; Auto).
Save.



  Hypothesis eq_dec: (x,y:A){x=y}+{~x=y}.

  Lemma list_index: (x:A)(l:List){n:nat| (first_item x l n)}+{~(In x l)}.
Realizer Fix list_index { list_index/2: A->List->(sumor nat) :=
  [x:A][l:List]Cases l of
    nil => (inright ?)
  | (cons y l1) => if (eq_dec x y) then (inleft ? O) else
           Cases (list_index x l1) of
             (inleft k) => (inleft ? (S k))
           | inright => (inright ?)
           end
  end}.
Program_all.
(Red; Intros).
Inversion H.

(Elim e; Auto).

(Red; Intros).
Apply n.
(Inversion_clear H; Auto).
(Elim n0; Auto).
Save.

End Listes.

  Hint item_hd item_tl insert_hd insert_tl trunc_O trunc_S.
  Hint In_hd In_tl fit_hd fit_tl trunc_O trunc_S.
  Hint Unfold incl.


  Fixpoint map [A,B:Set;f:(A->B);l:(list A)]: (list B) :=
      Cases l of
        nil => (nil B)
      | (cons x t) => (cons ? (f x) (
map ? ? f t))
      end.




13/02/97, 13:11