MyLogicType.v

Require MyList.


  Inductive ORT [A,B:Type]: Type :=
     LeftT: A->(ORT A B)
   | RightT: B->(ORT A B).


Section TListes.

  Variable A: Type.

  Inductive TList: Type :=
      TNl: TList
    | TCs: A->TList->TList.


  Fixpoint Tnth_def [d:A; l:TList]: nat->A :=
    [n:nat]Cases l n of
         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 O 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 TIns_hd TIns_tl.

  Lemma Tins_le: (k:nat)(f,g:TList)(d,x:A)(TIns x k f g)->(n:nat)(le k n)
         ->(Tnth_def d f n)==(Tnth_def d g (S n)).
(Induction 1;Auto).
(Destruct n0;Intros).
Inversion_clear H2.

Simpl.
Auto.
Save.

  Lemma Tins_gt: (k:nat)(f,g:TList)(d,x:A)(TIns x k f g)->(n:nat)(gt k n)
              ->(Tnth_def d f n)==(Tnth_def d g n).
(Induction 1;Auto).
Intros.
Inversion_clear H0.

(Destruct n0;Intros).
Auto.

(Simpl;Auto).
Save.

  Lemma Tins_eq: (k:nat)(f,g:TList)(d,x:A)
             (TIns x k f g)->(Tnth_def d g k)==x.
(Induction 1;Simpl;Auto).
Save.


  Inductive TTrunc: nat->TList->TList->Prop :=
     Ttr_O: (e:TList)(TTrunc O e e)
   | Ttr_S: (k:nat)(e,f:TList)(x:A)(TTrunc k e f)
                                      ->(TTrunc (S k) (TCs x e) f).

  Hint Ttr_O Ttr_S.

  Fixpoint TList_iter [B:Type; f:A->B->B; l:TList]: B->B :=
    [x:B]Cases l of
           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 TIns_hd TIns_tl Ttr_O Ttr_S.
  Hint Tfa_nil Tfa_cs Tfaf_nil Tfaf_cs.

  Fixpoint Tmap [A,B:Type; f:A->B; l:(TList A)]: (TList B) :=
    Cases l of
      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)]: (list B) :=
    Cases l of
      TNl => (nil B)
    | (TCs t tl) => (cons ? (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 Tfa2_nil Tfa2_cs.
13/02/97, 13:21