From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sorting/Heap.v | 20 ++++++++--------- theories/Sorting/PermutEq.v | 40 ++++++++++++++++----------------- theories/Sorting/PermutSetoid.v | 34 ++++++++++++++-------------- theories/Sorting/Permutation.v | 50 ++++++++++++++++++++--------------------- theories/Sorting/Sorting.v | 4 ++-- 5 files changed, 74 insertions(+), 74 deletions(-) (limited to 'theories/Sorting') diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 2d639d096..6d5564ed7 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -25,7 +25,7 @@ Section defs. Variable eqA : relation A. Let gtA (x y:A) := ~ leA x y. - + Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}. Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y. @@ -37,7 +37,7 @@ Section defs. Let emptyBag := EmptyBag A. Let singletonBag := SingletonBag _ eqA_dec. - + Inductive Tree := | Tree_Leaf : Tree | Tree_Node : A -> Tree -> Tree -> Tree. @@ -92,7 +92,7 @@ Section defs. forall T:Tree, is_heap T -> P T. Proof. simple induction T; auto with datatypes. - intros a G PG D PD PN. + intros a G PG D PD PN. elim (invert_heap a G D); auto with datatypes. intros H1 H2; elim H2; intros H3 H4; elim H4; intros. apply X0; auto with datatypes. @@ -109,7 +109,7 @@ Section defs. forall T:Tree, is_heap T -> P T. Proof. simple induction T; auto with datatypes. - intros a G PG D PD PN. + intros a G PG D PD PN. elim (invert_heap a G D); auto with datatypes. intros H1 H2; elim H2; intros H3 H4; elim H4; intros. apply X; auto with datatypes. @@ -167,15 +167,15 @@ Section defs. 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 in |- *; apply treesort_twist1; trivial with datatypes. elim (X a); intros T3 HeapT3 ConT3 LeA. - apply insert_exist with (Tree_Node a0 T2 T3); + apply insert_exist with (Tree_Node a0 T2 T3); auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes. apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes. - apply low_trans with a; auto with datatypes. + 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 in |- *; apply treesort_twist2; trivial with datatypes. Qed. @@ -186,7 +186,7 @@ Section defs. forall T:Tree, is_heap T -> meq (list_contents _ eqA_dec l) (contents T) -> build_heap l. - + Lemma list_to_heap : forall l:list A, build_heap l. Proof. simple induction l. @@ -204,7 +204,7 @@ Section defs. (** ** Building the sorted list *) - + Inductive flat_spec (T:Tree) : Type := flat_exist : forall l:list A, diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index f7bd37ee2..9bfe31ed1 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -13,22 +13,22 @@ Require Import Omega Relations Setoid List Multiset Permutation. Set Implicit Arguments. (** This file is similar to [PermutSetoid], except that the equality used here - is Coq usual one instead of a setoid equality. In particular, we can then - prove the equivalence between [List.Permutation] and + is Coq usual one instead of a setoid equality. In particular, we can then + prove the equivalence between [List.Permutation] and [Permutation.permutation]. *) Section Perm. - + Variable A : Type. Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}. - + Notation permutation := (permutation _ eq_dec). Notation list_contents := (list_contents _ eq_dec). (** we can use [multiplicity] to define [In] and [NoDup]. *) - Lemma multiplicity_In : + Lemma multiplicity_In : forall l a, In a l <-> 0 < multiplicity (list_contents l) a. Proof. induction l. @@ -49,18 +49,18 @@ Section Perm. Lemma multiplicity_In_O : forall l a, ~ In a l -> multiplicity (list_contents l) a = 0. Proof. - intros l a; rewrite multiplicity_In; + intros l a; rewrite multiplicity_In; destruct (multiplicity (list_contents l) a); auto. destruct 1; auto with arith. Qed. - + Lemma multiplicity_In_S : forall l a, In a l -> multiplicity (list_contents l) a >= 1. Proof. intros l a; rewrite multiplicity_In; auto. Qed. - Lemma multiplicity_NoDup : + Lemma multiplicity_NoDup : forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1). Proof. induction l. @@ -78,7 +78,7 @@ Section Perm. generalize (H a). destruct (eq_dec a a) as [H0|H0]. destruct (multiplicity (list_contents l) a); auto with arith. - simpl; inversion 1. + simpl; inversion 1. inversion H3. destruct H0; auto. rewrite IHl; intros. @@ -86,13 +86,13 @@ Section Perm. destruct (eq_dec a a0); simpl; auto with arith. Qed. - Lemma NoDup_permut : - forall l l', NoDup l -> NoDup l' -> + Lemma NoDup_permut : + forall l l', NoDup l -> NoDup l' -> (forall x, In x l <-> In x l') -> permutation l l'. Proof. intros. red; unfold meq; intros. - rewrite multiplicity_NoDup in H, H0. + rewrite multiplicity_NoDup in H, H0. generalize (H a) (H0 a) (H1 a); clear H H0 H1. do 2 rewrite multiplicity_In. destruct 3; omega. @@ -128,11 +128,11 @@ Section Perm. intro Abs; generalize (permut_In_In _ Abs H). inversion 1. Qed. - - (** When used with [eq], this permutation notion is equivalent to + + (** When used with [eq], this permutation notion is equivalent to the one defined in [List.v]. *) - Lemma permutation_Permutation : + Lemma permutation_Permutation : forall l l', Permutation l l' <-> permutation l l'. Proof. split. @@ -165,7 +165,7 @@ Section Perm. destruct (eq_dec b b) as [H|H]; [ | destruct H; auto]. destruct (eq_dec a b); simpl; auto; intros; discriminate. Qed. - + Lemma permut_length_2 : forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) -> (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1). @@ -177,7 +177,7 @@ Section Perm. apply permut_length_1. red; red; intros. generalize (P a); clear P; simpl. - destruct (eq_dec a1 a) as [H2|H2]; + destruct (eq_dec a1 a) as [H2|H2]; destruct (eq_dec a2 a) as [H3|H3]; auto. destruct H3; transitivity a1; auto. destruct H2; transitivity a2; auto. @@ -187,7 +187,7 @@ Section Perm. apply permut_length_1. red; red; intros. generalize (P a); clear P; simpl. - destruct (eq_dec a1 a) as [H2|H2]; + destruct (eq_dec a1 a) as [H2|H2]; destruct (eq_dec b2 a) as [H3|H3]; auto. simpl; rewrite <- plus_n_Sm; inversion 1; auto. destruct H3; transitivity a1; auto. @@ -210,12 +210,12 @@ Section Perm. Qed. Variable B : Type. - Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. + Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. (** Permutation is compatible with map. *) Lemma permutation_map : - forall f l1 l2, permutation l1 l2 -> + forall f l1 l2, permutation l1 l2 -> Permutation.permutation _ eqB_dec (map f l1) (map f l2). Proof. intros f; induction l1. diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 1ea71972b..803a6143f 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -12,8 +12,8 @@ Require Import Omega Relations Multiset Permutation SetoidList. Set Implicit Arguments. -(** This file contains additional results about permutations - with respect to a setoid equality (i.e. an equivalence relation). +(** This file contains additional results about permutations + with respect to a setoid equality (i.e. an equivalence relation). *) Section Perm. @@ -33,7 +33,7 @@ Variable eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z. (** we can use [multiplicity] to define [InA] and [NoDupA]. *) -Lemma multiplicity_InA : +Lemma multiplicity_InA : forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a. Proof. induction l. @@ -54,7 +54,7 @@ Qed. Lemma multiplicity_InA_O : forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0. Proof. - intros l a; rewrite multiplicity_InA; + intros l a; rewrite multiplicity_InA; destruct (multiplicity (list_contents l) a); auto with arith. destruct 1; auto with arith. Qed. @@ -65,7 +65,7 @@ Proof. intros l a; rewrite multiplicity_InA; auto with arith. Qed. -Lemma multiplicity_NoDupA : forall l, +Lemma multiplicity_NoDupA : forall l, NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1). Proof. induction l. @@ -83,7 +83,7 @@ Proof. generalize (H a). destruct (eqA_dec a a) as [H0|H0]. destruct (multiplicity (list_contents l) a); auto with arith. - simpl; inversion 1. + simpl; inversion 1. inversion H3. destruct H0; auto. rewrite IHl; intros. @@ -140,7 +140,7 @@ Proof. apply permut_length_1. red; red; intros. generalize (P a); clear P; simpl. - destruct (eqA_dec a1 a) as [H2|H2]; + destruct (eqA_dec a1 a) as [H2|H2]; destruct (eqA_dec a2 a) as [H3|H3]; auto. destruct H3; apply eqA_trans with a1; auto. destruct H2; apply eqA_trans with a2; auto. @@ -150,7 +150,7 @@ Proof. apply permut_length_1. red; red; intros. generalize (P a); clear P; simpl. - destruct (eqA_dec a1 a) as [H2|H2]; + destruct (eqA_dec a1 a) as [H2|H2]; destruct (eqA_dec b2 a) as [H3|H3]; auto. simpl; rewrite <- plus_n_Sm; inversion 1; auto. destruct H3; apply eqA_trans with a1; auto. @@ -174,19 +174,19 @@ Proof. apply permut_tran with (a::l1); auto. revert H1; unfold Permutation.permutation, meq; simpl. intros; f_equal; auto. - destruct (eqA_dec b a0) as [H2|H2]; + destruct (eqA_dec b a0) as [H2|H2]; destruct (eqA_dec a a0) as [H3|H3]; auto. destruct H3; apply eqA_trans with b; auto. destruct H2; apply eqA_trans with a; auto. Qed. -Lemma NoDupA_equivlistA_permut : - forall l l', NoDupA eqA l -> NoDupA eqA l' -> +Lemma NoDupA_equivlistA_permut : + forall l l', NoDupA eqA l -> NoDupA eqA l' -> equivlistA eqA l l' -> permutation l l'. Proof. intros. red; unfold meq; intros. - rewrite multiplicity_NoDupA in H, H0. + rewrite multiplicity_NoDupA in H, H0. generalize (H a) (H0 a) (H1 a); clear H H0 H1. do 2 rewrite multiplicity_InA. destruct 3; omega. @@ -195,15 +195,15 @@ Qed. Variable B : Type. Variable eqB : B->B->Prop. -Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }. +Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }. Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z. (** Permutation is compatible with map. *) Lemma permut_map : - forall f, + forall f, (forall x y, eqA x y -> eqB (f x) (f y)) -> - forall l1 l2, permutation l1 l2 -> + forall l1 l2, permutation l1 l2 -> Permutation.permutation _ eqB_dec (map f l1) (map f l2). Proof. intros f; induction l1. @@ -218,7 +218,7 @@ Proof. apply permut_tran with (f b :: map f l1). revert H1; unfold Permutation.permutation, meq; simpl. intros; f_equal; auto. - destruct (eqB_dec (f b) a0) as [H2|H2]; + destruct (eqB_dec (f b) a0) as [H2|H2]; destruct (eqB_dec (f a) a0) as [H3|H3]; auto. destruct H3; apply eqB_trans with (f b); auto. destruct H2; apply eqB_trans with (f a); auto. @@ -229,7 +229,7 @@ Proof. apply permut_tran with (a::l1); auto. revert H1; unfold Permutation.permutation, meq; simpl. intros; f_equal; auto. - destruct (eqA_dec b a0) as [H2|H2]; + destruct (eqA_dec b a0) as [H2|H2]; destruct (eqA_dec a a0) as [H3|H3]; auto. destruct H3; apply eqA_trans with b; auto. destruct H2; apply eqA_trans with a; auto. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index a92212054..9daf71b2b 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -10,9 +10,9 @@ Require Import Relations List Multiset Arith. -(** This file define a notion of permutation for lists, based on multisets: - there exists a permutation between two lists iff every elements have - the same multiplicity in the two lists. +(** This file define a notion of permutation for lists, based on multisets: + there exists a permutation between two lists iff every elements have + the same multiplicity in the two lists. Unlike [List.Permutation], the present notion of permutation requires the domain to be equipped with a decidable equality. This @@ -22,10 +22,10 @@ Require Import Relations List Multiset Arith. The present file contains basic results, obtained without any particular assumption on the decidable equality used. - File [PermutSetoid] contains additional results about permutations - with respect to an setoid equality (i.e. an equivalence relation). + File [PermutSetoid] contains additional results about permutations + with respect to an setoid equality (i.e. an equivalence relation). - Finally, file [PermutEq] concerns Coq equality : this file is similar + Finally, file [PermutEq] concerns Coq equality : this file is similar to the previous one, but proves in addition that [List.Permutation] and [permutation] are equivalent in this context. *) @@ -62,9 +62,9 @@ Section defs. auto with datatypes. Qed. - + (** * [permutation]: definition and basic properties *) - + Definition permutation (l m:list A) := meq (list_contents l) (list_contents m). @@ -72,42 +72,42 @@ Section defs. Proof. unfold permutation in |- *; 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. Qed. - + Lemma permut_tran : forall l m n:list A, permutation l m -> permutation m n -> permutation l n. Proof. unfold permutation in |- *; intros. apply meq_trans with (list_contents m); auto with datatypes. Qed. - + Lemma permut_cons : forall l m:list A, permutation l m -> forall a:A, permutation (a :: l) (a :: m). Proof. unfold permutation in |- *; simpl in |- *; auto with datatypes. Qed. - + 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. - apply meq_trans with (munion (list_contents l) (list_contents m)); + 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')); + 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)); auto using permut_cons, list_contents_app with datatypes. Qed. Lemma permut_add_inside : - forall a l1 l2 l3 l4, + forall a l1 l2 l3 l4, permutation (l1 ++ l2) (l3 ++ l4) -> permutation (l1 ++ a :: l2) (l3 ++ a :: l4). Proof. @@ -118,9 +118,9 @@ Section defs. destruct (eqA_dec a a0); simpl; auto with arith. do 2 rewrite <- plus_n_Sm; f_equal; auto. Qed. - + Lemma permut_add_cons_inside : - forall a l l1 l2, + forall a l l1 l2, permutation l (l1 ++ l2) -> permutation (a :: l) (l1 ++ a :: l2). Proof. @@ -134,17 +134,17 @@ Section defs. Proof. intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl. Qed. - + Lemma permut_sym_app : forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1). Proof. intros l1 l2; - unfold permutation, meq; - intro a; do 2 rewrite list_contents_app; simpl; + unfold permutation, meq; + intro a; do 2 rewrite list_contents_app; simpl; auto with arith. Qed. - Lemma permut_rev : + Lemma permut_rev : forall l, permutation l (rev l). Proof. induction l. @@ -162,7 +162,7 @@ Section defs. generalize (H a); apply plus_reg_l. Qed. - Lemma permut_app_inv1 : + Lemma permut_app_inv1 : forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2. Proof. intros l l1 l2; unfold permutation, meq; simpl; @@ -174,7 +174,7 @@ Section defs. trivial. Qed. - Lemma permut_app_inv2 : + Lemma permut_app_inv2 : forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2. Proof. intros l l1 l2; unfold permutation, meq; simpl; @@ -186,7 +186,7 @@ Section defs. Qed. Lemma permut_remove_hd : - forall l l1 l2 a, + forall l l1 l2 a, permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2). Proof. intros l l1 l2 a; unfold permutation, meq; simpl; intros H a0; generalize (H a0); clear H. @@ -200,6 +200,6 @@ Section defs. End defs. -(** For compatibilty *) +(** For compatibilty *) Notation permut_right := permut_cons. Unset Implicit Arguments. diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index 4c8173172..2d76b25a2 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -19,7 +19,7 @@ Section defs. Variable eqA : relation A. Let gtA (x y:A) := ~ leA x y. - + Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}. Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y. @@ -112,7 +112,7 @@ Section defs. (* 2 (leA a0 a) *) elim X0; simpl in |- *; intros. - apply merge_exist with (a0 :: l3); simpl in |- *; + apply merge_exist with (a0 :: l3); simpl in |- *; auto using cons_sort, cons_leA with datatypes. apply meq_trans with (munion (singletonBag a0) -- cgit v1.2.3