summaryrefslogtreecommitdiff
path: root/theories/Sorting
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sorting')
-rw-r--r--theories/Sorting/Heap.v44
-rw-r--r--theories/Sorting/PermutEq.v13
-rw-r--r--theories/Sorting/PermutSetoid.v19
-rw-r--r--theories/Sorting/Permutation.v9
-rw-r--r--theories/Sorting/Sorting.v25
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 06:43:44 +0000