Library MyList

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

Set Implicit Arguments.
Unset Strict Implicit.

Section Listes.

  Variable A : Set.

  Let List := list A.

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

  Lemma fun_item : ∀ u v e n, item u e n -> item v e n -> u = v.
simple induction 1; intros.
inversion_clear H0; auto.

inversion_clear H2; auto.
Qed.

  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 : ∀ x l n d, item x l n -> nth_def d l n = x.
simple induction 1; simpl in |- *; auto.
Qed.

  Lemma inv_nth_nl : ∀ x n, ~ item x nil n.
unfold not in |- *; intros.
inversion_clear H.
Qed.

  Lemma inv_nth_cs : ∀ x y l n, item x (y :: l) (S n) -> item x l n.
intros.
inversion_clear H; auto.
Qed.

  Inductive insert (x : A) : nat -> List -> List -> Prop :=
    | insert_hd : ∀ l, insert x 0 l (x :: l)
    | insert_tl :
        ∀ 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 : ∀ e, trunc 0 e e
    | trunc_S : ∀ k e f x, trunc k e f -> trunc (S k) (x :: e) f.

  Hint Constructors trunc: core.

  Lemma item_trunc :
   ∀ n e t, item t e n -> exists f : _, trunc (S n) e f.
simple induction n; intros.
inversion_clear H.
exists l; auto.

inversion_clear H0.
elim H with l t; intros; auto.
exists x; auto.
Qed.

  Lemma ins_le :
   ∀ k f g d x,
   insert x k f g -> ∀ n, k <= n -> nth_def d f n = nth_def d g (S n).
simple induction 1; auto.
simple destruct n0; intros.
inversion_clear H2.

simpl in |- *; auto with arith.
Qed.

  Lemma ins_gt :
   ∀ k f g d x,
   insert x k f g -> ∀ n, k > n -> nth_def d f n = nth_def d g n.
simple induction 1; auto.
intros.
inversion_clear H0.

simple destruct n0; intros.
auto.

simpl in |- *; auto with arith.
Qed.

  Lemma ins_eq : ∀ k f g d x, insert x k f g -> nth_def d g k = x.
simple induction 1; simpl in |- *; auto.
Qed.

  Lemma list_item :
   ∀ e n, {t : _ | item t e n} + {∀ t, ~ item t e n}.
fix itemrec 1.
intros e n.
case e; [ idtac | intros h f ].
right.
red in |- *; intros.
inversion_clear H.

case n; [ idtac | intros k ].
left.
exists h.
apply item_hd.

elim (itemrec f k).
intros (t, itm_t).
left; exists t.
apply item_tl; auto.

intros not_itm.
right; red in |- *; intros.
elim not_itm with t.
inversion H; trivial.
Defined.

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.