diff options
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/Heap.v | 24 | ||||
| -rw-r--r-- | theories/Sorting/Mergesort.v | 6 | ||||
| -rw-r--r-- | theories/Sorting/PermutEq.v | 4 | ||||
| -rw-r--r-- | theories/Sorting/PermutSetoid.v | 27 | ||||
| -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, 67 insertions, 90 deletions
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 76080aa9..8b1bdbd4 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-2012 *) (* \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 @@ -57,13 +55,13 @@ Section defs. Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf. Proof. - simpl in |- *; auto with datatypes. + simpl; auto with datatypes. Qed. Lemma leA_Tree_Node : forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D). Proof. - simpl in |- *; auto with datatypes. + simpl; auto with datatypes. Qed. @@ -123,7 +121,7 @@ Section defs. forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T. Proof. simple induction T; auto with datatypes. - intros; simpl in |- *; apply leA_trans with b; auto with datatypes. + intros; simpl; apply leA_trans with b; auto with datatypes. Qed. (** ** Merging two sorted lists *) @@ -215,12 +213,12 @@ Section defs. simple induction 1; intros. apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf); 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. + simpl; unfold meq, munion; auto using node_is_heap with datatypes. elim (leA_dec a 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. + simpl; apply treesort_twist1; trivial with datatypes. 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. @@ -228,7 +226,7 @@ Section defs. apply low_trans with a; auto with datatypes. apply LeA; auto with datatypes. apply low_trans with a; auto with datatypes. - simpl in |- *; apply treesort_twist2; trivial with datatypes. + simpl; apply treesort_twist2; trivial with datatypes. Qed. @@ -244,10 +242,10 @@ Section defs. Proof. simple induction l. apply (heap_exist nil Tree_Leaf); auto with datatypes. - simpl in |- *; unfold meq in |- *; exact nil_is_heap. + simpl; unfold meq; exact nil_is_heap. simple induction 1. intros T i m; elim (insert T i a). - intros; apply heap_exist with T1; simpl in |- *; auto with datatypes. + intros; apply heap_exist with T1; simpl; auto with datatypes. apply meq_trans with (munion (contents T) (singletonBag a)). apply meq_trans with (munion (singletonBag a) (contents T)). apply meq_right; trivial with datatypes. @@ -271,7 +269,7 @@ Section defs. apply flat_exist with (nil (A:=A)); auto with datatypes. elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2. elim (merge _ s1 _ s2); intros. - apply flat_exist with (a :: l); simpl in |- *; auto with datatypes. + apply flat_exist with (a :: l); simpl; auto with datatypes. apply meq_trans with (munion (list_contents _ eqA_dec l1) (munion (list_contents _ eqA_dec l2) (singletonBag a))). @@ -290,7 +288,7 @@ Section defs. forall l:list A, {m : list A | Sorted leA m & permutation _ eqA_dec l m}. Proof. - intro l; unfold permutation in |- *. + intro l; unfold permutation. elim (list_to_heap l). intros. elim (heap_to_list T); auto with datatypes. diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v index cded23ea..301a2142 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-2012 *) (* \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) *) @@ -133,7 +131,7 @@ Theorem Sorted_merge : forall l1 l2, Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2). Proof. induction l1; induction l2; intros; simpl; auto. - destruct (a <=? a0) as ()_eqn:Heq1. + destruct (a <=? a0) eqn:Heq1. invert H. simpl. constructor; trivial; rewrite Heq1; constructor. assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto). diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 00d6e7ce..cc47b500 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-2012 *) (* \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..2cd4f5f7 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-2012 *) (* \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. @@ -54,7 +52,7 @@ Lemma list_contents_app : forall l m:list A, meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)). Proof. - simple induction l; simpl in |- *; auto with datatypes. + simple induction l; simpl; auto with datatypes. intros. apply meq_trans with (munion (singletonBag a) (munion (list_contents l0) (list_contents m))); @@ -67,19 +65,19 @@ Definition permutation (l m:list A) := meq (list_contents l) (list_contents m). Lemma permut_refl : forall l:list A, permutation l l. Proof. - unfold permutation in |- *; auto with datatypes. + unfold permutation; auto with datatypes. Qed. Lemma permut_sym : forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1. Proof. - unfold permutation, meq; intros; apply sym_eq; trivial. + unfold permutation, meq; intros; symmetry; trivial. Qed. Lemma permut_trans : forall l m n:list A, permutation l m -> permutation m n -> permutation l n. Proof. - unfold permutation in |- *; intros. + unfold permutation; intros. apply meq_trans with (list_contents m); auto with datatypes. Qed. @@ -104,7 +102,7 @@ Lemma permut_app : forall l l' m m':list A, permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m'). Proof. - unfold permutation in |- *; intros. + unfold permutation; intros. apply meq_trans with (munion (list_contents l) (list_contents m)); auto using permut_cons, list_contents_app with datatypes. apply meq_trans with (munion (list_contents l') (list_contents m')); @@ -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..a69c4aa7 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-2012 *) (* \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..03952c95 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-2012 *) (* \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..ab03cb5e 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-2012 *) (* \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. |