From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/Sorting/Permutation.v | 86 ++++++++++++++++++++----------------------
 1 file changed, 40 insertions(+), 46 deletions(-)

(limited to 'theories/Sorting/Permutation.v')

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
-- 
cgit v1.2.3