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