Library Lambda.ListType


Require
 Import
 Arith.

Require
 Import
 Lambda.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
).




  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
.




  Lemma
 Tins_eq :

   ∀ (k
 : nat) (f
 g
 : TList) (d
 x
 : A
),

   TIns x
 k
 f
 g
 → Tnth_def d
 g
 k
 = x
.




  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
.