diff options
Diffstat (limited to 'theories/Sorting')
-rw-r--r-- | theories/Sorting/Heap.v | 22 | ||||
-rw-r--r-- | theories/Sorting/Mergesort.v | 4 | ||||
-rw-r--r-- | theories/Sorting/PermutEq.v | 2 | ||||
-rw-r--r-- | theories/Sorting/PermutSetoid.v | 12 | ||||
-rw-r--r-- | theories/Sorting/Permutation.v | 2 | ||||
-rw-r--r-- | theories/Sorting/Sorted.v | 2 | ||||
-rw-r--r-- | theories/Sorting/Sorting.v | 2 |
7 files changed, 23 insertions, 23 deletions
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 60bb50ce..8b1bdbd4 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -55,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. @@ -121,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 *) @@ -213,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. @@ -226,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. @@ -242,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. @@ -269,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))). @@ -288,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 7124cd53..301a2142 100644 --- a/theories/Sorting/Mergesort.v +++ b/theories/Sorting/Mergesort.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -131,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 d4e5fba4..cc47b500 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index fa807c15..2cd4f5f7 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -52,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))); @@ -65,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. @@ -102,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')); diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 797583d0..a69c4aa7 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 0e230b77..03952c95 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index 22e56592..ab03cb5e 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) |