Imported Upstream version 8.4~betaupstream/8.4_beta

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.