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