Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

5 files changed, 58 insertions, 52 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index e1e026f5..fe7902aa 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -6,18 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Heap.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Heap.v 10698 2008-03-19 18:46:59Z letouzey $ i*)
 
 (** A development of Treesort on Heap trees *)
 
 (* G. Huet 1-9-95 uses Multiset *)
 
-Require Import List.
-Require Import Multiset.
-Require Import Permutation.
-Require Import Relations.
-Require Import Sorting.
-
+Require Import List Multiset Permutation Relations Sorting.
 
 Section defs.
 
@@ -25,7 +20,7 @@ Section defs.
 
   (** ** Definition of trees over an ordered set *)
 
-  Variable A : Set.
+  Variable A : Type.
   Variable leA : relation A.
   Variable eqA : relation A.
 
@@ -43,7 +38,7 @@ Section defs.
   Let emptyBag := EmptyBag A.
   Let singletonBag := SingletonBag _ eqA_dec.
   
-  Inductive Tree : Set :=
+  Inductive Tree :=
     | Tree_Leaf : Tree
     | Tree_Node : A -> Tree -> Tree -> Tree.
 
@@ -87,6 +82,23 @@ Section defs.
   Qed.
 
   (* This lemma ought to be generated automatically by the Inversion tools *)
+  Lemma is_heap_rect :
+    forall P:Tree -> Type,
+      P Tree_Leaf ->
+      (forall (a:A) (T1 T2:Tree),
+	leA_Tree a T1 ->
+	leA_Tree a T2 ->
+	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+      forall T:Tree, is_heap T -> P T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros a G PG D PD PN. 
+    elim (invert_heap a G D); auto with datatypes.
+    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+    apply X0; auto with datatypes.
+  Qed.
+
+  (* This lemma ought to be generated automatically by the Inversion tools *)
   Lemma is_heap_rec :
     forall P:Tree -> Set,
       P Tree_Leaf ->
@@ -100,7 +112,7 @@ Section defs.
     intros a G PG D PD PN. 
     elim (invert_heap a G D); auto with datatypes.
     intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
-    apply H0; auto with datatypes.
+    apply X; auto with datatypes.
   Qed.
 
   Lemma low_trans :
@@ -136,7 +148,7 @@ Section defs.
 
   (** ** Specification of heap insertion *)
 
-  Inductive insert_spec (a:A) (T:Tree) : Set :=
+  Inductive insert_spec (a:A) (T:Tree) : Type :=
     insert_exist :
     forall T1:Tree,
       is_heap T1 ->
@@ -152,11 +164,11 @@ Section defs.
       auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
     simpl in |- *; unfold meq, munion in |- *; auto using node_is_heap with datatypes.
     elim (leA_dec a a0); intros.
-    elim (H3 a0); intros.
+    elim (X a0); intros.
     apply insert_exist with (Tree_Node a T2 T0);
       auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
     simpl in |- *; apply treesort_twist1; trivial with datatypes. 
-    elim (H3 a); intros T3 HeapT3 ConT3 LeA.
+    elim (X a); intros T3 HeapT3 ConT3 LeA.
     apply insert_exist with (Tree_Node a0 T2 T3); 
       auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
     apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
@@ -169,7 +181,7 @@ Section defs.
 
   (** ** Building a heap from a list *)
 
-  Inductive build_heap (l:list A) : Set :=
+  Inductive build_heap (l:list A) : Type :=
     heap_exist :
     forall T:Tree,
       is_heap T ->
@@ -193,7 +205,7 @@ Section defs.
 
   (** ** Building the sorted list *)
   
-  Inductive flat_spec (T:Tree) : Set :=
+  Inductive flat_spec (T:Tree) : Type :=
     flat_exist :
     forall l:list A,
       sort leA l ->
@@ -204,7 +216,7 @@ Section defs.
   Proof.
     intros T h; elim h; intros.
     apply flat_exist with (nil (A:=A)); auto with datatypes.
-    elim H2; intros l1 s1 i1 m1; elim H4; intros l2 s2 i2 m2.
+    elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
     elim (merge _ leA_dec eqA_dec s1 s2); intros.
     apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
     apply meq_trans with
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index f4986198..084aae92 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -6,14 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PermutEq.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: PermutEq.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
 
-Require Import Omega.
-Require Import Relations.
-Require Import Setoid.
-Require Import List.
-Require Import Multiset.
-Require Import Permutation. 
+Require Import Omega Relations Setoid List Multiset Permutation.
 
 Set Implicit Arguments.
 
@@ -25,7 +20,7 @@ Set Implicit Arguments.
 
 Section Perm.
   
-  Variable A : Set.
+  Variable A : Type.
   Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.
   
   Notation permutation := (permutation _ eq_dec).
@@ -214,7 +209,7 @@ Section Perm.
     apply permut_remove_hd with a; auto.
   Qed.
 
-  Variable B : Set.
+  Variable B : Type.
   Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. 
 
   (** Permutation is compatible with map. *)
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 65369a01..c3888cfa 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -6,14 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PermutSetoid.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: PermutSetoid.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
 
-Require Import Omega.
-Require Import Relations.
-Require Import List.
-Require Import Multiset.
-Require Import Permutation. 
-Require Import SetoidList.
+Require Import Omega Relations Multiset Permutation SetoidList.
 
 Set Implicit Arguments.
 
@@ -23,7 +18,7 @@ Set Implicit Arguments.
 
 Section Perm.
 
-Variable A : Set.
+Variable A : Type.
 Variable eqA : relation A.
 Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
@@ -81,7 +76,7 @@ Proof.
   rewrite IHl in H1.
   intros; destruct (eqA_dec a a0) as [H2|H2]; simpl; auto.
   rewrite multiplicity_InA_O; auto.
-  swap H0.
+  contradict H0.
   apply InA_eqA with a0; auto.
   intros; constructor.
   rewrite multiplicity_InA.
@@ -185,9 +180,9 @@ Proof.
   destruct H2; apply eqA_trans with a; auto.
 Qed.
 
-Lemma NoDupA_eqlistA_permut : 
+Lemma NoDupA_equivlistA_permut : 
   forall l l', NoDupA eqA l -> NoDupA eqA l' -> 
-    eqlistA eqA l l' -> permutation l l'.
+    equivlistA eqA l l' -> permutation l l'.
 Proof.
   intros.
   red; unfold meq; intros.
@@ -198,7 +193,7 @@ Proof.
 Qed.
 
 
-Variable B : Set.
+Variable B : Type.
 Variable eqB : B->B->Prop.
 Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }. 
 Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 3ff026c2..82294b70 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -6,12 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Permutation.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Permutation.v 10698 2008-03-19 18:46:59Z letouzey $ i*)
 
