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/Wellfounded/Disjoint_Union.v | 8 +-- theories/Wellfounded/Inclusion.v | 2 +- theories/Wellfounded/Inverse_Image.v | 4 +- .../Wellfounded/Lexicographic_Exponentiation.v | 78 +++++++++++----------- theories/Wellfounded/Lexicographic_Product.v | 26 ++++---- theories/Wellfounded/Transitive_Closure.v | 2 +- theories/Wellfounded/Union.v | 10 +-- theories/Wellfounded/Well_Ordering.v | 6 +- 8 files changed, 68 insertions(+), 68 deletions(-) (limited to 'theories/Wellfounded') diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index f6ce84f98..785d623b4 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -9,8 +9,8 @@ (*i $Id$ i*) (** Author: Cristina Cornes - From : Constructing Recursion Operators in Type Theory - L. Paulson JSC (1986) 2, 325-355 *) + From : Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) Require Import Relation_Operators. @@ -20,7 +20,7 @@ Section Wf_Disjoint_Union. Variable leB : B -> B -> Prop. Notation Le_AsB := (le_AsB A B leA leB). - + Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x). Proof. induction 1. @@ -47,7 +47,7 @@ Section Wf_Disjoint_Union. destruct a as [a| b]. apply (acc_A_sum a). apply (H a). - + apply (acc_B_sum H b). apply (H0 b). Qed. diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index e72b1e11d..01049989e 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -21,7 +21,7 @@ Section WfInclusion. induction 2. apply Acc_intro; auto with sets. Qed. - + Hint Resolve Acc_incl. Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index df6a61198..c57e70725 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -47,8 +47,8 @@ Section Inverse_Image. destruct H3. apply (IHAcc x1); auto. Qed. - - + + Theorem wf_inverse_rel : well_founded R -> well_founded RoF. Proof. red in |- *; constructor; intros. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 69421255d..ff1889000 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -10,7 +10,7 @@ (** Author: Cristina Cornes - From : Constructing Recursion Operators in Type Theory + From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355 *) Require Import List. @@ -20,12 +20,12 @@ Require Import Transitive_Closure. Section Wf_Lexicographic_Exponentiation. Variable A : Set. Variable leA : A -> A -> Prop. - + Notation Power := (Pow A leA). Notation Lex_Exp := (lex_exp A leA). Notation ltl := (Ltl A leA). Notation Descl := (Desc A leA). - + Notation List := (list A). Notation Nil := (nil (A:=A)). (* useless but symmetric *) @@ -33,13 +33,13 @@ Section Wf_Lexicographic_Exponentiation. Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100). (* Hint Resolve d_one d_nil t_step. *) - + Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z. Proof. simple induction x. simple induction z. simpl in |- *; intros H. - inversion_clear H. + inversion_clear H. simpl in |- *; intros; apply (Lt_nil A leA). intros a l HInd. simpl in |- *. @@ -71,12 +71,12 @@ Section Wf_Lexicographic_Exponentiation. rewrite H8. right; exists x2; auto with sets. Qed. - + Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x. Proof. intros. inversion H. - generalize (app_cons_not_nil _ _ _ H1); simple induction 1. + generalize (app_cons_not_nil _ _ _ H1); simple induction 1. cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets. intro. generalize (app_eq_unit _ _ H0). @@ -87,7 +87,7 @@ Section Wf_Lexicographic_Exponentiation. simple induction 1; intros. rewrite <- H4; auto with sets. Qed. - + Lemma desc_tail : forall (x:List) (a b:A), Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b. @@ -99,7 +99,7 @@ Section Wf_Lexicographic_Exponentiation. forall a b:A, Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b). intros. - + inversion H. cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil); auto with sets; intro. @@ -108,17 +108,17 @@ Section Wf_Lexicographic_Exponentiation. generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4); simple induction 1. intros. - + generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros. generalize H1. rewrite <- H10; rewrite <- H7; intro. apply (t_step A leA); auto with sets. - + intros. inversion H0. generalize (app_cons_not_nil _ _ _ H3); intro. elim H1. - + generalize H0. generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b); simple induction 1. @@ -127,11 +127,11 @@ Section Wf_Lexicographic_Exponentiation. generalize (H x0 b H6). intro. apply t_trans with (A := A) (y := x0); auto with sets. - + apply t_step. generalize H1. rewrite H4; intro. - + generalize (app_inj_tail _ _ _ _ H8); simple induction 1. intros. generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b). @@ -154,7 +154,7 @@ Section Wf_Lexicographic_Exponentiation. generalize (app_eq_nil _ _ H0); simple induction 1. intros. rewrite H2; rewrite H3; split; apply d_nil. - + intros. cut (x0 ++ y = Cons x Nil); auto with sets. intros E. @@ -162,15 +162,15 @@ Section Wf_Lexicographic_Exponentiation. simple induction 1; intros. rewrite H2; rewrite H3; split. apply d_nil. - + apply d_one. - + simple induction 1; intros. rewrite H2; rewrite H3; split. apply d_one. - + apply d_nil. - + do 5 intro. intros Hind. do 2 intro. @@ -181,13 +181,13 @@ Section Wf_Lexicographic_Exponentiation. forall x0:List, (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ y0 -> Descl x0 /\ Descl y0). - + intro. generalize (app_nil_end x1); simple induction 1; simple induction 1. split. apply d_conc; auto with sets. - + apply d_nil. - + do 3 intro. generalize x1. apply rev_ind with @@ -202,7 +202,7 @@ Section Wf_Lexicographic_Exponentiation. split. generalize (app_inj_tail _ _ _ _ H2); simple induction 1. simple induction 1; auto with sets. - + apply d_one. do 5 intro. generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)). @@ -219,7 +219,7 @@ Section Wf_Lexicographic_Exponentiation. generalize (Hind x4 (l1 ++ Cons x2 Nil) H11). simple induction 1; split. auto with sets. - + generalize H14. rewrite <- H10; intro. apply d_conc; auto with sets. @@ -233,11 +233,11 @@ Section Wf_Lexicographic_Exponentiation. intros. apply (dist_aux (x ++ y) H x y); auto with sets. Qed. - + Lemma desc_end : forall (a b:A) (x:List), Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) -> - clos_trans A leA a b. + clos_trans A leA a b. Proof. intros a b x. case x. @@ -246,14 +246,14 @@ Section Wf_Lexicographic_Exponentiation. intros. inversion H1; auto with sets. inversion H3. - + simple induction 1. generalize (app_comm_cons l (Cons a Nil) a0). intros E; rewrite <- E; intros. generalize (desc_tail l a a0 H0); intro. inversion H1. apply t_trans with (y := a0); auto with sets. - + inversion H4. Qed. @@ -268,15 +268,15 @@ Section Wf_Lexicographic_Exponentiation. intro. case x. intros; apply (Lt_nil A leA). - + simpl in |- *; intros. inversion_clear H0. apply (Lt_hd A leA a b); auto with sets. - + inversion_clear H1. Qed. - - + + Lemma acc_app : forall (x1 x2:List) (y1:Descl (x1 ++ x2)), Acc Lex_Exp << x1 ++ x2, y1 >> -> @@ -285,11 +285,11 @@ Section Wf_Lexicographic_Exponentiation. intros. apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)). auto with sets. - + unfold lex_exp in |- *; simpl in |- *; auto with sets. Qed. - - + + Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp. Proof. unfold well_founded at 2 in |- *. @@ -303,7 +303,7 @@ Section Wf_Lexicographic_Exponentiation. forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>). intros. inversion_clear H0. - + intro. generalize (well_founded_ind (wf_clos_trans A leA H)). intros GR. @@ -318,7 +318,7 @@ Section Wf_Lexicographic_Exponentiation. generalize (right_prefix x2 l (Cons x1 Nil) H1). simple induction 1. intro; apply (H0 x2 y1 H3). - + simple induction 1. intro; simple induction 1. clear H4 H2. @@ -340,8 +340,8 @@ Section Wf_Lexicographic_Exponentiation. unfold lex_exp at 1 in |- *. simpl in |- *; intros x4 y3. intros. apply (H0 x4 y3); auto with sets. - - intros. + + intros. generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1). simple induction 1. intros. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index f41b6e93d..5144c0bee 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -14,7 +14,7 @@ Require Import Eqdep. Require Import Relation_Operators. Require Import Transitive_Closure. -(** From : Constructing Recursion Operators in Type Theory +(** From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355 *) Section WfLexicographic_Product. @@ -24,7 +24,7 @@ Section WfLexicographic_Product. Variable leB : forall x:A, B x -> B x -> Prop. Notation LexProd := (lexprod A B leA leB). - + Lemma acc_A_B_lexprod : forall x:A, Acc leA x -> @@ -41,16 +41,16 @@ Section WfLexicographic_Product. intros. apply H2. apply t_trans with x2; auto with sets. - + red in H2. apply H2. auto with sets. - + injection H1. destruct 2. injection H3. destruct 2; auto with sets. - + rewrite <- H1. injection H3; intros _ Hx1. subst x1. @@ -105,7 +105,7 @@ End Wf_Symmetric_Product. Section Swap. - + Variable A : Type. Variable R : A -> A -> Prop. @@ -121,13 +121,13 @@ Section Swap. inversion_clear H; inversion_clear H1; apply H0. apply sp_swap. apply right_sym; auto with sets. - + apply sp_swap. apply left_sym; auto with sets. - + apply sp_noswap. apply right_sym; auto with sets. - + apply sp_noswap. apply left_sym; auto with sets. Qed. @@ -147,20 +147,20 @@ Section Swap. destruct y; intro H5. inversion_clear H5. inversion_clear H0; auto with sets. - + apply swap_Acc. inversion_clear H0; auto with sets. - + intros. apply IHAcc1; auto with sets; intros. apply Acc_inv with (y0, x1); auto with sets. apply sp_noswap. apply right_sym; auto with sets. - + auto with sets. Qed. - + Lemma wf_swapprod : well_founded R -> well_founded SwapProd. Proof. red in |- *. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 5e33da5ff..bce32af48 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -18,7 +18,7 @@ Section Wf_Transitive_Closure. Variable R : relation A. Notation trans_clos := (clos_trans A R). - + Lemma incl_clos_trans : inclusion A R trans_clos. red in |- *; auto with sets. Qed. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index ebf4ba98e..fbb3d9e3c 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -17,9 +17,9 @@ Require Import Transitive_Closure. Section WfUnion. Variable A : Type. Variables R1 R2 : relation A. - + Notation Union := (union A R1 R2). - + Remark strip_commut : commut A R1 R2 -> forall x y:A, @@ -29,7 +29,7 @@ Section WfUnion. induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros. elim H with y x z; auto with sets; intros x0 H2 H3. exists x0; auto with sets. - + elim IH1 with z0; auto with sets; intros. elim IH2 with x0; auto with sets; intros. exists x1; auto with sets. @@ -50,7 +50,7 @@ Section WfUnion. elim H8; intros. apply H6; auto with sets. apply t_trans with x0; auto with sets. - + elim strip_commut with x x0 y0; auto with sets; intros. apply Acc_inv_trans with x1; auto with sets. unfold union in |- *. @@ -63,7 +63,7 @@ Section WfUnion. apply Acc_intro; auto with sets. Qed. - + Theorem wf_union : commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union. Proof. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index 7296897ef..e11b89248 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -16,15 +16,15 @@ Require Import Eqdep. Section WellOrdering. Variable A : Type. - Variable B : A -> Type. - + Variable B : A -> Type. + Inductive WO : Type := sup : forall (a:A) (f:B a -> WO), WO. Inductive le_WO : WO -> WO -> Prop := le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f). - + Theorem wf_WO : well_founded le_WO. Proof. unfold well_founded in |- *; intro. -- cgit v1.2.3