diff options
Diffstat (limited to 'theories/Sorting/PermutSetoid.v')
| -rw-r--r-- | theories/Sorting/PermutSetoid.v | 12 |
1 files changed, 6 insertions, 6 deletions
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')); |