-Require Import Relations.
-Require Import List.
-Require Import Multiset.
-Require Import Arith.
+Require Import Relations List Multiset Arith.
 
 (** This file define a notion of permutation for lists, based on multisets: 
     there exists a permutation between two lists iff every elements have 
@@ -38,7 +35,7 @@ Section defs.
 
   (** * From lists to multisets *)
 
-  Variable A : Set.
+  Variable A : Type.
   Variable eqA : relation A.
   Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index f895d79e..aed8cd15 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -6,18 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Sorting.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Sorting.v 10698 2008-03-19 18:46:59Z letouzey $ i*)
 
-Require Import List.
-Require Import Multiset.
-Require Import Permutation.
-Require Import Relations.
+Require Import List Multiset Permutation Relations.
 
 Set Implicit Arguments.
 
 Section defs.
 
-  Variable A : Set.
+  Variable A : Type.
   Variable leA : relation A.
   Variable eqA : relation A.
 
@@ -59,6 +56,16 @@ Section defs.
     intros; inversion H; auto with datatypes.
   Qed.
 
+  Lemma sort_rect :
+    forall P:list A -> Type,
+      P nil ->
+      (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) ->
+      forall y:list A, sort y -> P y.
+  Proof.
+    simple induction y; auto with datatypes.
+    intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes.
+  Qed.
+
   Lemma sort_rec :
     forall P:list A -> Set,
       P nil ->
@@ -71,7 +78,7 @@ Section defs.
 
   (** * Merging two sorted lists *)
 
-  Inductive merge_lem (l1 l2:list A) : Set :=
+  Inductive merge_lem (l1 l2:list A) : Type :=
     merge_exist :
     forall l:list A,
       sort l ->
@@ -85,7 +92,7 @@ Section defs.
   Proof.
     simple induction 1; intros.
     apply merge_exist with l2; auto with datatypes.
-    elim H3; intros.
+    elim H2; intros.
     apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes.
     elim (leA_dec a a0); intros.
 
@@ -104,7 +111,7 @@ Section defs.
     apply lelistA_inv with l; trivial with datatypes.
 
     (* 2 (leA a0 a) *)
-    elim H5; simpl in |- *; intros.
+    elim X0; simpl in |- *; intros.
     apply merge_exist with (a0 :: l3); simpl in |- *; 
       auto using cons_sort, cons_leA with datatypes.
     apply meq_trans with