Library CoqInCoq.ListType

Require Import Arith.
Require Import MyList.

Section TListes.

Variable A : Type.

Inductive TList : Type :=
| TNl : TList
| TCs : ATListTList.

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

Inductive TIns (x : A) : natTListTListProp :=
| TIns_hd : l : TList, TIns x 0 l (TCs x l)
| TIns_tl :
(n : nat) (l il : TList) (y : A),
TIns x n l ilTIns 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 nTnth_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 > nTnth_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 gTnth_def d g k = x.
simple induction 1; simpl in |- *; auto with coc core arith datatypes.
Qed.

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

Hint Resolve Ttr_O Ttr_S: coc.

Fixpoint TList_iter (B : Type) (f : ABB)
(l : TList) {struct l} : BB :=
fun x : B
match l with
| TNlx
| TCs hd tlf hd (TList_iter _ f tl x)
end.

Inductive Tfor_all (P : AProp) : TListProp :=
| Tfa_nil : Tfor_all P TNl
| Tfa_cs :
(h : A) (t : TList),
P hTfor_all P tTfor_all P (TCs h t).

Inductive Tfor_all_fold (P : ATListProp) : TListProp :=
| Tfaf_nil : Tfor_all_fold P TNl
| Tfaf_cs :
(h : A) (t : TList),
P h tTfor_all_fold P tTfor_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 : AB) (l : TList A) {struct l} :
TList B :=
match l with
| TNlTNl B
| TCs t tlTCs _ (f t) (Tmap A B f tl)
end.

Fixpoint TSmap (A : Type) (B : Set) (f : AB)
(l : TList A) {struct l} : list B :=
match l with
| TNlnil (A:=B)
| TCs t tlf t :: TSmap A B f tl
end.

Inductive Tfor_all2 (A B : Type) (P : ABProp) :
TList ATList BProp :=
| 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 t2Tfor_all2 _ _ P (TCs _ h1 t1) (TCs _ h2 t2).

Hint Resolve Tfa2_nil Tfa2_cs: coc.