summaryrefslogtreecommitdiff
path: root/theories/Sorting
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/Sorting
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/Sorting')
-rw-r--r--theories/Sorting/Heap.v4
-rw-r--r--theories/Sorting/Mergesort.v4
-rw-r--r--theories/Sorting/PermutEq.v4
-rw-r--r--theories/Sorting/PermutSetoid.v17
-rw-r--r--theories/Sorting/Permutation.v86
-rw-r--r--theories/Sorting/Sorted.v6
-rw-r--r--theories/Sorting/Sorting.v4
7 files changed, 51 insertions, 74 deletions
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 76080aa9..60bb50ce 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Heap.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
(** A development of Treesort on Heap trees. It has an average
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index cded23ea..7124cd53 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mergesort.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** A modular implementation of mergesort (the complexity is O(n.log n) in
the length of the list) *)
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 00d6e7ce..d4e5fba4 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PermutEq.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
Set Implicit Arguments.
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 87b0b08d..fa807c15 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PermutSetoid.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Omega Relations Multiset SetoidList.
(** This file is deprecated, use [Permutation.v] instead.
@@ -344,8 +342,7 @@ Proof.
rewrite if_eqA_refl in H.
clear IHl; omega.
rewrite IHl; intros.
- specialize (H a0); auto with *.
- destruct (eqA_dec a a0); simpl; auto with *.
+ specialize (H a0). omega.
Qed.
(** Permutation is compatible with InA. *)
@@ -396,18 +393,14 @@ Proof.
apply permut_length_1.
red; red; intros.
specialize (P a). simpl in *.
- rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto.
- (** Bug omega: le "set" suivant ne devrait pas etre necessaire *)
- set (u:= if eqA_dec a2 a then 1 else 0) in *; omega.
+ rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega.
right.
inversion_clear H0; [|inversion H].
split; auto.
apply permut_length_1.
red; red; intros.
specialize (P a); simpl in *.
- rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto.
- (** Bug omega: idem *)
- set (u:= if eqA_dec b2 a then 1 else 0) in *; omega.
+ rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega.
Qed.
(** Permutation is compatible with length. *)
@@ -492,7 +485,7 @@ Qed.
End Permut_map.
-Require Import Permutation TheoryList.
+Require Import Permutation.
Section Permut_permut.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 7508ccc2..797583d0 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -1,15 +1,13 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Permutation.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*********************************************************************)
-(** ** List permutations as a composition of adjacent transpositions *)
+(** * List permutations as a composition of adjacent transpositions *)
(*********************************************************************)
(* Adapted in May 2006 by Jean-Marc Notin from initial contents by
@@ -139,32 +137,26 @@ Proof.
intros; apply Permutation_app; auto.
Qed.
+Lemma Permutation_cons_append : forall (l : list A) x,
+ Permutation (x :: l) (l ++ x :: nil).
+Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed.
+Local Hint Resolve Permutation_cons_append.
+
Theorem Permutation_app_comm : forall (l l' : list A),
Permutation (l ++ l') (l' ++ l).
Proof.
induction l as [|x l]; simpl; intro l'.
- rewrite app_nil_r; trivial.
- induction l' as [|y l']; simpl.
- rewrite app_nil_r; trivial.
- transitivity (x :: y :: l' ++ l).
- constructor; rewrite app_comm_cons; apply IHl.
- transitivity (y :: x :: l' ++ l); constructor.
- transitivity (x :: l ++ l'); auto.
+ rewrite app_nil_r; trivial. rewrite IHl.
+ rewrite app_comm_cons, Permutation_cons_append.
+ now rewrite <- app_assoc.
Qed.
+Local Hint Resolve Permutation_app_comm.
Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
-Proof.
- intros l l1; revert l.
- induction l1.
- simpl.
- intros; apply perm_skip; auto.
- simpl; intros.
- transitivity (a0::a::l1++l2).
- apply perm_skip; auto.
- transitivity (a::a0::l1++l2).
- apply perm_swap; auto.
- apply perm_skip; auto.
+Proof. intros l l1 l2 a H. rewrite H.
+ rewrite app_comm_cons, Permutation_cons_append.
+ now rewrite <- app_assoc.
Qed.
Local Hint Resolve Permutation_cons_app.
@@ -173,19 +165,20 @@ Theorem Permutation_middle : forall (l1 l2:list A) a,
Proof.
auto.
Qed.
+Local Hint Resolve Permutation_middle.
Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
Proof.
- induction l as [| x l]; simpl; trivial.
- apply Permutation_trans with (l' := [x] ++ rev l).
- simpl; auto.
- apply Permutation_app_comm.
+ induction l as [| x l]; simpl; trivial. now rewrite IHl at 1.
Qed.
+Add Parametric Morphism : (@rev A)
+ with signature @Permutation A ==> @Permutation A as Permutation_rev'.
+Proof. intros. now do 2 rewrite <- Permutation_rev. Qed.
+
Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.
Proof.
- intros l l' Hperm; induction Hperm; simpl; auto.
- apply trans_eq with (y:= (length l')); trivial.
+ intros l l' Hperm; induction Hperm; simpl; auto. now transitivity (length l').
Qed.
Theorem Permutation_ind_bis :
@@ -211,6 +204,12 @@ Ltac break_list l x l' H :=
destruct l as [|x l']; simpl in *;
injection H; intros; subst; clear H.
+Theorem Permutation_nil_app_cons : forall (l l' : list A) (x : A), ~ Permutation nil (l++x::l').
+Proof.
+ intros l l' x HF.
+ apply Permutation_nil in HF. destruct l; discriminate.
+Qed.
+
Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
Proof.
@@ -224,32 +223,27 @@ Proof.
(* skip *)
intros x l l' H IH; intros.
break_list l1 b l1' H0; break_list l3 c l3' H1.
- auto.
- apply perm_trans with (l3'++c::l4); auto.
- apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app.
- apply perm_skip.
- apply (IH a l1' l2 l3' l4); auto.
+ auto.
+ now rewrite H.
+ now rewrite <- H.
+ now rewrite (IH a _ _ _ _ eq_refl eq_refl).
(* contradict *)
intros x y l l' Hp IH; intros.
break_list l1 b l1' H; break_list l3 c l3' H0.
auto.
break_list l3' b l3'' H.
- auto.
- apply perm_trans with (c::l3''++b::l4); auto.
+ auto.
+ rewrite <- Permutation_middle in Hp. now rewrite Hp.
break_list l1' c l1'' H1.
- auto.
- apply perm_trans with (b::l1''++c::l2); auto.
+ auto.
+ rewrite <- Permutation_middle in Hp. now rewrite Hp.
break_list l3' d l3'' H; break_list l1' e l1'' H1.
auto.
- apply perm_trans with (e::a::l1''++l2); auto.
- apply perm_trans with (e::l1''++a::l2); auto.
- apply perm_trans with (d::a::l3''++l4); auto.
- apply perm_trans with (d::l3''++a::l4); auto.
- apply perm_trans with (e::d::l1''++l2); auto.
- apply perm_skip; apply perm_skip.
- apply (IH a l1'' l2 l3'' l4); auto.
+ rewrite <- Permutation_middle in Hp. rewrite perm_swap. auto.
+ rewrite perm_swap, Permutation_middle. auto.
+ now rewrite perm_swap, (IH a _ _ _ _ eq_refl eq_refl).
(*trans*)
- intros.
+ intros.
destruct (In_split a l') as (l'1,(l'2,H6)).
apply (Permutation_in a H).
subst l.
@@ -375,4 +369,4 @@ End Permutation_map.
(* begin hide *)
Notation Permutation_app_swap := Permutation_app_comm (only parsing).
-(* end hide *)
+(* end hide *) \ No newline at end of file
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 2c7c07e5..0e230b77 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Sorted.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* Made by Hugo Herbelin *)
(** This file defines two notions of sorted list:
@@ -27,7 +25,7 @@ Require Import List Relations Relations_1.
Set Implicit Arguments.
Local Notation "[ ]" := nil (at level 0).
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
-Implicit Arguments Transitive [U].
+Arguments Transitive [U] R.
Section defs.
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index bc1fdbcf..22e56592 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -1,12 +1,10 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Sorting.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Sorted.
Require Export Mergesort.