Require Import Arith.
Require Import MyList.

Section TListes.

  Variable A : Type.

  Inductive TList : Type :=
    | TNl : TList
    | TCs : A → TList → TList.

  Fixpoint Tnth_def (d : A) (l : TList) {struct l} :
   nat → A :=
    fun n : nat ⇒
    match l, n with
    | TNl, _ ⇒ d
    | TCs x _, O ⇒ x
    | TCs _ tl, S k ⇒ Tnth_def d tl k
    end.

  Inductive TIns (x : A) : nat → TList → TList → Prop :=
    | TIns_hd : ∀ l : TList, TIns x 0 l (TCs x l)
    | TIns_tl :
        ∀ (n : nat) (l il : TList) (y : A),
        TIns x n l il → TIns x (S n) (TCs y l) (TCs y il).

  Hint Resolve TIns_hd TIns_tl: coc.

  Lemma Tins_le :
   ∀ (k : nat) (f g : TList) (d x : A),
   TIns x k f g →
   ∀ n : nat, k ≤ n → Tnth_def d f n = Tnth_def d g (S n).
simple induction 1; auto with coc core arith datatypes.
simple destruct n0; intros.
inversion H2.

simpl in |- *; auto with coc core arith datatypes.
Qed.

  Lemma Tins_gt :
   ∀ (k : nat) (f g : TList) (d x : A),
   TIns x k f g → ∀ n : nat, k > n → Tnth_def d f n = Tnth_def d g n.
simple induction 1; auto with coc core arith datatypes.
intros.
inversion_clear H0.

simple destruct n0; intros.
auto with coc core arith datatypes.

simpl in |- *; auto with coc core arith datatypes.
Qed.

  Lemma Tins_eq :
   ∀ (k : nat) (f g : TList) (d x : A),
   TIns x k f g → Tnth_def d g k = x.
simple induction 1; simpl in |- *; auto with coc core arith datatypes.
Qed.

  Inductive TTrunc : nat → TList → TList → Prop :=
    | Ttr_O : ∀ e : TList, TTrunc 0 e e
    | Ttr_S :
        ∀ (k : nat) (e f : TList) (x : A),
        TTrunc k e f → TTrunc (S k) (TCs x e) f.

  Hint Resolve Ttr_O Ttr_S: coc.

  Fixpoint TList_iter (B : Type) (f : A → B → B)
   (l : TList) {struct l} : B → B :=
    fun x : B ⇒
    match l with
    | TNl ⇒ x
    | TCs hd tl ⇒ f hd (TList_iter _ f tl x)
    end.

  Inductive Tfor_all (P : A → Prop) : TList → Prop :=
    | Tfa_nil : Tfor_all P TNl
    | Tfa_cs :
        ∀ (h : A) (t : TList),
        P h → Tfor_all P t → Tfor_all P (TCs h t).

  Inductive Tfor_all_fold (P : A → TList → Prop) : TList → Prop :=
    | Tfaf_nil : Tfor_all_fold P TNl
    | Tfaf_cs :
        ∀ (h : A) (t : TList),
        P h t → Tfor_all_fold P t → Tfor_all_fold P (TCs h t).

End TListes.

  Hint Resolve TIns_hd TIns_tl Ttr_O Ttr_S: coc.
  Hint Resolve Tfa_nil Tfa_cs Tfaf_nil Tfaf_cs: coc.

  Fixpoint Tmap (A B : Type) (f : A → B) (l : TList A) {struct l} :
   TList B :=
    match l with
    | TNl ⇒ TNl B
    | TCs t tl ⇒ TCs _ (f t) (Tmap A B f tl)
    end.

  Fixpoint TSmap (A : Type) (B : Set) (f : A → B)
   (l : TList A) {struct l} : list B :=
    match l with
    | TNl ⇒ nil (A:=B)
    | TCs t tl ⇒ f t :: TSmap A B f tl
    end.

  Inductive Tfor_all2 (A B : Type) (P : A → B → Prop) :
  TList A → TList B → Prop :=
    | Tfa2_nil : Tfor_all2 _ _ P (TNl _) (TNl _)
    | Tfa2_cs :
        ∀ (h1 : A) (h2 : B) (t1 : TList A) (t2 : TList B),
        P h1 h2 →
        Tfor_all2 _ _ P t1 t2 → Tfor_all2 _ _ P (TCs _ h1 t1) (TCs _ h2 t2).

  Hint Resolve Tfa2_nil Tfa2_cs: coc.