From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 29 Nov 2003 17:28:49 +0000 Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sets/Classical_sets.v | 125 ++++---- theories/Sets/Constructive_sets.v | 145 +++++---- theories/Sets/Cpo.v | 110 +++---- theories/Sets/Ensembles.v | 85 +++--- theories/Sets/Finite_sets.v | 61 ++-- theories/Sets/Finite_sets_facts.v | 498 ++++++++++++++++--------------- theories/Sets/Image.v | 244 +++++++-------- theories/Sets/Infinite_sets.v | 330 ++++++++++---------- theories/Sets/Integers.v | 167 +++++------ theories/Sets/Multiset.v | 181 +++++------ theories/Sets/Partial_Order.v | 102 +++---- theories/Sets/Permut.v | 86 +++--- theories/Sets/Powerset.v | 228 +++++++------- theories/Sets/Powerset_Classical_facts.v | 486 +++++++++++++++--------------- theories/Sets/Powerset_facts.v | 286 +++++++++--------- theories/Sets/Relations_1.v | 42 +-- theories/Sets/Relations_1_facts.v | 97 +++--- theories/Sets/Relations_2.v | 34 +-- theories/Sets/Relations_2_facts.v | 152 +++++----- theories/Sets/Relations_3.v | 41 ++- theories/Sets/Relations_3_facts.v | 216 +++++++------- theories/Sets/Uniset.v | 201 +++++++------ 22 files changed, 1980 insertions(+), 1937 deletions(-) (limited to 'theories/Sets') diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index cd72483a3..e2d707367 100755 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -33,101 +33,100 @@ Require Export Classical_Type. (* Hints Unfold not . *) Section Ensembles_classical. -Variable U: Type. +Variable U : Type. -Lemma not_included_empty_Inhabited: - (A: (Ensemble U)) ~ (Included U A (Empty_set U)) -> (Inhabited U A). +Lemma not_included_empty_Inhabited : + forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A. Proof. -Intros A NI. -Elim (not_all_ex_not U [x:U]~(In U A x)). -Intros x H; Apply Inhabited_intro with x. -Apply NNPP; Auto with sets. -Red; Intro. -Apply NI; Red. -Intros x H'; Elim (H x); Trivial with sets. +intros A NI. +elim (not_all_ex_not U (fun x:U => ~ In U A x)). +intros x H; apply Inhabited_intro with x. +apply NNPP; auto with sets. +red in |- *; intro. +apply NI; red in |- *. +intros x H'; elim (H x); trivial with sets. Qed. -Hints Resolve not_included_empty_Inhabited. +Hint Resolve not_included_empty_Inhabited. -Lemma not_empty_Inhabited: - (A: (Ensemble U)) ~ A == (Empty_set U) -> (Inhabited U A). +Lemma not_empty_Inhabited : + forall A:Ensemble U, A <> Empty_set U -> Inhabited U A. Proof. -Intros; Apply not_included_empty_Inhabited. -Red; Auto with sets. +intros; apply not_included_empty_Inhabited. +red in |- *; auto with sets. Qed. Lemma Inhabited_Setminus : -(X, Y: (Ensemble U)) (Included U X Y) -> ~ (Included U Y X) -> - (Inhabited U (Setminus U Y X)). + 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. -Elim (not_all_ex_not U [x:U](In U Y x)->(In U X x) NI). -Intros x YX. -Apply Inhabited_intro with x. -Apply Setminus_intro. -Apply not_imply_elim with (In U X x); Trivial with sets. -Auto with sets. +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. +apply Setminus_intro. +apply not_imply_elim with (In U X x); trivial with sets. +auto with sets. Qed. -Hints Resolve Inhabited_Setminus. +Hint Resolve Inhabited_Setminus. -Lemma Strict_super_set_contains_new_element: - (X, Y: (Ensemble U)) (Included U X Y) -> ~ X == Y -> - (Inhabited U (Setminus U Y X)). +Lemma Strict_super_set_contains_new_element : + forall X Y:Ensemble U, + Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X). Proof. -Auto 7 with sets. +auto 7 with sets. Qed. -Hints Resolve Strict_super_set_contains_new_element. +Hint Resolve Strict_super_set_contains_new_element. -Lemma Subtract_intro: - (A: (Ensemble U)) (x, y: U) (In U A y) -> ~ x == y -> - (In U (Subtract U A x) y). +Lemma Subtract_intro : + forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y. Proof. -Unfold 1 Subtract; Auto with sets. +unfold Subtract at 1 in |- *; auto with sets. Qed. -Hints Resolve Subtract_intro. +Hint Resolve Subtract_intro. -Lemma Subtract_inv: - (A: (Ensemble U)) (x, y: U) (In U (Subtract U A x) y) -> - (In U A y) /\ ~ x == y. +Lemma Subtract_inv : + forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y. Proof. -Intros A x y H'; Elim H'; Auto with sets. +intros A x y H'; elim H'; auto with sets. Qed. -Lemma Included_Strict_Included: - (X, Y: (Ensemble U)) (Included U X Y) -> (Strict_Included U X Y) \/ X == Y. +Lemma Included_Strict_Included : + forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y. Proof. -Intros X Y H'; Try Assumption. -Elim (classic X == Y); Auto with sets. +intros X Y H'; try assumption. +elim (classic (X = Y)); auto with sets. Qed. -Lemma Strict_Included_inv: - (X, Y: (Ensemble U)) (Strict_Included U X Y) -> - (Included U X Y) /\ (Inhabited U (Setminus U Y X)). +Lemma Strict_Included_inv : + forall X Y:Ensemble U, + Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X). Proof. -Intros X Y H'; Red in H'. -Split; [Tauto | Idtac]. -Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'. -Apply Strict_super_set_contains_new_element; Auto with sets. +intros X Y H'; red in H'. +split; [ tauto | idtac ]. +elim H'; intros H'0 H'1; try exact H'1; clear H'. +apply Strict_super_set_contains_new_element; auto with sets. Qed. -Lemma not_SIncl_empty: - (X: (Ensemble U)) ~ (Strict_Included U X (Empty_set U)). +Lemma not_SIncl_empty : + forall X:Ensemble U, ~ Strict_Included U X (Empty_set U). Proof. -Intro X; Red; Intro H'; Try Exact H'. -LApply (Strict_Included_inv X (Empty_set U)); Auto with sets. -Intro H'0; Elim H'0; Intros H'1 H'2; Elim H'2; Clear H'0. -Intros x H'0; Elim H'0. -Intro H'3; Elim H'3. +intro X; red in |- *; intro H'; try exact H'. +lapply (Strict_Included_inv X (Empty_set U)); auto with sets. +intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0. +intros x H'0; elim H'0. +intro H'3; elim H'3. Qed. Lemma Complement_Complement : - (A: (Ensemble U)) (Complement U (Complement U A)) == A. + forall A:Ensemble U, Complement U (Complement U A) = A. Proof. -Unfold Complement; Intros; Apply Extensionality_Ensembles; Auto with sets. -Red; Split; Auto with sets. -Red; Intros; Apply NNPP; Auto with sets. +unfold Complement in |- *; intros; apply Extensionality_Ensembles; + auto with sets. +red in |- *; split; auto with sets. +red in |- *; intros; apply NNPP; auto with sets. Qed. End Ensembles_classical. -Hints Resolve Strict_super_set_contains_new_element Subtract_intro - not_SIncl_empty : sets v62. +Hint Resolve Strict_super_set_contains_new_element Subtract_intro + not_SIncl_empty: sets v62. \ No newline at end of file diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 78ad3d2f2..b4250be92 100755 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -29,134 +29,131 @@ Require Export Ensembles. Section Ensembles_facts. -Variable U: Type. +Variable U : Type. -Lemma Extension: (B, C: (Ensemble U)) B == C -> (Same_set U B C). +Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C. Proof. -Intros B C H'; Rewrite H'; Auto with sets. +intros B C H'; rewrite H'; auto with sets. Qed. -Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x). +Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x. Proof. -Red; NewDestruct 1. +red in |- *; destruct 1. Qed. -Hints Resolve Noone_in_empty. +Hint Resolve Noone_in_empty. -Lemma Included_Empty: (A: (Ensemble U))(Included U (Empty_set U) A). +Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A. Proof. -Intro; Red. -Intros x H; Elim (Noone_in_empty x); Auto with sets. +intro; red in |- *. +intros x H; elim (Noone_in_empty x); auto with sets. Qed. -Hints Resolve Included_Empty. +Hint Resolve Included_Empty. -Lemma Add_intro1: - (A: (Ensemble U)) (x, y: U) (In U A y) -> (In U (Add U A x) y). +Lemma Add_intro1 : + forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y. Proof. -Unfold 1 Add; Auto with sets. +unfold Add at 1 in |- *; auto with sets. Qed. -Hints Resolve Add_intro1. +Hint Resolve Add_intro1. -Lemma Add_intro2: (A: (Ensemble U)) (x: U) (In U (Add U A x) x). +Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x. Proof. -Unfold 1 Add; Auto with sets. +unfold Add at 1 in |- *; auto with sets. Qed. -Hints Resolve Add_intro2. +Hint Resolve Add_intro2. -Lemma Inhabited_add: (A: (Ensemble U)) (x: U) (Inhabited U (Add U A x)). +Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x). Proof. -Intros A x. -Apply Inhabited_intro with x := x; Auto with sets. +intros A x. +apply Inhabited_intro with (x := x); auto with sets. Qed. -Hints Resolve Inhabited_add. +Hint Resolve Inhabited_add. -Lemma Inhabited_not_empty: - (X: (Ensemble U)) (Inhabited U X) -> ~ X == (Empty_set U). +Lemma Inhabited_not_empty : + forall X:Ensemble U, Inhabited U X -> X <> Empty_set U. Proof. -Intros X H'; Elim H'. -Intros x H'0; Red; Intro H'1. -Absurd (In U X x); Auto with sets. -Rewrite H'1; Auto with sets. +intros X H'; elim H'. +intros x H'0; red in |- *; intro H'1. +absurd (In U X x); auto with sets. +rewrite H'1; auto with sets. Qed. -Hints Resolve Inhabited_not_empty. +Hint Resolve Inhabited_not_empty. -Lemma Add_not_Empty : - (A: (Ensemble U)) (x: U) ~ (Add U A x) == (Empty_set U). +Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U. Proof. -Auto with sets. +auto with sets. Qed. -Hints Resolve Add_not_Empty. +Hint Resolve Add_not_Empty. -Lemma not_Empty_Add : - (A: (Ensemble U)) (x: U) ~ (Empty_set U) == (Add U A x). +Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x. Proof. -Intros; Red; Intro H; Generalize (Add_not_Empty A x); Auto with sets. +intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets. Qed. -Hints Resolve not_Empty_Add. +Hint Resolve not_Empty_Add. -Lemma Singleton_inv: (x, y: U) (In U (Singleton U x) y) -> x == y. +Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y. Proof. -Intros x y H'; Elim H'; Trivial with sets. +intros x y H'; elim H'; trivial with sets. Qed. -Hints Resolve Singleton_inv. +Hint Resolve Singleton_inv. -Lemma Singleton_intro: (x, y: U) x == y -> (In U (Singleton U x) y). +Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y. Proof. -Intros x y H'; Rewrite H'; Trivial with sets. +intros x y H'; rewrite H'; trivial with sets. Qed. -Hints Resolve Singleton_intro. +Hint Resolve Singleton_intro. -Lemma Union_inv: (B, C: (Ensemble U)) (x: U) - (In U (Union U B C) x) -> (In U B x) \/ (In U C x). +Lemma Union_inv : + forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x. Proof. -Intros B C x H'; Elim H'; Auto with sets. +intros B C x H'; elim H'; auto with sets. Qed. -Lemma Add_inv: - (A: (Ensemble U)) (x, y: U) (In U (Add U A x) y) -> (In U A y) \/ x == y. +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'; Elim H'; Auto with sets. +intros A x y H'; elim H'; auto with sets. Qed. -Lemma Intersection_inv: - (B, C: (Ensemble U)) (x: U) (In U (Intersection U B C) x) -> - (In U B x) /\ (In U C x). +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. Proof. -Intros B C x H'; Elim H'; Auto with sets. +intros B C x H'; elim H'; auto with sets. Qed. -Hints Resolve Intersection_inv. +Hint Resolve Intersection_inv. -Lemma Couple_inv: (x, y, z: U) (In U (Couple U x y) z) -> z == x \/ z == y. +Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y. Proof. -Intros x y z H'; Elim H'; Auto with sets. +intros x y z H'; elim H'; auto with sets. Qed. -Hints Resolve Couple_inv. +Hint Resolve Couple_inv. -Lemma Setminus_intro: - (A, B: (Ensemble U)) (x: U) (In U A x) -> ~ (In U B x) -> - (In U (Setminus U A B) x). +Lemma Setminus_intro : + forall (A B:Ensemble U) (x:U), + In U A x -> ~ In U B x -> In U (Setminus U A B) x. Proof. -Unfold 1 Setminus; Red; Auto with sets. +unfold Setminus at 1 in |- *; red in |- *; auto with sets. Qed. -Hints Resolve Setminus_intro. +Hint Resolve Setminus_intro. -Lemma Strict_Included_intro: - (X, Y: (Ensemble U)) (Included U X Y) /\ ~ X == Y -> - (Strict_Included U X Y). +Lemma Strict_Included_intro : + forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y. Proof. -Auto with sets. +auto with sets. Qed. -Hints Resolve Strict_Included_intro. +Hint Resolve Strict_Included_intro. -Lemma Strict_Included_strict: (X: (Ensemble U)) ~ (Strict_Included U X X). +Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X. Proof. -Intro X; Red; Intro H'; Elim H'. -Intros H'0 H'1; Elim H'1; Auto with sets. +intro X; red in |- *; intro H'; elim H'. +intros H'0 H'1; elim H'1; auto with sets. Qed. -Hints Resolve Strict_Included_strict. +Hint Resolve Strict_Included_strict. End Ensembles_facts. -Hints Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2 - Intersection_inv Couple_inv Setminus_intro Strict_Included_intro - Strict_Included_strict Noone_in_empty Inhabited_not_empty - Add_not_Empty not_Empty_Add Inhabited_add Included_Empty : sets v62. +Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2 + Intersection_inv Couple_inv Setminus_intro Strict_Included_intro + Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty + not_Empty_Add Inhabited_add Included_Empty: sets v62. \ No newline at end of file diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index c234bd1c7..0d77c0617 100755 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -31,77 +31,79 @@ Require Export Relations_1. Require Export Partial_Order. Section Bounds. -Variable U: Type. -Variable D: (PO U). +Variable U : Type. +Variable D : PO U. -Local C := (Carrier_of U D). +Let C := Carrier_of U D. -Local R := (Rel_of U D). +Let R := Rel_of U D. -Inductive Upper_Bound [B:(Ensemble U); x:U]: Prop := - Upper_Bound_definition: - (In U C x) -> ((y: U) (In U B y) -> (R y x)) -> (Upper_Bound B x). +Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop := + Upper_Bound_definition : + In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x. -Inductive Lower_Bound [B:(Ensemble U); x:U]: Prop := - Lower_Bound_definition: - (In U C x) -> ((y: U) (In U B y) -> (R x y)) -> (Lower_Bound B x). +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) -> ((y: U) (Upper_Bound B y) -> (R x y)) -> (Lub 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. -Inductive Glb [B:(Ensemble U); x:U]: Prop := - Glb_definition: - (Lower_Bound B x) -> ((y: U) (Lower_Bound B y) -> (R y x)) -> (Glb B x). +Inductive Glb (B:Ensemble U) (x:U) : Prop := + Glb_definition : + Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x. -Inductive Bottom [bot:U]: Prop := - Bottom_definition: - (In U C bot) -> ((y: U) (In U C y) -> (R bot y)) -> (Bottom bot). +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) -> - (x: U) (y: U) (Included U (Couple U x y) B) -> (R x y) \/ (R y x)) -> - (Totally_ordered B). +Inductive Totally_ordered (B:Ensemble U) : Prop := + Totally_ordered_definition : + (Included U B C -> + forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) -> + Totally_ordered B. -Definition Compatible : (Relation U) := - [x: U] [y: U] (In U C x) -> (In U C y) -> - (EXT z | (In U C z) /\ (Upper_Bound (Couple U x y) z)). +Definition Compatible : Relation U := + fun x y:U => + In U C x -> + In U C y -> exists z : _ | In U C z /\ Upper_Bound (Couple U x y) z. -Inductive Directed [X:(Ensemble U)]: Prop := - Definition_of_Directed: - (Included U X C) -> - (Inhabited U X) -> - ((x1: U) (x2: U) (Included U (Couple U x1 x2) X) -> - (EXT x3 | (In U X x3) /\ (Upper_Bound (Couple U x1 x2) x3))) -> - (Directed X). +Inductive Directed (X:Ensemble U) : Prop := + Definition_of_Directed : + Included U X C -> + Inhabited U X -> + (forall x1 x2:U, + 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: - ((EXT bot | (Bottom bot))) -> - ((X: (Ensemble U)) (Directed X) -> (EXT bsup | (Lub X bsup))) -> - Complete. + Definition_of_Complete : + ( exists bot : _ | Bottom bot) -> + (forall X:Ensemble U, Directed X -> exists bsup : _ | Lub X bsup) -> + Complete. Inductive Conditionally_complete : Prop := - Definition_of_Conditionally_complete: - ((X: (Ensemble U)) - (Included U X C) -> (EXT maj | (Upper_Bound X maj)) -> - (EXT bsup | (Lub X bsup))) -> Conditionally_complete. + Definition_of_Conditionally_complete : + (forall X:Ensemble U, + Included U X C -> + ( exists maj : _ | Upper_Bound X maj) -> + exists bsup : _ | Lub X bsup) -> Conditionally_complete. End Bounds. -Hints Resolve Totally_ordered_definition Upper_Bound_definition - Lower_Bound_definition Lub_definition Glb_definition - Bottom_definition Definition_of_Complete - Definition_of_Complete Definition_of_Conditionally_complete. +Hint Resolve Totally_ordered_definition Upper_Bound_definition + Lower_Bound_definition Lub_definition Glb_definition Bottom_definition + Definition_of_Complete Definition_of_Complete + Definition_of_Conditionally_complete. Section Specific_orders. -Variable U: Type. +Variable U : Type. -Record Cpo : Type := Definition_of_cpo { - PO_of_cpo: (PO U); - Cpo_cond: (Complete U PO_of_cpo) }. +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)) }. +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)}. -End Specific_orders. +End Specific_orders. \ No newline at end of file diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index af202239e..eae50a3d1 100755 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -27,20 +27,18 @@ (*i $Id$ i*) Section Ensembles. -Variable U: Type. +Variable U : Type. -Definition Ensemble := U -> Prop. +Definition Ensemble := U -> Prop. -Definition In : Ensemble -> U -> Prop := [A: Ensemble] [x: U] (A x). +Definition In (A:Ensemble) (x:U) : Prop := A x. -Definition Included : Ensemble -> Ensemble -> Prop := - [B, C: Ensemble] (x: U) (In B x) -> (In C x). +Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x. -Inductive Empty_set : Ensemble := - . +Inductive Empty_set : Ensemble :=. Inductive Full_set : Ensemble := - Full_intro: (x: U) (In Full_set x). + Full_intro : forall x:U, In Full_set x. (** NB: The following definition builds-in equality of elements in [U] as Leibniz equality. @@ -49,60 +47,55 @@ Inductive Full_set : Ensemble := with its own equality [eqs], with [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *) -Inductive Singleton [x:U] : Ensemble := - In_singleton: (In (Singleton x) x). +Inductive Singleton (x:U) : Ensemble := + In_singleton : In (Singleton x) x. -Inductive Union [B, C: Ensemble] : Ensemble := - Union_introl: (x: U) (In B x) -> (In (Union B C) x) - | Union_intror: (x: U) (In C x) -> (In (Union B C) x). +Inductive Union (B C:Ensemble) : Ensemble := + | Union_introl : forall x:U, In B x -> In (Union B C) x + | Union_intror : forall x:U, In C x -> In (Union B C) x. -Definition Add : Ensemble -> U -> Ensemble := - [B: Ensemble] [x: U] (Union B (Singleton x)). +Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x). -Inductive Intersection [B, C:Ensemble] : Ensemble := - Intersection_intro: - (x: U) (In B x) -> (In C x) -> (In (Intersection B C) x). +Inductive Intersection (B C:Ensemble) : Ensemble := + Intersection_intro : + forall x:U, In B x -> In C x -> In (Intersection B C) x. -Inductive Couple [x,y:U] : Ensemble := - Couple_l: (In (Couple x y) x) - | Couple_r: (In (Couple x y) y). +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). +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 : Ensemble -> Ensemble := - [A: Ensemble] [x: U] ~ (In A x). +Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x. -Definition Setminus : Ensemble -> Ensemble -> Ensemble := - [B: Ensemble] [C: Ensemble] [x: U] (In B x) /\ ~ (In C x). +Definition Setminus (B C:Ensemble) : Ensemble := + fun x:U => In B x /\ ~ In C x. -Definition Subtract : Ensemble -> U -> Ensemble := - [B: Ensemble] [x: U] (Setminus B (Singleton x)). +Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x). -Inductive Disjoint [B, C:Ensemble] : Prop := - Disjoint_intro: ((x: U) ~ (In (Intersection B C) x)) -> (Disjoint B C). +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: (x: U) (In B x) -> (Inhabited B). +Inductive Inhabited (B:Ensemble) : Prop := + Inhabited_intro : forall x:U, In B x -> Inhabited B. -Definition Strict_Included : Ensemble -> Ensemble -> Prop := - [B, C: Ensemble] (Included B C) /\ ~ B == C. +Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C. -Definition Same_set : Ensemble -> Ensemble -> Prop := - [B, C: Ensemble] (Included B C) /\ (Included C B). +Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B. (** Extensionality Axiom *) -Axiom Extensionality_Ensembles: - (A,B: Ensemble) (Same_set A B) -> A == B. -Hints Resolve Extensionality_Ensembles. +Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B. +Hint Resolve Extensionality_Ensembles. End Ensembles. -Hints Unfold In Included Same_set Strict_Included Add Setminus Subtract : sets v62. +Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets + v62. -Hints Resolve Union_introl Union_intror Intersection_intro In_singleton Couple_l - Couple_r Triple_l Triple_m Triple_r Disjoint_intro - Extensionality_Ensembles : sets v62. +Hint Resolve Union_introl Union_intror Intersection_intro In_singleton + Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro + Extensionality_Ensembles: sets v62. \ No newline at end of file diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 1e7168791..28b2d6fb9 100755 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -26,49 +26,56 @@ (*i $Id$ i*) -Require Ensembles. +Require Import Ensembles. Section Ensembles_finis. -Variable U: Type. +Variable U : Type. -Inductive Finite : (Ensemble U) -> Prop := - Empty_is_finite: (Finite (Empty_set U)) - | Union_is_finite: - (A: (Ensemble U)) (Finite A) -> - (x: U) ~ (In U A x) -> (Finite (Add U A x)). +Inductive Finite : Ensemble U -> Prop := + | Empty_is_finite : Finite (Empty_set U) + | Union_is_finite : + forall A:Ensemble U, + Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x). -Inductive cardinal : (Ensemble U) -> nat -> Prop := - card_empty: (cardinal (Empty_set U) O) - | card_add: - (A: (Ensemble U)) (n: nat) (cardinal A n) -> - (x: U) ~ (In U A x) -> (cardinal (Add U A x) (S n)). +Inductive cardinal : Ensemble U -> nat -> Prop := + | card_empty : cardinal (Empty_set U) 0 + | card_add : + forall (A:Ensemble U) (n:nat), + cardinal A n -> forall x:U, ~ In U A x -> cardinal (Add U A x) (S n). End Ensembles_finis. -Hints Resolve Empty_is_finite Union_is_finite : sets v62. -Hints Resolve card_empty card_add : sets v62. +Hint Resolve Empty_is_finite Union_is_finite: sets v62. +Hint Resolve card_empty card_add: sets v62. -Require Constructive_sets. +Require Import Constructive_sets. Section Ensembles_finis_facts. -Variable U: Type. +Variable U : Type. Lemma cardinal_invert : - (X: (Ensemble U)) (p:nat)(cardinal U X p) -> Case p of - X == (Empty_set U) - [n:nat] (EXT A | (EXT x | - X == (Add U A x) /\ ~ (In U A x) /\ (cardinal U A n))) end. + forall (X:Ensemble U) (p:nat), + cardinal U X p -> + match p with + | O => X = Empty_set U + | S n => + exists A : _ + | ( exists x : _ | X = Add U A x /\ ~ In U A x /\ cardinal U A n) + end. Proof. -NewInduction 1; Simpl; Auto. -Exists A; Exists x; Auto. +induction 1; simpl in |- *; auto. +exists A; exists x; auto. Qed. Lemma cardinal_elim : - (X: (Ensemble U)) (p:nat)(cardinal U X p) -> Case p of - X == (Empty_set U) - [n:nat](Inhabited U X) end. + forall (X:Ensemble U) (p:nat), + cardinal U X p -> + match p with + | O => X = Empty_set U + | S n => Inhabited U X + end. Proof. -Intros X p C; Elim C; Simpl; Trivial with sets. +intros X p C; elim C; simpl in |- *; trivial with sets. Qed. -End Ensembles_finis_facts. +End Ensembles_finis_facts. \ No newline at end of file diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 4e7b6931f..2849bce6c 100755 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -37,309 +37,311 @@ Require Export Gt. Require Export Lt. Section Finite_sets_facts. -Variable U: Type. +Variable U : Type. Lemma finite_cardinal : - (X: (Ensemble U)) (Finite U X) -> (EX n:nat |(cardinal U X n)). + forall X:Ensemble U, Finite U X -> exists n : nat | cardinal U X n. Proof. -NewInduction 1 as [|A _ [n H]]. -Exists O; Auto with sets. -Exists (S n); Auto with sets. +induction 1 as [| A _ [n H]]. +exists 0; auto with sets. +exists (S n); auto with sets. Qed. -Lemma cardinal_finite: - (X: (Ensemble U)) (n: nat) (cardinal U X n) -> (Finite U X). +Lemma cardinal_finite : + forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X. Proof. -NewInduction 1; Auto with sets. +induction 1; auto with sets. Qed. -Theorem Add_preserves_Finite: - (X: (Ensemble U)) (x: U) (Finite U X) -> (Finite U (Add U X x)). +Theorem Add_preserves_Finite : + forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x). Proof. -Intros X x H'. -Elim (classic (In U X x)); Intro H'0; Auto with sets. -Rewrite (Non_disjoint_union U X x); Auto with sets. +intros X x H'. +elim (classic (In U X x)); intro H'0; auto with sets. +rewrite (Non_disjoint_union U X x); auto with sets. Qed. -Hints Resolve Add_preserves_Finite. +Hint Resolve Add_preserves_Finite. -Theorem Singleton_is_finite: (x: U) (Finite U (Singleton U x)). +Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x). Proof. -Intro x; Rewrite <- (Empty_set_zero U (Singleton U x)). -Change (Finite U (Add U (Empty_set U) x)); Auto with sets. +intro x; rewrite <- (Empty_set_zero U (Singleton U x)). +change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets. Qed. -Hints Resolve Singleton_is_finite. +Hint Resolve Singleton_is_finite. -Theorem Union_preserves_Finite: - (X, Y: (Ensemble U)) (Finite U X) -> (Finite U Y) -> - (Finite U (Union U X Y)). +Theorem Union_preserves_Finite : + forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y). Proof. -Intros X Y H'; Elim H'. -Rewrite (Empty_set_zero U Y); Auto with sets. -Intros A H'0 H'1 x H'2 H'3. -Rewrite (Union_commutative U (Add U A x) Y). -Rewrite <- (Union_add U Y A x). -Rewrite (Union_commutative U Y A); Auto with sets. +intros X Y H'; elim H'. +rewrite (Empty_set_zero U Y); auto with sets. +intros A H'0 H'1 x H'2 H'3. +rewrite (Union_commutative U (Add U A x) Y). +rewrite <- (Union_add U Y A x). +rewrite (Union_commutative U Y A); auto with sets. Qed. -Lemma Finite_downward_closed: - (A: (Ensemble U)) (Finite U A) -> - (X: (Ensemble U)) (Included U X A) -> (Finite U X). +Lemma Finite_downward_closed : + forall A:Ensemble U, + Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X. Proof. -Intros A H'; Elim H'; Auto with sets. -Intros X H'0. -Rewrite (less_than_empty U X H'0); Auto with sets. -Intros; Elim Included_Add with U X A0 x; Auto with sets. -NewDestruct 1 as [A' [H5 H6]]. -Rewrite H5; Auto with sets. +intros A H'; elim H'; auto with sets. +intros X H'0. +rewrite (less_than_empty U X H'0); auto with sets. +intros; elim Included_Add with U X A0 x; auto with sets. +destruct 1 as [A' [H5 H6]]. +rewrite H5; auto with sets. Qed. -Lemma Intersection_preserves_finite: - (A: (Ensemble U)) (Finite U A) -> - (X: (Ensemble U)) (Finite U (Intersection U X A)). +Lemma Intersection_preserves_finite : + forall A:Ensemble U, + Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A). Proof. -Intros A H' X; Apply Finite_downward_closed with A; Auto with sets. +intros A H' X; apply Finite_downward_closed with A; auto with sets. Qed. -Lemma cardinalO_empty: - (X: (Ensemble U)) (cardinal U X O) -> X == (Empty_set U). +Lemma cardinalO_empty : + forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U. Proof. -Intros X H; Apply (cardinal_invert U X O); Trivial with sets. +intros X H; apply (cardinal_invert U X 0); trivial with sets. Qed. -Hints Resolve cardinalO_empty. +Hint Resolve cardinalO_empty. -Lemma inh_card_gt_O: - (X: (Ensemble U)) (Inhabited U X) -> (n: nat) (cardinal U X n) -> (gt n O). +Lemma inh_card_gt_O : + forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0. Proof. -NewInduction 1 as [x H']. -Intros n H'0. -Elim (gt_O_eq n); Auto with sets. -Intro H'1; Generalize H'; Generalize H'0. -Rewrite <- H'1; Intro H'2. -Rewrite (cardinalO_empty X); Auto with sets. -Intro H'3; Elim H'3. +induction 1 as [x H']. +intros n H'0. +elim (gt_O_eq n); auto with sets. +intro H'1; generalize H'; generalize H'0. +rewrite <- H'1; intro H'2. +rewrite (cardinalO_empty X); auto with sets. +intro H'3; elim H'3. Qed. -Lemma card_soustr_1: - (X: (Ensemble U)) (n: nat) (cardinal U X n) -> - (x: U) (In U X x) -> (cardinal U (Subtract U X x) (pred n)). +Lemma card_soustr_1 : + forall (X:Ensemble U) (n:nat), + cardinal U X n -> + forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n). Proof. -Intros X n H'; Elim H'. -Intros x H'0; Elim H'0. -Clear H' n X. -Intros X n H' H'0 x H'1 x0 H'2. -Elim (classic (In U X x0)). -Intro H'4; Rewrite (add_soustr_xy U X x x0). -Elim (classic x == x0). -Intro H'5. -Absurd (In U X x0); Auto with sets. -Rewrite <- H'5; Auto with sets. -Intro H'3; Try Assumption. -Cut (S (pred n)) = (pred (S n)). -Intro H'5; Rewrite <- H'5. -Apply card_add; Auto with sets. -Red; Intro H'6; Elim H'6. -Intros H'7 H'8; Try Assumption. -Elim H'1; Auto with sets. -Unfold 2 pred; Symmetry. -Apply S_pred with m := O. -Change (gt n O). -Apply inh_card_gt_O with X := X; Auto with sets. -Apply Inhabited_intro with x := x0; Auto with sets. -Red; Intro H'3. -Apply H'1. -Elim H'3; Auto with sets. -Rewrite H'3; Auto with sets. -Elim (classic x == x0). -Intro H'3; Rewrite <- H'3. -Cut (Subtract U (Add U X x) x) == X; Auto with sets. -Intro H'4; Rewrite H'4; Auto with sets. -Intros H'3 H'4; Try Assumption. -Absurd (In U (Add U X x) x0); Auto with sets. -Red; Intro H'5; Try Exact H'5. -LApply (Add_inv U X x x0); Tauto. +intros X n H'; elim H'. +intros x H'0; elim H'0. +clear H' n X. +intros X n H' H'0 x H'1 x0 H'2. +elim (classic (In U X x0)). +intro H'4; rewrite (add_soustr_xy U X x x0). +elim (classic (x = x0)). +intro H'5. +absurd (In U X x0); auto with sets. +rewrite <- H'5; auto with sets. +intro H'3; try assumption. +cut (S (pred n) = pred (S n)). +intro H'5; rewrite <- H'5. +apply card_add; auto with sets. +red in |- *; intro H'6; elim H'6. +intros H'7 H'8; try assumption. +elim H'1; auto with sets. +unfold pred at 2 in |- *; symmetry in |- *. +apply S_pred with (m := 0). +change (n > 0) in |- *. +apply inh_card_gt_O with (X := X); auto with sets. +apply Inhabited_intro with (x := x0); auto with sets. +red in |- *; intro H'3. +apply H'1. +elim H'3; auto with sets. +rewrite H'3; auto with sets. +elim (classic (x = x0)). +intro H'3; rewrite <- H'3. +cut (Subtract U (Add U X x) x = X); auto with sets. +intro H'4; rewrite H'4; auto with sets. +intros H'3 H'4; try assumption. +absurd (In U (Add U X x) x0); auto with sets. +red in |- *; intro H'5; try exact H'5. +lapply (Add_inv U X x x0); tauto. Qed. -Lemma cardinal_is_functional: - (X: (Ensemble U)) (c1: nat) (cardinal U X c1) -> - (Y: (Ensemble U)) (c2: nat) (cardinal U Y c2) -> X == Y -> - c1 = c2. +Lemma cardinal_is_functional : + forall (X:Ensemble U) (c1:nat), + cardinal U X c1 -> + forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2. Proof. -Intros X c1 H'; Elim H'. -Intros Y c2 H'0; Elim H'0; Auto with sets. -Intros A n H'1 H'2 x H'3 H'5. -Elim (not_Empty_Add U A x); Auto with sets. -Clear H' c1 X. -Intros X n H' H'0 x H'1 Y c2 H'2. -Elim H'2. -Intro H'3. -Elim (not_Empty_Add U X x); Auto with sets. -Clear H'2 c2 Y. -Intros X0 c2 H'2 H'3 x0 H'4 H'5. -Elim (classic (In U X0 x)). -Intro H'6; Apply f_equal with nat. -Apply H'0 with Y := (Subtract U (Add U X0 x0) x). -ElimType (pred (S c2)) = c2; Auto with sets. -Apply card_soustr_1; Auto with sets. -Rewrite <- H'5. -Apply Sub_Add_new; Auto with sets. -Elim (classic x == x0). -Intros H'6 H'7; Apply f_equal with nat. -Apply H'0 with Y := X0; Auto with sets. -Apply Simplify_add with x := x; Auto with sets. -Pattern 2 x; Rewrite H'6; Auto with sets. -Intros H'6 H'7. -Absurd (Add U X x) == (Add U X0 x0); Auto with sets. -Clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2. -Red; Intro H'. -LApply (Extension U (Add U X x) (Add U X0 x0)); Auto with sets. -Clear H'. -Intro H'; Red in H'. -Elim H'; Intros H'0 H'1; Red in H'0; Clear H' H'1. -Absurd (In U (Add U X0 x0) x); Auto with sets. -LApply (Add_inv U X0 x0 x); [ Intuition | Apply (H'0 x); Apply Add_intro2 ]. +intros X c1 H'; elim H'. +intros Y c2 H'0; elim H'0; auto with sets. +intros A n H'1 H'2 x H'3 H'5. +elim (not_Empty_Add U A x); auto with sets. +clear H' c1 X. +intros X n H' H'0 x H'1 Y c2 H'2. +elim H'2. +intro H'3. +elim (not_Empty_Add U X x); auto with sets. +clear H'2 c2 Y. +intros X0 c2 H'2 H'3 x0 H'4 H'5. +elim (classic (In U X0 x)). +intro H'6; apply f_equal with nat. +apply H'0 with (Y := Subtract U (Add U X0 x0) x). +elimtype (pred (S c2) = c2); auto with sets. +apply card_soustr_1; auto with sets. +rewrite <- H'5. +apply Sub_Add_new; auto with sets. +elim (classic (x = x0)). +intros H'6 H'7; apply f_equal with nat. +apply H'0 with (Y := X0); auto with sets. +apply Simplify_add with (x := x); auto with sets. +pattern x at 2 in |- *; rewrite H'6; auto with sets. +intros H'6 H'7. +absurd (Add U X x = Add U X0 x0); auto with sets. +clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2. +red in |- *; intro H'. +lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets. +clear H'. +intro H'; red in H'. +elim H'; intros H'0 H'1; red in H'0; clear H' H'1. +absurd (In U (Add U X0 x0) x); auto with sets. +lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ]. Qed. -Lemma cardinal_Empty : (m:nat)(cardinal U (Empty_set U) m) -> O = m. +Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m. Proof. -Intros m Cm; Generalize (cardinal_invert U (Empty_set U) m Cm). -Elim m; Auto with sets. -Intros; Elim H0; Intros; Elim H1; Intros; Elim H2; Intros. -Elim (not_Empty_Add U x x0 H3). +intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm). +elim m; auto with sets. +intros; elim H0; intros; elim H1; intros; elim H2; intros. +elim (not_Empty_Add U x x0 H3). Qed. Lemma cardinal_unicity : - (X: (Ensemble U)) (n: nat) (cardinal U X n) -> - (m: nat) (cardinal U X m) -> n = m. + forall (X:Ensemble U) (n:nat), + cardinal U X n -> forall m:nat, cardinal U X m -> n = m. Proof. -Intros; Apply cardinal_is_functional with X X; Auto with sets. +intros; apply cardinal_is_functional with X X; auto with sets. Qed. -Lemma card_Add_gen: - (A: (Ensemble U)) - (x: U) (n, n': nat) (cardinal U A n) -> (cardinal U (Add U A x) n') -> - (le n' (S n)). +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. Proof. -Intros A x n n' H'. -Elim (classic (In U A x)). -Intro H'0. -Rewrite (Non_disjoint_union U A x H'0). -Intro H'1; Cut n = n'. -Intro E; Rewrite E; Auto with sets. -Apply cardinal_unicity with A; Auto with sets. -Intros H'0 H'1. -Cut n'=(S n). -Intro E; Rewrite E; Auto with sets. -Apply cardinal_unicity with (Add U A x); Auto with sets. +intros A x n n' H'. +elim (classic (In U A x)). +intro H'0. +rewrite (Non_disjoint_union U A x H'0). +intro H'1; cut (n = n'). +intro E; rewrite E; auto with sets. +apply cardinal_unicity with A; auto with sets. +intros H'0 H'1. +cut (n' = S n). +intro E; rewrite E; auto with sets. +apply cardinal_unicity with (Add U A x); auto with sets. Qed. -Lemma incl_st_card_lt: - (X: (Ensemble U)) (c1: nat) (cardinal U X c1) -> - (Y: (Ensemble U)) (c2: nat) (cardinal U Y c2) -> (Strict_Included U X Y) -> - (gt c2 c1). +Lemma incl_st_card_lt : + forall (X:Ensemble U) (c1:nat), + cardinal U X c1 -> + forall (Y:Ensemble U) (c2:nat), + cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1. Proof. -Intros X c1 H'; Elim H'. -Intros Y c2 H'0; Elim H'0; Auto with sets arith. -Intro H'1. -Elim (Strict_Included_strict U (Empty_set U)); Auto with sets arith. -Clear H' c1 X. -Intros X n H' H'0 x H'1 Y c2 H'2. -Elim H'2. -Intro H'3; Elim (not_SIncl_empty U (Add U X x)); Auto with sets arith. -Clear H'2 c2 Y. -Intros X0 c2 H'2 H'3 x0 H'4 H'5; Elim (classic (In U X0 x)). -Intro H'6; Apply gt_n_S. -Apply H'0 with Y := (Subtract U (Add U X0 x0) x). -ElimType (pred (S c2)) = c2; Auto with sets arith. -Apply card_soustr_1; Auto with sets arith. -Apply incl_st_add_soustr; Auto with sets arith. -Elim (classic x == x0). -Intros H'6 H'7; Apply gt_n_S. -Apply H'0 with Y := X0; Auto with sets arith. -Apply sincl_add_x with x := x0. -Rewrite <- H'6; Auto with sets arith. -Pattern 1 x0; Rewrite <- H'6; Trivial with sets arith. -Intros H'6 H'7; Red in H'5. -Elim H'5; Intros H'8 H'9; Try Exact H'8; Clear H'5. -Red in H'8. -Generalize (H'8 x). -Intro H'5; LApply H'5; Auto with sets arith. -Intro H; Elim Add_inv with U X0 x0 x; Auto with sets arith. -Intro; Absurd (In U X0 x); Auto with sets arith. -Intro; Absurd x==x0; Auto with sets arith. +intros X c1 H'; elim H'. +intros Y c2 H'0; elim H'0; auto with sets arith. +intro H'1. +elim (Strict_Included_strict U (Empty_set U)); auto with sets arith. +clear H' c1 X. +intros X n H' H'0 x H'1 Y c2 H'2. +elim H'2. +intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith. +clear H'2 c2 Y. +intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)). +intro H'6; apply gt_n_S. +apply H'0 with (Y := Subtract U (Add U X0 x0) x). +elimtype (pred (S c2) = c2); auto with sets arith. +apply card_soustr_1; auto with sets arith. +apply incl_st_add_soustr; auto with sets arith. +elim (classic (x = x0)). +intros H'6 H'7; apply gt_n_S. +apply H'0 with (Y := X0); auto with sets arith. +apply sincl_add_x with (x := x0). +rewrite <- H'6; auto with sets arith. +pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith. +intros H'6 H'7; red in H'5. +elim H'5; intros H'8 H'9; try exact H'8; clear H'5. +red in H'8. +generalize (H'8 x). +intro H'5; lapply H'5; auto with sets arith. +intro H; elim Add_inv with U X0 x0 x; auto with sets arith. +intro; absurd (In U X0 x); auto with sets arith. +intro; absurd (x = x0); auto with sets arith. Qed. -Lemma incl_card_le: - (X,Y: (Ensemble U)) (n,m: nat) (cardinal U X n) -> (cardinal U Y m) -> - (Included U X Y) -> (le n m). +Lemma incl_card_le : + forall (X Y:Ensemble U) (n m:nat), + cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m. Proof. -Intros; -Elim Included_Strict_Included with U X Y; Auto with sets arith; Intro. -Cut (gt m n); Auto with sets arith. -Apply incl_st_card_lt with X := X Y := Y; Auto with sets arith. -Generalize H0; Rewrite <- H2; Intro. -Cut n=m. -Intro E; Rewrite E; Auto with sets arith. -Apply cardinal_unicity with X; Auto with sets arith. +intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro. +cut (m > n); auto with sets arith. +apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith. +generalize H0; rewrite <- H2; intro. +cut (n = m). +intro E; rewrite E; auto with sets arith. +apply cardinal_unicity with X; auto with sets arith. Qed. -Lemma G_aux: - (P:(Ensemble U) ->Prop) - ((X:(Ensemble U)) - (Finite U X) -> ((Y:(Ensemble U)) (Strict_Included U Y X) ->(P Y)) ->(P X)) -> - (P (Empty_set U)). +Lemma G_aux : + forall P:Ensemble U -> Prop, + (forall X:Ensemble U, + Finite U X -> + (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) -> + P (Empty_set U). Proof. -Intros P H'; Try Assumption. -Apply H'; Auto with sets. -Clear H'; Auto with sets. -Intros Y H'; Try Assumption. -Red in H'. -Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'. -LApply (less_than_empty U Y); [Intro H'3; Try Exact H'3 | Assumption]. -Elim H'1; Auto with sets. +intros P H'; try assumption. +apply H'; auto with sets. +clear H'; auto with sets. +intros Y H'; try assumption. +red in H'. +elim H'; intros H'0 H'1; try exact H'1; clear H'. +lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ]. +elim H'1; auto with sets. Qed. -Hints Unfold not. +Hint Unfold not. -Lemma Generalized_induction_on_finite_sets: - (P:(Ensemble U) ->Prop) - ((X:(Ensemble U)) - (Finite U X) -> ((Y:(Ensemble U)) (Strict_Included U Y X) ->(P Y)) ->(P X)) -> - (X:(Ensemble U)) (Finite U X) ->(P X). +Lemma Generalized_induction_on_finite_sets : + forall P:Ensemble U -> Prop, + (forall X:Ensemble U, + Finite U X -> + (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) -> + forall X:Ensemble U, Finite U X -> P X. Proof. -Intros P H'0 X H'1. -Generalize P H'0; Clear H'0 P. -Elim H'1. -Intros P H'0. -Apply G_aux; Auto with sets. -Clear H'1 X. -Intros A H' H'0 x H'1 P H'3. -Cut (Y:(Ensemble U)) (Included U Y (Add U A x)) ->(P Y); Auto with sets. -Generalize H'1. -Apply H'0. -Intros X K H'5 L Y H'6; Apply H'3; Auto with sets. -Apply Finite_downward_closed with A := (Add U X x); Auto with sets. -Intros Y0 H'7. -Elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x)); Auto with sets. -Intros H'2 H'4. -Elim (Included_Add U Y0 X x); - [Intro H'14 | - Intro H'14; Elim H'14; Intros A' E; Elim E; Intros H'15 H'16; Clear E H'14 | - Idtac]; Auto with sets. -Elim (Included_Strict_Included U Y0 X); Auto with sets. -Intro H'9; Apply H'5 with Y := Y0; Auto with sets. -Intro H'9; Rewrite H'9. -Apply H'3; Auto with sets. -Intros Y1 H'8; Elim H'8. -Intros H'10 H'11; Apply H'5 with Y := Y1; Auto with sets. -Elim (Included_Strict_Included U A' X); Auto with sets. -Intro H'8; Apply H'5 with Y := A'; Auto with sets. -Rewrite <- H'15; Auto with sets. -Intro H'8. -Elim H'7. -Intros H'9 H'10; Apply H'10 Orelse Elim H'10; Try Assumption. -Generalize H'6. -Rewrite <- H'8. -Rewrite <- H'15; Auto with sets. +intros P H'0 X H'1. +generalize P H'0; clear H'0 P. +elim H'1. +intros P H'0. +apply G_aux; auto with sets. +clear H'1 X. +intros A H' H'0 x H'1 P H'3. +cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets. +generalize H'1. +apply H'0. +intros X K H'5 L Y H'6; apply H'3; auto with sets. +apply Finite_downward_closed with (A := Add U X x); auto with sets. +intros Y0 H'7. +elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x)); + auto with sets. +intros H'2 H'4. +elim (Included_Add U Y0 X x); + [ intro H'14 + | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14 + | idtac ]; auto with sets. +elim (Included_Strict_Included U Y0 X); auto with sets. +intro H'9; apply H'5 with (Y := Y0); auto with sets. +intro H'9; rewrite H'9. +apply H'3; auto with sets. +intros Y1 H'8; elim H'8. +intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets. +elim (Included_Strict_Included U A' X); auto with sets. +intro H'8; apply H'5 with (Y := A'); auto with sets. +rewrite <- H'15; auto with sets. +intro H'8. +elim H'7. +intros H'9 H'10; apply H'10 || elim H'10; try assumption. +generalize H'6. +rewrite <- H'8. +rewrite <- H'15; auto with sets. Qed. -End Finite_sets_facts. +End Finite_sets_facts. \ No newline at end of file diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index d5f42e3f9..85b83d3ab 100755 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -39,161 +39,167 @@ Require Export Le. Require Export Finite_sets_facts. Section Image. -Variables U, V: Type. +Variables U V : Type. -Inductive Im [X:(Ensemble U); f:U -> V]: (Ensemble V) := - Im_intro: (x: U) (In ? X x) -> (y: V) y == (f x) -> (In ? (Im X f) y). +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: - (X: (Ensemble U)) (f: U -> V) (x: U) (In ? X x) -> (In ? (Im X f) (f x)). +Lemma Im_def : + forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x). Proof. -Intros X f x H'; Try Assumption. -Apply Im_intro with x := x; Auto with sets. +intros X f x H'; try assumption. +apply Im_intro with (x := x); auto with sets. Qed. -Hints Resolve Im_def. +Hint Resolve Im_def. -Lemma Im_add: - (X: (Ensemble U)) (x: U) (f: U -> V) - (Im (Add ? X x) f) == (Add ? (Im X f) (f x)). +Lemma Im_add : + forall (X:Ensemble U) (x:U) (f:U -> V), + Im (Add _ X x) f = Add _ (Im X f) (f x). Proof. -Intros X x f. -Apply Extensionality_Ensembles. -Split; Red; Intros x0 H'. -Elim H'; Intros. -Rewrite H0. -Elim Add_inv with U X x x1; Auto with sets. -NewDestruct 1; Auto with sets. -Elim Add_inv with V (Im X f) (f x) x0; Auto with sets. -NewDestruct 1 as [x0 H y H0]. -Rewrite H0; Auto with sets. -NewDestruct 1; Auto with sets. +intros X x f. +apply Extensionality_Ensembles. +split; red in |- *; intros x0 H'. +elim H'; intros. +rewrite H0. +elim Add_inv with U X x x1; auto with sets. +destruct 1; auto with sets. +elim Add_inv with V (Im X f) (f x) x0; auto with sets. +destruct 1 as [x0 H y H0]. +rewrite H0; auto with sets. +destruct 1; auto with sets. Qed. -Lemma image_empty: (f: U -> V) (Im (Empty_set U) f) == (Empty_set V). +Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V. Proof. -Intro f; Try Assumption. -Apply Extensionality_Ensembles. -Split; Auto with sets. -Red. -Intros x H'; Elim H'. -Intros x0 H'0; Elim H'0; Auto with sets. +intro f; try assumption. +apply Extensionality_Ensembles. +split; auto with sets. +red in |- *. +intros x H'; elim H'. +intros x0 H'0; elim H'0; auto with sets. Qed. -Hints Resolve image_empty. +Hint Resolve image_empty. -Lemma finite_image: - (X: (Ensemble U)) (f: U -> V) (Finite ? X) -> (Finite ? (Im X f)). +Lemma finite_image : + forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f). Proof. -Intros X f H'; Elim H'. -Rewrite (image_empty f); Auto with sets. -Intros A H'0 H'1 x H'2; Clear H' X. -Rewrite (Im_add A x f); Auto with sets. -Apply Add_preserves_Finite; Auto with sets. +intros X f H'; elim H'. +rewrite (image_empty f); auto with sets. +intros A H'0 H'1 x H'2; clear H' X. +rewrite (Im_add A x f); auto with sets. +apply Add_preserves_Finite; auto with sets. Qed. -Hints Resolve finite_image. +Hint Resolve finite_image. -Lemma Im_inv: - (X: (Ensemble U)) (f: U -> V) (y: V) (In ? (Im X f) y) -> - (exT ? [x: U] (In ? X x) /\ (f x) == y). +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. Proof. -Intros X f y H'; Elim H'. -Intros x H'0 y0 H'1; Rewrite H'1. -Exists x; Auto with sets. +intros X f y H'; elim H'. +intros x H'0 y0 H'1; rewrite H'1. +exists x; auto with sets. Qed. -Definition injective := [f: U -> V] (x, y: U) (f x) == (f y) -> x == y. +Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y. -Lemma not_injective_elim: - (f: U -> V) ~ (injective f) -> - (EXT x | (EXT y | (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). Proof. -Unfold injective; Intros f H. -Cut (EXT x | ~ ((y: U) (f x) == (f y) -> x == y)). -2: Apply not_all_ex_not with P:=[x:U](y: U) (f x) == (f y) -> x == y; - Trivial with sets. -NewDestruct 1 as [x C]; Exists x. -Cut (EXT y | ~((f x)==(f y)->x==y)). -2: Apply not_all_ex_not with P:=[y:U](f x)==(f y)->x==y; Trivial with sets. -NewDestruct 1 as [y D]; Exists y. -Apply imply_to_and; Trivial with sets. +unfold injective in |- *; intros f H. +cut ( exists x : _ | ~ (forall y:U, f x = f y -> x = y)). +2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y); + trivial with sets. +destruct 1 as [x C]; exists x. +cut ( exists y : _ | ~ (f x = f y -> x = y)). +2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y); + trivial with sets. +destruct 1 as [y D]; exists y. +apply imply_to_and; trivial with sets. Qed. -Lemma cardinal_Im_intro: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) -> - (EX p: nat | (cardinal ? (Im A f) p)). +Lemma cardinal_Im_intro : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal _ A n -> exists p : nat | cardinal _ (Im A f) p. Proof. -Intros. -Apply finite_cardinal; Apply finite_image. -Apply cardinal_finite with n; Trivial with sets. +intros. +apply finite_cardinal; apply finite_image. +apply cardinal_finite with n; trivial with sets. Qed. -Lemma In_Image_elim: - (A: (Ensemble U)) (f: U -> V) (injective f) -> - (x: U) (In ? (Im A f) (f x)) -> (In ? A x). +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. Proof. -Intros. -Elim Im_inv with A f (f x); Trivial with sets. -Intros z C; Elim C; Intros InAz E. -Elim (H z x E); Trivial with sets. +intros. +elim Im_inv with A f (f x); trivial with sets. +intros z C; elim C; intros InAz E. +elim (H z x E); trivial with sets. Qed. -Lemma injective_preserves_cardinal: - (A: (Ensemble U)) (f: U -> V) (n: nat) (injective f) -> (cardinal ? A n) -> - (n': nat) (cardinal ? (Im A f) n') -> n' = n. +Lemma injective_preserves_cardinal : + forall (A:Ensemble U) (f:U -> V) (n:nat), + injective f -> + cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n. Proof. -NewInduction 2 as [|A n H'0 H'1 x H'2]; Auto with sets. -Rewrite (image_empty f). -Intros n' CE. -Apply cardinal_unicity with V (Empty_set V); Auto with sets. -Intro n'. -Rewrite (Im_add A x f). -Intro H'3. -Elim cardinal_Im_intro with A f n; Trivial with sets. -Intros i CI. -LApply (H'1 i); Trivial with sets. -Cut ~ (In ? (Im A f) (f x)). -Intros H0 H1. -Apply cardinal_unicity with V (Add ? (Im A f) (f x)); Trivial with sets. -Apply card_add; Auto with sets. -Rewrite <- H1; Trivial with sets. -Red; Intro; Apply H'2. -Apply In_Image_elim with f; Trivial with sets. +induction 2 as [| A n H'0 H'1 x H'2]; auto with sets. +rewrite (image_empty f). +intros n' CE. +apply cardinal_unicity with V (Empty_set V); auto with sets. +intro n'. +rewrite (Im_add A x f). +intro H'3. +elim cardinal_Im_intro with A f n; trivial with sets. +intros i CI. +lapply (H'1 i); trivial with sets. +cut (~ In _ (Im A f) (f x)). +intros H0 H1. +apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets. +apply card_add; auto with sets. +rewrite <- H1; trivial with sets. +red in |- *; intro; apply H'2. +apply In_Image_elim with f; trivial with sets. Qed. -Lemma cardinal_decreases: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) -> - (n': nat) (cardinal V (Im A f) n') -> (le n' n). +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. Proof. -NewInduction 1 as [|A n H'0 H'1 x H'2]; Auto with sets. -Rewrite (image_empty f); Intros. -Cut n' = O. -Intro E; Rewrite E; Trivial with sets. -Apply cardinal_unicity with V (Empty_set V); Auto with sets. -Intro n'. -Rewrite (Im_add A x f). -Elim cardinal_Im_intro with A f n; Trivial with sets. -Intros p C H'3. -Apply le_trans with (S p). -Apply card_Add_gen with V (Im A f) (f x); Trivial with sets. -Apply le_n_S; Auto with sets. +induction 1 as [| A n H'0 H'1 x H'2]; auto with sets. +rewrite (image_empty f); intros. +cut (n' = 0). +intro E; rewrite E; trivial with sets. +apply cardinal_unicity with V (Empty_set V); auto with sets. +intro n'. +rewrite (Im_add A x f). +elim cardinal_Im_intro with A f n; trivial with sets. +intros p C H'3. +apply le_trans with (S p). +apply card_Add_gen with V (Im A f) (f x); trivial with sets. +apply le_n_S; auto with sets. Qed. -Theorem Pigeonhole: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) -> - (n': nat) (cardinal V (Im A f) n') -> (lt n' n) -> ~ (injective f). +Theorem Pigeonhole : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal U A n -> + forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f. Proof. -Unfold not; Intros A f n CAn n' CIfn' ltn'n I. -Cut n' = n. -Intro E; Generalize ltn'n; Rewrite E; Exact (lt_n_n n). -Apply injective_preserves_cardinal with A := A f := f n := n; Trivial with sets. +unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I. +cut (n' = n). +intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n). +apply injective_preserves_cardinal with (A := A) (f := f) (n := n); + trivial with sets. Qed. -Lemma Pigeonhole_principle: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) -> - (n': nat) (cardinal ? (Im A f) n') -> (lt n' n) -> - (EXT x | (EXT y | (f x) == (f y) /\ ~ x == y)). +Lemma Pigeonhole_principle : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal _ A n -> + forall n':nat, + cardinal _ (Im A f) n' -> + n' < n -> exists x : _ | ( exists y : _ | f x = f y /\ x <> y). Proof. -Intros; Apply not_injective_elim. -Apply Pigeonhole with A n n'; Trivial with sets. +intros; apply not_injective_elim. +apply Pigeonhole with A n n'; trivial with sets. Qed. End Image. -Hints Resolve Im_def image_empty finite_image : sets v62. +Hint Resolve Im_def image_empty finite_image: sets v62. \ No newline at end of file diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index c6233453a..20ec73fa6 100755 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -40,193 +40,205 @@ Require Export Finite_sets_facts. Require Export Image. Section Approx. -Variable U: Type. +Variable U : Type. -Inductive Approximant [A, X:(Ensemble U)] : Prop := - Defn_of_Approximant: (Finite U X) -> (Included U X A) -> (Approximant A X). +Inductive Approximant (A X:Ensemble U) : Prop := + Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X. End Approx. -Hints Resolve Defn_of_Approximant. +Hint Resolve Defn_of_Approximant. Section Infinite_sets. -Variable U: Type. +Variable U : Type. -Lemma make_new_approximant: - (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> (Approximant U A X) -> - (Inhabited U (Setminus U A X)). +Lemma make_new_approximant : + forall A X:Ensemble U, + ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X). Proof. -Intros A X H' H'0. -Elim H'0; Intros H'1 H'2. -Apply Strict_super_set_contains_new_element; Auto with sets. -Red; Intro H'3; Apply H'. -Rewrite <- H'3; Auto with sets. +intros A X H' H'0. +elim H'0; intros H'1 H'2. +apply Strict_super_set_contains_new_element; auto with sets. +red in |- *; intro H'3; apply H'. +rewrite <- H'3; auto with sets. Qed. -Lemma approximants_grow: - (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> - (n: nat) (cardinal U X n) -> (Included U X A) -> - (EXT Y | (cardinal U Y (S n)) /\ (Included U Y A)). +Lemma approximants_grow : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, + cardinal U X n -> + Included U X A -> exists Y : _ | cardinal U Y (S n) /\ Included U Y A. Proof. -Intros A X H' n H'0; Elim H'0; Auto with sets. -Intro H'1. -Cut (Inhabited U (Setminus U A (Empty_set U))). -Intro H'2; Elim H'2. -Intros x H'3. -Exists (Add U (Empty_set U) x); Auto with sets. -Split. -Apply card_add; Auto with sets. -Cut (In U A x). -Intro H'4; Red; Auto with sets. -Intros x0 H'5; Elim H'5; Auto with sets. -Intros x1 H'6; Elim H'6; Auto with sets. -Elim H'3; Auto with sets. -Apply make_new_approximant; Auto with sets. -Intros A0 n0 H'1 H'2 x H'3 H'5. -LApply H'2; [Intro H'6; Elim H'6; Clear H'2 | Clear H'2]; Auto with sets. -Intros x0 H'2; Try Assumption. -Elim H'2; Intros H'7 H'8; Try Exact H'8; Clear H'2. -Elim (make_new_approximant A x0); Auto with sets. -Intros x1 H'2; Try Assumption. -Exists (Add U x0 x1); Auto with sets. -Split. -Apply card_add; Auto with sets. -Elim H'2; Auto with sets. -Red. -Intros x2 H'9; Elim H'9; Auto with sets. -Intros x3 H'10; Elim H'10; Auto with sets. -Elim H'2; Auto with sets. -Auto with sets. -Apply Defn_of_Approximant; Auto with sets. -Apply cardinal_finite with n := (S n0); Auto with sets. +intros A X H' n H'0; elim H'0; auto with sets. +intro H'1. +cut (Inhabited U (Setminus U A (Empty_set U))). +intro H'2; elim H'2. +intros x H'3. +exists (Add U (Empty_set U) x); auto with sets. +split. +apply card_add; auto with sets. +cut (In U A x). +intro H'4; red in |- *; auto with sets. +intros x0 H'5; elim H'5; auto with sets. +intros x1 H'6; elim H'6; auto with sets. +elim H'3; auto with sets. +apply make_new_approximant; auto with sets. +intros A0 n0 H'1 H'2 x H'3 H'5. +lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets. +intros x0 H'2; try assumption. +elim H'2; intros H'7 H'8; try exact H'8; clear H'2. +elim (make_new_approximant A x0); auto with sets. +intros x1 H'2; try assumption. +exists (Add U x0 x1); auto with sets. +split. +apply card_add; auto with sets. +elim H'2; auto with sets. +red in |- *. +intros x2 H'9; elim H'9; auto with sets. +intros x3 H'10; elim H'10; auto with sets. +elim H'2; auto with sets. +auto with sets. +apply Defn_of_Approximant; auto with sets. +apply cardinal_finite with (n := S n0); auto with sets. Qed. -Lemma approximants_grow': - (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> - (n: nat) (cardinal U X n) -> (Approximant U A X) -> - (EXT Y | (cardinal U Y (S n)) /\ (Approximant U A Y)). +Lemma approximants_grow' : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, + cardinal U X n -> + Approximant U A X -> + exists Y : _ | cardinal U Y (S n) /\ Approximant U A Y. Proof. -Intros A X H' n H'0 H'1; Try Assumption. -Elim H'1. -Intros H'2 H'3. -ElimType (EXT Y | (cardinal U Y (S n)) /\ (Included U Y A)). -Intros x H'4; Elim H'4; Intros H'5 H'6; Try Exact H'5; Clear H'4. -Exists x; Auto with sets. -Split; [Auto with sets | Idtac]. -Apply Defn_of_Approximant; Auto with sets. -Apply cardinal_finite with n := (S n); Auto with sets. -Apply approximants_grow with X := X; Auto with sets. +intros A X H' n H'0 H'1; try assumption. +elim H'1. +intros H'2 H'3. +elimtype ( exists Y : _ | cardinal U Y (S n) /\ Included U Y A). +intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4. +exists x; auto with sets. +split; [ auto with sets | idtac ]. +apply Defn_of_Approximant; auto with 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: - (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> - (n: nat) (EXT Y | (cardinal U Y n) /\ (Approximant U A Y)). +Lemma approximant_can_be_any_size : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, exists Y : _ | cardinal U Y n /\ Approximant U A Y. Proof. -Intros A H' H'0 n; Elim n. -Exists (Empty_set U); Auto with sets. -Intros n0 H'1; Elim H'1. -Intros x H'2. -Apply approximants_grow' with X := x; Tauto. +intros A H' H'0 n; elim n. +exists (Empty_set U); auto with sets. +intros n0 H'1; elim H'1. +intros x H'2. +apply approximants_grow' with (X := x); tauto. Qed. -Variable V: Type. +Variable V : Type. -Theorem Image_set_continuous: - (A: (Ensemble U)) - (f: U -> V) (X: (Ensemble V)) (Finite V X) -> (Included V X (Im U V A f)) -> - (EX n | - (EXT Y | ((cardinal U Y n) /\ (Included U Y A)) /\ (Im U V Y f) == X)). +Theorem Image_set_continuous : + forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), + Finite V X -> + Included V X (Im U V A f) -> + exists n : _ + | ( exists Y : _ | (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X). Proof. -Intros A f X H'; Elim H'. -Intro H'0; Exists O. -Exists (Empty_set U); Auto with sets. -Intros A0 H'0 H'1 x H'2 H'3; Try Assumption. -LApply H'1; - [Intro H'4; Elim H'4; Intros n E; Elim E; Clear H'4 H'1 | Clear H'1]; Auto with sets. -Intros x0 H'1; Try Assumption. -Exists (S n); Try Assumption. -Elim H'1; Intros H'4 H'5; Elim H'4; Intros H'6 H'7; Try Exact H'6; Clear H'4 H'1. -Clear E. -Generalize H'2. -Rewrite <- H'5. -Intro H'1; Try Assumption. -Red in H'3. -Generalize (H'3 x). -Intro H'4; LApply H'4; [Intro H'8; Try Exact H'8; Clear H'4 | Clear H'4]; Auto with sets. -Specialize 5 Im_inv with U := U V:=V X := A f := f y := x; Intro H'11; - LApply H'11; [Intro H'13; Elim H'11; Clear H'11 | Clear H'11]; Auto with sets. -Intros x1 H'4; Try Assumption. -Apply exT_intro with x := (Add U x0 x1). -Split; [Split; [Try Assumption | Idtac] | Idtac]. -Apply card_add; Auto with sets. -Red; Intro H'9; Try Exact H'9. -Apply H'1. -Elim H'4; Intros H'10 H'11; Rewrite <- H'11; Clear H'4; Auto with sets. -Elim H'4; Intros H'9 H'10; Try Exact H'9; Clear H'4; Auto with sets. -Red; Auto with sets. -Intros x2 H'4; Elim H'4; Auto with sets. -Intros x3 H'11; Elim H'11; Auto with sets. -Elim H'4; Intros H'9 H'10; Rewrite <- H'10; Clear H'4; Auto with sets. -Apply Im_add; Auto with sets. +intros A f X H'; elim H'. +intro H'0; exists 0. +exists (Empty_set U); auto with sets. +intros A0 H'0 H'1 x H'2 H'3; try assumption. +lapply H'1; + [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ]; + auto with sets. +intros x0 H'1; try assumption. +exists (S n); try assumption. +elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6; + clear H'4 H'1. +clear E. +generalize H'2. +rewrite <- H'5. +intro H'1; try assumption. +red in H'3. +generalize (H'3 x). +intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ]; + auto with sets. +specialize 5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x); + intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ]; + auto with sets. +intros x1 H'4; try assumption. +apply ex_intro with (x := Add U x0 x1). +split; [ split; [ try assumption | idtac ] | idtac ]. +apply card_add; auto with sets. +red in |- *; intro H'9; try exact H'9. +apply H'1. +elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets. +elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets. +red in |- *; auto with sets. +intros x2 H'4; elim H'4; auto with sets. +intros x3 H'11; elim H'11; auto with sets. +elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets. +apply Im_add; auto with sets. Qed. -Theorem Image_set_continuous': - (A: (Ensemble U)) - (f: U -> V) (X: (Ensemble V)) (Approximant V (Im U V A f) X) -> - (EXT Y | (Approximant U A Y) /\ (Im U V Y f) == X). +Theorem Image_set_continuous' : + forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), + Approximant V (Im U V A f) X -> + exists Y : _ | Approximant U A Y /\ Im U V Y f = X. Proof. -Intros A f X H'; Try Assumption. -Cut (EX n | (EXT Y | - ((cardinal U Y n) /\ (Included U Y A)) /\ (Im U V Y f) == X)). -Intro H'0; Elim H'0; Intros n E; Elim E; Clear H'0. -Intros x H'0; Try Assumption. -Elim H'0; Intros H'1 H'2; Elim H'1; Intros H'3 H'4; Try Exact H'3; - Clear H'1 H'0; Auto with sets. -Exists x. -Split; [Idtac | Try Assumption]. -Apply Defn_of_Approximant; Auto with sets. -Apply cardinal_finite with n := n; Auto with sets. -Apply Image_set_continuous; Auto with sets. -Elim H'; Auto with sets. -Elim H'; Auto with sets. +intros A f X H'; try assumption. +cut + ( exists n : _ + | ( exists Y : _ | (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)). +intro H'0; elim H'0; intros n E; elim E; clear H'0. +intros x H'0; try assumption. +elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3; + clear H'1 H'0; auto with sets. +exists x. +split; [ idtac | try assumption ]. +apply Defn_of_Approximant; auto with sets. +apply cardinal_finite with (n := n); auto with sets. +apply Image_set_continuous; auto with sets. +elim H'; auto with sets. +elim H'; auto with sets. Qed. -Theorem Pigeonhole_bis: - (A: (Ensemble U)) (f: U -> V) ~ (Finite U A) -> (Finite V (Im U V A f)) -> - ~ (injective U V f). +Theorem Pigeonhole_bis : + forall (A:Ensemble U) (f:U -> V), + ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f. Proof. -Intros A f H'0 H'1; Try Assumption. -Elim (Image_set_continuous' A f (Im U V A f)); Auto with sets. -Intros x H'2; Elim H'2; Intros H'3 H'4; Try Exact H'3; Clear H'2. -Elim (make_new_approximant A x); Auto with sets. -Intros x0 H'2; Elim H'2. -Intros H'5 H'6. -Elim (finite_cardinal V (Im U V A f)); Auto with sets. -Intros n E. -Elim (finite_cardinal U x); Auto with sets. -Intros n0 E0. -Apply Pigeonhole with A := (Add U x x0) n := (S n0) n' := n. -Apply card_add; Auto with sets. -Rewrite (Im_add U V x x0 f); Auto with sets. -Cut (In V (Im U V x f) (f x0)). -Intro H'8. -Rewrite (Non_disjoint_union V (Im U V x f) (f x0)); Auto with sets. -Rewrite H'4; Auto with sets. -Elim (Extension V (Im U V x f) (Im U V A f)); Auto with sets. -Apply le_lt_n_Sm. -Apply cardinal_decreases with U := U V := V A := x f := f; Auto with sets. -Rewrite H'4; Auto with sets. -Elim H'3; Auto with sets. +intros A f H'0 H'1; try assumption. +elim (Image_set_continuous' A f (Im U V A f)); auto with sets. +intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2. +elim (make_new_approximant A x); auto with sets. +intros x0 H'2; elim H'2. +intros H'5 H'6. +elim (finite_cardinal V (Im U V A f)); auto with sets. +intros n E. +elim (finite_cardinal U x); auto with sets. +intros n0 E0. +apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n). +apply card_add; auto with sets. +rewrite (Im_add U V x x0 f); auto with sets. +cut (In V (Im U V x f) (f x0)). +intro H'8. +rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets. +rewrite H'4; auto with sets. +elim (Extension V (Im U V x f) (Im U V A f)); auto with sets. +apply le_lt_n_Sm. +apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f); + auto with sets. +rewrite H'4; auto with sets. +elim H'3; auto with sets. Qed. -Theorem Pigeonhole_ter: - (A: (Ensemble U)) - (f: U -> V) (n: nat) (injective U V f) -> (Finite V (Im U V A f)) -> - (Finite U A). +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. Proof. -Intros A f H' H'0 H'1. -Apply NNPP. -Red; Intro H'2. -Elim (Pigeonhole_bis A f); Auto with sets. +intros A f H' H'0 H'1. +apply NNPP. +red in |- *; intro H'2. +elim (Pigeonhole_bis A f); auto with sets. Qed. -End Infinite_sets. +End Infinite_sets. \ No newline at end of file diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index dbfc6b463..7f8e1695a 100755 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -46,116 +46,118 @@ Require Export Cpo. Section Integers_sect. -Inductive Integers : (Ensemble nat) := - Integers_defn: (x: nat) (In nat Integers x). -Hints Resolve Integers_defn. +Inductive Integers : Ensemble nat := + Integers_defn : forall x:nat, In nat Integers x. +Hint Resolve Integers_defn. -Lemma le_reflexive: (Reflexive nat le). +Lemma le_reflexive : Reflexive nat le. Proof. -Red; Auto with arith. +red in |- *; auto with arith. Qed. -Lemma le_antisym: (Antisymmetric nat le). +Lemma le_antisym : Antisymmetric nat le. Proof. -Red; Intros x y H H';Rewrite (le_antisym x y);Auto. +red in |- *; intros x y H H'; rewrite (le_antisym x y); auto. Qed. -Lemma le_trans: (Transitive nat le). +Lemma le_trans : Transitive nat le. Proof. -Red; Intros; Apply le_trans with y;Auto. +red in |- *; intros; apply le_trans with y; auto. Qed. -Hints Resolve le_reflexive le_antisym le_trans. +Hint Resolve le_reflexive le_antisym le_trans. -Lemma le_Order: (Order nat le). +Lemma le_Order : Order nat le. Proof. -Auto with sets arith. +auto with sets arith. Qed. -Hints Resolve le_Order. +Hint Resolve le_Order. -Lemma triv_nat: (n: nat) (In nat Integers n). +Lemma triv_nat : forall n:nat, In nat Integers n. Proof. -Auto with sets arith. +auto with sets arith. Qed. -Hints Resolve triv_nat. +Hint Resolve triv_nat. -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 := O; Auto with sets arith. +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); auto with sets arith. Defined. -Hints Unfold nat_po. +Hint Unfold nat_po. -Lemma le_total_order: (Totally_ordered nat nat_po Integers). +Lemma le_total_order : Totally_ordered nat nat_po Integers. Proof. -Apply Totally_ordered_definition. -Simpl. -Intros H' x y H'0. -Specialize 2 le_or_lt with n := x m := y; Intro H'2; Elim H'2. -Intro H'1; Left; Auto with sets arith. -Intro H'1; Right. -Cut (le y x); Auto with sets arith. +apply Totally_ordered_definition. +simpl in |- *. +intros H' x y H'0. +specialize 2le_or_lt with (n := x) (m := y); intro H'2; elim H'2. +intro H'1; left; auto with sets arith. +intro H'1; right. +cut (y <= x); auto with sets arith. Qed. -Hints Resolve le_total_order. +Hint Resolve le_total_order. -Lemma Finite_subset_has_lub: - (X: (Ensemble nat)) (Finite nat X) -> - (EXT m: nat | (Upper_Bound nat nat_po X m)). +Lemma Finite_subset_has_lub : + forall X:Ensemble nat, + Finite nat X -> exists m : nat | Upper_Bound nat nat_po X m. Proof. -Intros X H'; Elim H'. -Exists O. -Apply Upper_Bound_definition; Auto with sets arith. -Intros y H'0; Elim H'0; Auto with sets arith. -Intros A H'0 H'1 x H'2; Try Assumption. -Elim H'1; Intros x0 H'3; Clear H'1. -Elim le_total_order. -Simpl. -Intro H'1; Try Assumption. -LApply H'1; [Intro H'4; Idtac | Try Assumption]; Auto with sets arith. -Generalize (H'4 x0 x). -Clear H'4. -Clear H'1. -Intro H'1; LApply H'1; - [Intro H'4; Elim H'4; - [Intro H'5; Try Exact H'5; Clear H'4 H'1 | Intro H'5; Clear H'4 H'1] | - Clear H'1]. -Exists x. -Apply Upper_Bound_definition; Auto with sets arith; Simpl. -Intros y H'1; Elim H'1. -Generalize le_trans. -Intro H'4; Red in H'4. -Intros x1 H'6; Try Assumption. -Apply H'4 with y := x0; Auto with sets arith. -Elim H'3; Simpl; Auto with sets arith. -Intros x1 H'4; Elim H'4; Auto with sets arith. -Exists x0. -Apply Upper_Bound_definition; Auto with sets arith; Simpl. -Intros y H'1; Elim H'1. -Intros x1 H'4; Try Assumption. -Elim H'3; Simpl; Auto with sets arith. -Intros x1 H'4; Elim H'4; Auto with sets arith. -Red. -Intros x1 H'1; Elim H'1; Auto with sets arith. +intros X H'; elim H'. +exists 0. +apply Upper_Bound_definition; auto with sets arith. +intros y H'0; elim H'0; auto with sets arith. +intros A H'0 H'1 x H'2; try assumption. +elim H'1; intros x0 H'3; clear H'1. +elim le_total_order. +simpl in |- *. +intro H'1; try assumption. +lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith. +generalize (H'4 x0 x). +clear H'4. +clear H'1. +intro H'1; lapply H'1; + [ intro H'4; elim H'4; + [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ] + | clear H'1 ]. +exists x. +apply Upper_Bound_definition; auto with sets arith; simpl in |- *. +intros y H'1; elim H'1. +generalize le_trans. +intro H'4; red in H'4. +intros x1 H'6; try assumption. +apply H'4 with (y := x0); auto with sets arith. +elim H'3; simpl in |- *; auto with sets arith. +intros x1 H'4; elim H'4; auto with sets arith. +exists x0. +apply Upper_Bound_definition; auto with sets arith; simpl in |- *. +intros y H'1; elim H'1. +intros x1 H'4; try assumption. +elim H'3; simpl in |- *; auto with sets arith. +intros x1 H'4; elim H'4; auto with sets arith. +red in |- *. +intros x1 H'1; elim H'1; auto with sets arith. Qed. -Lemma Integers_has_no_ub: ~ (EXT m:nat | (Upper_Bound nat nat_po Integers m)). +Lemma Integers_has_no_ub : + ~ ( exists m : nat | Upper_Bound nat nat_po Integers m). Proof. -Red; Intro H'; Elim H'. -Intros x H'0. -Elim H'0; Intros H'1 H'2. -Cut (In nat Integers (S x)). -Intro H'3. -Specialize 1 H'2 with y := (S x); Intro H'4; LApply H'4; - [Intro H'5; Clear H'4 | Try Assumption; Clear H'4]. -Simpl in H'5. -Absurd (le (S x) x); Auto with arith. -Auto with sets arith. +red in |- *; intro H'; elim H'. +intros x H'0. +elim H'0; intros H'1 H'2. +cut (In nat Integers (S x)). +intro H'3. +specialize 1H'2 with (y := S x); intro H'4; lapply H'4; + [ intro H'5; clear H'4 | try assumption; clear H'4 ]. +simpl in H'5. +absurd (S x <= x); auto with arith. +auto with sets arith. Qed. -Lemma Integers_infinite: ~ (Finite nat Integers). +Lemma Integers_infinite : ~ Finite nat Integers. Proof. -Generalize Integers_has_no_ub. -Intro H'; Red; Intro H'0; Try Exact H'0. -Apply H'. -Apply Finite_subset_has_lub; Auto with sets arith. +generalize Integers_has_no_ub. +intro H'; red in |- *; intro H'0; try exact H'0. +apply H'. +apply Finite_subset_has_lub; auto with sets arith. Qed. End Integers_sect. @@ -163,4 +165,3 @@ End Integers_sect. - diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 37fb47e27..a3ae98d0a 100755 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -10,7 +10,7 @@ (* G. Huet 1-9-95 *) -Require Permut. +Require Import Permut. Set Implicit Arguments. @@ -18,155 +18,159 @@ Section multiset_defs. Variable A : Set. Variable eqA : A -> A -> Prop. -Hypothesis Aeq_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}. +Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. -Inductive multiset : Set := - Bag : (A->nat) -> multiset. +Inductive multiset : Set := + Bag : (A -> nat) -> multiset. -Definition EmptyBag := (Bag [a:A]O). -Definition SingletonBag := [a:A] - (Bag [a':A]Cases (Aeq_dec a a') of - (left _) => (S O) - | (right _) => O - end - ). +Definition EmptyBag := Bag (fun a:A => 0). +Definition SingletonBag (a:A) := + Bag (fun a':A => match Aeq_dec a a' with + | left _ => 1 + | right _ => 0 + end). -Definition multiplicity : multiset -> A -> nat := - [m:multiset][a:A]let (f) = m in (f a). +Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a. (** multiset equality *) -Definition meq := [m1,m2:multiset] - (a:A)(multiplicity m1 a)=(multiplicity m2 a). +Definition meq (m1 m2:multiset) := + forall a:A, multiplicity m1 a = multiplicity m2 a. -Hints Unfold meq multiplicity. +Hint Unfold meq multiplicity. -Lemma meq_refl : (x:multiset)(meq x x). +Lemma meq_refl : forall x:multiset, meq x x. Proof. -NewDestruct x; Auto. +destruct x; auto. Qed. -Hints Resolve meq_refl. +Hint Resolve meq_refl. -Lemma meq_trans : (x,y,z:multiset)(meq x y)->(meq y z)->(meq x z). +Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z. Proof. -Unfold meq. -NewDestruct x; NewDestruct y; NewDestruct z. -Intros; Rewrite H; Auto. +unfold meq in |- *. +destruct x; destruct y; destruct z. +intros; rewrite H; auto. Qed. -Lemma meq_sym : (x,y:multiset)(meq x y)->(meq y x). +Lemma meq_sym : forall x y:multiset, meq x y -> meq y x. Proof. -Unfold meq. -NewDestruct x; NewDestruct y; Auto. +unfold meq in |- *. +destruct x; destruct y; auto. Qed. -Hints Immediate meq_sym. +Hint Immediate meq_sym. (** multiset union *) -Definition munion := [m1,m2:multiset] - (Bag [a:A](plus (multiplicity m1 a)(multiplicity m2 a))). +Definition munion (m1 m2:multiset) := + Bag (fun a:A => multiplicity m1 a + multiplicity m2 a). -Lemma munion_empty_left : - (x:multiset)(meq x (munion EmptyBag x)). +Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x). Proof. -Unfold meq; Unfold munion; Simpl; Auto. +unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. Qed. -Hints Resolve munion_empty_left. +Hint Resolve munion_empty_left. -Lemma munion_empty_right : - (x:multiset)(meq x (munion x EmptyBag)). +Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag). Proof. -Unfold meq; Unfold munion; Simpl; Auto. +unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. Qed. -Require Plus. (* comm. and ass. of plus *) +Require Import Plus. (* comm. and ass. of plus *) -Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)). +Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). Proof. -Unfold meq; Unfold multiplicity; Unfold munion. -NewDestruct x; NewDestruct y; Auto with arith. +unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *. +destruct x; destruct y; auto with arith. Qed. -Hints Resolve munion_comm. +Hint Resolve munion_comm. -Lemma munion_ass : - (x,y,z:multiset)(meq (munion (munion x y) z) (munion x (munion y z))). +Lemma munion_ass : + forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)). Proof. -Unfold meq; Unfold munion; Unfold multiplicity. -NewDestruct x; NewDestruct y; NewDestruct z; Auto with arith. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z; auto with arith. Qed. -Hints Resolve munion_ass. +Hint Resolve munion_ass. -Lemma meq_left : (x,y,z:multiset)(meq x y)->(meq (munion x z) (munion y z)). +Lemma meq_left : + forall x y z:multiset, meq x y -> meq (munion x z) (munion y z). Proof. -Unfold meq; Unfold munion; Unfold multiplicity. -NewDestruct x; NewDestruct y; NewDestruct z. -Intros; Elim H; Auto with arith. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto with arith. Qed. -Hints Resolve meq_left. +Hint Resolve meq_left. -Lemma meq_right : (x,y,z:multiset)(meq x y)->(meq (munion z x) (munion z y)). +Lemma meq_right : + forall x y z:multiset, meq x y -> meq (munion z x) (munion z y). Proof. -Unfold meq; Unfold munion; Unfold multiplicity. -NewDestruct x; NewDestruct y; NewDestruct z. -Intros; Elim H; Auto. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto. Qed. -Hints Resolve meq_right. +Hint Resolve meq_right. (** Here we should make multiset an abstract datatype, by hiding [Bag], [munion], [multiplicity]; all further properties are proved abstractly *) Lemma munion_rotate : - (x,y,z:multiset)(meq (munion x (munion y z)) (munion z (munion x y))). + forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)). Proof. -Intros; Apply (op_rotate multiset munion meq); Auto. -Exact meq_trans. +intros; apply (op_rotate multiset munion meq); auto. +exact meq_trans. Qed. -Lemma meq_congr : (x,y,z,t:multiset)(meq x y)->(meq z t)-> - (meq (munion x z) (munion y t)). +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. -Exact meq_trans. +intros; apply (cong_congr multiset munion meq); auto. +exact meq_trans. Qed. Lemma munion_perm_left : - (x,y,z:multiset)(meq (munion x (munion y z)) (munion y (munion x z))). + 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. -Exact meq_trans. +intros; apply (perm_left multiset munion meq); auto. +exact meq_trans. Qed. -Lemma multiset_twist1 : (x,y,z,t:multiset) - (meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z)). +Lemma multiset_twist1 : + forall x y z t:multiset, + meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z). Proof. -Intros; Apply (twist multiset munion meq); Auto. -Exact meq_trans. +intros; apply (twist multiset munion meq); auto. +exact meq_trans. Qed. -Lemma multiset_twist2 : (x,y,z,t:multiset) - (meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t)). +Lemma multiset_twist2 : + forall x y z t:multiset, + meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t). Proof. -Intros; Apply meq_trans with (munion (munion x (munion y z)) t). -Apply meq_sym; Apply munion_ass. -Apply meq_left; Apply munion_perm_left. +intros; apply meq_trans with (munion (munion x (munion y z)) t). +apply meq_sym; apply munion_ass. +apply meq_left; apply munion_perm_left. Qed. (** specific for treesort *) -Lemma treesort_twist1 : (x,y,z,t,u:multiset) (meq u (munion y z)) -> - (meq (munion x (munion u t)) (munion (munion y (munion x t)) z)). +Lemma treesort_twist1 : + forall x y z t u:multiset, + meq u (munion y z) -> + meq (munion x (munion u t)) (munion (munion y (munion x t)) z). Proof. -Intros; Apply meq_trans with (munion x (munion (munion y z) t)). -Apply meq_right; Apply meq_left; Trivial. -Apply multiset_twist1. +intros; apply meq_trans with (munion x (munion (munion y z) t)). +apply meq_right; apply meq_left; trivial. +apply multiset_twist1. Qed. -Lemma treesort_twist2 : (x,y,z,t,u:multiset) (meq u (munion y z)) -> - (meq (munion x (munion u t)) (munion (munion y (munion x z)) t)). +Lemma treesort_twist2 : + forall x y z t u:multiset, + meq u (munion y z) -> + meq (munion x (munion u t)) (munion (munion y (munion x z)) t). Proof. -Intros; Apply meq_trans with (munion x (munion (munion y z) t)). -Apply meq_right; Apply meq_left; Trivial. -Apply multiset_twist2. +intros; apply meq_trans with (munion x (munion (munion y z) t)). +apply meq_right; apply meq_left; trivial. +apply multiset_twist2. Qed. @@ -181,6 +185,7 @@ End multiset_defs. Unset Implicit Arguments. -Hints Unfold meq multiplicity : v62 datatypes. -Hints Resolve munion_empty_right munion_comm munion_ass meq_left meq_right munion_empty_left : v62 datatypes. -Hints Immediate meq_sym : v62 datatypes. +Hint Unfold meq multiplicity: v62 datatypes. +Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right + munion_empty_left: v62 datatypes. +Hint Immediate meq_sym: v62 datatypes. \ No newline at end of file diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index f3d692b85..5ef6bc9b0 100755 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -30,71 +30,71 @@ Require Export Ensembles. Require Export Relations_1. Section Partial_orders. -Variable U: Type. +Variable U : Type. -Definition Carrier := (Ensemble U). +Definition Carrier := Ensemble U. -Definition Rel := (Relation 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. +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 := [x, y: U] (Rel_of p x y) /\ ~ x == y. +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) -> - ~ (EXT z | (Strict_Rel_of x z) /\ (Strict_Rel_of z y)) -> - (covers y x). +Inductive covers (y x:U) : Prop := + Definition_of_covers : + Strict_Rel_of x y -> + ~ ( exists z : _ | Strict_Rel_of x z /\ Strict_Rel_of z y) -> + covers y x. End Partial_orders. -Hints Unfold Carrier_of Rel_of Strict_Rel_of : sets v62. -Hints Resolve Definition_of_covers : sets v62. +Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62. +Hint Resolve Definition_of_covers: sets v62. Section Partial_order_facts. -Variable U:Type. -Variable D:(PO U). +Variable U : Type. +Variable D : PO U. -Lemma Strict_Rel_Transitive_with_Rel: - (x:U) (y:U) (z:U) (Strict_Rel_of U D x y) -> (Rel_of U D y z) -> - (Strict_Rel_of U D x z). -Unfold 1 Strict_Rel_of. -Red. -Elim D; Simpl. -Intros C R H' H'0; Elim H'0. -Intros H'1 H'2 H'3 x y z H'4 H'5; Split. -Apply H'2 with y := y; Tauto. -Red; Intro H'6. -Elim H'4; Intros H'7 H'8; Apply H'8; Clear H'4. -Apply H'3; Auto. -Rewrite H'6; Tauto. +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. +unfold Strict_Rel_of at 1 in |- *. +red in |- *. +elim D; simpl in |- *. +intros C R H' H'0; elim H'0. +intros H'1 H'2 H'3 x y z H'4 H'5; split. +apply H'2 with (y := y); tauto. +red in |- *; intro H'6. +elim H'4; intros H'7 H'8; apply H'8; clear H'4. +apply H'3; auto. +rewrite H'6; tauto. Qed. -Lemma Strict_Rel_Transitive_with_Rel_left: - (x:U) (y:U) (z:U) (Rel_of U D x y) -> (Strict_Rel_of U D y z) -> - (Strict_Rel_of U D x z). -Unfold 1 Strict_Rel_of. -Red. -Elim D; Simpl. -Intros C R H' H'0; Elim H'0. -Intros H'1 H'2 H'3 x y z H'4 H'5; Split. -Apply H'2 with y := y; Tauto. -Red; Intro H'6. -Elim H'5; Intros H'7 H'8; Apply H'8; Clear H'5. -Apply H'3; Auto. -Rewrite <- H'6; Auto. +Lemma Strict_Rel_Transitive_with_Rel_left : + forall x y z:U, + Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z. +unfold Strict_Rel_of at 1 in |- *. +red in |- *. +elim D; simpl in |- *. +intros C R H' H'0; elim H'0. +intros H'1 H'2 H'3 x y z H'4 H'5; split. +apply H'2 with (y := y); tauto. +red in |- *; intro H'6. +elim H'5; intros H'7 H'8; apply H'8; clear H'5. +apply H'3; auto. +rewrite <- H'6; auto. Qed. -Lemma Strict_Rel_Transitive: (Transitive U (Strict_Rel_of U D)). -Red. -Intros x y z H' H'0. -Apply Strict_Rel_Transitive_with_Rel with y := y; - [ Intuition | Unfold Strict_Rel_of in H' H'0; Intuition ]. +Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D). +red in |- *. +intros x y z H' H'0. +apply Strict_Rel_Transitive_with_Rel with (y := y); + [ intuition | unfold Strict_Rel_of in H', H'0; intuition ]. Qed. -End Partial_order_facts. +End Partial_order_facts. \ No newline at end of file diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 03a8b7428..c3a1da01c 100755 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -15,77 +15,77 @@ Section Axiomatisation. -Variable U: Set. +Variable U : Set. -Variable op: U -> U -> U. +Variable op : U -> U -> U. Variable cong : U -> U -> Prop. -Hypothesis op_comm : (x,y:U)(cong (op x y) (op y x)). -Hypothesis op_ass : (x,y,z:U)(cong (op (op x y) z) (op x (op y z))). +Hypothesis op_comm : forall x y:U, cong (op x y) (op y x). +Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)). -Hypothesis cong_left : (x,y,z:U)(cong x y)->(cong (op x z) (op y z)). -Hypothesis cong_right : (x,y,z:U)(cong x y)->(cong (op z x) (op z y)). -Hypothesis cong_trans : (x,y,z:U)(cong x y)->(cong y z)->(cong x z). -Hypothesis cong_sym : (x,y:U)(cong x y)->(cong y x). +Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z). +Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y). +Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z. +Hypothesis cong_sym : forall x y:U, cong x y -> cong y x. (** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *) Lemma cong_congr : - (x,y,z,t:U)(cong x y)->(cong z t)->(cong (op x z) (op y t)). + forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t). Proof. -Intros; Apply cong_trans with (op y z). -Apply cong_left; Trivial. -Apply cong_right; Trivial. +intros; apply cong_trans with (op y z). +apply cong_left; trivial. +apply cong_right; trivial. Qed. -Lemma comm_right : (x,y,z:U)(cong (op x (op y z)) (op x (op z y))). +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. +intros; apply cong_right; apply op_comm. Qed. -Lemma comm_left : (x,y,z:U)(cong (op (op x y) z) (op (op y x) z)). +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. +intros; apply cong_left; apply op_comm. Qed. -Lemma perm_right : (x,y,z:U)(cong (op (op x y) z) (op (op x z) y)). +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_right; Apply op_comm. -Apply cong_sym; Apply op_ass. +intros. +apply cong_trans with (op x (op y z)). +apply op_ass. +apply cong_trans with (op x (op z y)). +apply cong_right; apply op_comm. +apply cong_sym; apply op_ass. Qed. -Lemma perm_left : (x,y,z:U)(cong (op x (op y z)) (op y (op x z))). +Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)). Proof. -Intros. -Apply cong_trans with (op (op x y) z). -Apply cong_sym; Apply op_ass. -Apply cong_trans with (op (op y x) z). -Apply cong_left; Apply op_comm. -Apply op_ass. +intros. +apply cong_trans with (op (op x y) z). +apply cong_sym; apply op_ass. +apply cong_trans with (op (op y x) z). +apply cong_left; apply op_comm. +apply op_ass. Qed. -Lemma op_rotate : (x,y,z,t:U)(cong (op x (op y z)) (op z (op x y))). +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). -Apply cong_sym; Apply op_ass. -Apply op_comm. +intros; apply cong_trans with (op (op x y) z). +apply cong_sym; apply op_ass. +apply op_comm. Qed. (* Needed for treesort ... *) -Lemma twist : (x,y,z,t:U) - (cong (op x (op (op y z) t)) (op (op y (op x t)) z)). +Lemma twist : + forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z). Proof. -Intros. -Apply cong_trans with (op x (op (op y t) z)). -Apply cong_right; Apply perm_right. -Apply cong_trans with (op (op x (op y t)) z). -Apply cong_sym; Apply op_ass. -Apply cong_left; Apply perm_left. +intros. +apply cong_trans with (op x (op (op y t) z)). +apply cong_right; apply perm_right. +apply cong_trans with (op (op x (op y t)) z). +apply cong_sym; apply op_ass. +apply cong_left; apply perm_left. Qed. -End Axiomatisation. +End Axiomatisation. \ No newline at end of file diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index c9c7188b1..543702276 100755 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -33,156 +33,158 @@ Require Export Partial_Order. Require Export Cpo. Section The_power_set_partial_order. -Variable U: Type. +Variable U : Type. -Inductive Power_set [A:(Ensemble U)]: (Ensemble (Ensemble U)) := - Definition_of_Power_set: - (X: (Ensemble U)) (Included U X A) -> (In (Ensemble U) (Power_set A) X). -Hints Resolve Definition_of_Power_set. +Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) := + Definition_of_Power_set : + forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X. +Hint Resolve Definition_of_Power_set. -Theorem Empty_set_minimal: (X: (Ensemble U)) (Included U (Empty_set U) X). -Intro X; Red. -Intros x H'; Elim H'. +Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X. +intro X; red in |- *. +intros x H'; elim H'. Qed. -Hints Resolve Empty_set_minimal. +Hint Resolve Empty_set_minimal. -Theorem Power_set_Inhabited: - (X: (Ensemble U)) (Inhabited (Ensemble U) (Power_set X)). -Intro X. -Apply Inhabited_intro with (Empty_set U); Auto with sets. +Theorem Power_set_Inhabited : + forall X:Ensemble U, Inhabited (Ensemble U) (Power_set X). +intro X. +apply Inhabited_intro with (Empty_set U); auto with sets. Qed. -Hints Resolve Power_set_Inhabited. +Hint Resolve Power_set_Inhabited. -Theorem Inclusion_is_an_order: (Order (Ensemble U) (Included U)). -Auto 6 with sets. +Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U). +auto 6 with sets. Qed. -Hints Resolve Inclusion_is_an_order. +Hint Resolve Inclusion_is_an_order. -Theorem Inclusion_is_transitive: (Transitive (Ensemble U) (Included U)). -Elim Inclusion_is_an_order; Auto with sets. +Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U). +elim Inclusion_is_an_order; auto with sets. Qed. -Hints Resolve Inclusion_is_transitive. +Hint Resolve Inclusion_is_transitive. -Definition Power_set_PO: (Ensemble U) -> (PO (Ensemble U)). -Intro A; Try Assumption. -Apply Definition_of_PO with (Power_set A) (Included U); Auto with sets. +Definition Power_set_PO : Ensemble U -> PO (Ensemble U). +intro A; try assumption. +apply Definition_of_PO with (Power_set A) (Included U); auto with sets. Defined. -Hints Unfold Power_set_PO. +Hint Unfold Power_set_PO. -Theorem Strict_Rel_is_Strict_Included: - (same_relation - (Ensemble U) (Strict_Included U) - (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U)))). -Auto with sets. +Theorem Strict_Rel_is_Strict_Included : + same_relation (Ensemble U) (Strict_Included U) + (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))). +auto with sets. Qed. -Hints Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included. +Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included. -Lemma Strict_inclusion_is_transitive_with_inclusion: - (x, y, z:(Ensemble U)) (Strict_Included U x y) -> (Included U y z) -> - (Strict_Included U x z). -Intros x y z H' H'0; Try Assumption. -Elim Strict_Rel_is_Strict_Included. -Unfold contains. -Intros H'1 H'2; Try Assumption. -Apply H'1. -Apply Strict_Rel_Transitive_with_Rel with y := y; Auto with sets. +Lemma Strict_inclusion_is_transitive_with_inclusion : + forall x y z:Ensemble U, + Strict_Included U x y -> Included U y z -> Strict_Included U x z. +intros x y z H' H'0; try assumption. +elim Strict_Rel_is_Strict_Included. +unfold contains in |- *. +intros H'1 H'2; try assumption. +apply H'1. +apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets. Qed. -Lemma Strict_inclusion_is_transitive_with_inclusion_left: - (x, y, z:(Ensemble U)) (Included U x y) -> (Strict_Included U y z) -> - (Strict_Included U x z). -Intros x y z H' H'0; Try Assumption. -Elim Strict_Rel_is_Strict_Included. -Unfold contains. -Intros H'1 H'2; Try Assumption. -Apply H'1. -Apply Strict_Rel_Transitive_with_Rel_left with y := y; Auto with sets. +Lemma Strict_inclusion_is_transitive_with_inclusion_left : + forall x y z:Ensemble U, + Included U x y -> Strict_Included U y z -> Strict_Included U x z. +intros x y z H' H'0; try assumption. +elim Strict_Rel_is_Strict_Included. +unfold contains in |- *. +intros H'1 H'2; try assumption. +apply H'1. +apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets. Qed. -Lemma Strict_inclusion_is_transitive: - (Transitive (Ensemble U) (Strict_Included U)). -Apply cong_transitive_same_relation - with R := (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))); Auto with sets. +Lemma Strict_inclusion_is_transitive : + Transitive (Ensemble U) (Strict_Included U). +apply cong_transitive_same_relation with + (R := Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))); + auto with sets. Qed. -Theorem Empty_set_is_Bottom: - (A: (Ensemble U)) (Bottom (Ensemble U) (Power_set_PO A) (Empty_set U)). -Intro A; Apply Bottom_definition; Simpl; Auto with sets. +Theorem Empty_set_is_Bottom : + forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U). +intro A; apply Bottom_definition; simpl in |- *; auto with sets. Qed. -Hints Resolve Empty_set_is_Bottom. +Hint Resolve Empty_set_is_Bottom. -Theorem Union_minimal: - (a, b, X: (Ensemble U)) (Included U a X) -> (Included U b X) -> - (Included U (Union U a b) X). -Intros a b X H' H'0; Red. -Intros x H'1; Elim H'1; Auto with sets. +Theorem Union_minimal : + forall a b X:Ensemble U, + Included U a X -> Included U b X -> Included U (Union U a b) X. +intros a b X H' H'0; red in |- *. +intros x H'1; elim H'1; auto with sets. Qed. -Hints Resolve Union_minimal. +Hint Resolve Union_minimal. -Theorem Intersection_maximal: - (a, b, X: (Ensemble U)) (Included U X a) -> (Included U X b) -> - (Included U X (Intersection U a b)). -Auto with sets. +Theorem Intersection_maximal : + forall a b X:Ensemble U, + Included U X a -> Included U X b -> Included U X (Intersection U a b). +auto with sets. Qed. -Theorem Union_increases_l: (a, b: (Ensemble U)) (Included U a (Union U a b)). -Auto with sets. +Theorem Union_increases_l : forall a b:Ensemble U, Included U a (Union U a b). +auto with sets. Qed. -Theorem Union_increases_r: (a, b: (Ensemble U)) (Included U b (Union U a b)). -Auto with sets. +Theorem Union_increases_r : forall a b:Ensemble U, Included U b (Union U a b). +auto with sets. Qed. -Theorem Intersection_decreases_l: - (a, b: (Ensemble U)) (Included U (Intersection U a b) a). -Intros a b; Red. -Intros x H'; Elim H'; Auto with sets. +Theorem Intersection_decreases_l : + forall a b:Ensemble U, Included U (Intersection U a b) a. +intros a b; red in |- *. +intros x H'; elim H'; auto with sets. Qed. -Theorem Intersection_decreases_r: - (a, b: (Ensemble U)) (Included U (Intersection U a b) b). -Intros a b; Red. -Intros x H'; Elim H'; Auto with sets. +Theorem Intersection_decreases_r : + forall a b:Ensemble U, Included U (Intersection U a b) b. +intros a b; red in |- *. +intros x H'; elim H'; auto with sets. Qed. -Hints Resolve Union_increases_l Union_increases_r Intersection_decreases_l - Intersection_decreases_r. +Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l + Intersection_decreases_r. -Theorem Union_is_Lub: - (A: (Ensemble U)) (a, b: (Ensemble U)) (Included U a A) -> (Included U b A) -> - (Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b)). -Intros A a b H' H'0. -Apply Lub_definition; Simpl. -Apply Upper_Bound_definition; Simpl; Auto with sets. -Intros y H'1; Elim H'1; Auto with sets. -Intros y H'1; Elim H'1; Simpl; Auto with sets. +Theorem Union_is_Lub : + forall A a b:Ensemble U, + Included U a A -> + Included U b A -> + Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b). +intros A a b H' H'0. +apply Lub_definition; simpl in |- *. +apply Upper_Bound_definition; simpl in |- *; auto with sets. +intros y H'1; elim H'1; auto with sets. +intros y H'1; elim H'1; simpl in |- *; auto with sets. Qed. -Theorem Intersection_is_Glb: - (A: (Ensemble U)) (a, b: (Ensemble U)) (Included U a A) -> (Included U b A) -> - (Glb - (Ensemble U) - (Power_set_PO A) - (Couple (Ensemble U) a b) - (Intersection U a b)). -Intros A a b H' H'0. -Apply Glb_definition; Simpl. -Apply Lower_Bound_definition; Simpl; Auto with sets. -Apply Definition_of_Power_set. -Generalize Inclusion_is_transitive; Intro IT; Red in IT; Apply IT with a; Auto with sets. -Intros y H'1; Elim H'1; Auto with sets. -Intros y H'1; Elim H'1; Simpl; Auto with sets. +Theorem Intersection_is_Glb : + forall A a b:Ensemble U, + Included U a A -> + Included U b A -> + Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) + (Intersection U a b). +intros A a b H' H'0. +apply Glb_definition; simpl in |- *. +apply Lower_Bound_definition; simpl in |- *; auto with sets. +apply Definition_of_Power_set. +generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a; + auto with sets. +intros y H'1; elim H'1; auto with sets. +intros y H'1; elim H'1; simpl in |- *; auto with sets. Qed. End The_power_set_partial_order. -Hints Resolve Empty_set_minimal : sets v62. -Hints Resolve Power_set_Inhabited : sets v62. -Hints Resolve Inclusion_is_an_order : sets v62. -Hints Resolve Inclusion_is_transitive : sets v62. -Hints Resolve Union_minimal : sets v62. -Hints Resolve Union_increases_l : sets v62. -Hints Resolve Union_increases_r : sets v62. -Hints Resolve Intersection_decreases_l : sets v62. -Hints Resolve Intersection_decreases_r : sets v62. -Hints Resolve Empty_set_is_Bottom : sets v62. -Hints Resolve Strict_inclusion_is_transitive : sets v62. +Hint Resolve Empty_set_minimal: sets v62. +Hint Resolve Power_set_Inhabited: sets v62. +Hint Resolve Inclusion_is_an_order: sets v62. +Hint Resolve Inclusion_is_transitive: sets v62. +Hint Resolve Union_minimal: sets v62. +Hint Resolve Union_increases_l: sets v62. +Hint Resolve Union_increases_r: sets v62. +Hint Resolve Intersection_decreases_l: sets v62. +Hint Resolve Intersection_decreases_r: sets v62. +Hint Resolve Empty_set_is_Bottom: sets v62. +Hint Resolve Strict_inclusion_is_transitive: sets v62. \ No newline at end of file diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 6b3443b7d..988bbd25a 100755 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -39,300 +39,304 @@ Require Export Classical_sets. Section Sets_as_an_algebra. -Variable U: Type. +Variable U : Type. -Lemma sincl_add_x: - (A, B: (Ensemble U)) - (x: U) ~ (In U A x) -> (Strict_Included U (Add U A x) (Add U B x)) -> - (Strict_Included U A B). +Lemma sincl_add_x : + forall (A B:Ensemble U) (x:U), + ~ In U A x -> + Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B. Proof. -Intros A B x H' H'0; Red. -LApply (Strict_Included_inv U (Add U A x) (Add U B x)); Auto with sets. -Clear H'0; Intro H'0; Split. -Apply incl_add_x with x := x; Tauto. -Elim H'0; Intros H'1 H'2; Elim H'2; Clear H'0 H'2. -Intros x0 H'0. -Red; Intro H'2. -Elim H'0; Clear H'0. -Rewrite <- H'2; Auto with sets. +intros A B x H' H'0; red in |- *. +lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets. +clear H'0; intro H'0; split. +apply incl_add_x with (x := x); tauto. +elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2. +intros x0 H'0. +red in |- *; intro H'2. +elim H'0; clear H'0. +rewrite <- H'2; auto with sets. Qed. -Lemma incl_soustr_in: - (X: (Ensemble U)) (x: U) (In U X x) -> (Included U (Subtract U X x) X). +Lemma incl_soustr_in : + forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X. Proof. -Intros X x H'; Red. -Intros x0 H'0; Elim H'0; Auto with sets. +intros X x H'; red in |- *. +intros x0 H'0; elim H'0; auto with sets. Qed. -Hints Resolve incl_soustr_in : sets v62. +Hint Resolve incl_soustr_in: sets v62. -Lemma incl_soustr: - (X, Y: (Ensemble U)) (x: U) (Included U X Y) -> - (Included U (Subtract U X x) (Subtract U Y x)). +Lemma incl_soustr : + forall (X Y:Ensemble U) (x:U), + Included U X Y -> Included U (Subtract U X x) (Subtract U Y x). Proof. -Intros X Y x H'; Red. -Intros x0 H'0; Elim H'0. -Intros H'1 H'2. -Apply Subtract_intro; Auto with sets. +intros X Y x H'; red in |- *. +intros x0 H'0; elim H'0. +intros H'1 H'2. +apply Subtract_intro; auto with sets. Qed. -Hints Resolve incl_soustr : sets v62. +Hint Resolve incl_soustr: sets v62. -Lemma incl_soustr_add_l: - (X: (Ensemble U)) (x: U) (Included U (Subtract U (Add U X x) x) X). +Lemma incl_soustr_add_l : + forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X. Proof. -Intros X x; Red. -Intros x0 H'; Elim H'; Auto with sets. -Intro H'0; Elim H'0; Auto with sets. -Intros t H'1 H'2; Elim H'2; Auto with sets. +intros X x; red in |- *. +intros x0 H'; elim H'; auto with sets. +intro H'0; elim H'0; auto with sets. +intros t H'1 H'2; elim H'2; auto with sets. Qed. -Hints Resolve incl_soustr_add_l : sets v62. +Hint Resolve incl_soustr_add_l: sets v62. -Lemma incl_soustr_add_r: - (X: (Ensemble U)) (x: U) ~ (In U X x) -> - (Included U X (Subtract U (Add U X x) x)). +Lemma incl_soustr_add_r : + forall (X:Ensemble U) (x:U), + ~ In U X x -> Included U X (Subtract U (Add U X x) x). Proof. -Intros X x H'; Red. -Intros x0 H'0; Try Assumption. -Apply Subtract_intro; Auto with sets. -Red; Intro H'1; Apply H'; Rewrite H'1; Auto with sets. +intros X x H'; red in |- *. +intros x0 H'0; try assumption. +apply Subtract_intro; auto with sets. +red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets. Qed. -Hints Resolve incl_soustr_add_r : sets v62. +Hint Resolve incl_soustr_add_r: sets v62. -Lemma add_soustr_2: - (X: (Ensemble U)) (x: U) (In U X x) -> - (Included U X (Add U (Subtract U X x) x)). +Lemma add_soustr_2 : + forall (X:Ensemble U) (x:U), + In U X x -> Included U X (Add U (Subtract U X x) x). Proof. -Intros X x H'; Red. -Intros x0 H'0; Try Assumption. -Elim (classic x == x0); Intro K; Auto with sets. -Elim K; Auto with sets. +intros X x H'; red in |- *. +intros x0 H'0; try assumption. +elim (classic (x = x0)); intro K; auto with sets. +elim K; auto with sets. Qed. -Lemma add_soustr_1: - (X: (Ensemble U)) (x: U) (In U X x) -> - (Included U (Add U (Subtract U X x) x) X). +Lemma add_soustr_1 : + forall (X:Ensemble U) (x:U), + In U X x -> Included U (Add U (Subtract U X x) x) X. Proof. -Intros X x H'; Red. -Intros x0 H'0; Elim H'0; Auto with sets. -Intros y H'1; Elim H'1; Auto with sets. -Intros t H'1; Try Assumption. -Rewrite <- (Singleton_inv U x t); Auto with sets. +intros X x H'; red in |- *. +intros x0 H'0; elim H'0; auto with sets. +intros y H'1; elim H'1; auto with sets. +intros t H'1; try assumption. +rewrite <- (Singleton_inv U x t); auto with sets. Qed. -Hints Resolve add_soustr_1 add_soustr_2 : sets v62. +Hint Resolve add_soustr_1 add_soustr_2: sets v62. -Lemma add_soustr_xy: - (X: (Ensemble U)) (x, y: U) ~ x == y -> - (Subtract U (Add U X x) y) == (Add U (Subtract U X y) x). +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. Proof. -Intros X x y H'; Apply Extensionality_Ensembles. -Split; Red. -Intros x0 H'0; Elim H'0; Auto with sets. -Intro H'1; Elim H'1. -Intros u H'2 H'3; Try Assumption. -Apply Add_intro1. -Apply Subtract_intro; Auto with sets. -Intros t H'2 H'3; Try Assumption. -Elim (Singleton_inv U x t); Auto with sets. -Intros u H'2; Try Assumption. -Elim (Add_inv U (Subtract U X y) x u); Auto with sets. -Intro H'0; Elim H'0; Auto with sets. -Intro H'0; Rewrite <- H'0; Auto with sets. +intros X x y H'; apply Extensionality_Ensembles. +split; red in |- *. +intros x0 H'0; elim H'0; auto with sets. +intro H'1; elim H'1. +intros u H'2 H'3; try assumption. +apply Add_intro1. +apply Subtract_intro; auto with sets. +intros t H'2 H'3; try assumption. +elim (Singleton_inv U x t); auto with sets. +intros u H'2; try assumption. +elim (Add_inv U (Subtract U X y) x u); auto with sets. +intro H'0; elim H'0; auto with sets. +intro H'0; rewrite <- H'0; auto with sets. Qed. -Hints Resolve add_soustr_xy : sets v62. +Hint Resolve add_soustr_xy: sets v62. -Lemma incl_st_add_soustr: - (X, Y: (Ensemble U)) (x: U) ~ (In U X x) -> - (Strict_Included U (Add U X x) Y) -> - (Strict_Included U X (Subtract U Y x)). +Lemma incl_st_add_soustr : + forall (X Y:Ensemble U) (x:U), + ~ In U X x -> + Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x). Proof. -Intros X Y x H' H'0; Apply sincl_add_x with x := x; Auto with sets. -Split. -Elim H'0. -Intros H'1 H'2. -Generalize (Inclusion_is_transitive U). -Intro H'4; Red in H'4. -Apply H'4 with y := Y; Auto with sets. -Red in H'0. -Elim H'0; Intros H'1 H'2; Try Exact H'1; Clear H'0. (* PB *) -Red; Intro H'0; Apply H'2. -Rewrite H'0; Auto 8 with sets. +intros X Y x H' H'0; apply sincl_add_x with (x := x); auto with sets. +split. +elim H'0. +intros H'1 H'2. +generalize (Inclusion_is_transitive U). +intro H'4; red in H'4. +apply H'4 with (y := Y); auto with sets. +red in H'0. +elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *) +red in |- *; intro H'0; apply H'2. +rewrite H'0; auto 8 with sets. Qed. -Lemma Sub_Add_new: - (X: (Ensemble U)) (x: U) ~ (In U X x) -> X == (Subtract U (Add U X x) x). +Lemma Sub_Add_new : + forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x. Proof. -Auto with sets. +auto with sets. Qed. -Lemma Simplify_add: - (X, X0 : (Ensemble U)) (x: U) - ~ (In U X x) -> ~ (In U X0 x) -> (Add U X x) == (Add U X0 x) -> X == X0. +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. Proof. -Intros X X0 x H' H'0 H'1; Try Assumption. -Rewrite (Sub_Add_new X x); Auto with sets. -Rewrite (Sub_Add_new X0 x); Auto with sets. -Rewrite H'1; Auto with sets. +intros X X0 x H' H'0 H'1; try assumption. +rewrite (Sub_Add_new X x); auto with sets. +rewrite (Sub_Add_new X0 x); auto with sets. +rewrite H'1; auto with sets. Qed. -Lemma Included_Add: - (X, A: (Ensemble U)) (x: U) (Included U X (Add U A x)) -> - (Included U X A) \/ - (EXT A' | X == (Add U A' x) /\ (Included U A' A)). +Lemma Included_Add : + forall (X A:Ensemble U) (x:U), + Included U X (Add U A x) -> + Included U X A \/ ( exists A' : _ | X = Add U A' x /\ Included U A' A). Proof. -Intros X A x H'0; Try Assumption. -Elim (classic (In U X x)). -Intro H'1; Right; Try Assumption. -Exists (Subtract U X x). -Split; Auto with sets. -Red in H'0. -Red. -Intros x0 H'2; Try Assumption. -LApply (Subtract_inv U X x x0); Auto with sets. -Intro H'3; Elim H'3; Intros K K'; Clear H'3. -LApply (H'0 x0); Auto with sets. -Intro H'3; Try Assumption. -LApply (Add_inv U A x x0); Auto with sets. -Intro H'4; Elim H'4; - [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4]. -Elim K'; Auto with sets. -Intro H'1; Left; Try Assumption. -Red in H'0. -Red. -Intros x0 H'2; Try Assumption. -LApply (H'0 x0); Auto with sets. -Intro H'3; Try Assumption. -LApply (Add_inv U A x x0); Auto with sets. -Intro H'4; Elim H'4; - [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4]. -Absurd (In U X x0); Auto with sets. -Rewrite <- H'5; Auto with sets. +intros X A x H'0; try assumption. +elim (classic (In U X x)). +intro H'1; right; try assumption. +exists (Subtract U X x). +split; auto with sets. +red in H'0. +red in |- *. +intros x0 H'2; try assumption. +lapply (Subtract_inv U X x x0); auto with sets. +intro H'3; elim H'3; intros K K'; clear H'3. +lapply (H'0 x0); auto with sets. +intro H'3; try assumption. +lapply (Add_inv U A x x0); auto with sets. +intro H'4; elim H'4; + [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ]. +elim K'; auto with sets. +intro H'1; left; try assumption. +red in H'0. +red in |- *. +intros x0 H'2; try assumption. +lapply (H'0 x0); auto with sets. +intro H'3; try assumption. +lapply (Add_inv U A x x0); auto with sets. +intro H'4; elim H'4; + [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ]. +absurd (In U X x0); auto with sets. +rewrite <- H'5; auto with sets. Qed. -Lemma setcover_inv: - (A: (Ensemble U)) - (x, y: (Ensemble U)) (covers (Ensemble U) (Power_set_PO U A) y x) -> - (Strict_Included U x y) /\ - ((z: (Ensemble U)) (Included U x z) -> (Included U z y) -> x == z \/ z == y). +Lemma setcover_inv : + forall A x y:Ensemble U, + covers (Ensemble U) (Power_set_PO U A) y x -> + Strict_Included U x y /\ + (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y). Proof. -Intros A x y H'; Elim H'. -Unfold Strict_Rel_of; Simpl. -Intros H'0 H'1; Split; [Auto with sets | Idtac]. -Intros z H'2 H'3; Try Assumption. -Elim (classic x == z); Auto with sets. -Intro H'4; Right; Try Assumption. -Elim (classic z == y); Auto with sets. -Intro H'5; Try Assumption. -Elim H'1. -Exists z; Auto with sets. +intros A x y H'; elim H'. +unfold Strict_Rel_of in |- *; simpl in |- *. +intros H'0 H'1; split; [ auto with sets | idtac ]. +intros z H'2 H'3; try assumption. +elim (classic (x = z)); auto with sets. +intro H'4; right; try assumption. +elim (classic (z = y)); auto with sets. +intro H'5; try assumption. +elim H'1. +exists z; auto with sets. Qed. -Theorem Add_covers: - (A: (Ensemble U)) (a: (Ensemble U)) (Included U a A) -> - (x: U) (In U A x) -> ~ (In U a x) -> - (covers (Ensemble U) (Power_set_PO U A) (Add U a x) a). +Theorem Add_covers : + forall A a:Ensemble U, + Included U a A -> + forall x:U, + In U A x -> + ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a. Proof. -Intros A a H' x H'0 H'1; Try Assumption. -Apply setcover_intro; Auto with sets. -Red. -Split; [Idtac | Red; Intro H'2; Try Exact H'2]; Auto with sets. -Apply H'1. -Rewrite H'2; Auto with sets. -Red; Intro H'2; Elim H'2; Clear H'2. -Intros z H'2; Elim H'2; Intros H'3 H'4; Try Exact H'3; Clear H'2. -LApply (Strict_Included_inv U a z); Auto with sets; Clear H'3. -Intro H'2; Elim H'2; Intros H'3 H'5; Elim H'5; Clear H'2 H'5. -Intros x0 H'2; Elim H'2. -Intros H'5 H'6; Try Assumption. -Generalize H'4; Intro K. -Red in H'4. -Elim H'4; Intros H'8 H'9; Red in H'8; Clear H'4. -LApply (H'8 x0); Auto with sets. -Intro H'7; Try Assumption. -Elim (Add_inv U a x x0); Auto with sets. -Intro H'15. -Cut (Included U (Add U a x) z). -Intro H'10; Try Assumption. -Red in K. -Elim K; Intros H'11 H'12; Apply H'12; Clear K; Auto with sets. -Rewrite H'15. -Red. -Intros x1 H'10; Elim H'10; Auto with sets. -Intros x2 H'11; Elim H'11; Auto with sets. +intros A a H' x H'0 H'1; try assumption. +apply setcover_intro; auto with sets. +red in |- *. +split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets. +apply H'1. +rewrite H'2; auto with sets. +red in |- *; intro H'2; elim H'2; clear H'2. +intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2. +lapply (Strict_Included_inv U a z); auto with sets; clear H'3. +intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5. +intros x0 H'2; elim H'2. +intros H'5 H'6; try assumption. +generalize H'4; intro K. +red in H'4. +elim H'4; intros H'8 H'9; red in H'8; clear H'4. +lapply (H'8 x0); auto with sets. +intro H'7; try assumption. +elim (Add_inv U a x x0); auto with sets. +intro H'15. +cut (Included U (Add U a x) z). +intro H'10; try assumption. +red in K. +elim K; intros H'11 H'12; apply H'12; clear K; auto with sets. +rewrite H'15. +red in |- *. +intros x1 H'10; elim H'10; auto with sets. +intros x2 H'11; elim H'11; auto with sets. Qed. -Theorem covers_Add: - (A: (Ensemble U)) - (a, a': (Ensemble U)) - (Included U a A) -> - (Included U a' A) -> (covers (Ensemble U) (Power_set_PO U A) a' a) -> - (EXT x | a' == (Add U a x) /\ ((In U A x) /\ ~ (In U a x))). +Theorem covers_Add : + forall A a a':Ensemble U, + Included U a A -> + Included U a' A -> + covers (Ensemble U) (Power_set_PO U A) a' a -> + exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x. Proof. -Intros A a a' H' H'0 H'1; Try Assumption. -Elim (setcover_inv A a a'); Auto with sets. -Intros H'6 H'7. -Clear H'1. -Elim (Strict_Included_inv U a a'); Auto with sets. -Intros H'5 H'8; Elim H'8. -Intros x H'1; Elim H'1. -Intros H'2 H'3; Try Assumption. -Exists x. -Split; [Try Assumption | Idtac]. -Clear H'8 H'1. -Elim (H'7 (Add U a x)); Auto with sets. -Intro H'1. -Absurd a ==(Add U a x); Auto with sets. -Red; Intro H'8; Try Exact H'8. -Apply H'3. -Rewrite H'8; Auto with sets. -Auto with sets. -Red. -Intros x0 H'1; Elim H'1; Auto with sets. -Intros x1 H'8; Elim H'8; Auto with sets. -Split; [Idtac | Try Assumption]. -Red in H'0; Auto with sets. +intros A a a' H' H'0 H'1; try assumption. +elim (setcover_inv A a a'); auto with sets. +intros H'6 H'7. +clear H'1. +elim (Strict_Included_inv U a a'); auto with sets. +intros H'5 H'8; elim H'8. +intros x H'1; elim H'1. +intros H'2 H'3; try assumption. +exists x. +split; [ try assumption | idtac ]. +clear H'8 H'1. +elim (H'7 (Add U a x)); auto with sets. +intro H'1. +absurd (a = Add U a x); auto with sets. +red in |- *; intro H'8; try exact H'8. +apply H'3. +rewrite H'8; auto with sets. +auto with sets. +red in |- *. +intros x0 H'1; elim H'1; auto with sets. +intros x1 H'8; elim H'8; auto with sets. +split; [ idtac | try assumption ]. +red in H'0; auto with sets. Qed. -Theorem covers_is_Add: - (A: (Ensemble U)) - (a, a': (Ensemble U)) (Included U a A) -> (Included U a' A) -> - (iff - (covers (Ensemble U) (Power_set_PO U A) a' a) - (EXT x | a' == (Add U a x) /\ ((In U A x) /\ ~ (In U a x)))). +Theorem covers_is_Add : + forall A a a':Ensemble U, + Included U a A -> + Included U a' A -> + (covers (Ensemble U) (Power_set_PO U A) a' a <-> + ( exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x)). Proof. -Intros A a a' H' H'0; Split; Intro K. -Apply covers_Add with A := A; Auto with sets. -Elim K. -Intros x H'1; Elim H'1; Intros H'2 H'3; Rewrite H'2; Clear H'1. -Apply Add_covers; Intuition. +intros A a a' H' H'0; split; intro K. +apply covers_Add with (A := A); auto with sets. +elim K. +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: - (x:U) (A:(Ensemble U)) (In U A x) -> - (covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U)). -Intros x A H'. -Rewrite <- (Empty_set_zero' U x). -Apply Add_covers; Auto with sets. +Theorem Singleton_atomic : + forall (x:U) (A:Ensemble U), + In U A x -> + covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U). +intros x A H'. +rewrite <- (Empty_set_zero' U x). +apply Add_covers; auto with sets. Qed. -Lemma less_than_singleton: - (X:(Ensemble U)) (x:U) (Strict_Included U X (Singleton U x)) -> - X ==(Empty_set U). -Intros X x H'; Try Assumption. -Red in H'. -LApply (Singleton_atomic x (Full_set U)); - [Intro H'2; Try Exact H'2 | Apply Full_intro]. -Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'. -Elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x)); - [Intros H'6 H'7; Try Exact H'7 | Idtac]; Auto with sets. -Elim (H'7 X); [Intro H'5; Try Exact H'5 | Intro H'5 | Idtac | Idtac]; Auto with sets. -Elim H'1; Auto with sets. +Lemma less_than_singleton : + forall (X:Ensemble U) (x:U), + Strict_Included U X (Singleton U x) -> X = Empty_set U. +intros X x H'; try assumption. +red in H'. +lapply (Singleton_atomic x (Full_set U)); + [ intro H'2; try exact H'2 | apply Full_intro ]. +elim H'; intros H'0 H'1; try exact H'1; clear H'. +elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x)); + [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets. +elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ]; + auto with sets. +elim H'1; auto with sets. Qed. End Sets_as_an_algebra. -Hints Resolve incl_soustr_in : sets v62. -Hints Resolve incl_soustr : sets v62. -Hints Resolve incl_soustr_add_l : sets v62. -Hints Resolve incl_soustr_add_r : sets v62. -Hints Resolve add_soustr_1 add_soustr_2 : sets v62. -Hints Resolve add_soustr_xy : sets v62. +Hint Resolve incl_soustr_in: sets v62. +Hint Resolve incl_soustr: sets v62. +Hint Resolve incl_soustr_add_l: sets v62. +Hint Resolve incl_soustr_add_r: sets v62. +Hint Resolve add_soustr_1 add_soustr_2: sets v62. +Hint Resolve add_soustr_xy: sets v62. \ No newline at end of file diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 3e1837078..c587744a3 100755 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -35,242 +35,234 @@ Require Export Cpo. Require Export Powerset. Section Sets_as_an_algebra. -Variable U: Type. -Hints Unfold not. +Variable U : Type. +Hint Unfold not. -Theorem Empty_set_zero : - (X: (Ensemble U)) (Union U (Empty_set U) X) == X. +Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X. Proof. -Auto 6 with sets. +auto 6 with sets. Qed. -Hints Resolve Empty_set_zero. +Hint Resolve Empty_set_zero. -Theorem Empty_set_zero' : - (x: U) (Add U (Empty_set U) x) == (Singleton U x). +Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. Proof. -Unfold 1 Add; Auto with sets. +unfold Add at 1 in |- *; auto with sets. Qed. -Hints Resolve Empty_set_zero'. +Hint Resolve Empty_set_zero'. Lemma less_than_empty : - (X: (Ensemble U)) (Included U X (Empty_set U)) -> X == (Empty_set U). + forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U. Proof. -Auto with sets. +auto with sets. Qed. -Hints Resolve less_than_empty. +Hint Resolve less_than_empty. -Theorem Union_commutative : - (A,B: (Ensemble U)) (Union U A B) == (Union U B A). +Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A. Proof. -Auto with sets. +auto with sets. Qed. Theorem Union_associative : - (A, B, C: (Ensemble U)) - (Union U (Union U A B) C) == (Union U A (Union U B C)). + 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. +auto 9 with sets. Qed. -Hints Resolve Union_associative. +Hint Resolve Union_associative. -Theorem Union_idempotent : (A: (Ensemble U)) (Union U A A) == A. +Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A. Proof. -Auto 7 with sets. +auto 7 with sets. Qed. Lemma Union_absorbs : - (A, B: (Ensemble U)) (Included U B A) -> (Union U A B) == A. + forall A B:Ensemble U, Included U B A -> Union U A B = A. Proof. -Auto 7 with sets. +auto 7 with sets. Qed. -Theorem Couple_as_union: - (x, y: U) (Union U (Singleton U x) (Singleton U y)) == (Couple U x y). +Theorem Couple_as_union : + forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y. Proof. -Intros x y; Apply Extensionality_Ensembles; Split; Red. -Intros x0 H'; Elim H'; (Intros x1 H'0; Elim H'0; Auto with sets). -Intros x0 H'; Elim H'; Auto with sets. +intros x y; apply Extensionality_Ensembles; split; red in |- *. +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 : - (x, y, z: U) - (Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z)) == - (Triple U x y z). + forall x y z:U, + Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) = + Triple U x y z. Proof. -Intros x y z; Apply Extensionality_Ensembles; Split; Red. -Intros x0 H'; Elim H'. -Intros x1 H'0; Elim H'0; (Intros x2 H'1; Elim H'1; Auto with sets). -Intros x1 H'0; Elim H'0; Auto with sets. -Intros x0 H'; Elim H'; Auto with sets. +intros x y z; apply Extensionality_Ensembles; split; red in |- *. +intros x0 H'; elim H'. +intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets). +intros x1 H'0; elim H'0; auto with sets. +intros x0 H'; elim H'; auto with sets. Qed. -Theorem Triple_as_Couple : (x, y: U) (Couple U x y) == (Triple U x x y). +Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y. Proof. -Intros x y. -Rewrite <- (Couple_as_union x y). -Rewrite <- (Union_idempotent (Singleton U x)). -Apply Triple_as_union. +intros x y. +rewrite <- (Couple_as_union x y). +rewrite <- (Union_idempotent (Singleton U x)). +apply Triple_as_union. Qed. Theorem Triple_as_Couple_Singleton : - (x, y, z: U) (Triple U x y z) == (Union U (Couple U x y) (Singleton U z)). + forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z). Proof. -Intros x y z. -Rewrite <- (Triple_as_union x y z). -Rewrite <- (Couple_as_union x y); Auto with sets. +intros x y z. +rewrite <- (Triple_as_union x y z). +rewrite <- (Couple_as_union x y); auto with sets. Qed. Theorem Intersection_commutative : - (A,B: (Ensemble U)) (Intersection U A B) == (Intersection U B A). + forall A B:Ensemble U, Intersection U A B = Intersection U B A. Proof. -Intros A B. -Apply Extensionality_Ensembles. -Split; Red; Intros x H'; Elim H'; Auto with sets. +intros A B. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'; elim H'; auto with sets. Qed. Theorem Distributivity : - (A, B, C: (Ensemble U)) - (Intersection U A (Union U B C)) == - (Union U (Intersection U A B) (Intersection U A C)). + forall A B C:Ensemble U, + Intersection U A (Union U B C) = + Union U (Intersection U A B) (Intersection U A C). Proof. -Intros A B C. -Apply Extensionality_Ensembles. -Split; Red; Intros x H'. -Elim H'. -Intros x0 H'0 H'1; Generalize H'0. -Elim H'1; Auto with sets. -Elim H'; Intros x0 H'0; Elim H'0; Auto with sets. +intros A B C. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'. +elim H'. +intros x0 H'0 H'1; generalize H'0. +elim H'1; auto with sets. +elim H'; intros x0 H'0; elim H'0; auto with sets. Qed. Theorem Distributivity' : - (A, B, C: (Ensemble U)) - (Union U A (Intersection U B C)) == - (Intersection U (Union U A B) (Union U A C)). + forall A B C:Ensemble U, + Union U A (Intersection U B C) = + Intersection U (Union U A B) (Union U A C). Proof. -Intros A B C. -Apply Extensionality_Ensembles. -Split; Red; Intros x H'. -Elim H'; Auto with sets. -Intros x0 H'0; Elim H'0; Auto with sets. -Elim H'. -Intros x0 H'0; Elim H'0; Auto with sets. -Intros x1 H'1 H'2; Try Exact H'2. -Generalize H'1. -Elim H'2; Auto with sets. +intros A B C. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'. +elim H'; auto with sets. +intros x0 H'0; elim H'0; auto with sets. +elim H'. +intros x0 H'0; elim H'0; auto with sets. +intros x1 H'1 H'2; try exact H'2. +generalize H'1. +elim H'2; auto with sets. Qed. Theorem Union_add : - (A, B: (Ensemble U)) (x: U) - (Add U (Union U A B) x) == (Union U A (Add U B x)). + forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x). Proof. -Unfold Add; Auto with sets. +unfold Add in |- *; auto with sets. Qed. -Hints Resolve Union_add. +Hint Resolve Union_add. Theorem Non_disjoint_union : - (X: (Ensemble U)) (x: U) (In U X x) -> (Add U X x) == X. -Intros X x H'; Unfold Add. -Apply Extensionality_Ensembles; Red. -Split; Red; Auto with sets. -Intros x0 H'0; Elim H'0; Auto with sets. -Intros t H'1; Elim H'1; Auto with sets. + forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X. +intros X x H'; unfold Add in |- *. +apply Extensionality_Ensembles; red in |- *. +split; red in |- *; auto with sets. +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' : - (X: (Ensemble U)) (x: U) ~ (In U X x) -> (Subtract U X x) == X. + forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X. Proof. -Intros X x H'; Unfold Subtract. -Apply Extensionality_Ensembles. -Split; Red; Auto with sets. -Intros x0 H'0; Elim H'0; Auto with sets. -Intros x0 H'0; Apply Setminus_intro; Auto with sets. -Red; Intro H'1; Elim H'1. -LApply (Singleton_inv U x x0); Auto with sets. -Intro H'4; Apply H'; Rewrite H'4; Auto with sets. +intros X x H'; unfold Subtract in |- *. +apply Extensionality_Ensembles. +split; red in |- *; auto with sets. +intros x0 H'0; elim H'0; auto with sets. +intros x0 H'0; apply Setminus_intro; auto with sets. +red in |- *; intro H'1; elim H'1. +lapply (Singleton_inv U x x0); auto with sets. +intro H'4; apply H'; rewrite H'4; auto with sets. Qed. -Lemma singlx : (x, y: U) (In U (Add U (Empty_set U) x) y) -> x == y. +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. +intro x; rewrite (Empty_set_zero' x); auto with sets. Qed. -Hints Resolve singlx. +Hint Resolve singlx. Lemma incl_add : - (A, B: (Ensemble U)) (x: U) (Included U A B) -> - (Included U (Add U A x) (Add U B x)). + forall (A B:Ensemble U) (x:U), + Included U A B -> Included U (Add U A x) (Add U B x). Proof. -Intros A B x H'; Red; Auto with sets. -Intros x0 H'0. -LApply (Add_inv U A x x0); Auto with sets. -Intro H'1; Elim H'1; - [Intro H'2; Clear H'1 | Intro H'2; Rewrite <- H'2; Clear H'1]; Auto with sets. +intros A B x H'; red in |- *; auto with sets. +intros x0 H'0. +lapply (Add_inv U A x x0); auto with sets. +intro H'1; elim H'1; + [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ]; + auto with sets. Qed. -Hints Resolve incl_add. +Hint Resolve incl_add. Lemma incl_add_x : - (A, B: (Ensemble U)) - (x: U) ~ (In U A x) -> (Included U (Add U A x) (Add U B x)) -> - (Included U A B). + forall (A B:Ensemble U) (x:U), + ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B. Proof. -Unfold Included. -Intros A B x H' H'0 x0 H'1. -LApply (H'0 x0); Auto with sets. -Intro H'2; LApply (Add_inv U B x x0); Auto with sets. -Intro H'3; Elim H'3; - [Intro H'4; Try Exact H'4; Clear H'3 | Intro H'4; Clear H'3]. -Absurd (In U A x0); Auto with sets. -Rewrite <- H'4; Auto with sets. +unfold Included in |- *. +intros A B x H' H'0 x0 H'1. +lapply (H'0 x0); auto with sets. +intro H'2; lapply (Add_inv U B x x0); auto with sets. +intro H'3; elim H'3; + [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ]. +absurd (In U A x0); auto with sets. +rewrite <- H'4; auto with sets. Qed. Lemma Add_commutative : - (A: (Ensemble U)) (x, y: U) (Add U (Add U A x) y) == (Add U (Add U A y) x). + forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x. Proof. -Intros A x y. -Unfold Add. -Rewrite (Union_associative A (Singleton U x) (Singleton U y)). -Rewrite (Union_commutative (Singleton U x) (Singleton U y)). -Rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); Auto with sets. +intros A x y. +unfold Add in |- *. +rewrite (Union_associative A (Singleton U x) (Singleton U y)). +rewrite (Union_commutative (Singleton U x) (Singleton U y)). +rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); + auto with sets. Qed. Lemma Add_commutative' : - (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). + 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. Proof. -Intros A x y z. -Rewrite (Add_commutative (Add U A x) y z). -Rewrite (Add_commutative A x z); Auto with sets. +intros A x y z. +rewrite (Add_commutative (Add U A x) y z). +rewrite (Add_commutative A x z); auto with sets. Qed. Lemma Add_distributes : - (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)). + 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). Proof. -Intros A B x y H'; Try Assumption. -Rewrite <- (Union_add (Add U A x) B y). -Unfold 4 Add. -Rewrite (Union_commutative A (Singleton U x)). -Rewrite Union_associative. -Rewrite (Union_absorbs A B H'). -Rewrite (Union_commutative (Singleton U x) A). -Auto with sets. +intros A B x y H'; try assumption. +rewrite <- (Union_add (Add U A x) B y). +unfold Add at 4 in |- *. +rewrite (Union_commutative A (Singleton U x)). +rewrite Union_associative. +rewrite (Union_absorbs A B H'). +rewrite (Union_commutative (Singleton U x) A). +auto with sets. Qed. Lemma setcover_intro : - (U: Type) - (A: (Ensemble U)) - (x, y: (Ensemble U)) - (Strict_Included U x y) -> - ~ (EXT z | (Strict_Included U x z) - /\ (Strict_Included U z y)) -> - (covers (Ensemble U) (Power_set_PO U A) y x). + forall (U:Type) (A x y:Ensemble U), + Strict_Included U x y -> + ~ ( exists z : _ | Strict_Included U x z /\ Strict_Included U z y) -> + covers (Ensemble U) (Power_set_PO U A) y x. Proof. -Intros; Apply Definition_of_covers; Auto with sets. +intros; apply Definition_of_covers; auto with sets. Qed. -Hints Resolve setcover_intro. +Hint Resolve setcover_intro. End Sets_as_an_algebra. -Hints Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add - singlx incl_add : sets v62. - +Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add + singlx incl_add: sets v62. diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 74c031726..16a00740d 100755 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -27,41 +27,41 @@ (*i $Id$ i*) Section Relations_1. - Variable U: Type. + Variable U : Type. - Definition Relation := U -> U -> Prop. - Variable R: Relation. + Definition Relation := U -> U -> Prop. + Variable R : Relation. - Definition Reflexive : Prop := (x: U) (R x x). + Definition Reflexive : Prop := forall x:U, R x x. - Definition Transitive : Prop := (x,y,z: U) (R x y) -> (R y z) -> (R x z). + Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z. - Definition Symmetric : Prop := (x,y: U) (R x y) -> (R y x). + Definition Symmetric : Prop := forall x y:U, R x y -> R y x. - Definition Antisymmetric : Prop := - (x: U) (y: U) (R x y) -> (R y x) -> x == y. + Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y. - Definition contains : Relation -> Relation -> Prop := - [R,R': Relation] (x: U) (y: U) (R' x y) -> (R x y). + Definition contains (R R':Relation) : Prop := + forall x y:U, R' x y -> R x y. - Definition same_relation : Relation -> Relation -> Prop := - [R,R': Relation] (contains R R') /\ (contains R' R). + Definition same_relation (R R':Relation) : Prop := + contains R R' /\ contains R' R. Inductive Preorder : Prop := - Definition_of_preorder: Reflexive -> Transitive -> Preorder. + Definition_of_preorder : Reflexive -> Transitive -> Preorder. Inductive Order : Prop := - Definition_of_order: Reflexive -> Transitive -> Antisymmetric -> Order. + Definition_of_order : + Reflexive -> Transitive -> Antisymmetric -> Order. Inductive Equivalence : Prop := - Definition_of_equivalence: - Reflexive -> Transitive -> Symmetric -> Equivalence. + Definition_of_equivalence : + Reflexive -> Transitive -> Symmetric -> Equivalence. Inductive PER : Prop := - Definition_of_PER: Symmetric -> Transitive -> PER. + Definition_of_PER : Symmetric -> Transitive -> PER. End Relations_1. -Hints Unfold Reflexive Transitive Antisymmetric Symmetric contains - same_relation : sets v62. -Hints Resolve Definition_of_preorder Definition_of_order - Definition_of_equivalence Definition_of_PER : sets v62. +Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains + same_relation: sets v62. +Hint Resolve Definition_of_preorder Definition_of_order + Definition_of_equivalence Definition_of_PER: sets v62. \ No newline at end of file diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index b490fa7a0..61557aff7 100755 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -28,82 +28,85 @@ Require Export Relations_1. -Definition Complement : (U: Type) (Relation U) -> (Relation U) := - [U: Type] [R: (Relation U)] [x,y: U] ~ (R x y). +Definition Complement (U:Type) (R:Relation U) : Relation U := + fun x y:U => ~ R x y. -Theorem Rsym_imp_notRsym: (U: Type) (R: (Relation U)) (Symmetric U R) -> - (Symmetric U (Complement U R)). +Theorem Rsym_imp_notRsym : + forall (U:Type) (R:Relation U), + Symmetric U R -> Symmetric U (Complement U R). Proof. -Unfold Symmetric Complement. -Intros U R H' x y H'0; Red; Intro H'1; Apply H'0; Auto with sets. +unfold Symmetric, Complement in |- *. +intros U R H' x y H'0; red in |- *; intro H'1; apply H'0; auto with sets. Qed. Theorem Equiv_from_preorder : - (U: Type) (R: (Relation U)) (Preorder U R) -> - (Equivalence U [x,y: U] (R x y) /\ (R y x)). + forall (U:Type) (R:Relation U), + Preorder U R -> Equivalence U (fun x y:U => R x y /\ R y x). Proof. -Intros U R H'; Elim H'; Intros H'0 H'1. -Apply Definition_of_equivalence. -Red in H'0; Auto 10 with sets. -2:Red; Intros x y h; Elim h; Intros H'3 H'4; Auto 10 with sets. -Red in H'1; Red; Auto 10 with sets. -Intros x y z h; Elim h; Intros H'3 H'4; Clear h. -Intro h; Elim h; Intros H'5 H'6; Clear h. -Split; Apply H'1 with y; Auto 10 with sets. +intros U R H'; elim H'; intros H'0 H'1. +apply Definition_of_equivalence. +red in H'0; auto 10 with sets. +2: red in |- *; intros x y h; elim h; intros H'3 H'4; auto 10 with sets. +red in H'1; red in |- *; auto 10 with sets. +intros x y z h; elim h; intros H'3 H'4; clear h. +intro h; elim h; intros H'5 H'6; clear h. +split; apply H'1 with y; auto 10 with sets. Qed. -Hints Resolve Equiv_from_preorder. +Hint Resolve Equiv_from_preorder. Theorem Equiv_from_order : - (U: Type) (R: (Relation U)) (Order U R) -> - (Equivalence U [x,y: U] (R x y) /\ (R y x)). + forall (U:Type) (R:Relation U), + Order U R -> Equivalence U (fun x y:U => R x y /\ R y x). Proof. -Intros U R H'; Elim H'; Auto 10 with sets. +intros U R H'; elim H'; auto 10 with sets. Qed. -Hints Resolve Equiv_from_order. +Hint Resolve Equiv_from_order. Theorem contains_is_preorder : - (U: Type) (Preorder (Relation U) (contains U)). + forall U:Type, Preorder (Relation U) (contains U). Proof. -Auto 10 with sets. +auto 10 with sets. Qed. -Hints Resolve contains_is_preorder. +Hint Resolve contains_is_preorder. Theorem same_relation_is_equivalence : - (U: Type) (Equivalence (Relation U) (same_relation U)). + forall U:Type, Equivalence (Relation U) (same_relation U). Proof. -Unfold 1 same_relation; Auto 10 with sets. +unfold same_relation at 1 in |- *; auto 10 with sets. Qed. -Hints Resolve same_relation_is_equivalence. +Hint Resolve same_relation_is_equivalence. -Theorem cong_reflexive_same_relation: - (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Reflexive U R) -> - (Reflexive U R'). +Theorem cong_reflexive_same_relation : + forall (U:Type) (R R':Relation U), + same_relation U R R' -> Reflexive U R -> Reflexive U R'. Proof. -Unfold same_relation; Intuition. +unfold same_relation in |- *; intuition. Qed. -Theorem cong_symmetric_same_relation: - (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Symmetric U R) -> - (Symmetric U R'). +Theorem cong_symmetric_same_relation : + forall (U:Type) (R R':Relation U), + same_relation U R R' -> Symmetric U R -> Symmetric U R'. Proof. - Compute;Intros;Elim H;Intros;Clear H;Apply (H3 y x (H0 x y (H2 x y H1))). + compute in |- *; intros; elim H; intros; clear H; + apply (H3 y x (H0 x y (H2 x y H1))). (*Intuition.*) Qed. -Theorem cong_antisymmetric_same_relation: - (U:Type) (R, R':(Relation U)) (same_relation U R R') -> - (Antisymmetric U R) -> (Antisymmetric U R'). +Theorem cong_antisymmetric_same_relation : + forall (U:Type) (R R':Relation U), + same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'. Proof. - Compute;Intros;Elim H;Intros;Clear H;Apply (H0 x y (H3 x y H1) (H3 y x H2)). + compute in |- *; intros; elim H; intros; clear H; + apply (H0 x y (H3 x y H1) (H3 y x H2)). (*Intuition.*) Qed. -Theorem cong_transitive_same_relation: - (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Transitive U R) -> - (Transitive U R'). +Theorem cong_transitive_same_relation : + forall (U:Type) (R R':Relation U), + same_relation U R R' -> Transitive U R -> Transitive U R'. Proof. -Intros U R R' H' H'0; Red. -Elim H'. -Intros H'1 H'2 x y z H'3 H'4; Apply H'2. -Apply H'0 with y; Auto with sets. -Qed. +intros U R R' H' H'0; red in |- *. +elim H'. +intros H'1 H'2 x y z H'3 H'4; apply H'2. +apply H'0 with y; auto with sets. +Qed. \ No newline at end of file diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index 65363d816..d7ee68b66 100755 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -29,28 +29,28 @@ Require Export Relations_1. Section Relations_2. -Variable U: Type. -Variable R: (Relation U). +Variable U : Type. +Variable R : Relation U. -Inductive Rstar : (Relation U) := - Rstar_0: (x: U) (Rstar x x) - | Rstar_n: (x, y, z: U) (R x y) -> (Rstar y z) -> (Rstar x z). +Inductive Rstar : Relation U := + | Rstar_0 : forall x:U, Rstar x x + | Rstar_n : forall x y z:U, R x y -> Rstar y z -> Rstar x z. -Inductive Rstar1 : (Relation U) := - Rstar1_0: (x: U) (Rstar1 x x) - | Rstar1_1: (x: U) (y: U) (R x y) -> (Rstar1 x y) - | Rstar1_n: (x, y, z: U) (Rstar1 x y) -> (Rstar1 y z) -> (Rstar1 x z). +Inductive Rstar1 : Relation U := + | Rstar1_0 : forall x:U, Rstar1 x x + | Rstar1_1 : forall x y:U, R x y -> Rstar1 x y + | Rstar1_n : forall x y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z. -Inductive Rplus : (Relation U) := - Rplus_0: (x, y: U) (R x y) -> (Rplus x y) - | Rplus_n: (x, y, z: U) (R x y) -> (Rplus y z) -> (Rplus x z). +Inductive Rplus : Relation U := + | Rplus_0 : forall x y:U, R x y -> Rplus x y + | Rplus_n : forall x y z:U, R x y -> Rplus y z -> Rplus x z. Definition Strongly_confluent : Prop := - (x, a, b: U) (R x a) -> (R x b) -> (exT U [z: U] (R a z) /\ (R b z)). + forall x a b:U, R x a -> R x b -> ex (fun z:U => R a z /\ R b z). End Relations_2. -Hints Resolve Rstar_0 : sets v62. -Hints Resolve Rstar1_0 : sets v62. -Hints Resolve Rstar1_1 : sets v62. -Hints Resolve Rplus_0 : sets v62. +Hint Resolve Rstar_0: sets v62. +Hint Resolve Rstar1_0: sets v62. +Hint Resolve Rstar1_1: sets v62. +Hint Resolve Rplus_0: sets v62. \ No newline at end of file diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index 588b7f431..4fda8d8e9 100755 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -30,122 +30,124 @@ Require Export Relations_1. Require Export Relations_1_facts. Require Export Relations_2. -Theorem Rstar_reflexive : - (U: Type) (R: (Relation U)) (Reflexive U (Rstar U R)). +Theorem Rstar_reflexive : + forall (U:Type) (R:Relation U), Reflexive U (Rstar U R). Proof. -Auto with sets. +auto with sets. Qed. Theorem Rplus_contains_R : - (U: Type) (R: (Relation U)) (contains U (Rplus U R) R). + forall (U:Type) (R:Relation U), contains U (Rplus U R) R. Proof. -Auto with sets. +auto with sets. Qed. Theorem Rstar_contains_R : - (U: Type) (R: (Relation U)) (contains U (Rstar U R) R). + forall (U:Type) (R:Relation U), contains U (Rstar U R) R. Proof. -Intros U R; Red; Intros x y H'; Apply Rstar_n with y; Auto with sets. +intros U R; red in |- *; intros x y H'; apply Rstar_n with y; auto with sets. Qed. Theorem Rstar_contains_Rplus : - (U: Type) (R: (Relation U)) (contains U (Rstar U R) (Rplus U R)). + forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R). Proof. -Intros U R; Red. -Intros x y H'; Elim H'. -Generalize Rstar_contains_R; Intro T; Red in T; Auto with sets. -Intros x0 y0 z H'0 H'1 H'2; Apply Rstar_n with y0; Auto with sets. +intros U R; red in |- *. +intros x y H'; elim H'. +generalize Rstar_contains_R; intro T; red in T; auto with sets. +intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets. Qed. Theorem Rstar_transitive : - (U: Type) (R: (Relation U)) (Transitive U (Rstar U R)). + forall (U:Type) (R:Relation U), Transitive U (Rstar U R). Proof. -Intros U R; Red. -Intros x y z H'; Elim H'; Auto with sets. -Intros x0 y0 z0 H'0 H'1 H'2 H'3; Apply Rstar_n with y0; Auto with sets. +intros U R; red in |- *. +intros x y z H'; elim H'; auto with sets. +intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto with sets. Qed. Theorem Rstar_cases : - (U: Type) (R: (Relation U)) (x, y: U) (Rstar U R x y) -> - x == y \/ (EXT u | (R x u) /\ (Rstar U R u y)). + forall (U:Type) (R:Relation U) (x y:U), + Rstar U R x y -> x = y \/ ( exists u : _ | R x u /\ Rstar U R u y). Proof. -Intros U R x y H'; Elim H'; Auto with sets. -Intros x0 y0 z H'0 H'1 H'2; Right; Exists y0; Auto with sets. +intros U R x y H'; elim H'; auto with sets. +intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto with sets. Qed. Theorem Rstar_equiv_Rstar1 : - (U: Type) (R: (Relation U)) (same_relation U (Rstar U R) (Rstar1 U R)). + forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R). Proof. -Generalize Rstar_contains_R; Intro T; Red in T. -Intros U R; Unfold same_relation contains. -Split; Intros x y H'; Elim H'; Auto with sets. -Generalize Rstar_transitive; Intro T1; Red in T1. -Intros x0 y0 z H'0 H'1 H'2 H'3; Apply T1 with y0; Auto with sets. -Intros x0 y0 z H'0 H'1 H'2; Apply Rstar1_n with y0; Auto with sets. +generalize Rstar_contains_R; intro T; red in T. +intros U R; unfold same_relation, contains in |- *. +split; intros x y H'; elim H'; auto with sets. +generalize Rstar_transitive; intro T1; red in T1. +intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets. +intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets. Qed. Theorem Rsym_imp_Rstarsym : - (U: Type) (R: (Relation U)) (Symmetric U R) -> (Symmetric U (Rstar U R)). + forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R). Proof. -Intros U R H'; Red. -Intros x y H'0; Elim H'0; Auto with sets. -Intros x0 y0 z H'1 H'2 H'3. -Generalize Rstar_transitive; Intro T1; Red in T1. -Apply T1 with y0; Auto with sets. -Apply Rstar_n with x0; Auto with sets. +intros U R H'; red in |- *. +intros x y H'0; elim H'0; auto with sets. +intros x0 y0 z H'1 H'2 H'3. +generalize Rstar_transitive; intro T1; red in T1. +apply T1 with y0; auto with sets. +apply Rstar_n with x0; auto with sets. Qed. Theorem Sstar_contains_Rstar : - (U: Type) (R, S: (Relation U)) (contains U (Rstar U S) R) -> - (contains U (Rstar U S) (Rstar U R)). + forall (U:Type) (R S:Relation U), + contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R). Proof. -Unfold contains. -Intros U R S H' x y H'0; Elim H'0; Auto with sets. -Generalize Rstar_transitive; Intro T1; Red in T1. -Intros x0 y0 z H'1 H'2 H'3; Apply T1 with y0; Auto with sets. +unfold contains in |- *. +intros U R S H' x y H'0; elim H'0; auto with sets. +generalize Rstar_transitive; intro T1; red in T1. +intros x0 y0 z H'1 H'2 H'3; apply T1 with y0; auto with sets. Qed. Theorem star_monotone : - (U: Type) (R, S: (Relation U)) (contains U S R) -> - (contains U (Rstar U S) (Rstar U R)). + forall (U:Type) (R S:Relation U), + contains U S R -> contains U (Rstar U S) (Rstar U R). Proof. -Intros U R S H'. -Apply Sstar_contains_Rstar; Auto with sets. -Generalize (Rstar_contains_R U S); Auto with sets. +intros U R S H'. +apply Sstar_contains_Rstar; auto with sets. +generalize (Rstar_contains_R U S); auto with sets. Qed. Theorem RstarRplus_RRstar : - (U: Type) (R: (Relation U)) (x, y, z: U) - (Rstar U R x y) -> (Rplus U R y z) -> - (EXT u | (R x u) /\ (Rstar U R u z)). + forall (U:Type) (R:Relation U) (x y z:U), + Rstar U R x y -> Rplus U R y z -> exists u : _ | R x u /\ Rstar U R u z. Proof. -Generalize Rstar_contains_Rplus; Intro T; Red in T. -Generalize Rstar_transitive; Intro T1; Red in T1. -Intros U R x y z H'; Elim H'. -Intros x0 H'0; Elim H'0. -Intros x1 y0 H'1; Exists y0; Auto with sets. -Intros x1 y0 z0 H'1 H'2 H'3; Exists y0; Auto with sets. -Intros x0 y0 z0 H'0 H'1 H'2 H'3; Exists y0. -Split; [Try Assumption | Idtac]. -Apply T1 with z0; Auto with sets. +generalize Rstar_contains_Rplus; intro T; red in T. +generalize Rstar_transitive; intro T1; red in T1. +intros U R x y z H'; elim H'. +intros x0 H'0; elim H'0. +intros x1 y0 H'1; exists y0; auto with sets. +intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets. +intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0. +split; [ try assumption | idtac ]. +apply T1 with z0; auto with sets. Qed. -Theorem Lemma1 : - (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> - (x, b: U) (Rstar U R x b) -> - (a: U) (R x a) -> (EXT z | (Rstar U R a z) /\ (R b z)). +Theorem Lemma1 : + forall (U:Type) (R:Relation U), + Strongly_confluent U R -> + forall x b:U, + Rstar U R x b -> + forall a:U, R x a -> exists z : _ | Rstar U R a z /\ R b z. Proof. -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 3 H' with x := x0 a := a b := y; Intro H'7; LApply H'7; - [Intro H'8; LApply H'8; - [Intro H'9; Try Exact H'9; Clear H'8 H'7 | Clear H'8 H'7] | Clear H'7]; Auto with sets. -Elim H'9. -Intros t H'5; Elim H'5; Intros H'6 H'7; Try Exact H'6; Clear H'5. -Elim (H'3 t); Auto with sets. -Intros z1 H'5; Elim H'5; Intros H'8 H'10; Try Exact H'8; Clear H'5. -Exists z1; Split; [Idtac | Assumption]. -Apply Rstar_n with t; Auto with sets. -Qed. +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 3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7; + [ intro H'8; lapply H'8; + [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ] + | clear H'7 ]; auto with sets. +elim H'9. +intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5. +elim (H'3 t); auto with sets. +intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5. +exists z1; split; [ idtac | assumption ]. +apply Rstar_n with t; auto with sets. +Qed. \ No newline at end of file diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 90c055775..1fe689002 100755 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -30,34 +30,33 @@ Require Export Relations_1. Require Export Relations_2. Section Relations_3. - Variable U: Type. - Variable R: (Relation U). + Variable U : Type. + Variable R : Relation U. - Definition coherent : U -> U -> Prop := - [x,y: U] (EXT z | (Rstar U R x z) /\ (Rstar U R y z)). + Definition coherent (x y:U) : Prop := + exists z : _ | Rstar U R x z /\ Rstar U R y z. - Definition locally_confluent : U -> Prop := - [x: U] (y,z: U) (R x y) -> (R x z) -> (coherent 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 := (x: U) (locally_confluent x). + Definition Locally_confluent : Prop := forall x:U, locally_confluent x. - Definition confluent : U -> Prop := - [x: U] (y,z: U) (Rstar U R x y) -> (Rstar U R x z) -> (coherent y z). + 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 := (x: U) (confluent x). + Definition Confluent : Prop := forall x:U, confluent x. - Inductive noetherian : U -> Prop := - definition_of_noetherian: - (x: U) ((y: U) (R x y) -> (noetherian y)) -> (noetherian x). + Inductive noetherian : U -> Prop := + definition_of_noetherian : + forall x:U, (forall y:U, R x y -> noetherian y) -> noetherian x. - Definition Noetherian : Prop := (x: U) (noetherian x). + Definition Noetherian : Prop := forall x:U, noetherian x. End Relations_3. -Hints Unfold coherent : sets v62. -Hints Unfold locally_confluent : sets v62. -Hints Unfold confluent : sets v62. -Hints Unfold Confluent : sets v62. -Hints Resolve definition_of_noetherian : sets v62. -Hints Unfold Noetherian : sets v62. - +Hint Unfold coherent: sets v62. +Hint Unfold locally_confluent: sets v62. +Hint Unfold confluent: sets v62. +Hint Unfold Confluent: sets v62. +Hint Resolve definition_of_noetherian: sets v62. +Hint Unfold Noetherian: sets v62. diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index a57487d1e..5b1ce9e31 100755 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -33,125 +33,139 @@ Require Export Relations_2_facts. Require Export Relations_3. Theorem Rstar_imp_coherent : - (U: Type) (R: (Relation U)) (x: U) (y: U) (Rstar U R x y) -> - (coherent U R x y). + forall (U:Type) (R:Relation U) (x y:U), Rstar U R x y -> coherent U R x y. Proof. -Intros U R x y H'; Red. -Exists y; Auto with sets. +intros U R x y H'; red in |- *. +exists y; auto with sets. Qed. -Hints Resolve Rstar_imp_coherent. +Hint Resolve Rstar_imp_coherent. Theorem coherent_symmetric : - (U: Type) (R: (Relation U)) (Symmetric U (coherent U R)). + forall (U:Type) (R:Relation U), Symmetric U (coherent U R). Proof. -Unfold 1 coherent. -Intros U R; Red. -Intros x y H'; Elim H'. -Intros z H'0; Exists z; Tauto. +unfold coherent at 1 in |- *. +intros U R; red in |- *. +intros x y H'; elim H'. +intros z H'0; exists z; tauto. Qed. Theorem Strong_confluence : - (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R). + forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R. Proof. -Intros U R H'; Red. -Intro x; Red; Intros a b H'0. -Unfold 1 coherent. -Generalize b; Clear b. -Elim H'0; Clear H'0. -Intros x0 b H'1; Exists b; Auto with sets. -Intros x0 y z H'1 H'2 H'3 b H'4. -Generalize (Lemma1 U R); Intro h; LApply h; - [Intro H'0; Generalize (H'0 x0 b); Intro h0; LApply h0; - [Intro H'5; Generalize (H'5 y); Intro h1; LApply h1; - [Intro h2; Elim h2; Intros z0 h3; Elim h3; Intros H'6 H'7; - Clear h h0 h1 h2 h3 | Clear h h0 h1] | Clear h h0] | Clear h]; Auto with sets. -Generalize (H'3 z0); Intro h; LApply h; - [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h h0 h1 | - Clear h]; Auto with sets. -Exists z1; Split; Auto with sets. -Apply Rstar_n with z0; Auto with sets. +intros U R H'; red in |- *. +intro x; red in |- *; intros a b H'0. +unfold coherent at 1 in |- *. +generalize b; clear b. +elim H'0; clear H'0. +intros x0 b H'1; exists b; auto with sets. +intros x0 y z H'1 H'2 H'3 b H'4. +generalize (Lemma1 U R); intro h; lapply h; + [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0; + [ intro H'5; generalize (H'5 y); intro h1; lapply h1; + [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7; + clear h h0 h1 h2 h3 + | clear h h0 h1 ] + | clear h h0 ] + | clear h ]; auto with sets. +generalize (H'3 z0); intro h; lapply h; + [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1 + | clear h ]; auto with sets. +exists z1; split; auto with sets. +apply Rstar_n with z0; auto with sets. Qed. Theorem Strong_confluence_direct : - (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R). + forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R. Proof. -Intros U R H'; Red. -Intro x; Red; Intros a b H'0. -Unfold 1 coherent. -Generalize b; Clear b. -Elim H'0; Clear H'0. -Intros x0 b H'1; Exists b; Auto with sets. -Intros x0 y z H'1 H'2 H'3 b H'4. -Cut (exT U [t: U] (Rstar U R y t) /\ (R b t)). -Intro h; Elim h; Intros t h0; Elim h0; Intros H'0 H'5; Clear h h0. -Generalize (H'3 t); Intro h; LApply h; - [Intro h0; Elim h0; Intros z0 h1; Elim h1; Intros H'6 H'7; Clear h h0 h1 | - Clear h]; Auto with sets. -Exists z0; Split; [Assumption | Idtac]. -Apply Rstar_n with t; Auto with sets. -Generalize H'1; Generalize y; Clear H'1. -Elim H'4. -Intros x1 y0 H'0; Exists y0; Auto with sets. -Intros x1 y0 z0 H'0 H'1 H'5 y1 H'6. -Red in H'. -Generalize (H' x1 y0 y1); Intro h; LApply h; - [Intro H'7; LApply H'7; - [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h H'7 h0 h1 | - Clear h] | Clear h]; Auto with sets. -Generalize (H'5 z1); Intro h; LApply h; - [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'7 H'10; Clear h h0 h1 | - Clear h]; Auto with sets. -Exists t; Split; Auto with sets. -Apply Rstar_n with z1; Auto with sets. +intros U R H'; red in |- *. +intro x; red in |- *; intros a b H'0. +unfold coherent at 1 in |- *. +generalize b; clear b. +elim H'0; clear H'0. +intros x0 b H'1; exists b; auto with sets. +intros x0 y z H'1 H'2 H'3 b H'4. +cut (ex (fun t:U => Rstar U R y t /\ R b t)). +intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0. +generalize (H'3 t); intro h; lapply h; + [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1 + | clear h ]; auto with sets. +exists z0; split; [ assumption | idtac ]. +apply Rstar_n with t; auto with sets. +generalize H'1; generalize y; clear H'1. +elim H'4. +intros x1 y0 H'0; exists y0; auto with sets. +intros x1 y0 z0 H'0 H'1 H'5 y1 H'6. +red in H'. +generalize (H' x1 y0 y1); intro h; lapply h; + [ intro H'7; lapply H'7; + [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; + clear h H'7 h0 h1 + | clear h ] + | clear h ]; auto with sets. +generalize (H'5 z1); intro h; lapply h; + [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1 + | clear h ]; auto with sets. +exists t; split; auto with sets. +apply Rstar_n with z1; auto with sets. Qed. Theorem Noetherian_contains_Noetherian : - (U: Type) (R, R': (Relation U)) (Noetherian U R) -> (contains U R R') -> - (Noetherian U R'). + forall (U:Type) (R R':Relation U), + Noetherian U R -> contains U R R' -> Noetherian U R'. Proof. -Unfold 2 Noetherian. -Intros U R R' H' H'0 x. -Elim (H' x); Auto with sets. +unfold Noetherian at 2 in |- *. +intros U R R' H' H'0 x. +elim (H' x); auto with sets. Qed. Theorem Newman : - (U: Type) (R: (Relation U)) (Noetherian U R) -> (Locally_confluent U R) -> - (Confluent U R). + forall (U:Type) (R:Relation U), + Noetherian U R -> Locally_confluent U R -> Confluent U R. Proof. -Intros U R H' H'0; Red; Intro x. -Elim (H' x); Unfold confluent. -Intros x0 H'1 H'2 y z H'3 H'4. -Generalize (Rstar_cases U R x0 y); Intro h; LApply h; - [Intro h0; Elim h0; - [Clear h h0; Intro h1 | - Intro h1; Elim h1; Intros u h2; Elim h2; Intros H'5 H'6; Clear h h0 h1 h2] | - Clear h]; Auto with sets. -Elim h1; Auto with sets. -Generalize (Rstar_cases U R x0 z); Intro h; LApply h; - [Intro h0; Elim h0; - [Clear h h0; Intro h1 | - Intro h1; Elim h1; Intros v h2; Elim h2; Intros H'7 H'8; Clear h h0 h1 h2] | - Clear h]; Auto with sets. -Elim h1; Generalize coherent_symmetric; Intro t; Red in t; Auto with sets. -Unfold Locally_confluent locally_confluent coherent in H'0. -Generalize (H'0 x0 u v); Intro h; LApply h; - [Intro H'9; LApply H'9; - [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'10 H'11; - Clear h H'9 h0 h1 | Clear h] | Clear h]; Auto with sets. -Clear H'0. -Unfold 1 coherent in H'2. -Generalize (H'2 u); Intro h; LApply h; - [Intro H'0; Generalize (H'0 y t); Intro h0; LApply h0; - [Intro H'9; LApply H'9; - [Intro h1; Elim h1; Intros y1 h2; Elim h2; Intros H'12 H'13; - Clear h h0 H'9 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets. -Generalize Rstar_transitive; Intro T; Red in T. -Generalize (H'2 v); Intro h; LApply h; - [Intro H'9; Generalize (H'9 y1 z); Intro h0; LApply h0; - [Intro H'14; LApply H'14; - [Intro h1; Elim h1; Intros z1 h2; Elim h2; Intros H'15 H'16; - Clear h h0 H'14 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets. -Red; (Exists z1; Split); Auto with sets. -Apply T with y1; Auto with sets. -Apply T with t; Auto with sets. -Qed. +intros U R H' H'0; red in |- *; intro x. +elim (H' x); unfold confluent in |- *. +intros x0 H'1 H'2 y z H'3 H'4. +generalize (Rstar_cases U R x0 y); intro h; lapply h; + [ intro h0; elim h0; + [ clear h h0; intro h1 + | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6; + clear h h0 h1 h2 ] + | clear h ]; auto with sets. +elim h1; auto with sets. +generalize (Rstar_cases U R x0 z); intro h; lapply h; + [ intro h0; elim h0; + [ clear h h0; intro h1 + | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8; + clear h h0 h1 h2 ] + | clear h ]; auto with sets. +elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets. +unfold Locally_confluent, locally_confluent, coherent in H'0. +generalize (H'0 x0 u v); intro h; lapply h; + [ intro H'9; lapply H'9; + [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11; + clear h H'9 h0 h1 + | clear h ] + | clear h ]; auto with sets. +clear H'0. +unfold coherent at 1 in H'2. +generalize (H'2 u); intro h; lapply h; + [ intro H'0; generalize (H'0 y t); intro h0; lapply h0; + [ intro H'9; lapply H'9; + [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13; + clear h h0 H'9 h1 h2 + | clear h h0 ] + | clear h h0 ] + | clear h ]; auto with sets. +generalize Rstar_transitive; intro T; red in T. +generalize (H'2 v); intro h; lapply h; + [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0; + [ intro H'14; lapply H'14; + [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16; + clear h h0 H'14 h1 h2 + | clear h h0 ] + | clear h h0 ] + | clear h ]; auto with sets. +red in |- *; (exists z1; split); auto with sets. +apply T with y1; auto with sets. +apply T with t; auto with sets. +Qed. \ No newline at end of file diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 5b28d6c2b..e1ba00209 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -13,7 +13,7 @@ (* G. Huet 1-9-95 *) (* Updated Papageno 12/98 *) -Require Bool. +Require Import Bool. Set Implicit Arguments. @@ -21,121 +21,118 @@ Section defs. Variable A : Set. Variable eqA : A -> A -> Prop. -Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}. +Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. -Inductive uniset : Set := - Charac : (A->bool) -> uniset. +Inductive uniset : Set := + Charac : (A -> bool) -> uniset. -Definition charac : uniset -> A -> bool := - [s:uniset][a:A]Case s of [f:A->bool](f a) end. +Definition charac (s:uniset) (a:A) : bool := let (f) := s in f a. -Definition Emptyset := (Charac [a:A]false). +Definition Emptyset := Charac (fun a:A => false). -Definition Fullset := (Charac [a:A]true). +Definition Fullset := Charac (fun a:A => true). -Definition Singleton := [a:A](Charac [a':A] - Case (eqA_dec a a') of - [h:(eqA a a')] true - [h: ~(eqA a a')] false end). +Definition Singleton (a:A) := + Charac + (fun a':A => + match eqA_dec a a' with + | left h => true + | right h => false + end). -Definition In : uniset -> A -> Prop := - [s:uniset][a:A](charac s a)=true. -Hints Unfold In. +Definition In (s:uniset) (a:A) : Prop := charac s a = true. +Hint Unfold In. (** uniset inclusion *) -Definition incl := [s1,s2:uniset] - (a:A)(leb (charac s1 a) (charac s2 a)). -Hints Unfold incl. +Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a). +Hint Unfold incl. (** uniset equality *) -Definition seq := [s1,s2:uniset] - (a:A)(charac s1 a) = (charac s2 a). -Hints Unfold seq. +Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. +Hint Unfold seq. -Lemma leb_refl : (b:bool)(leb b b). +Lemma leb_refl : forall b:bool, leb b b. Proof. -NewDestruct b; Simpl; Auto. +destruct b; simpl in |- *; auto. Qed. -Hints Resolve leb_refl. +Hint Resolve leb_refl. -Lemma incl_left : (s1,s2:uniset)(seq s1 s2)->(incl s1 s2). +Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. -Unfold incl; Intros s1 s2 E a; Elim (E a); Auto. +unfold incl in |- *; intros s1 s2 E a; elim (E a); auto. Qed. -Lemma incl_right : (s1,s2:uniset)(seq s1 s2)->(incl s2 s1). +Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1. Proof. -Unfold incl; Intros s1 s2 E a; Elim (E a); Auto. +unfold incl in |- *; intros s1 s2 E a; elim (E a); auto. Qed. -Lemma seq_refl : (x:uniset)(seq x x). +Lemma seq_refl : forall x:uniset, seq x x. Proof. -NewDestruct x; Unfold seq; Auto. +destruct x; unfold seq in |- *; auto. Qed. -Hints Resolve seq_refl. +Hint Resolve seq_refl. -Lemma seq_trans : (x,y,z:uniset)(seq x y)->(seq y z)->(seq x z). +Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z. Proof. -Unfold seq. -NewDestruct x; NewDestruct y; NewDestruct z; Simpl; Intros. -Rewrite H; Auto. +unfold seq in |- *. +destruct x; destruct y; destruct z; simpl in |- *; intros. +rewrite H; auto. Qed. -Lemma seq_sym : (x,y:uniset)(seq x y)->(seq y x). +Lemma seq_sym : forall x y:uniset, seq x y -> seq y x. Proof. -Unfold seq. -NewDestruct x; NewDestruct y; Simpl; Auto. +unfold seq in |- *. +destruct x; destruct y; simpl in |- *; auto. Qed. (** uniset union *) -Definition union := [m1,m2:uniset] - (Charac [a:A](orb (charac m1 a)(charac m2 a))). +Definition union (m1 m2:uniset) := + Charac (fun a:A => orb (charac m1 a) (charac m2 a)). -Lemma union_empty_left : - (x:uniset)(seq x (union Emptyset x)). +Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). Proof. -Unfold seq; Unfold union; Simpl; Auto. +unfold seq in |- *; unfold union in |- *; simpl in |- *; auto. Qed. -Hints Resolve union_empty_left. +Hint Resolve union_empty_left. -Lemma union_empty_right : - (x:uniset)(seq x (union x Emptyset)). +Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset). Proof. -Unfold seq; Unfold union; Simpl. -Intros x a; Rewrite (orb_b_false (charac x a)); Auto. +unfold seq in |- *; unfold union in |- *; simpl in |- *. +intros x a; rewrite (orb_b_false (charac x a)); auto. Qed. -Hints Resolve union_empty_right. +Hint Resolve union_empty_right. -Lemma union_comm : (x,y:uniset)(seq (union x y) (union y x)). +Lemma union_comm : forall x y:uniset, seq (union x y) (union y x). Proof. -Unfold seq; Unfold charac; Unfold union. -NewDestruct x; NewDestruct y; Auto with bool. +unfold seq in |- *; unfold charac in |- *; unfold union in |- *. +destruct x; destruct y; auto with bool. Qed. -Hints Resolve union_comm. +Hint Resolve union_comm. -Lemma union_ass : - (x,y,z:uniset)(seq (union (union x y) z) (union x (union y z))). +Lemma union_ass : + forall x y z:uniset, seq (union (union x y) z) (union x (union y z)). Proof. -Unfold seq; Unfold union; Unfold charac. -NewDestruct x; NewDestruct y; NewDestruct z; Auto with bool. +unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +destruct x; destruct y; destruct z; auto with bool. Qed. -Hints Resolve union_ass. +Hint Resolve union_ass. -Lemma seq_left : (x,y,z:uniset)(seq x y)->(seq (union x z) (union y z)). +Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z). Proof. -Unfold seq; Unfold union; Unfold charac. -NewDestruct x; NewDestruct y; NewDestruct z. -Intros; Elim H; Auto. +unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto. Qed. -Hints Resolve seq_left. +Hint Resolve seq_left. -Lemma seq_right : (x,y,z:uniset)(seq x y)->(seq (union z x) (union z y)). +Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y). Proof. -Unfold seq; Unfold union; Unfold charac. -NewDestruct x; NewDestruct y; NewDestruct z. -Intros; Elim H; Auto. +unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto. Qed. -Hints Resolve seq_right. +Hint Resolve seq_right. (** All the proofs that follow duplicate [Multiset_of_A] *) @@ -143,60 +140,66 @@ Hints Resolve seq_right. (** Here we should make uniset an abstract datatype, by hiding [Charac], [union], [charac]; all further properties are proved abstractly *) -Require Permut. +Require Import Permut. Lemma union_rotate : - (x,y,z:uniset)(seq (union x (union y z)) (union z (union x y))). + forall x y z:uniset, seq (union x (union y z)) (union z (union x y)). Proof. -Intros; Apply (op_rotate uniset union seq); Auto. -Exact seq_trans. +intros; apply (op_rotate uniset union seq); auto. +exact seq_trans. Qed. -Lemma seq_congr : (x,y,z,t:uniset)(seq x y)->(seq z t)-> - (seq (union x z) (union y t)). +Lemma seq_congr : + forall x y z t:uniset, seq x y -> seq z t -> seq (union x z) (union y t). Proof. -Intros; Apply (cong_congr uniset union seq); Auto. -Exact seq_trans. +intros; apply (cong_congr uniset union seq); auto. +exact seq_trans. Qed. Lemma union_perm_left : - (x,y,z:uniset)(seq (union x (union y z)) (union y (union x z))). + forall x y z:uniset, seq (union x (union y z)) (union y (union x z)). Proof. -Intros; Apply (perm_left uniset union seq); Auto. -Exact seq_trans. +intros; apply (perm_left uniset union seq); auto. +exact seq_trans. Qed. -Lemma uniset_twist1 : (x,y,z,t:uniset) - (seq (union x (union (union y z) t)) (union (union y (union x t)) z)). +Lemma uniset_twist1 : + forall x y z t:uniset, + seq (union x (union (union y z) t)) (union (union y (union x t)) z). Proof. -Intros; Apply (twist uniset union seq); Auto. -Exact seq_trans. +intros; apply (twist uniset union seq); auto. +exact seq_trans. Qed. -Lemma uniset_twist2 : (x,y,z,t:uniset) - (seq (union x (union (union y z) t)) (union (union y (union x z)) t)). +Lemma uniset_twist2 : + forall x y z t:uniset, + seq (union x (union (union y z) t)) (union (union y (union x z)) t). Proof. -Intros; Apply seq_trans with (union (union x (union y z)) t). -Apply seq_sym; Apply union_ass. -Apply seq_left; Apply union_perm_left. +intros; apply seq_trans with (union (union x (union y z)) t). +apply seq_sym; apply union_ass. +apply seq_left; apply union_perm_left. Qed. (** specific for treesort *) -Lemma treesort_twist1 : (x,y,z,t,u:uniset) (seq u (union y z)) -> - (seq (union x (union u t)) (union (union y (union x t)) z)). +Lemma treesort_twist1 : + forall x y z t u:uniset, + seq u (union y z) -> + seq (union x (union u t)) (union (union y (union x t)) z). Proof. -Intros; Apply seq_trans with (union x (union (union y z) t)). -Apply seq_right; Apply seq_left; Trivial. -Apply uniset_twist1. +intros; apply seq_trans with (union x (union (union y z) t)). +apply seq_right; apply seq_left; trivial. +apply uniset_twist1. Qed. -Lemma treesort_twist2 : (x,y,z,t,u:uniset) (seq u (union y z)) -> - (seq (union x (union u t)) (union (union y (union x z)) t)). +Lemma treesort_twist2 : + forall x y z t u:uniset, + seq u (union y z) -> + seq (union x (union u t)) (union (union y (union x z)) t). Proof. -Intros; Apply seq_trans with (union x (union (union y z) t)). -Apply seq_right; Apply seq_left; Trivial. -Apply uniset_twist2. +intros; apply seq_trans with (union x (union (union y z) t)). +apply seq_right; apply seq_left; trivial. +apply uniset_twist2. Qed. @@ -209,4 +212,4 @@ i*) End defs. -Unset Implicit Arguments. +Unset Implicit Arguments. \ No newline at end of file -- cgit v1.2.3