1 files changed, 0 insertions, 286 deletions
diff --git a/coqprime/Coqprime/UList.v b/coqprime/Coqprime/UList.v
deleted file mode 100644
index b787aad41..000000000
--- a/coqprime/Coqprime/UList.v
+++ /dev/null
@@ -1,286 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
-
-(***********************************************************************
-      UList.v
-
-      Definition of list with distinct elements
-
-      Definition: ulist
-************************************************************************)
-Require Import List.
-Require Import Arith.
-Require Import Permutation.
-Require Import ListSet.
-
-Section UniqueList.
-Variable A : Set.
-Variable eqA_dec : forall (a b : A),  ({ a = b }) + ({ a <> b }).
-(* A list is unique if there is not twice the same element in the list *)
-
-Inductive ulist : list A ->  Prop :=
-  ulist_nil: ulist nil
- | ulist_cons: forall a l, ~ In a l -> ulist l ->  ulist (a :: l) .
-Hint Constructors ulist .
-(* Inversion theorem *)
-
-Theorem ulist_inv: forall a l, ulist (a :: l) ->  ulist l.
-intros a l H; inversion H; auto.
-Qed.
-(* The append of two unique list is unique if the list are distinct *)
-
-Theorem ulist_app:
- forall l1 l2,
- ulist l1 ->
- ulist l2 -> (forall (a : A), In a l1 -> In a l2 ->  False) ->  ulist (l1 ++ l2).
-intros L1; elim L1; simpl; auto.
-intros a l H l2 H0 H1 H2; apply ulist_cons; simpl; auto.
-red; intros H3; case in_app_or with ( 1 := H3 ); auto; intros H4.
-inversion H0; auto.
-apply H2 with a; auto.
-apply H; auto.
-apply ulist_inv with ( 1 := H0 ); auto.
-intros a0 H3 H4; apply (H2 a0); auto.
-Qed.
-(* Iinversion theorem the appended list *)
-
-Theorem ulist_app_inv:
- forall l1 l2 (a : A), ulist (l1 ++ l2) -> In a l1 -> In a l2 ->  False.
-intros l1; elim l1; simpl; auto.
-intros a l H l2 a0 H0 [H1|H1] H2.
-inversion H0 as [|a1 l0 H3 H4 H5]; auto.
-case H3; rewrite H1; auto with datatypes.
-apply (H l2 a0); auto.
-apply ulist_inv with ( 1 := H0 ); auto.
-Qed.
-(* Iinversion theorem the appended list *)
-
-Theorem ulist_app_inv_l: forall (l1 l2 : list A), ulist (l1 ++ l2) ->  ulist l1.
-intros l1; elim l1; simpl; auto.
-intros a l H l2 H0.
-inversion H0 as [|il1 iH1 iH2 il2 [iH4 iH5]]; apply ulist_cons; auto.
-intros H5; case iH2; auto with datatypes.
-apply H with l2; auto.
-Qed.
-(* Iinversion theorem the appended list *)
-
-Theorem ulist_app_inv_r: forall (l1 l2 : list A), ulist (l1 ++ l2) ->  ulist l2.
-intros l1; elim l1; simpl; auto.
-intros a l H l2 H0; inversion H0; auto.
-Qed.
-(* Uniqueness is decidable *)
-
-Definition ulist_dec: forall l,  ({ ulist l }) + ({ ~ ulist l }).
-intros l; elim l; auto.
-intros a l1 [H|H]; auto.
-case (In_dec eqA_dec a l1); intros H2; auto.
-right; red; intros H1; inversion H1; auto.
-right; intros H1; case H; apply ulist_inv with ( 1 := H1 ).
-Defined.
-(* Uniqueness is compatible with permutation *)
-
-Theorem ulist_perm:
- forall (l1 l2 : list A), permutation l1 l2 -> ulist l1 ->  ulist l2.
-intros l1 l2 H; elim H; clear H l1 l2; simpl; auto.
-intros a l1 l2 H0 H1 H2; apply ulist_cons; auto.
-inversion_clear H2 as [|ia il iH1 iH2 [iH3 iH4]]; auto.
-intros H3; case iH1;
- apply permutation_in with ( 1 := permutation_sym _ _ _ H0 ); auto.
-inversion H2; auto.
-intros a b L H0; apply ulist_cons; auto.
-inversion_clear H0 as [|ia il iH1 iH2]; auto.
-inversion_clear iH2 as [|ia il iH3 iH4]; auto.
-intros H; case H; auto.
-intros H1; case iH1; rewrite H1; simpl; auto.
-apply ulist_cons; auto.
-inversion_clear H0 as [|ia il iH1 iH2]; auto.
-intros H; case iH1; simpl; auto.
-inversion_clear H0 as [|ia il iH1 iH2]; auto.
-inversion iH2; auto.
-Qed.
-
-Theorem ulist_def:
- forall l a,
- In a l -> ulist l ->  ~ (exists l1 , permutation l (a :: (a :: l1)) ).
-intros l a H H0 [l1 H1].
-absurd (ulist (a :: (a :: l1))); auto.
-intros H2; inversion_clear H2; simpl; auto with datatypes.
-apply ulist_perm with ( 1 := H1 ); auto.
-Qed.
-
-Theorem ulist_incl_permutation:
- forall (l1 l2 : list A),
- ulist l1 -> incl l1 l2 ->  (exists l3 , permutation l2 (l1 ++ l3) ).
-intros l1; elim l1; simpl; auto.
-intros l2 H H0; exists l2; simpl; auto.
-intros a l H l2 H0 H1; auto.
-case (in_permutation_ex _ a l2); auto with datatypes.
-intros l3 Hl3.
-case (H l3); auto.
-apply ulist_inv with ( 1 := H0 ); auto.
-intros b Hb.
-assert (H2: In b (a :: l3)).
-apply permutation_in with ( 1 := permutation_sym _ _ _ Hl3 );
- auto with datatypes.
-simpl in H2 |-; case H2; intros H3; simpl; auto.
-inversion_clear H0 as [|c lc Hk1]; auto.
-case Hk1; subst a; auto.
-intros l4 H4; exists l4.
-apply permutation_trans with (a :: l3); auto.
-apply permutation_sym; auto.
-Qed.
-
-Theorem ulist_eq_permutation:
- forall (l1 l2 : list A),
- ulist l1 -> incl l1 l2 -> length l1 = length l2 ->  permutation l1 l2.
-intros l1 l2 H1 H2 H3.
-case (ulist_incl_permutation l1 l2); auto.
-intros l3 H4.
-assert (H5: l3 = @nil A).
-generalize (permutation_length _ _ _ H4); rewrite length_app; rewrite H3.
-rewrite plus_comm; case l3; simpl; auto.
-intros a l H5; absurd (lt (length l2) (length l2)); auto with arith.
-pattern (length l2) at 2; rewrite H5; auto with arith.
-replace l1 with (app l1 l3); auto.
-apply permutation_sym; auto.
-rewrite H5; rewrite app_nil_end; auto.
-Qed.
-
-
-Theorem ulist_incl_length:
- forall (l1 l2 : list A), ulist l1 -> incl l1 l2 ->  le (length l1) (length l2).
-intros l1 l2 H1 Hi; case ulist_incl_permutation with ( 2 := Hi ); auto.
-intros l3 Hl3; rewrite permutation_length with ( 1 := Hl3 ); auto.
-rewrite length_app; simpl; auto with arith.
-Qed.
-
-Theorem ulist_incl2_permutation:
- forall (l1 l2 : list A),
- ulist l1 -> ulist l2 -> incl l1 l2 -> incl l2 l1  ->  permutation l1 l2.
-intros l1 l2 H1 H2 H3 H4.
-apply ulist_eq_permutation; auto.
-apply le_antisym; apply ulist_incl_length; auto.
-Qed.
-
-
-Theorem ulist_incl_length_strict:
- forall (l1 l2 : list A),
- ulist l1 -> incl l1 l2 -> ~ incl l2 l1 ->  lt (length l1) (length l2).
-intros l1 l2 H1 Hi Hi0; case ulist_incl_permutation with ( 2 := Hi ); auto.
-intros l3 Hl3; rewrite permutation_length with ( 1 := Hl3 ); auto.
-rewrite length_app; simpl; auto with arith.
-generalize Hl3; case l3; simpl; auto with arith.
-rewrite <- app_nil_end; auto.
-intros H2; case Hi0; auto.
-intros a HH; apply permutation_in with ( 1 := H2 ); auto.
-intros a l Hl0; (rewrite plus_comm; simpl; rewrite plus_comm; auto with arith).
-Qed.
-
-Theorem in_inv_dec:
- forall (a b : A) l, In a (cons b l) ->  a = b \/ ~ a = b /\ In a l.
-intros a b l H; case (eqA_dec a b); auto; intros H1.
-right; split; auto; inversion H; auto.
-case H1; auto.
-Qed.
-
-Theorem in_ex_app_first:
- forall (a : A) (l : list A),
- In a l ->
-  (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2) /\ ~ In a l1  ).
-intros a l; elim l; clear l; auto.
-intros H; case H.
-intros a1 l H H1; auto.
-generalize (in_inv_dec _ _ _ H1); intros [H2|[H2 H3]].
-exists (nil (A:=A)); exists l; simpl; split; auto.
-subst; auto.
-case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl;
- split; auto.
-subst; auto.
-intros H4; case H4; auto.
-Qed.
-
-Theorem ulist_inv_ulist:
- forall (l : list A),
- ~ ulist l ->
-  (exists a ,
-   exists l1 ,
-   exists l2 ,
-   exists l3 , l = l1 ++ ((a :: l2) ++ (a :: l3)) /\ ulist (l1 ++ (a :: l2))    ).
-intros l; elim l  using list_length_ind; clear l.
-intros l; case l; simpl; auto; clear l.
-intros Rec H0; case H0; auto.
-intros a l H H0.
-case (In_dec eqA_dec a l); intros H1; auto.
-case in_ex_app_first with ( 1 := H1 ); intros l1 [l2 [Hl1 Hl2]]; subst l.
-case (ulist_dec l1); intros H2.
-exists a; exists (@nil A); exists l1; exists l2; split; auto.
-simpl; apply ulist_cons; auto.
-case (H l1); auto.
-rewrite length_app; auto with arith.
-intros b [l3 [l4 [l5 [Hl3 Hl4]]]]; subst l1.
-exists b; exists (a :: l3); exists l4; exists (l5 ++ (a :: l2)); split; simpl;
- auto.
-(repeat (rewrite <- ass_app; simpl)); auto.
-apply ulist_cons; auto.
-contradict Hl2; auto.
-replace (l3 ++ (b :: (l4 ++ (b :: l5)))) with ((l3 ++ (b :: l4)) ++ (b :: l5));
- auto with datatypes.
-(repeat (rewrite <- ass_app; simpl)); auto.
-case (H l); auto; intros a1 [l1 [l2 [l3 [Hl3 Hl4]]]]; subst l.
-exists a1; exists (a :: l1); exists l2; exists l3; split; auto.
-simpl; apply ulist_cons; auto.
-contradict H1.
-replace (l1 ++ (a1 :: (l2 ++ (a1 :: l3))))
-     with ((l1 ++ (a1 :: l2)) ++ (a1 :: l3)); auto with datatypes.
-(repeat (rewrite <- ass_app; simpl)); auto.
-Qed.
-
-Theorem incl_length_repetition:
- forall (l1 l2 : list A),
- incl l1 l2 ->
- lt (length l2) (length l1) ->
-  (exists a ,
-   exists ll1 ,
-   exists ll2 ,
-   exists ll3 ,
-   l1 = ll1 ++ ((a :: ll2) ++ (a :: ll3)) /\ ulist (ll1 ++ (a :: ll2))    ).
-intros l1 l2 H H0; apply ulist_inv_ulist.
-intros H1; absurd (le (length l1) (length l2)); auto with arith.
-apply ulist_incl_length; auto.
-Qed.
-
-End UniqueList.
-Arguments ulist [A].
-Hint Constructors ulist .
-
-Theorem ulist_map:
- forall (A B : Set) (f : A ->  B) l,
- (forall x y, (In x l) -> (In y l) ->  f x = f y ->  x = y) -> ulist l ->  ulist (map f l).
-intros a b f l Hf Hl; generalize Hf; elim Hl; clear Hf;  auto.
-simpl; auto.
-intros a1 l1 H1 H2 H3 Hf; simpl.
-apply ulist_cons; auto with datatypes.
-contradict H1.
-case in_map_inv with ( 1 := H1 ); auto with datatypes.
-intros b1 [Hb1 Hb2].
-replace a1 with b1; auto with datatypes.
-Qed.
-
-Theorem ulist_list_prod:
- forall (A : Set) (l1 l2 : list A),
- ulist l1 -> ulist l2 ->  ulist (list_prod l1 l2).
-intros A l1 l2 Hl1 Hl2; elim Hl1; simpl; auto.
-intros a l H1 H2 H3; apply ulist_app; auto.
-apply ulist_map; auto.
-intros x y _ _ H; inversion H; auto.
-intros p Hp1 Hp2; case H1.
-case in_map_inv with ( 1 := Hp1 ); intros a1 [Ha1 Ha2]; auto.
-case in_list_prod_inv with ( 1 := Hp2 ); intros b1 [c1 [Hb1 [Hb2 Hb3]]]; auto.
-replace a with b1; auto.
-rewrite Ha2 in Hb1; injection Hb1; auto.
-Qed.