Library MyList

Require Import Le.
Require Import Gt.
Require Export List.


Section Listes.

  Variable A : Set.

  Let List := list A.

  Inductive item (x : A) : List -> nat -> Prop :=
    | item_hd : forall l, item x (x :: l) 0
    | item_tl : forall l n y, item x l n -> item x (y :: l) (S n).

  Lemma fun_item : forall u v e n, item u e n -> item v e n -> u = v.

  Fixpoint nth_def (d : A) (l : List) (n : nat) {struct l} : A :=
    match l, n with
    | nil, _ => d
    | x :: _, O => x
    | _ :: tl, S k => nth_def d tl k
    end.

  Lemma nth_sound : forall x l n d, item x l n -> nth_def d l n = x.

  Lemma inv_nth_nl : forall x n, ~ item x nil n.

  Lemma inv_nth_cs : forall x y l n, item x (y :: l) (S n) -> item x l n.

  Inductive insert (x : A) : nat -> List -> List -> Prop :=
    | insert_hd : forall l, insert x 0 l (x :: l)
    | insert_tl :
        forall n l il y, insert x n l il -> insert x (S n) (y :: l) (y :: il).

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

  Hint Constructors trunc: core.

  Lemma item_trunc :
   forall n e t, item t e n -> exists f : _, trunc (S n) e f.

  Lemma ins_le :
   forall k f g d x,
   insert x k f g -> forall n, k <= n -> nth_def d f n = nth_def d g (S n).

  Lemma ins_gt :
   forall k f g d x,
   insert x k f g -> forall n, k > n -> nth_def d f n = nth_def d g n.

  Lemma ins_eq : forall k f g d x, insert x k f g -> nth_def d g k = x.

  Lemma list_item :
   forall e n, {t : _ | item t e n} + {forall t, ~ item t e n}.

End Listes.

  Hint Constructors item: core.
  Hint Constructors insert: core.
  Hint Constructors trunc: core.

  Fixpoint map (A B : Set) (f : A -> B) (l : list A) {struct l} : list B :=
    match l with
    | nil => nil (A:=B)
    | x :: t => f x :: map f t
    end.