diff options
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/Heap.v | 4 | ||||
| -rw-r--r-- | theories/Sorting/Mergesort.v | 4 | ||||
| -rw-r--r-- | theories/Sorting/PermutEq.v | 4 | ||||
| -rw-r--r-- | theories/Sorting/PermutSetoid.v | 17 | ||||
| -rw-r--r-- | theories/Sorting/Permutation.v | 86 | ||||
| -rw-r--r-- | theories/Sorting/Sorted.v | 6 | ||||
| -rw-r--r-- | theories/Sorting/Sorting.v | 4 |
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. |