Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 199 insertions, 116 deletions

diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index ca86ffcc..f6205542 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FSetList.v 8667 2006-03-28 11:59:44Z letouzey $ *)
+(* $Id: FSetList.v 8834 2006-05-20 00:41:35Z letouzey $ *)
 
 (** * Finite sets library *)
 
@@ -199,6 +199,8 @@ Module Raw (X: OrderedType).
 
   (** ** Proofs of set operation specifications. *)
 
+  Section ForNotations.
+
   Notation Sort := (sort X.lt).
   Notation Inf := (lelistA X.lt).
   Notation In := (InA X.eq).
@@ -1020,6 +1022,9 @@ Module Raw (X: OrderedType).
   destruct (e1 a0); auto.
   Defined.
 
+  End ForNotations. 
+  Hint Constructors lt.
+
 End Raw.
 
 (** * Encapsulation
@@ -1029,135 +1034,213 @@ End Raw.
 
 Module Make (X: OrderedType) <: S with Module E := X.
 
- Module E := X.
  Module Raw := Raw X. 
+ Module E := X.
 
- Record slist : Set :=  {this :> Raw.t; sorted : sort X.lt this}.
+ Record slist : Set :=  {this :> Raw.t; sorted : sort E.lt this}.
  Definition t := slist. 
- Definition elt := X.t.
+ Definition elt := E.t.
  
- Definition In (x : elt) (s : t) := InA X.eq x s.(this).
- Definition Equal s s' := forall a : elt, In a s <-> In a s'.
- Definition Subset s s' := forall a : elt, In a s -> In a s'.
- Definition Empty s := forall a : elt, ~ In a s.
- Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
- Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
-  
- Definition In_1 (s : t) := Raw.MX.In_eq (l:=s.(this)).
- 
- Definition mem (x : elt) (s : t) := Raw.mem x s.
- Definition mem_1 (s : t) := Raw.mem_1 (sorted s). 
- Definition mem_2 (s : t) := Raw.mem_2 (s:=s).
-
- Definition add x s := Build_slist (Raw.add_sort (sorted s) x).
- Definition add_1 (s : t) := Raw.add_1 (sorted s).
- Definition add_2 (s : t) := Raw.add_2 (sorted s).
- Definition add_3 (s : t) := Raw.add_3 (sorted s).
-
- Definition remove x s := Build_slist (Raw.remove_sort (sorted s) x).
- Definition remove_1 (s : t) := Raw.remove_1 (sorted s).
- Definition remove_2 (s : t) := Raw.remove_2 (sorted s).
- Definition remove_3 (s : t) := Raw.remove_3 (sorted s).
- 
- Definition singleton x := Build_slist (Raw.singleton_sort x).
- Definition singleton_1 := Raw.singleton_1.
- Definition singleton_2 := Raw.singleton_2.
-  
- Definition union (s s' : t) :=
+ Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this).
+ Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
+ Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
+ Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
+ Definition For_all (P : elt -> Prop)(s:t) : Prop := forall x, In x s -> P x.
+ Definition Exists (P : elt -> Prop)(s:t) : Prop := exists x, In x s /\ P x.
+
+ Definition mem (x : elt) (s : t) : bool := Raw.mem x s.
+ Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_sort (sorted s) x).
+ Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_sort (sorted s) x).
+ Definition singleton (x : elt) : t  := Build_slist (Raw.singleton_sort x).
+ Definition union (s s' : t) : t :=
    Build_slist (Raw.union_sort (sorted s) (sorted s')). 
- Definition union_1 (s s' : t) := Raw.union_1 (sorted s) (sorted s').
- Definition union_2 (s s' : t) := Raw.union_2 (sorted s) (sorted s').
- Definition union_3 (s s' : t) := Raw.union_3 (sorted s) (sorted s').
-
- Definition inter (s s' : t) :=
+ Definition inter (s s' : t) : t :=
    Build_slist (Raw.inter_sort (sorted s) (sorted s')). 
- Definition inter_1 (s s' : t) := Raw.inter_1 (sorted s) (sorted s').
- Definition inter_2 (s s' : t) := Raw.inter_2 (sorted s) (sorted s').
- Definition inter_3 (s s' : t) := Raw.inter_3 (sorted s) (sorted s').
- 
- Definition diff (s s' : t) :=
+ Definition diff (s s' : t) : t :=
    Build_slist (Raw.diff_sort (sorted s) (sorted s')). 
- Definition diff_1 (s s' : t) := Raw.diff_1 (sorted s) (sorted s').
- Definition diff_2 (s s' : t) := Raw.diff_2 (sorted s) (sorted s').
- Definition diff_3 (s s' : t) := Raw.diff_3 (sorted s) (sorted s').
- 
- Definition equal (s s' : t) := Raw.equal s s'. 
- Definition equal_1 (s s' : t) := Raw.equal_1 (sorted s) (sorted s').  
- Definition equal_2 (s s' : t) := Raw.equal_2 (s:=s) (s':=s').
- 
- Definition subset (s s' : t) := Raw.subset s s'.
- Definition subset_1 (s s' : t) := Raw.subset_1 (sorted s) (sorted s').  
- Definition subset_2 (s s' : t) := Raw.subset_2 (s:=s) (s':=s').
+ Definition equal (s s' : t) : bool := Raw.equal s s'. 
+ Definition subset (s s' : t) : bool := Raw.subset s s'.
+ Definition empty : t := Build_slist Raw.empty_sort.
+ Definition is_empty (s : t) : bool := Raw.is_empty s.
+ Definition elements (s : t) : list elt := Raw.elements s.
+ Definition min_elt (s : t) : option elt := Raw.min_elt s.
+ Definition max_elt (s : t) : option elt := Raw.max_elt s.
+ Definition choose (s : t) : option elt  := Raw.choose s.
+ Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. 
+ Definition cardinal (s : t) : nat := Raw.cardinal s.
+ Definition filter (f : elt -> bool) (s : t) : t :=
+   Build_slist (Raw.filter_sort (sorted s) f).
+ Definition for_all (f : elt -> bool) (s : t) : bool := Raw.for_all f s.
+ Definition exists_ (f : elt -> bool) (s : t) : bool := Raw.exists_ f s.
+ Definition partition (f : elt -> bool) (s : t) : t * t :=
+   let p := Raw.partition f s in
+   (Build_slist (this:=fst p) (Raw.partition_sort_1 (sorted s) f),
+   Build_slist (this:=snd p) (Raw.partition_sort_2 (sorted s) f)).
+ Definition eq (s s' : t) : Prop := Raw.eq s s'.
+ Definition lt (s s' : t) : Prop := Raw.lt s s'.
 
- Definition empty := Build_slist Raw.empty_sort.
- Definition empty_1 := Raw.empty_1.
- 
- Definition is_empty (s : t) := Raw.is_empty s.
- Definition is_empty_1 (s : t) := Raw.is_empty_1 (s:=s).
- Definition is_empty_2 (s : t) := Raw.is_empty_2 (s:=s).
-
- Definition elements (s : t) := Raw.elements s.
- Definition elements_1 (s : t) := Raw.elements_1 (s:=s).
- Definition elements_2 (s : t) := Raw.elements_2 (s:=s).
- Definition elements_3 (s : t) := Raw.elements_3 (sorted s).
- 
- Definition min_elt (s : t) := Raw.min_elt s.
- Definition min_elt_1 (s : t) := Raw.min_elt_1 (s:=s).
- Definition min_elt_2 (s : t) := Raw.min_elt_2 (sorted s).
- Definition min_elt_3 (s : t) := Raw.min_elt_3 (s:=s).
-
- Definition max_elt (s : t) := Raw.max_elt s.
- Definition max_elt_1 (s : t) := Raw.max_elt_1 (s:=s).
- Definition max_elt_2 (s : t) := Raw.max_elt_2 (sorted s).
- Definition max_elt_3 (s : t) := Raw.max_elt_3 (s:=s).
-  
- Definition choose := min_elt.
- Definition choose_1 := min_elt_1.
- Definition choose_2 := min_elt_3.
+ Section Spec. 
+  Variable s s' s'': t.
+  Variable x y : elt.
+
+  Lemma In_1 : E.eq x y -> In x s -> In y s. 
+  Proof. exact (fun H H' => Raw.MX.In_eq H H'). Qed.
  
- Definition fold (B : Set) (f : elt -> B -> B) (s : t) := Raw.fold (B:=B) f s. 
- Definition fold_1 (s : t) := Raw.fold_1 (sorted s). 
+  Lemma mem_1 : In x s -> mem x s = true.
+  Proof. exact (fun H => Raw.mem_1 s.(sorted) H). Qed.
+  Lemma mem_2 : mem x s = true -> In x s. 
+  Proof. exact (fun H => Raw.mem_2 H). Qed.
  
- Definition cardinal (s : t) := Raw.cardinal s.
- Definition cardinal_1 (s : t) := Raw.cardinal_1 (sorted s). 
+  Lemma equal_1 : Equal s s' -> equal s s' = true.
+  Proof. exact (Raw.equal_1 s.(sorted) s'.(sorted)). Qed.
+  Lemma equal_2 : equal s s' = true -> Equal s s'.
+  Proof. exact (fun H => Raw.equal_2 H). Qed.
+
+  Lemma subset_1 : Subset s s' -> subset s s' = true.
+  Proof. exact (Raw.subset_1 s.(sorted) s'.(sorted)). Qed.
+  Lemma subset_2 : subset s s' = true -> Subset s s'.
+  Proof. exact (fun H => Raw.subset_2 H). Qed.
+
+  Lemma empty_1 : Empty empty.
+  Proof. exact Raw.empty_1. Qed.
+
+  Lemma is_empty_1 : Empty s -> is_empty s = true. 
+  Proof. exact (fun H => Raw.is_empty_1 H). Qed.
+  Lemma is_empty_2 : is_empty s = true -> Empty s.
+  Proof. exact (fun H => Raw.is_empty_2 H). Qed.
  
- Definition filter (f : elt -> bool) (s : t) :=
-   Build_slist (Raw.filter_sort (sorted s) f).
- Definition filter_1 (s : t) := Raw.filter_1 (s:=s).
- Definition filter_2 (s : t) := Raw.filter_2 (s:=s).
- Definition filter_3 (s : t) := Raw.filter_3 (s:=s).
+  Lemma add_1 : E.eq x y -> In y (add x s).
+  Proof. exact (fun H => Raw.add_1 s.(sorted) H). Qed.
+  Lemma add_2 : In y s -> In y (add x s).
+  Proof. exact (fun H => Raw.add_2 s.(sorted) x H). Qed.
+  Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. 
+  Proof. exact (fun H => Raw.add_3 s.(sorted) H). Qed.
+
+  Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
+  Proof. exact (fun H => Raw.remove_1 s.(sorted) H). Qed.
+  Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
+  Proof. exact (fun H H' => Raw.remove_2 s.(sorted) H H'). Qed.
+  Lemma remove_3 : In y (remove x s) -> In y s.
+  Proof. exact (fun H => Raw.remove_3 s.(sorted) H). Qed.
+
+  Lemma singleton_1 : In y (singleton x) -> E.eq x y. 
+  Proof. exact (fun H => Raw.singleton_1 H). Qed.
+  Lemma singleton_2 : E.eq x y -> In y (singleton x). 
+  Proof. exact (fun H => Raw.singleton_2 H). Qed.
+
+  Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
+  Proof. exact (fun H => Raw.union_1 s.(sorted) s'.(sorted) H). Qed.
+  Lemma union_2 : In x s -> In x (union s s'). 
+  Proof. exact (fun H => Raw.union_2 s.(sorted) s'.(sorted) H). Qed.
+  Lemma union_3 : In x s' -> In x (union s s').
+  Proof. exact (fun H => Raw.union_3 s.(sorted) s'.(sorted) H). Qed.
+
+  Lemma inter_1 : In x (inter s s') -> In x s.
+  Proof. exact (fun H => Raw.inter_1 s.(sorted) s'.(sorted) H). Qed.
+  Lemma inter_2 : In x (inter s s') -> In x s'.
+  Proof. exact (fun H => Raw.inter_2 s.(sorted) s'.(sorted) H). Qed.
+  Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
+  Proof. exact (fun H => Raw.inter_3 s.(sorted) s'.(sorted) H). Qed.
+
+  Lemma diff_1 : In x (diff s s') -> In x s. 
+  Proof. exact (fun H => Raw.diff_1 s.(sorted) s'.(sorted) H). Qed.
+  Lemma diff_2 : In x (diff s s') -> ~ In x s'.
+  Proof. exact (fun H => Raw.diff_2 s.(sorted) s'.(sorted) H). Qed.
+  Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
+  Proof. exact (fun H => Raw.diff_3 s.(sorted) s'.(sorted) H). Qed.
  
- Definition for_all (f : elt -> bool) (s : t) := Raw.for_all f s.
- Definition for_all_1 (s : t) := Raw.for_all_1 (s:=s). 
- Definition for_all_2 (s : t) := Raw.for_all_2 (s:=s). 
+  Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+      fold f s i = fold_left (fun a e => f e a) (elements s) i.
+  Proof. exact (Raw.fold_1 s.(sorted)). Qed.
 
- Definition exists_ (f : elt -> bool) (s : t) := Raw.exists_ f s.
- Definition exists_1 (s : t) := Raw.exists_1 (s:=s). 
- Definition exists_2 (s : t) := Raw.exists_2 (s:=s). 
+  Lemma cardinal_1 : cardinal s = length (elements s).
+  Proof. exact (Raw.cardinal_1 s.(sorted)). Qed.
 
- Definition partition (f : elt -> bool) (s : t) :=
-   let p := Raw.partition f s in
-   (Build_slist (this:=fst p) (Raw.partition_sort_1 (sorted s) f),
-   Build_slist (this:=snd p) (Raw.partition_sort_2 (sorted s) f)).
- Definition partition_1 (s : t) := Raw.partition_1 s.
- Definition partition_2 (s : t) := Raw.partition_2 s. 
-
- Definition eq (s s' : t) := Raw.eq s s'.
- Definition eq_refl (s : t) := Raw.eq_refl s.
- Definition eq_sym (s s' : t) := Raw.eq_sym (s:=s) (s':=s').
- Definition eq_trans (s s' s'' : t) :=
-   Raw.eq_trans (s:=s) (s':=s') (s'':=s'').
+  Section Filter.
   
- Definition lt (s s' : t) := Raw.lt s s'.
- Definition lt_trans (s s' s'' : t) :=
-   Raw.lt_trans (s:=s) (s':=s') (s'':=s'').
- Definition lt_not_eq (s s' : t) := Raw.lt_not_eq (sorted s) (sorted s').
-
- Definition compare : forall s s' : t, Compare lt eq s s'.
- Proof.
- intros; elim (Raw.compare (sorted s) (sorted s'));
-  [ constructor 1 | constructor 2 | constructor 3 ]; 
-  auto. 
- Defined.
+  Variable f : elt -> bool.
+
+  Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. 
+  Proof. exact (@Raw.filter_1 s x f). Qed.
+  Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. 
+  Proof. exact (@Raw.filter_2 s x f). Qed.
+  Lemma filter_3 :
+      compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
+  Proof. exact (@Raw.filter_3 s x f). Qed.
+
+  Lemma for_all_1 :
+      compat_bool E.eq f ->
+      For_all (fun x => f x = true) s -> for_all f s = true.
+  Proof. exact (@Raw.for_all_1 s f). Qed.
+  Lemma for_all_2 :
+      compat_bool E.eq f ->
+      for_all f s = true -> For_all (fun x => f x = true) s.
+  Proof. exact (@Raw.for_all_2 s f). Qed.
+
+  Lemma exists_1 :
+      compat_bool E.eq f ->
+      Exists (fun x => f x = true) s -> exists_ f s = true.
+  Proof. exact (@Raw.exists_1 s f). Qed.
+  Lemma exists_2 :
+      compat_bool E.eq f ->
+      exists_ f s = true -> Exists (fun x => f x = true) s.
+  Proof. exact (@Raw.exists_2 s f). Qed.
+
+  Lemma partition_1 :
+      compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
+  Proof. exact (@Raw.partition_1 s f). Qed.
+  Lemma partition_2 :
+      compat_bool E.eq f ->
+      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+  Proof. exact (@Raw.partition_2 s f). Qed.
+
+  End Filter.
+
+  Lemma elements_1 : In x s -> InA E.eq x (elements s).
+  Proof. exact (fun H => Raw.elements_1 H). Qed.
+  Lemma elements_2 : InA E.eq x (elements s) -> In x s.
+  Proof. exact (fun H => Raw.elements_2 H). Qed.
+  Lemma elements_3 : sort E.lt (elements s).
+  Proof. exact (Raw.elements_3 s.(sorted)). Qed.
+
+  Lemma min_elt_1 : min_elt s = Some x -> In x s. 
+  Proof. exact (fun H => Raw.min_elt_1 H). Qed.
+  Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. 
+  Proof. exact (fun H => Raw.min_elt_2 s.(sorted) H). Qed.
+  Lemma min_elt_3 : min_elt s = None -> Empty s.
+  Proof. exact (fun H => Raw.min_elt_3 H). Qed.
+
+  Lemma max_elt_1 : max_elt s = Some x -> In x s. 
+  Proof. exact (fun H => Raw.max_elt_1 H). Qed.
+  Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. 
+  Proof. exact (fun H => Raw.max_elt_2 s.(sorted) H). Qed.
+  Lemma max_elt_3 : max_elt s = None -> Empty s.
+  Proof. exact (fun H => Raw.max_elt_3 H). Qed.
+
+  Lemma choose_1 : choose s = Some x -> In x s.
+  Proof. exact (fun H => Raw.choose_1 H). Qed.
+  Lemma choose_2 : choose s = None -> Empty s.
+  Proof. exact (fun H => Raw.choose_2 H). Qed.
+
+  Lemma eq_refl : eq s s.
+  Proof. exact (Raw.eq_refl s). Qed.
+  Lemma eq_sym : eq s s' -> eq s' s.
+  Proof. exact (@Raw.eq_sym s s'). Qed.
+  Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''.
+  Proof. exact (@Raw.eq_trans s s' s''). Qed.
+
+  Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''.
+  Proof. exact (@Raw.lt_trans s s' s''). Qed.
+  Lemma lt_not_eq : lt s s' -> ~ eq s s'.
+  Proof. exact (Raw.lt_not_eq s.(sorted) s'.(sorted)). Qed.
+
+  Definition compare : Compare lt eq s s'.
+  Proof.
+  elim (Raw.compare s.(sorted) s'.(sorted));
+   [ constructor 1 | constructor 2 | constructor 3 ]; 
+   auto. 
+  Defined.
+
+ End Spec.
 
 End Make.