MyList.v
Require Le.
Require Gt.
Require Export PolyList.
Require Export PolyListSyntax.
Section Listes.
Variable A:Set.
Local List:=(list A).
Inductive
In [x:A]: List->Prop :=
In_hd: (l:List)(In x (cons ? x l))
| In_tl: (y:A)(l:List) (In x l) -> (In x (cons ? y l)).
Hint In_hd In_tl.
Lemma
In_app: (x:A)(l1,l2:List)
(In x l1^l2)->(In x l1)\/(In x l2).
(Induction l1; Simpl; Intros;Auto).
(Inversion_clear H0; Auto).
(Elim H with l2; Auto).
Save.
Definition
incl: List->List->Prop :=
[l1,l2](x:A)(In x l1)->(In x l2).
Hint Unfold incl.
Lemma
incl_app_sym: (l1,l2:List)(incl l1^l2 l2^l1).
(Red; Intros).
(Elim In_app with x l1 l2; Intros; Auto).
(Elim l2; Simpl; Auto).
(Elim H0; Simpl; Auto).
Save.
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.
Definition
list_disjoint: List->List->Prop :=
[l1,l2](x:A)(In x l1)->(In x l2)->False.
Inductive
first_item [x:A]: List->nat->Prop :=
fit_hd: (l:List)(first_item x (cons ? x l) O)
| fit_tl: (l:List)(y:A)(n:nat) (first_item x l n) -> ~x=y
-> (first_item x (cons ? y l) (S n)).
Hint fit_hd fit_tl.
Lemma
first_item_is_item: (x:A)(l:List)(n:nat)(first_item x l n)
->(item x l n).
(Induction 1; Intros).
Apply item_hd.
(Apply item_tl; Trivial).
Save.
Lemma
first_item_unique: (x:A)(l:List)(n:nat)(first_item x l n)
-> (m:nat)(first_item x l m) -> m=n.
(Induction 1; Intros; Auto).
Inversion_clear H0;Auto.
(Elim H2; Auto).
Generalize H2 .
(Inversion_clear H3; Intros).
(Elim H3; Auto).
(Elim H1 with n1; Auto).
Save.
Hypothesis eq_dec: (x,y:A){x=y}+{~x=y}.
Lemma
list_index: (x:A)(l:List){n:nat| (first_item x l n)}+{~(In x l)}.
Realizer Fix list_index { list_index/2: A->List->(sumor nat) :=
[x:A][l:List]Cases l of
nil => (inright ?)
| (cons y l1) => if (eq_dec x y) then (inleft ? O) else
Cases (list_index x l1) of
(inleft k) => (inleft ? (S k))
| inright => (inright ?)
end
end}.
Program_all.
(Red; Intros).
Inversion H.
(Elim e; Auto).
(Red; Intros).
Apply n.
(Inversion_clear H; Auto).
(Elim n0; Auto).
Save.
End Listes.
Hint item_hd item_tl insert_hd insert_tl trunc_O trunc_S.
Hint In_hd In_tl fit_hd fit_tl trunc_O trunc_S.
Hint Unfold incl.
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.
13/02/97, 13:11