MyList.v
Require Le.
Require Gt.
Require Export PolyList.
Section Listes.
Variable A:Set.
Local List:=(list A).
Inductive
item [x:A]: List->nat->Prop :=
item_hd: (l:List)(item x (cons ? x l) O)
| item_tl: (l:List)(n:nat)(y:A)(item x l n)->(item x (cons ? y l) (S n)).
Lemma
fun_item: (u,v:A)(e:List)(n:nat)(item u e n)->(item v e n)->(u=v).
(Induction 1;Intros).
(Inversion_clear H0;Auto).
(Inversion_clear H2;Auto).
Save.
Fixpoint
nth_def [d:A; l:List]: nat->A :=
[n:nat]Cases l n of
nil _ => d
| (cons x _) O => x
| (cons _ tl) (S k) => (nth_def d tl k)
end.
Lemma
nth_sound: (x:A)(l:List)(n:nat)(item x l n)->(d:A)(nth_def d l n)=x.
(Induction 1;Simpl;Auto).
Save.
Lemma
inv_nth_nl: (x:A)(n:nat)~(item x (nil ?) n).
(Unfold not ;Intros).
Inversion_clear H.
Save.
Lemma
inv_nth_cs: (x,y:A)(l:List)(n:nat)(item x (cons ? y l) (S n))
->(item x l n).
Intros.
(Inversion_clear H;Auto).
Save.
Inductive
insert [x:A]: nat->List->List->Prop :=
insert_hd: (l:List)(insert x O l (cons ? x l))
| insert_tl: (n:nat)(l,il:List)(y:A)(insert x n l il)
->(insert x (S n) (cons ? y l) (cons ? y il)).
Inductive
trunc: nat->List->List->Prop :=
trunc_O: (e:List)(trunc O e e)
| trunc_S: (k:nat)(e,f:List)(x:A)(trunc k e f)
->(trunc (S k) (cons ? x e) f).
Hint trunc_O trunc_S.
Lemma
item_trunc: (n:nat)(e:List)(t:A)(item t e n)
->(Ex [f:List](trunc (S n) e f)).
(Induction n;Intros).
Inversion_clear H.
(Exists l;Auto).
Inversion_clear H0.
(Elim H with l t ;Intros;Auto).
(Exists x;Auto).
Save.
Lemma
ins_le: (k:nat)(f,g:List)(d,x:A)(insert x k f g)->(n:nat)(le k n)
->(nth_def d f n)=(nth_def d g (S n)).
(Induction 1;Auto).
(Destruct n0;Intros).
Inversion_clear H2.
Simpl.
Auto.
Save.
Lemma
ins_gt: (k:nat)(f,g:List)(d,x:A)(insert x k f g)->(n:nat)(gt k n)
->(nth_def d f n)=(nth_def d g n).
(Induction 1;Auto).
Intros.
Inversion_clear H0.
(Destruct n0;Intros).
Auto.
(Simpl;Auto).
Save.
Lemma
ins_eq: (k:nat)(f,g:List)(d,x:A)
(insert x k f g)->(nth_def d g k)=x.
(Induction 1;Simpl;Auto).
Save.
Lemma
list_item: (e:List)(n:nat) {t:A|(item t e n)}+{(t:A)~(item t e n)}.
Realizer [e:List]<nat->(sumor A)>Match e with
[_:nat](inright A)
[h:A][f:List][itemf:nat->(sumor A)][n:nat]<sumor A>Case n of
(inleft A h)
[k:nat]<sumor A>Case (itemf k) of
[u:A](inleft A u)
(inright A)
end
end
end.
Program_all.
(Red; Intros).
Inversion_clear H.
Apply item_hd.
(Apply item_tl; Auto).
(Red; Intros).
Inversion_clear H.
(Elim n1 with t; Auto).
Save.
End Listes.
Hint item_hd item_tl insert_hd insert_tl trunc_O trunc_S.
Fixpoint
map [A,B:Set;f:(A->B);l:(list A)]: (list B) :=
Cases l of
nil => (nil B)
| (cons x t) => (cons ? (f x) (map ? ? f t))
end.
06/11/96, 12:29