From 58c70113a815a42593c566f64f2de840fc7e48a1 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 4 Mar 2008 17:33:35 +0000
Subject: migration from Set to Type of FSet/FMap + some dependencies...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Sorting/Heap.v         | 35 ++++++++++++++++++++++++++---------
 theories/Sorting/PermutEq.v     |  4 ++--
 theories/Sorting/PermutSetoid.v |  4 ++--
 theories/Sorting/Permutation.v  |  2 +-
 theories/Sorting/Sorting.v      | 18 ++++++++++++++----
 5 files changed, 45 insertions(+), 18 deletions(-)

(limited to 'theories/Sorting')

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 2f5dfafef..573d5adb8 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -25,7 +25,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 +43,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.
 
@@ -86,6 +86,23 @@ Section defs.
     intros; inversion H; auto with datatypes.
   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,
@@ -100,7 +117,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 +153,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 +169,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 +186,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 +210,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 +221,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 166b59a9f..8ff4e460e 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -25,7 +25,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 +214,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 84eac9905..e012bde19 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -23,7 +23,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}.
 
@@ -198,7 +198,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 4c23f0f93..026a305b1 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -38,7 +38,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 c1a43f64f..9828d1a24 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -17,7 +17,7 @@ Set Implicit Arguments.
 
 Section defs.
 
-  Variable A : Set.
+  Variable A : Type.
   Variable leA : relation A.
   Variable eqA : relation A.
 
@@ -59,6 +59,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 +81,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 +95,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 +114,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
-- 
cgit v1.2.3