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/Sets/Classical_sets.v | 4 ++-- theories/Sets/Constructive_sets.v | 12 +++++----- theories/Sets/Cpo.v | 10 ++++---- theories/Sets/Ensembles.v | 36 ++++++++++++++-------------- theories/Sets/Finite_sets.v | 2 +- theories/Sets/Finite_sets_facts.v | 8 +++---- theories/Sets/Image.v | 24 +++++++++---------- theories/Sets/Infinite_sets.v | 12 +++++----- theories/Sets/Integers.v | 20 ++++++++-------- theories/Sets/Multiset.v | 26 ++++++++++----------- theories/Sets/Partial_Order.v | 12 +++++----- theories/Sets/Permut.v | 10 ++++---- theories/Sets/Powerset_Classical_facts.v | 30 ++++++++++++------------ theories/Sets/Powerset_facts.v | 40 ++++++++++++++++---------------- theories/Sets/Relations_1.v | 24 +++++++++---------- theories/Sets/Relations_2_facts.v | 2 +- theories/Sets/Relations_3.v | 16 ++++++------- theories/Sets/Uniset.v | 10 ++++---- 18 files changed, 149 insertions(+), 149 deletions(-) (limited to 'theories/Sets') diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 62fd4df1a..5f6860997 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -56,7 +56,7 @@ Section Ensembles_classical. forall X Y:Ensemble U, Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X). Proof. - intros X Y I NI. + intros X Y I NI. elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI). intros x YX. apply Inhabited_intro with x. @@ -78,7 +78,7 @@ Section Ensembles_classical. unfold Subtract at 1 in |- *; auto with sets. Qed. Hint Resolve Subtract_intro : sets. - + Lemma Subtract_inv : forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y. Proof. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 65ce03e28..0719365f1 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -30,7 +30,7 @@ Require Export Ensembles. Section Ensembles_facts. Variable U : Type. - + Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C. Proof. intros B C H'; rewrite H'; auto with sets. @@ -52,7 +52,7 @@ Section Ensembles_facts. Proof. unfold Add at 1 in |- *; auto with sets. Qed. - + Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x. Proof. unfold Add at 1 in |- *; auto with sets. @@ -98,15 +98,15 @@ Section Ensembles_facts. Proof. intros B C x H'; elim H'; auto with sets. Qed. - + Lemma Add_inv : forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y. Proof. - intros A x y H'; induction H'. + intros A x y H'; induction H'. left; assumption. right; apply Singleton_inv; assumption. Qed. - + Lemma Intersection_inv : forall (B C:Ensemble U) (x:U), In U (Intersection U B C) x -> In U B x /\ In U C x. @@ -125,7 +125,7 @@ Section Ensembles_facts. Proof. unfold Setminus at 1 in |- *; red in |- *; auto with sets. Qed. - + Lemma Strict_Included_intro : forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y. Proof. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index c1e64babc..8c69e6877 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -35,7 +35,7 @@ Section Bounds. Variable D : PO U. Let C := Carrier_of U D. - + Let R := Rel_of U D. Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop := @@ -45,7 +45,7 @@ Section Bounds. Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop := Lower_Bound_definition : In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x. - + Inductive Lub (B:Ensemble U) (x:U) : Prop := Lub_definition : Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x. @@ -57,7 +57,7 @@ Section Bounds. Inductive Bottom (bot:U) : Prop := Bottom_definition : In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot. - + Inductive Totally_ordered (B:Ensemble U) : Prop := Totally_ordered_definition : (Included U B C -> @@ -77,7 +77,7 @@ Section Bounds. Included U (Couple U x1 x2) X -> exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) -> Directed X. - + Inductive Complete : Prop := Definition_of_Complete : (exists bot : _, Bottom bot) -> @@ -102,7 +102,7 @@ Section Specific_orders. Record Cpo : Type := Definition_of_cpo {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}. - + Record Chain : Type := Definition_of_chain {PO_of_chain : PO U; Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}. diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 339298572..0fa9c74a8 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -28,23 +28,23 @@ Section Ensembles. Variable U : Type. - - Definition Ensemble := U -> Prop. + + Definition Ensemble := U -> Prop. Definition In (A:Ensemble) (x:U) : Prop := A x. - + Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x. - + Inductive Empty_set : Ensemble :=. - + Inductive Full_set : Ensemble := Full_intro : forall x:U, In Full_set x. -(** NB: The following definition builds-in equality of elements in [U] as - Leibniz equality. +(** NB: The following definition builds-in equality of elements in [U] as + Leibniz equality. - This may have to be changed if we replace [U] by a Setoid on [U] - with its own equality [eqs], with + This may have to be changed if we replace [U] by a Setoid on [U] + with its own equality [eqs], with [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *) Inductive Singleton (x:U) : Ensemble := @@ -55,7 +55,7 @@ Section Ensembles. | Union_intror : forall x:U, In C x -> In (Union B C) x. Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x). - + Inductive Intersection (B C:Ensemble) : Ensemble := Intersection_intro : forall x:U, In B x -> In C x -> In (Intersection B C) x. @@ -63,29 +63,29 @@ Section Ensembles. Inductive Couple (x y:U) : Ensemble := | Couple_l : In (Couple x y) x | Couple_r : In (Couple x y) y. - + Inductive Triple (x y z:U) : Ensemble := | Triple_l : In (Triple x y z) x | Triple_m : In (Triple x y z) y | Triple_r : In (Triple x y z) z. - + Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x. - + Definition Setminus (B C:Ensemble) : Ensemble := fun x:U => In B x /\ ~ In C x. - + Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x). - + Inductive Disjoint (B C:Ensemble) : Prop := Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C. Inductive Inhabited (B:Ensemble) : Prop := Inhabited_intro : forall x:U, In B x -> Inhabited B. - + Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C. - + Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B. - + (** Extensionality Axiom *) Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B. diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index a75c3b767..019c25a55 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -52,7 +52,7 @@ Require Import Constructive_sets. Section Ensembles_finis_facts. Variable U : Type. - + Lemma cardinal_invert : forall (X:Ensemble U) (p:nat), cardinal U X p -> diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 0615c9c9d..fdcc4150f 100644 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -72,7 +72,7 @@ Section Finite_sets_facts. Proof. intros X Y H; induction H as [|A Fin_A Hind x]. rewrite (Empty_set_zero U Y). trivial. - intros. + intros. rewrite (Union_commutative U (Add U A x) Y). rewrite <- (Union_add U Y A x). rewrite (Union_commutative U Y A). @@ -98,7 +98,7 @@ Section Finite_sets_facts. Proof. intros A H' X; apply Finite_downward_closed with A; auto with sets. Qed. - + Lemma cardinalO_empty : forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U. Proof. @@ -212,7 +212,7 @@ Section Finite_sets_facts. Proof. intros; apply cardinal_is_functional with X X; auto with sets. Qed. - + Lemma card_Add_gen : forall (A:Ensemble U) (x:U) (n n':nat), cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n. @@ -279,7 +279,7 @@ Section Finite_sets_facts. intro E; rewrite E; auto with sets arith. apply cardinal_unicity with X; auto with sets arith. Qed. - + Lemma G_aux : forall P:Ensemble U -> Prop, (forall X:Ensemble U, diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index da3aec320..64c341bd3 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -40,10 +40,10 @@ Require Export Finite_sets_facts. Section Image. Variables U V : Type. - + Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V := Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y. - + Lemma Im_def : forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x). Proof. @@ -62,13 +62,13 @@ Section Image. rewrite H0. elim Add_inv with U X x x1; auto using Im_def with sets. destruct 1; auto using Im_def with sets. - elim Add_inv with V (Im X f) (f x) x0. + elim Add_inv with V (Im X f) (f x) x0. destruct 1 as [x0 H y H0]. rewrite H0; auto using Im_def with sets. destruct 1; auto using Im_def with sets. trivial. Qed. - + Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V. Proof. intro f; try assumption. @@ -88,7 +88,7 @@ Section Image. rewrite (Im_add A x f); auto with sets. apply Add_preserves_Finite; auto with sets. Qed. - + Lemma Im_inv : forall (X:Ensemble U) (f:U -> V) (y:V), In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y. @@ -97,9 +97,9 @@ Section Image. intros x H'0 y0 H'1; rewrite H'1. exists x; auto with sets. Qed. - + Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y. - + Lemma not_injective_elim : forall f:U -> V, ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y). @@ -115,7 +115,7 @@ Section Image. destruct 1 as [y D]; exists y. apply imply_to_and; trivial with sets. Qed. - + Lemma cardinal_Im_intro : forall (A:Ensemble U) (f:U -> V) (n:nat), cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p. @@ -124,7 +124,7 @@ Section Image. apply finite_cardinal; apply finite_image. apply cardinal_finite with n; trivial with sets. Qed. - + Lemma In_Image_elim : forall (A:Ensemble U) (f:U -> V), injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x. @@ -134,7 +134,7 @@ Section Image. intros z C; elim C; intros InAz E. elim (H z x E); trivial with sets. Qed. - + Lemma injective_preserves_cardinal : forall (A:Ensemble U) (f:U -> V) (n:nat), injective f -> @@ -158,7 +158,7 @@ Section Image. red in |- *; intro; apply H'2. apply In_Image_elim with f; trivial with sets. Qed. - + Lemma cardinal_decreases : forall (A:Ensemble U) (f:U -> V) (n:nat), cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n. @@ -188,7 +188,7 @@ Section Image. apply injective_preserves_cardinal with (A := A) (f := f) (n := n); trivial with sets. Qed. - + Lemma Pigeonhole_principle : forall (A:Ensemble U) (f:U -> V) (n:nat), cardinal _ A n -> diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index 6b02e8383..b63ec1d47 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -50,7 +50,7 @@ Hint Resolve Defn_of_Approximant. Section Infinite_sets. Variable U : Type. - + Lemma make_new_approximant : forall A X:Ensemble U, ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X). @@ -61,7 +61,7 @@ Section Infinite_sets. red in |- *; intro H'3; apply H'. rewrite <- H'3; auto with sets. Qed. - + Lemma approximants_grow : forall A X:Ensemble U, ~ Finite U A -> @@ -101,7 +101,7 @@ Section Infinite_sets. apply Defn_of_Approximant; auto with sets. apply cardinal_finite with (n := S n0); auto with sets. Qed. - + Lemma approximants_grow' : forall A X:Ensemble U, ~ Finite U A -> @@ -121,7 +121,7 @@ Section Infinite_sets. apply cardinal_finite with (n := S n); auto with sets. apply approximants_grow with (X := X); auto with sets. Qed. - + Lemma approximant_can_be_any_size : forall A X:Ensemble U, ~ Finite U A -> @@ -135,7 +135,7 @@ Section Infinite_sets. Qed. Variable V : Type. - + Theorem Image_set_continuous : forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), Finite V X -> @@ -230,7 +230,7 @@ Section Infinite_sets. rewrite H'4; auto with sets. elim H'3; auto with sets. Qed. - + Theorem Pigeonhole_ter : forall (A:Ensemble U) (f:U -> V) (n:nat), injective U V f -> Finite V (Im U V A f) -> Finite U A. diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index ec44a6e58..443713211 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -45,7 +45,7 @@ Require Export Partial_Order. Require Export Cpo. Section Integers_sect. - + Inductive Integers : Ensemble nat := Integers_defn : forall x:nat, In nat Integers x. @@ -53,7 +53,7 @@ Section Integers_sect. Proof. red in |- *; auto with arith. Qed. - + Lemma le_antisym : Antisymmetric nat le. Proof. red in |- *; intros x y H H'; rewrite (le_antisym x y); auto. @@ -63,12 +63,12 @@ Section Integers_sect. Proof. red in |- *; intros; apply le_trans with y; auto. Qed. - + Lemma le_Order : Order nat le. Proof. - split; [exact le_reflexive | exact le_trans | exact le_antisym]. + split; [exact le_reflexive | exact le_trans | exact le_antisym]. Qed. - + Lemma triv_nat : forall n:nat, In nat Integers n. Proof. exact Integers_defn. @@ -77,11 +77,11 @@ Section Integers_sect. Definition nat_po : PO nat. apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le); auto with sets arith. - apply Inhabited_intro with (x := 0). + apply Inhabited_intro with (x := 0). apply Integers_defn. exact le_Order. Defined. - + Lemma le_total_order : Totally_ordered nat nat_po Integers. Proof. apply Totally_ordered_definition. @@ -92,7 +92,7 @@ Section Integers_sect. intro H'1; right. cut (y <= x); auto with sets arith. Qed. - + Lemma Finite_subset_has_lub : forall X:Ensemble nat, Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m. @@ -124,7 +124,7 @@ Section Integers_sect. apply H'4 with (y := x0). elim H'3; simpl in |- *; auto with sets arith. trivial. intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial. exists x0. - apply Upper_Bound_definition. + apply Upper_Bound_definition. unfold nat_po. simpl. apply triv_nat. intros y H'1; elim H'1. intros x1 H'4; try assumption. @@ -148,7 +148,7 @@ Section Integers_sect. absurd (S x <= x); auto with arith. apply triv_nat. Qed. - + Lemma Integers_infinite : ~ Finite nat Integers. Proof. generalize Integers_has_no_ub. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 42130bbb5..75b9f2efa 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -22,7 +22,7 @@ Section multiset_defs. Inductive multiset : Type := Bag : (A -> nat) -> multiset. - + Definition EmptyBag := Bag (fun a:A => 0). Definition SingletonBag (a:A) := Bag (fun a':A => match Aeq_dec a a' with @@ -31,23 +31,23 @@ Section multiset_defs. end). Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a. - + (** multiset equality *) Definition meq (m1 m2:multiset) := forall a:A, multiplicity m1 a = multiplicity m2 a. - + Lemma meq_refl : forall x:multiset, meq x x. Proof. destruct x; unfold meq; reflexivity. Qed. - + Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z. Proof. unfold meq in |- *. destruct x; destruct y; destruct z. intros; rewrite H; auto. Qed. - + Lemma meq_sym : forall x y:multiset, meq x y -> meq y x. Proof. unfold meq in |- *. @@ -62,7 +62,7 @@ Section multiset_defs. Proof. unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. Qed. - + Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag). Proof. unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. @@ -70,7 +70,7 @@ Section multiset_defs. Require Plus. (* comm. and ass. of plus *) - + Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). Proof. unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *. @@ -106,28 +106,28 @@ Section multiset_defs. Lemma munion_rotate : forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)). Proof. - intros; apply (op_rotate multiset munion meq). + intros; apply (op_rotate multiset munion meq). apply munion_comm. apply munion_ass. exact meq_trans. exact meq_sym. trivial. Qed. - + Lemma meq_congr : forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t). Proof. intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right. exact meq_trans. Qed. - + Lemma munion_perm_left : forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)). Proof. intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym. exact meq_trans. Qed. - + Lemma multiset_twist1 : forall x y z t:multiset, meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z). @@ -156,7 +156,7 @@ Section multiset_defs. apply meq_right; apply meq_left; trivial. apply multiset_twist1. Qed. - + Lemma treesort_twist2 : forall x y z t u:multiset, meq u (munion y z) -> @@ -168,7 +168,7 @@ Section multiset_defs. Qed. -(*i theory of minter to do similarly +(*i theory of minter to do similarly Require Min. (* multiset intersection *) Definition minter := [m1,m2:multiset] diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 8589f387e..4fe8f4f6a 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -31,20 +31,20 @@ Require Export Relations_1. Section Partial_orders. Variable U : Type. - + Definition Carrier := Ensemble U. - + Definition Rel := Relation U. - + Record PO : Type := Definition_of_PO { Carrier_of : Ensemble U; Rel_of : Relation U; PO_cond1 : Inhabited U Carrier_of; PO_cond2 : Order U Rel_of }. Variable p : PO. - + Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y. - + Inductive covers (y x:U) : Prop := Definition_of_covers : Strict_Rel_of x y -> @@ -60,7 +60,7 @@ Hint Resolve Definition_of_covers: sets v62. Section Partial_order_facts. Variable U : Type. Variable D : PO U. - + Lemma Strict_Rel_Transitive_with_Rel : forall x y z:U, Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z. diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 6c9a064c1..f593031a0 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -36,23 +36,23 @@ Section Axiomatisation. apply cong_left; trivial. apply cong_right; trivial. Qed. - + Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)). Proof. intros; apply cong_right; apply op_comm. Qed. - + Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z). Proof. intros; apply cong_left; apply op_comm. Qed. - + Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y). Proof. intros. apply cong_trans with (op x (op y z)). apply op_ass. - apply cong_trans with (op x (op z y)). + apply cong_trans with (op x (op z y)). apply cong_right; apply op_comm. apply cong_sym; apply op_ass. Qed. @@ -66,7 +66,7 @@ Section Axiomatisation. apply cong_left; apply op_comm. apply op_ass. Qed. - + Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)). Proof. intros; apply cong_trans with (op (op x y) z). diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 8116045b6..36d2150c3 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -40,7 +40,7 @@ Require Export Classical_sets. Section Sets_as_an_algebra. Variable U : Type. - + Lemma sincl_add_x : forall (A B:Ensemble U) (x:U), ~ In U A x -> @@ -63,7 +63,7 @@ Section Sets_as_an_algebra. intros X x H'; red in |- *. intros x0 H'0; elim H'0; auto with sets. Qed. - + Lemma incl_soustr : forall (X Y:Ensemble U) (x:U), Included U X Y -> Included U (Subtract U X x) (Subtract U Y x). @@ -73,7 +73,7 @@ Section Sets_as_an_algebra. intros H'1 H'2. apply Subtract_intro; auto with sets. Qed. - + Lemma incl_soustr_add_l : forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X. Proof. @@ -93,7 +93,7 @@ Section Sets_as_an_algebra. red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets. Qed. Hint Resolve incl_soustr_add_r: sets v62. - + Lemma add_soustr_2 : forall (X:Ensemble U) (x:U), In U X x -> Included U X (Add U (Subtract U X x) x). @@ -103,7 +103,7 @@ Section Sets_as_an_algebra. elim (classic (x = x0)); intro K; auto with sets. elim K; auto with sets. Qed. - + Lemma add_soustr_1 : forall (X:Ensemble U) (x:U), In U X x -> Included U (Add U (Subtract U X x) x) X. @@ -114,7 +114,7 @@ Section Sets_as_an_algebra. intros t H'1; try assumption. rewrite <- (Singleton_inv U x t); auto with sets. Qed. - + Lemma add_soustr_xy : forall (X:Ensemble U) (x y:U), x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x. @@ -133,7 +133,7 @@ Section Sets_as_an_algebra. intro H'0; elim H'0; auto with sets. intro H'0; rewrite <- H'0; auto with sets. Qed. - + Lemma incl_st_add_soustr : forall (X Y:Ensemble U) (x:U), ~ In U X x -> @@ -151,13 +151,13 @@ Section Sets_as_an_algebra. red in |- *; intro H'0; apply H'2. rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets. Qed. - + Lemma Sub_Add_new : forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x. Proof. auto using incl_soustr_add_l with sets. Qed. - + Lemma Simplify_add : forall (X X0:Ensemble U) (x:U), ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0. @@ -167,7 +167,7 @@ Section Sets_as_an_algebra. rewrite (Sub_Add_new X0 x); auto with sets. rewrite H'1; auto with sets. Qed. - + Lemma Included_Add : forall (X A:Ensemble U) (x:U), Included U X (Add U A x) -> @@ -201,7 +201,7 @@ Section Sets_as_an_algebra. absurd (In U X x0); auto with sets. rewrite <- H'5; auto with sets. Qed. - + Lemma setcover_inv : forall A x y:Ensemble U, covers (Ensemble U) (Power_set_PO U A) y x -> @@ -219,7 +219,7 @@ Section Sets_as_an_algebra. elim H'1. exists z; auto with sets. Qed. - + Theorem Add_covers : forall A a:Ensemble U, Included U a A -> @@ -255,7 +255,7 @@ Section Sets_as_an_algebra. intros x1 H'10; elim H'10; auto with sets. intros x2 H'11; elim H'11; auto with sets. Qed. - + Theorem covers_Add : forall A a a':Ensemble U, Included U a A -> @@ -301,7 +301,7 @@ Section Sets_as_an_algebra. intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1. apply Add_covers; intuition. Qed. - + Theorem Singleton_atomic : forall (x:U) (A:Ensemble U), In U A x -> @@ -311,7 +311,7 @@ Section Sets_as_an_algebra. rewrite <- (Empty_set_zero' U x). apply Add_covers; auto with sets. Qed. - + Lemma less_than_singleton : forall (X:Ensemble U) (x:U), Strict_Included U X (Singleton U x) -> X = Empty_set U. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index dee4af65a..76f7f1ec8 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -41,34 +41,34 @@ Section Sets_as_an_algebra. Proof. auto 6 with sets. Qed. - + Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. Proof. unfold Add at 1 in |- *; auto using Empty_set_zero with sets. Qed. - + Lemma less_than_empty : forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U. Proof. auto with sets. Qed. - + Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A. Proof. auto with sets. Qed. - + Theorem Union_associative : forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C). Proof. auto 9 with sets. Qed. - + Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A. Proof. auto 7 with sets. Qed. - + Lemma Union_absorbs : forall A B:Ensemble U, Included U B A -> Union U A B = A. Proof. @@ -82,7 +82,7 @@ Section Sets_as_an_algebra. intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets). intros x0 H'; elim H'; auto with sets. Qed. - + Theorem Triple_as_union : forall x y z:U, Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) = @@ -94,7 +94,7 @@ Section Sets_as_an_algebra. intros x1 H'0; elim H'0; auto with sets. intros x0 H'; elim H'; auto with sets. Qed. - + Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y. Proof. intros x y. @@ -102,7 +102,7 @@ Section Sets_as_an_algebra. rewrite <- (Union_idempotent (Singleton U x)). apply Triple_as_union. Qed. - + Theorem Triple_as_Couple_Singleton : forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z). Proof. @@ -110,7 +110,7 @@ Section Sets_as_an_algebra. rewrite <- (Triple_as_union x y z). rewrite <- (Couple_as_union x y); auto with sets. Qed. - + Theorem Intersection_commutative : forall A B:Ensemble U, Intersection U A B = Intersection U B A. Proof. @@ -118,7 +118,7 @@ Section Sets_as_an_algebra. apply Extensionality_Ensembles. split; red in |- *; intros x H'; elim H'; auto with sets. Qed. - + Theorem Distributivity : forall A B C:Ensemble U, Intersection U A (Union U B C) = @@ -132,7 +132,7 @@ Section Sets_as_an_algebra. elim H'1; auto with sets. elim H'; intros x0 H'0; elim H'0; auto with sets. Qed. - + Theorem Distributivity' : forall A B C:Ensemble U, Union U A (Intersection U B C) = @@ -149,13 +149,13 @@ Section Sets_as_an_algebra. generalize H'1. elim H'2; auto with sets. Qed. - + Theorem Union_add : forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x). Proof. unfold Add in |- *; auto using Union_associative with sets. Qed. - + Theorem Non_disjoint_union : forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X. Proof. @@ -165,7 +165,7 @@ Section Sets_as_an_algebra. intros x0 H'0; elim H'0; auto with sets. intros t H'1; elim H'1; auto with sets. Qed. - + Theorem Non_disjoint_union' : forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X. Proof. @@ -178,12 +178,12 @@ Section Sets_as_an_algebra. lapply (Singleton_inv U x x0); auto with sets. intro H'4; apply H'; rewrite H'4; auto with sets. Qed. - + Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y. Proof. intro x; rewrite (Empty_set_zero' x); auto with sets. Qed. - + Lemma incl_add : forall (A B:Ensemble U) (x:U), Included U A B -> Included U (Add U A x) (Add U B x). @@ -209,7 +209,7 @@ Section Sets_as_an_algebra. absurd (In U A x0); auto with sets. rewrite <- H'4; auto with sets. Qed. - + Lemma Add_commutative : forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x. Proof. @@ -220,7 +220,7 @@ Section Sets_as_an_algebra. rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); auto with sets. Qed. - + Lemma Add_commutative' : forall (A:Ensemble U) (x y z:U), Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y. @@ -229,7 +229,7 @@ Section Sets_as_an_algebra. rewrite (Add_commutative (Add U A x) y z). rewrite (Add_commutative A x z); auto with sets. Qed. - + Lemma Add_distributes : forall (A B:Ensemble U) (x y:U), Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y). diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index f15bf19e6..85d0cffcc 100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -28,38 +28,38 @@ Section Relations_1. Variable U : Type. - + Definition Relation := U -> U -> Prop. Variable R : Relation. - + Definition Reflexive : Prop := forall x:U, R x x. - + Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z. - + Definition Symmetric : Prop := forall x y:U, R x y -> R y x. - + Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y. - + Definition contains (R R':Relation) : Prop := forall x y:U, R' x y -> R x y. - + Definition same_relation (R R':Relation) : Prop := contains R R' /\ contains R' R. - + Inductive Preorder : Prop := Definition_of_preorder : Reflexive -> Transitive -> Preorder. - + Inductive Order : Prop := Definition_of_order : Reflexive -> Transitive -> Antisymmetric -> Order. - + Inductive Equivalence : Prop := Definition_of_equivalence : Reflexive -> Transitive -> Symmetric -> Equivalence. - + Inductive PER : Prop := Definition_of_PER : Symmetric -> Transitive -> PER. - + End Relations_1. Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains same_relation: sets v62. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index d5257c12c..3554901b9 100644 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -140,7 +140,7 @@ intros U R H' x b H'0; elim H'0. intros x0 a H'1; exists a; auto with sets. intros x0 y z H'1 H'2 H'3 a H'4. red in H'. -specialize H' with (x := x0) (a := a) (b := y); lapply H'; +specialize H' with (x := x0) (a := a) (b := y); lapply H'; [ intro H'8; lapply H'8; [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ] | clear H' ]; auto with sets. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index ec8fb7e6d..970db1827 100644 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -32,26 +32,26 @@ Require Export Relations_2. Section Relations_3. Variable U : Type. Variable R : Relation U. - + Definition coherent (x y:U) : Prop := exists z : _, Rstar U R x z /\ Rstar U R y z. - + Definition locally_confluent (x:U) : Prop := forall y z:U, R x y -> R x z -> coherent y z. - + Definition Locally_confluent : Prop := forall x:U, locally_confluent x. - + Definition confluent (x:U) : Prop := forall y z:U, Rstar U R x y -> Rstar U R x z -> coherent y z. - + Definition Confluent : Prop := forall x:U, confluent x. - + Inductive noetherian (x: U) : Prop := definition_of_noetherian : (forall y:U, R x y -> noetherian y) -> noetherian x. - + Definition Noetherian : Prop := forall x:U, noetherian x. - + End Relations_3. Hint Unfold coherent: sets v62. Hint Unfold locally_confluent: sets v62. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 03dc55ef9..909c79838 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -90,10 +90,10 @@ Qed. Definition union (m1 m2:uniset) := Charac (fun a:A => orb (charac m1 a) (charac m2 a)). -Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). -Proof. -unfold seq in |- *; unfold union in |- *; simpl in |- *; auto. -Qed. +Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). +Proof. +unfold seq in |- *; unfold union in |- *; simpl in |- *; auto. +Qed. Hint Resolve union_empty_left. Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset). @@ -203,7 +203,7 @@ apply uniset_twist2. Qed. -(*i theory of minter to do similarly +(*i theory of minter to do similarly Require Min. (* uniset intersection *) Definition minter := [m1,m2:uniset] -- cgit v1.2.3