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/Relations/Operators_Properties.v | 44 +++++++++++++++---------------- theories/Relations/Relation_Definitions.v | 26 +++++++++--------- theories/Relations/Relation_Operators.v | 14 +++++----- 3 files changed, 42 insertions(+), 42 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 2ced22298..d35841e00 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -24,7 +24,7 @@ Section Properties. Variable R : relation A. Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y. - + Section Clos_Refl_Trans. (** Correctness of the reflexive-transitive closure operator *) @@ -33,7 +33,7 @@ Section Properties. Proof. apply Build_preorder. exact (rt_refl A R). - + exact (rt_trans A R). Qed. @@ -114,7 +114,7 @@ Section Properties. apply t1n_trans; auto. Qed. - Lemma t1n_trans_equiv : forall x y, + Lemma t1n_trans_equiv : forall x y, clos_trans A R x y <-> clos_trans_1n A R x y. Proof. split. @@ -144,7 +144,7 @@ Section Properties. right with y0; auto. Qed. - Lemma tn1_trans_equiv : forall x y, + Lemma tn1_trans_equiv : forall x y, clos_trans A R x y <-> clos_trans_n1 A R x y. Proof. split. @@ -152,7 +152,7 @@ Section Properties. apply tn1_trans. Qed. - (** Direct reflexive-transitive closure is equivalent to + (** Direct reflexive-transitive closure is equivalent to transitivity by left-step extension *) Lemma R_rt1n : forall x y, R x y -> clos_refl_trans_1n A R x y. @@ -167,7 +167,7 @@ Section Properties. right with x;[assumption|left]. Qed. - Lemma rt1n_trans : forall x y, + Lemma rt1n_trans : forall x y, clos_refl_trans_1n A R x y -> clos_refl_trans A R x y. Proof. induction 1. @@ -176,7 +176,7 @@ Section Properties. constructor 1; auto. Qed. - Lemma trans_rt1n : forall x y, + Lemma trans_rt1n : forall x y, clos_refl_trans A R x y -> clos_refl_trans_1n A R x y. Proof. induction 1. @@ -190,7 +190,7 @@ Section Properties. apply rt1n_trans; auto. Qed. - Lemma rt1n_trans_equiv : forall x y, + Lemma rt1n_trans_equiv : forall x y, clos_refl_trans A R x y <-> clos_refl_trans_1n A R x y. Proof. split. @@ -198,7 +198,7 @@ Section Properties. apply rt1n_trans. Qed. - (** Direct reflexive-transitive closure is equivalent to + (** Direct reflexive-transitive closure is equivalent to transitivity by right-step extension *) Lemma rtn1_trans : forall x y, @@ -210,7 +210,7 @@ Section Properties. constructor 1; assumption. Qed. - Lemma trans_rtn1 : forall x y, + Lemma trans_rtn1 : forall x y, clos_refl_trans A R x y -> clos_refl_trans_n1 A R x y. Proof. induction 1. @@ -221,7 +221,7 @@ Section Properties. right with y0; auto. Qed. - Lemma rtn1_trans_equiv : forall x y, + Lemma rtn1_trans_equiv : forall x y, clos_refl_trans A R x y <-> clos_refl_trans_n1 A R x y. Proof. split. @@ -240,7 +240,7 @@ Section Properties. revert H H0. induction H1; intros; auto with sets. apply H1 with x; auto with sets. - + apply IHclos_refl_trans2. apply IHclos_refl_trans1; auto with sets. @@ -270,10 +270,10 @@ Section Properties. eauto. Qed. - (** Direct reflexive-symmetric-transitive closure is equivalent to + (** Direct reflexive-symmetric-transitive closure is equivalent to transitivity by symmetric left-step extension *) - Lemma rts1n_rts : forall x y, + Lemma rts1n_rts : forall x y, clos_refl_sym_trans_1n A R x y -> clos_refl_sym_trans A R x y. Proof. induction 1. @@ -283,7 +283,7 @@ Section Properties. Qed. Lemma rts_1n_trans : forall x y, clos_refl_sym_trans_1n A R x y -> - forall z, clos_refl_sym_trans_1n A R y z -> + forall z, clos_refl_sym_trans_1n A R y z -> clos_refl_sym_trans_1n A R x z. induction 1. auto. @@ -301,7 +301,7 @@ Section Properties. left. Qed. - Lemma rts_rts1n : forall x y, + Lemma rts_rts1n : forall x y, clos_refl_sym_trans A R x y -> clos_refl_sym_trans_1n A R x y. induction 1. constructor 2 with y; auto. @@ -311,7 +311,7 @@ Section Properties. eapply rts_1n_trans; eauto. Qed. - Lemma rts_rts1n_equiv : forall x y, + Lemma rts_rts1n_equiv : forall x y, clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_1n A R x y. Proof. split. @@ -319,10 +319,10 @@ Section Properties. apply rts1n_rts. Qed. - (** Direct reflexive-symmetric-transitive closure is equivalent to + (** Direct reflexive-symmetric-transitive closure is equivalent to transitivity by symmetric right-step extension *) - Lemma rtsn1_rts : forall x y, + Lemma rtsn1_rts : forall x y, clos_refl_sym_trans_n1 A R x y -> clos_refl_sym_trans A R x y. Proof. induction 1. @@ -332,7 +332,7 @@ Section Properties. Qed. Lemma rtsn1_trans : forall y z, clos_refl_sym_trans_n1 A R y z-> - forall x, clos_refl_sym_trans_n1 A R x y -> + forall x, clos_refl_sym_trans_n1 A R x y -> clos_refl_sym_trans_n1 A R x z. Proof. induction 1. @@ -352,7 +352,7 @@ Section Properties. left. Qed. - Lemma rts_rtsn1 : forall x y, + Lemma rts_rtsn1 : forall x y, clos_refl_sym_trans A R x y -> clos_refl_sym_trans_n1 A R x y. Proof. induction 1. @@ -363,7 +363,7 @@ Section Properties. eapply rtsn1_trans; eauto. Qed. - Lemma rts_rtsn1_equiv : forall x y, + Lemma rts_rtsn1_equiv : forall x y, clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_n1 A R x y. Proof. split. diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 977135fab..c03c4b95f 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -11,14 +11,14 @@ Section Relation_Definition. Variable A : Type. - + Definition relation := A -> A -> Prop. Variable R : relation. - + Section General_Properties_of_Relations. - + Definition reflexive : Prop := forall x:A, R x x. Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z. Definition symmetric : Prop := forall x y:A, R x y -> R y x. @@ -32,33 +32,33 @@ Section Relation_Definition. Section Sets_of_Relations. - - Record preorder : Prop := + + Record preorder : Prop := { preord_refl : reflexive; preord_trans : transitive}. - - Record order : Prop := + + Record order : Prop := { ord_refl : reflexive; ord_trans : transitive; ord_antisym : antisymmetric}. - - Record equivalence : Prop := + + Record equivalence : Prop := { equiv_refl : reflexive; equiv_trans : transitive; equiv_sym : symmetric}. - + Record PER : Prop := {per_sym : symmetric; per_trans : transitive}. End Sets_of_Relations. Section Relations_of_Relations. - + Definition inclusion (R1 R2:relation) : Prop := forall x y:A, R1 x y -> R2 x y. - + Definition same_relation (R1 R2:relation) : Prop := inclusion R1 R2 /\ inclusion R2 R1. - + Definition commut (R1 R2:relation) : Prop := forall x y:A, R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index eec3f8ebd..2d1503f23 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -65,7 +65,7 @@ Section Reflexive_Transitive_Closure. Inductive clos_refl_trans_1n (x: A) : A -> Prop := | rt1n_refl : clos_refl_trans_1n x x - | rt1n_trans (y z:A) : + | rt1n_trans (y z:A) : R x y -> clos_refl_trans_1n y z -> clos_refl_trans_1n x z. (** Alternative definition by transitive extension on the right *) @@ -82,7 +82,7 @@ End Reflexive_Transitive_Closure. Section Reflexive_Symetric_Transitive_Closure. Variable A : Type. Variable R : relation A. - + (** Definition by direct reflexive-symmetric-transitive closure *) Inductive clos_refl_sym_trans : relation A := @@ -104,7 +104,7 @@ Section Reflexive_Symetric_Transitive_Closure. Inductive clos_refl_sym_trans_n1 (x: A) : A -> Prop := | rtsn1_refl : clos_refl_sym_trans_n1 x x - | rtsn1_trans (y z:A) : R y z \/ R z y -> + | rtsn1_trans (y z:A) : R y z \/ R z y -> clos_refl_sym_trans_n1 x y -> clos_refl_sym_trans_n1 x z. End Reflexive_Symetric_Transitive_Closure. @@ -139,7 +139,7 @@ Inductive le_AsB : A + B -> A + B -> Prop := | le_ab (x:A) (y:B) : le_AsB (inl _ x) (inr _ y) | le_bb (x y:B) : leB x y -> le_AsB (inr _ x) (inr _ y). -End Disjoint_Union. +End Disjoint_Union. (** ** Lexicographic order on dependent pairs *) @@ -189,12 +189,12 @@ End Swap. Section Lexicographic_Exponentiation. - + Variable A : Set. Variable leA : A -> A -> Prop. Let Nil := nil (A:=A). Let List := list A. - + Inductive Ltl : List -> List -> Prop := | Lt_nil (a:A) (x:List) : Ltl Nil (a :: x) | Lt_hd (a b:A) : leA a b -> forall x y:list A, Ltl (a :: x) (b :: y) @@ -207,7 +207,7 @@ Section Lexicographic_Exponentiation. leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil). Definition Pow : Set := sig Desc. - + Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b). End Lexicographic_Exponentiation. -- cgit v1.2.3