diff options
Diffstat (limited to 'theories7/Sets')
| -rwxr-xr-x | theories7/Sets/Classical_sets.v | 133 | ||||
| -rwxr-xr-x | theories7/Sets/Constructive_sets.v | 162 | ||||
| -rwxr-xr-x | theories7/Sets/Cpo.v | 107 | ||||
| -rwxr-xr-x | theories7/Sets/Ensembles.v | 108 | ||||
| -rwxr-xr-x | theories7/Sets/Finite_sets.v | 74 | ||||
| -rwxr-xr-x | theories7/Sets/Finite_sets_facts.v | 345 | ||||
| -rwxr-xr-x | theories7/Sets/Image.v | 199 | ||||
| -rwxr-xr-x | theories7/Sets/Infinite_sets.v | 232 | ||||
| -rwxr-xr-x | theories7/Sets/Integers.v | 166 | ||||
| -rwxr-xr-x | theories7/Sets/Multiset.v | 186 | ||||
| -rwxr-xr-x | theories7/Sets/Partial_Order.v | 100 | ||||
| -rwxr-xr-x | theories7/Sets/Permut.v | 91 | ||||
| -rwxr-xr-x | theories7/Sets/Powerset.v | 188 | ||||
| -rwxr-xr-x | theories7/Sets/Powerset_Classical_facts.v | 338 | ||||
| -rwxr-xr-x | theories7/Sets/Powerset_facts.v | 276 | ||||
| -rwxr-xr-x | theories7/Sets/Relations_1.v | 67 | ||||
| -rwxr-xr-x | theories7/Sets/Relations_1_facts.v | 109 | ||||
| -rwxr-xr-x | theories7/Sets/Relations_2.v | 56 | ||||
| -rwxr-xr-x | theories7/Sets/Relations_2_facts.v | 151 | ||||
| -rwxr-xr-x | theories7/Sets/Relations_3.v | 63 | ||||
| -rwxr-xr-x | theories7/Sets/Relations_3_facts.v | 157 | ||||
| -rw-r--r-- | theories7/Sets/Uniset.v | 212 |
22 files changed, 0 insertions, 3520 deletions
diff --git a/theories7/Sets/Classical_sets.v b/theories7/Sets/Classical_sets.v deleted file mode 100755 index a6928ffd..00000000 --- a/theories7/Sets/Classical_sets.v +++ /dev/null @@ -1,133 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Classical_sets.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*) - -Require Export Ensembles. -Require Export Constructive_sets. -Require Export Classical_Type. - -(* Hints Unfold not . *) - -Section Ensembles_classical. -Variable U: Type. - -Lemma not_included_empty_Inhabited: - (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. -Qed. -Hints Resolve not_included_empty_Inhabited. - -Lemma not_empty_Inhabited: - (A: (Ensemble U)) ~ A == (Empty_set U) -> (Inhabited U A). -Proof. -Intros; Apply not_included_empty_Inhabited. -Red; 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)). -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. -Qed. -Hints 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)). -Proof. -Auto 7 with sets. -Qed. -Hints 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). -Proof. -Unfold 1 Subtract; Auto with sets. -Qed. -Hints 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. -Proof. -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. -Proof. -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)). -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. -Qed. - -Lemma not_SIncl_empty: - (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. -Qed. - -Lemma Complement_Complement : - (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. -Qed. - -End Ensembles_classical. - -Hints Resolve Strict_super_set_contains_new_element Subtract_intro - not_SIncl_empty : sets v62. diff --git a/theories7/Sets/Constructive_sets.v b/theories7/Sets/Constructive_sets.v deleted file mode 100755 index 35c88e9d..00000000 --- a/theories7/Sets/Constructive_sets.v +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Constructive_sets.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*) - -Require Export Ensembles. - -Section Ensembles_facts. -Variable U: Type. - -Lemma Extension: (B, C: (Ensemble U)) B == C -> (Same_set U B C). -Proof. -Intros B C H'; Rewrite H'; Auto with sets. -Qed. - -Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x). -Proof. -Red; NewDestruct 1. -Qed. -Hints Resolve Noone_in_empty. - -Lemma Included_Empty: (A: (Ensemble U))(Included U (Empty_set U) A). -Proof. -Intro; Red. -Intros x H; Elim (Noone_in_empty x); Auto with sets. -Qed. -Hints Resolve Included_Empty. - -Lemma Add_intro1: - (A: (Ensemble U)) (x, y: U) (In U A y) -> (In U (Add U A x) y). -Proof. -Unfold 1 Add; Auto with sets. -Qed. -Hints Resolve Add_intro1. - -Lemma Add_intro2: (A: (Ensemble U)) (x: U) (In U (Add U A x) x). -Proof. -Unfold 1 Add; Auto with sets. -Qed. -Hints Resolve Add_intro2. - -Lemma Inhabited_add: (A: (Ensemble U)) (x: U) (Inhabited U (Add U A x)). -Proof. -Intros A x. -Apply Inhabited_intro with x := x; Auto with sets. -Qed. -Hints Resolve Inhabited_add. - -Lemma Inhabited_not_empty: - (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. -Qed. -Hints Resolve Inhabited_not_empty. - -Lemma Add_not_Empty : - (A: (Ensemble U)) (x: U) ~ (Add U A x) == (Empty_set U). -Proof. -Auto with sets. -Qed. -Hints Resolve Add_not_Empty. - -Lemma not_Empty_Add : - (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. -Qed. -Hints Resolve not_Empty_Add. - -Lemma Singleton_inv: (x, y: U) (In U (Singleton U x) y) -> x == y. -Proof. -Intros x y H'; Elim H'; Trivial with sets. -Qed. -Hints Resolve Singleton_inv. - -Lemma Singleton_intro: (x, y: U) x == y -> (In U (Singleton U x) y). -Proof. -Intros x y H'; Rewrite H'; Trivial with sets. -Qed. -Hints 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). -Proof. -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. -Proof. -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). -Proof. -Intros B C x H'; Elim H'; Auto with sets. -Qed. -Hints Resolve Intersection_inv. - -Lemma Couple_inv: (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. -Qed. -Hints 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). -Proof. -Unfold 1 Setminus; Red; Auto with sets. -Qed. -Hints Resolve Setminus_intro. - -Lemma Strict_Included_intro: - (X, Y: (Ensemble U)) (Included U X Y) /\ ~ X == Y -> - (Strict_Included U X Y). -Proof. -Auto with sets. -Qed. -Hints Resolve Strict_Included_intro. - -Lemma Strict_Included_strict: (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. -Qed. -Hints 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. diff --git a/theories7/Sets/Cpo.v b/theories7/Sets/Cpo.v deleted file mode 100755 index 2fe46be6..00000000 --- a/theories7/Sets/Cpo.v +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Cpo.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*) - -Require Export Ensembles. -Require Export Relations_1. -Require Export Partial_Order. - -Section Bounds. -Variable U: Type. -Variable D: (PO U). - -Local C := (Carrier_of U D). - -Local 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 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 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 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 Bottom [bot:U]: Prop := - Bottom_definition: - (In U C bot) -> ((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). - -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)). - -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 Complete : Prop := - Definition_of_Complete: - ((EXT bot | (Bottom bot))) -> - ((X: (Ensemble U)) (Directed X) -> (EXT 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. -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. - -Section Specific_orders. -Variable U: Type. - -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)) }. - -End Specific_orders. diff --git a/theories7/Sets/Ensembles.v b/theories7/Sets/Ensembles.v deleted file mode 100755 index c3a044c0..00000000 --- a/theories7/Sets/Ensembles.v +++ /dev/null @@ -1,108 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Ensembles.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Section Ensembles. -Variable U: Type. - -Definition Ensemble := U -> Prop. - -Definition In : Ensemble -> U -> Prop := [A: Ensemble] [x: U] (A x). - -Definition Included : Ensemble -> Ensemble -> Prop := - [B, C: Ensemble] (x: U) (In B x) -> (In C x). - -Inductive Empty_set : Ensemble := - . - -Inductive Full_set : Ensemble := - Full_intro: (x: U) (In Full_set x). - -(** NB: The following definition builds-in equality of elements in [U] as - Leibniz equality. - - This may have to be changed if we replace [U] by a Setoid on [U] - with its own equality [eqs], with - [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *) - -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). - -Definition Add : Ensemble -> U -> Ensemble := - [B: Ensemble] [x: U] (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 Couple [x,y:U] : Ensemble := - Couple_l: (In (Couple x y) x) - | Couple_r: (In (Couple x y) y). - -Inductive Triple[x, y, z:U] : Ensemble := - Triple_l: (In (Triple x y z) x) - | Triple_m: (In (Triple x y z) y) - | Triple_r: (In (Triple x y z) z). - -Definition Complement : Ensemble -> Ensemble := - [A: Ensemble] [x: U] ~ (In A x). - -Definition Setminus : Ensemble -> Ensemble -> Ensemble := - [B: Ensemble] [C: Ensemble] [x: U] (In B x) /\ ~ (In C x). - -Definition Subtract : Ensemble -> U -> Ensemble := - [B: Ensemble] [x: U] (Setminus B (Singleton x)). - -Inductive Disjoint [B, C:Ensemble] : Prop := - Disjoint_intro: ((x: U) ~ (In (Intersection B C) x)) -> (Disjoint B C). - -Inductive Inhabited [B:Ensemble] : Prop := - Inhabited_intro: (x: U) (In B x) -> (Inhabited B). - -Definition Strict_Included : Ensemble -> Ensemble -> Prop := - [B, C: Ensemble] (Included B C) /\ ~ B == C. - -Definition Same_set : Ensemble -> Ensemble -> Prop := - [B, C: Ensemble] (Included B C) /\ (Included C B). - -(** Extensionality Axiom *) - -Axiom Extensionality_Ensembles: - (A,B: Ensemble) (Same_set A B) -> A == B. -Hints Resolve Extensionality_Ensembles. - -End Ensembles. - -Hints 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. diff --git a/theories7/Sets/Finite_sets.v b/theories7/Sets/Finite_sets.v deleted file mode 100755 index fb53994d..00000000 --- a/theories7/Sets/Finite_sets.v +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Finite_sets.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Ensembles. - -Section Ensembles_finis. -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 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)). - -End Ensembles_finis. - -Hints Resolve Empty_is_finite Union_is_finite : sets v62. -Hints Resolve card_empty card_add : sets v62. - -Require Constructive_sets. - -Section Ensembles_finis_facts. -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. -Proof. -NewInduction 1; Simpl; 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. -Proof. -Intros X p C; Elim C; Simpl; Trivial with sets. -Qed. - -End Ensembles_finis_facts. diff --git a/theories7/Sets/Finite_sets_facts.v b/theories7/Sets/Finite_sets_facts.v deleted file mode 100755 index 63d4d2ad..00000000 --- a/theories7/Sets/Finite_sets_facts.v +++ /dev/null @@ -1,345 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Finite_sets_facts.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Finite_sets. -Require Export Constructive_sets. -Require Export Classical_Type. -Require Export Classical_sets. -Require Export Powerset. -Require Export Powerset_facts. -Require Export Powerset_Classical_facts. -Require Export Gt. -Require Export Lt. - -Section Finite_sets_facts. -Variable U: Type. - -Lemma finite_cardinal : - (X: (Ensemble U)) (Finite U X) -> (EX n:nat |(cardinal U X n)). -Proof. -NewInduction 1 as [|A _ [n H]]. -Exists O; 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). -Proof. -NewInduction 1; Auto with sets. -Qed. - -Theorem Add_preserves_Finite: - (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. -Qed. -Hints Resolve Add_preserves_Finite. - -Theorem Singleton_is_finite: (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. -Qed. -Hints Resolve Singleton_is_finite. - -Theorem Union_preserves_Finite: - (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. -Qed. - -Lemma Finite_downward_closed: - (A: (Ensemble U)) (Finite U A) -> - (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. -Qed. - -Lemma Intersection_preserves_finite: - (A: (Ensemble U)) (Finite U A) -> - (X: (Ensemble U)) (Finite U (Intersection U X A)). -Proof. -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). -Proof. -Intros X H; Apply (cardinal_invert U X O); Trivial with sets. -Qed. -Hints Resolve cardinalO_empty. - -Lemma inh_card_gt_O: - (X: (Ensemble U)) (Inhabited U X) -> (n: nat) (cardinal U X n) -> (gt n O). -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. -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)). -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. -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. -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 ]. -Qed. - -Lemma cardinal_Empty : (m:nat)(cardinal U (Empty_set U) m) -> O = 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). -Qed. - -Lemma cardinal_unicity : - (X: (Ensemble U)) (n: nat) (cardinal U X n) -> - (m: nat) (cardinal U X m) -> n = m. -Proof. -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)). -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. -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). -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. -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). -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. -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)). -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. -Qed. - -Hints 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). -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. -Qed. - -End Finite_sets_facts. diff --git a/theories7/Sets/Image.v b/theories7/Sets/Image.v deleted file mode 100755 index 0794a3bb..00000000 --- a/theories7/Sets/Image.v +++ /dev/null @@ -1,199 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Image.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Finite_sets. -Require Export Constructive_sets. -Require Export Classical_Type. -Require Export Classical_sets. -Require Export Powerset. -Require Export Powerset_facts. -Require Export Powerset_Classical_facts. -Require Export Gt. -Require Export Lt. -Require Export Le. -Require Export Finite_sets_facts. - -Section Image. -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). - -Lemma Im_def: - (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. -Qed. -Hints 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)). -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. -Qed. - -Lemma image_empty: (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. -Qed. -Hints Resolve image_empty. - -Lemma finite_image: - (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. -Qed. -Hints 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). -Proof. -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. - -Lemma not_injective_elim: - (f: U -> V) ~ (injective f) -> - (EXT x | (EXT 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. -Qed. - -Lemma cardinal_Im_intro: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) -> - (EX p: nat | (cardinal ? (Im A f) p)). -Proof. -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). -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. -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. -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. -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). -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. -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). -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. -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)). -Proof. -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. diff --git a/theories7/Sets/Infinite_sets.v b/theories7/Sets/Infinite_sets.v deleted file mode 100755 index bf423753..00000000 --- a/theories7/Sets/Infinite_sets.v +++ /dev/null @@ -1,232 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Infinite_sets.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Finite_sets. -Require Export Constructive_sets. -Require Export Classical_Type. -Require Export Classical_sets. -Require Export Powerset. -Require Export Powerset_facts. -Require Export Powerset_Classical_facts. -Require Export Gt. -Require Export Lt. -Require Export Le. -Require Export Finite_sets_facts. -Require Export Image. - -Section Approx. -Variable U: Type. - -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. - -Section Infinite_sets. -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)). -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. -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)). -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. -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)). -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. -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)). -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. -Qed. - -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)). -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. -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). -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. -Qed. - -Theorem Pigeonhole_bis: - (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. -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). -Proof. -Intros A f H' H'0 H'1. -Apply NNPP. -Red; Intro H'2. -Elim (Pigeonhole_bis A f); Auto with sets. -Qed. - -End Infinite_sets. diff --git a/theories7/Sets/Integers.v b/theories7/Sets/Integers.v deleted file mode 100755 index 7dee371f..00000000 --- a/theories7/Sets/Integers.v +++ /dev/null @@ -1,166 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Integers.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Finite_sets. -Require Export Constructive_sets. -Require Export Classical_Type. -Require Export Classical_sets. -Require Export Powerset. -Require Export Powerset_facts. -Require Export Powerset_Classical_facts. -Require Export Gt. -Require Export Lt. -Require Export Le. -Require Export Finite_sets_facts. -Require Export Image. -Require Export Infinite_sets. -Require Export Compare_dec. -Require Export Relations_1. -Require Export Partial_Order. -Require Export Cpo. - -Section Integers_sect. - -Inductive Integers : (Ensemble nat) := - Integers_defn: (x: nat) (In nat Integers x). -Hints Resolve Integers_defn. - -Lemma le_reflexive: (Reflexive nat le). -Proof. -Red; Auto with arith. -Qed. - -Lemma le_antisym: (Antisymmetric nat le). -Proof. -Red; Intros x y H H';Rewrite (le_antisym x y);Auto. -Qed. - -Lemma le_trans: (Transitive nat le). -Proof. -Red; Intros; Apply le_trans with y;Auto. -Qed. -Hints Resolve le_reflexive le_antisym le_trans. - -Lemma le_Order: (Order nat le). -Proof. -Auto with sets arith. -Qed. -Hints Resolve le_Order. - -Lemma triv_nat: (n: nat) (In nat Integers n). -Proof. -Auto with sets arith. -Qed. -Hints 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. -Defined. -Hints Unfold nat_po. - -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. -Qed. -Hints 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)). -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. -Qed. - -Lemma Integers_has_no_ub: ~ (EXT 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. -Qed. - -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. -Qed. - -End Integers_sect. - - - - - diff --git a/theories7/Sets/Multiset.v b/theories7/Sets/Multiset.v deleted file mode 100755 index b5d5edf7..00000000 --- a/theories7/Sets/Multiset.v +++ /dev/null @@ -1,186 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Multiset.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -(* G. Huet 1-9-95 *) - -Require Permut. - -Set Implicit Arguments. - -Section multiset_defs. - -Variable A : Set. -Variable eqA : A -> A -> Prop. -Hypothesis Aeq_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}. - -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 multiplicity : multiset -> A -> nat := - [m:multiset][a:A]let (f) = m in (f a). - -(** multiset equality *) -Definition meq := [m1,m2:multiset] - (a:A)(multiplicity m1 a)=(multiplicity m2 a). - -Hints Unfold meq multiplicity. - -Lemma meq_refl : (x:multiset)(meq x x). -Proof. -NewDestruct x; Auto. -Qed. -Hints Resolve meq_refl. - -Lemma meq_trans : (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. -Qed. - -Lemma meq_sym : (x,y:multiset)(meq x y)->(meq y x). -Proof. -Unfold meq. -NewDestruct x; NewDestruct y; Auto. -Qed. -Hints Immediate meq_sym. - -(** multiset union *) -Definition munion := [m1,m2:multiset] - (Bag [a:A](plus (multiplicity m1 a)(multiplicity m2 a))). - -Lemma munion_empty_left : - (x:multiset)(meq x (munion EmptyBag x)). -Proof. -Unfold meq; Unfold munion; Simpl; Auto. -Qed. -Hints Resolve munion_empty_left. - -Lemma munion_empty_right : - (x:multiset)(meq x (munion x EmptyBag)). -Proof. -Unfold meq; Unfold munion; Simpl; Auto. -Qed. - - -Require Plus. (* comm. and ass. of plus *) - -Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)). -Proof. -Unfold meq; Unfold multiplicity; Unfold munion. -NewDestruct x; NewDestruct y; Auto with arith. -Qed. -Hints Resolve munion_comm. - -Lemma munion_ass : - (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. -Qed. -Hints Resolve munion_ass. - -Lemma meq_left : (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. -Qed. -Hints Resolve meq_left. - -Lemma meq_right : (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. -Qed. -Hints 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))). -Proof. -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)). -Proof. -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))). -Proof. -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)). -Proof. -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)). -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. -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)). -Proof. -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)). -Proof. -Intros; Apply meq_trans with (munion x (munion (munion y z) t)). -Apply meq_right; Apply meq_left; Trivial. -Apply multiset_twist2. -Qed. - - -(*i theory of minter to do similarly -Require Min. -(* multiset intersection *) -Definition minter := [m1,m2:multiset] - (Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))). -i*) - -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. diff --git a/theories7/Sets/Partial_Order.v b/theories7/Sets/Partial_Order.v deleted file mode 100755 index 759cf4e2..00000000 --- a/theories7/Sets/Partial_Order.v +++ /dev/null @@ -1,100 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Partial_Order.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Ensembles. -Require Export Relations_1. - -Section Partial_orders. -Variable U: Type. - -Definition Carrier := (Ensemble U). - -Definition Rel := (Relation U). - -Record PO : Type := Definition_of_PO { - Carrier_of: (Ensemble U); - Rel_of: (Relation U); - PO_cond1: (Inhabited U Carrier_of); - PO_cond2: (Order U Rel_of) }. -Variable p: PO. - -Definition Strict_Rel_of : Rel := [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). - -End Partial_orders. - -Hints Unfold Carrier_of Rel_of Strict_Rel_of : sets v62. -Hints Resolve Definition_of_covers : sets v62. - - -Section Partial_order_facts. -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. -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. -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 ]. -Qed. -End Partial_order_facts. diff --git a/theories7/Sets/Permut.v b/theories7/Sets/Permut.v deleted file mode 100755 index 2d0413a8..00000000 --- a/theories7/Sets/Permut.v +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Permut.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -(* G. Huet 1-9-95 *) - -(** We consider a Set [U], given with a commutative-associative operator [op], - and a congruence [cong]; we show permutation lemmas *) - -Section Axiomatisation. - -Variable U: Set. - -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 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). - -(** 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)). -Proof. -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))). -Proof. -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)). -Proof. -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)). -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. -Qed. - -Lemma perm_left : (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. -Qed. - -Lemma op_rotate : (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. -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)). -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. -Qed. - -End Axiomatisation. diff --git a/theories7/Sets/Powerset.v b/theories7/Sets/Powerset.v deleted file mode 100755 index b1fa892c..00000000 --- a/theories7/Sets/Powerset.v +++ /dev/null @@ -1,188 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Powerset.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Ensembles. -Require Export Relations_1. -Require Export Relations_1_facts. -Require Export Partial_Order. -Require Export Cpo. - -Section The_power_set_partial_order. -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. - -Theorem Empty_set_minimal: (X: (Ensemble U)) (Included U (Empty_set U) X). -Intro X; Red. -Intros x H'; Elim H'. -Qed. -Hints 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. -Qed. -Hints Resolve Power_set_Inhabited. - -Theorem Inclusion_is_an_order: (Order (Ensemble U) (Included U)). -Auto 6 with sets. -Qed. -Hints Resolve Inclusion_is_an_order. - -Theorem Inclusion_is_transitive: (Transitive (Ensemble U) (Included U)). -Elim Inclusion_is_an_order; Auto with sets. -Qed. -Hints 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. -Defined. -Hints 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. -Qed. -Hints 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. -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. -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. -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. -Qed. -Hints 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. -Qed. -Hints 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. -Qed. - -Theorem Union_increases_l: (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. -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. -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. -Qed. -Hints 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. -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. -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. diff --git a/theories7/Sets/Powerset_Classical_facts.v b/theories7/Sets/Powerset_Classical_facts.v deleted file mode 100755 index 1a51c562..00000000 --- a/theories7/Sets/Powerset_Classical_facts.v +++ /dev/null @@ -1,338 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Powerset_Classical_facts.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Ensembles. -Require Export Constructive_sets. -Require Export Relations_1. -Require Export Relations_1_facts. -Require Export Partial_Order. -Require Export Cpo. -Require Export Powerset. -Require Export Powerset_facts. -Require Export Classical_Type. -Require Export Classical_sets. - -Section Sets_as_an_algebra. - -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). -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. -Qed. - -Lemma incl_soustr_in: - (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. -Qed. -Hints 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)). -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. -Qed. -Hints 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). -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. -Qed. -Hints 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)). -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. -Qed. -Hints 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)). -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. -Qed. - -Lemma add_soustr_1: - (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. -Qed. -Hints 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). -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. -Qed. -Hints 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)). -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. -Qed. - -Lemma Sub_Add_new: - (X: (Ensemble U)) (x: U) ~ (In U X x) -> X == (Subtract U (Add U X x) x). -Proof. -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. -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. -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)). -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. -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). -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. -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). -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. -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))). -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. -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)))). -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. -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. -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. -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. diff --git a/theories7/Sets/Powerset_facts.v b/theories7/Sets/Powerset_facts.v deleted file mode 100755 index fbe7d93e..00000000 --- a/theories7/Sets/Powerset_facts.v +++ /dev/null @@ -1,276 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Powerset_facts.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Ensembles. -Require Export Constructive_sets. -Require Export Relations_1. -Require Export Relations_1_facts. -Require Export Partial_Order. -Require Export Cpo. -Require Export Powerset. - -Section Sets_as_an_algebra. -Variable U: Type. -Hints Unfold not. - -Theorem Empty_set_zero : - (X: (Ensemble U)) (Union U (Empty_set U) X) == X. -Proof. -Auto 6 with sets. -Qed. -Hints Resolve Empty_set_zero. - -Theorem Empty_set_zero' : - (x: U) (Add U (Empty_set U) x) == (Singleton U x). -Proof. -Unfold 1 Add; Auto with sets. -Qed. -Hints Resolve Empty_set_zero'. - -Lemma less_than_empty : - (X: (Ensemble U)) (Included U X (Empty_set U)) -> X == (Empty_set U). -Proof. -Auto with sets. -Qed. -Hints Resolve less_than_empty. - -Theorem Union_commutative : - (A,B: (Ensemble U)) (Union U A B) == (Union U B A). -Proof. -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)). -Proof. -Auto 9 with sets. -Qed. -Hints Resolve Union_associative. - -Theorem Union_idempotent : (A: (Ensemble U)) (Union U A A) == A. -Proof. -Auto 7 with sets. -Qed. - -Lemma Union_absorbs : - (A, B: (Ensemble U)) (Included U B A) -> (Union U A B) == A. -Proof. -Auto 7 with sets. -Qed. - -Theorem Couple_as_union: - (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. -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). -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. -Qed. - -Theorem Triple_as_Couple : (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. -Qed. - -Theorem Triple_as_Couple_Singleton : - (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. -Qed. - -Theorem Intersection_commutative : - (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. -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)). -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. -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)). -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. -Qed. - -Theorem Union_add : - (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. -Qed. -Hints 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. -Qed. - -Theorem Non_disjoint_union' : - (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. -Qed. - -Lemma singlx : (x, y: U) (In U (Add U (Empty_set U) x) y) -> x == y. -Proof. -Intro x; Rewrite (Empty_set_zero' x); Auto with sets. -Qed. -Hints 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)). -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. -Qed. -Hints 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). -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. -Qed. - -Lemma Add_commutative : - (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. -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). -Proof. -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)). -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. -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). -Proof. -Intros; Apply Definition_of_covers; Auto with sets. -Qed. -Hints 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. - - diff --git a/theories7/Sets/Relations_1.v b/theories7/Sets/Relations_1.v deleted file mode 100755 index d4ed823b..00000000 --- a/theories7/Sets/Relations_1.v +++ /dev/null @@ -1,67 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Relations_1.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Section Relations_1. - Variable U: Type. - - Definition Relation := U -> U -> Prop. - Variable R: Relation. - - Definition Reflexive : Prop := (x: U) (R x x). - - Definition Transitive : Prop := (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 Antisymmetric : Prop := - (x: U) (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 same_relation : Relation -> Relation -> Prop := - [R,R': Relation] (contains R R') /\ (contains R' R). - - Inductive Preorder : Prop := - Definition_of_preorder: Reflexive -> Transitive -> Preorder. - - Inductive Order : Prop := - Definition_of_order: Reflexive -> Transitive -> Antisymmetric -> Order. - - Inductive Equivalence : Prop := - Definition_of_equivalence: - Reflexive -> Transitive -> Symmetric -> Equivalence. - - Inductive PER : Prop := - Definition_of_PER: Symmetric -> Transitive -> PER. - -End Relations_1. -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. diff --git a/theories7/Sets/Relations_1_facts.v b/theories7/Sets/Relations_1_facts.v deleted file mode 100755 index cf73ce8b..00000000 --- a/theories7/Sets/Relations_1_facts.v +++ /dev/null @@ -1,109 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Relations_1_facts.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*) - -Require Export Relations_1. - -Definition Complement : (U: Type) (Relation U) -> (Relation U) := - [U: Type] [R: (Relation U)] [x,y: U] ~ (R x y). - -Theorem Rsym_imp_notRsym: (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. -Qed. - -Theorem Equiv_from_preorder : - (U: Type) (R: (Relation U)) (Preorder U R) -> - (Equivalence U [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. -Qed. -Hints 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)). -Proof. -Intros U R H'; Elim H'; Auto 10 with sets. -Qed. -Hints Resolve Equiv_from_order. - -Theorem contains_is_preorder : - (U: Type) (Preorder (Relation U) (contains U)). -Proof. -Auto 10 with sets. -Qed. -Hints Resolve contains_is_preorder. - -Theorem same_relation_is_equivalence : - (U: Type) (Equivalence (Relation U) (same_relation U)). -Proof. -Unfold 1 same_relation; Auto 10 with sets. -Qed. -Hints 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'). -Proof. -Unfold same_relation; Intuition. -Qed. - -Theorem cong_symmetric_same_relation: - (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))). -(*Intuition.*) -Qed. - -Theorem cong_antisymmetric_same_relation: - (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)). -(*Intuition.*) -Qed. - -Theorem cong_transitive_same_relation: - (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. diff --git a/theories7/Sets/Relations_2.v b/theories7/Sets/Relations_2.v deleted file mode 100755 index 92a1236e..00000000 --- a/theories7/Sets/Relations_2.v +++ /dev/null @@ -1,56 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Relations_2.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*) - -Require Export Relations_1. - -Section Relations_2. -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 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 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). - -Definition Strongly_confluent : Prop := - (x, a, b: U) (R x a) -> (R x b) -> (exT U [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. diff --git a/theories7/Sets/Relations_2_facts.v b/theories7/Sets/Relations_2_facts.v deleted file mode 100755 index b82438eb..00000000 --- a/theories7/Sets/Relations_2_facts.v +++ /dev/null @@ -1,151 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Relations_2_facts.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*) - -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)). -Proof. -Auto with sets. -Qed. - -Theorem Rplus_contains_R : - (U: Type) (R: (Relation U)) (contains U (Rplus U R) R). -Proof. -Auto with sets. -Qed. - -Theorem Rstar_contains_R : - (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. -Qed. - -Theorem Rstar_contains_Rplus : - (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. -Qed. - -Theorem Rstar_transitive : - (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. -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)). -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. -Qed. - -Theorem Rstar_equiv_Rstar1 : - (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. -Qed. - -Theorem Rsym_imp_Rstarsym : - (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. -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)). -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. -Qed. - -Theorem star_monotone : - (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. -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)). -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. -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)). -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. diff --git a/theories7/Sets/Relations_3.v b/theories7/Sets/Relations_3.v deleted file mode 100755 index 092fc534..00000000 --- a/theories7/Sets/Relations_3.v +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Relations_3.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*) - -Require Export Relations_1. -Require Export Relations_2. - -Section Relations_3. - 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 locally_confluent : U -> Prop := - [x: U] (y,z: U) (R x y) -> (R x z) -> (coherent y z). - - Definition Locally_confluent : Prop := (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 : Prop := (x: U) (confluent x). - - Inductive noetherian : U -> Prop := - definition_of_noetherian: - (x: U) ((y: U) (R x y) -> (noetherian y)) -> (noetherian x). - - Definition Noetherian : Prop := (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. - - diff --git a/theories7/Sets/Relations_3_facts.v b/theories7/Sets/Relations_3_facts.v deleted file mode 100755 index 822f550a..00000000 --- a/theories7/Sets/Relations_3_facts.v +++ /dev/null @@ -1,157 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Relations_3_facts.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*) - -Require Export Relations_1. -Require Export Relations_1_facts. -Require Export Relations_2. -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). -Proof. -Intros U R x y H'; Red. -Exists y; Auto with sets. -Qed. -Hints Resolve Rstar_imp_coherent. - -Theorem coherent_symmetric : - (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. -Qed. - -Theorem Strong_confluence : - (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. -Qed. - -Theorem Strong_confluence_direct : - (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. -Qed. - -Theorem Noetherian_contains_Noetherian : - (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. -Qed. - -Theorem Newman : - (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. diff --git a/theories7/Sets/Uniset.v b/theories7/Sets/Uniset.v deleted file mode 100644 index 33880214..00000000 --- a/theories7/Sets/Uniset.v +++ /dev/null @@ -1,212 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Uniset.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*) - -(** Sets as characteristic functions *) - -(* G. Huet 1-9-95 *) -(* Updated Papageno 12/98 *) - -Require Bool. - -Set Implicit Arguments. - -Section defs. - -Variable A : Set. -Variable eqA : A -> A -> Prop. -Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}. - -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 Emptyset := (Charac [a:A]false). - -Definition Fullset := (Charac [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 In : uniset -> A -> Prop := - [s:uniset][a:A](charac s a)=true. -Hints Unfold In. - -(** uniset inclusion *) -Definition incl := [s1,s2:uniset] - (a:A)(leb (charac s1 a) (charac s2 a)). -Hints Unfold incl. - -(** uniset equality *) -Definition seq := [s1,s2:uniset] - (a:A)(charac s1 a) = (charac s2 a). -Hints Unfold seq. - -Lemma leb_refl : (b:bool)(leb b b). -Proof. -NewDestruct b; Simpl; Auto. -Qed. -Hints Resolve leb_refl. - -Lemma incl_left : (s1,s2:uniset)(seq s1 s2)->(incl s1 s2). -Proof. -Unfold incl; Intros s1 s2 E a; Elim (E a); Auto. -Qed. - -Lemma incl_right : (s1,s2:uniset)(seq s1 s2)->(incl s2 s1). -Proof. -Unfold incl; Intros s1 s2 E a; Elim (E a); Auto. -Qed. - -Lemma seq_refl : (x:uniset)(seq x x). -Proof. -NewDestruct x; Unfold seq; Auto. -Qed. -Hints Resolve seq_refl. - -Lemma seq_trans : (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. -Qed. - -Lemma seq_sym : (x,y:uniset)(seq x y)->(seq y x). -Proof. -Unfold seq. -NewDestruct x; NewDestruct y; Simpl; Auto. -Qed. - -(** uniset union *) -Definition union := [m1,m2:uniset] - (Charac [a:A](orb (charac m1 a)(charac m2 a))). - -Lemma union_empty_left : - (x:uniset)(seq x (union Emptyset x)). -Proof. -Unfold seq; Unfold union; Simpl; Auto. -Qed. -Hints Resolve union_empty_left. - -Lemma union_empty_right : - (x:uniset)(seq x (union x Emptyset)). -Proof. -Unfold seq; Unfold union; Simpl. -Intros x a; Rewrite (orb_b_false (charac x a)); Auto. -Qed. -Hints Resolve union_empty_right. - -Lemma union_comm : (x,y:uniset)(seq (union x y) (union y x)). -Proof. -Unfold seq; Unfold charac; Unfold union. -NewDestruct x; NewDestruct y; Auto with bool. -Qed. -Hints Resolve union_comm. - -Lemma union_ass : - (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. -Qed. -Hints Resolve union_ass. - -Lemma seq_left : (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. -Qed. -Hints Resolve seq_left. - -Lemma seq_right : (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. -Qed. -Hints Resolve seq_right. - - -(** All the proofs that follow duplicate [Multiset_of_A] *) - -(** Here we should make uniset an abstract datatype, by hiding [Charac], - [union], [charac]; all further properties are proved abstractly *) - -Require Permut. - -Lemma union_rotate : - (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. -Qed. - -Lemma seq_congr : (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. -Qed. - -Lemma union_perm_left : - (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. -Qed. - -Lemma uniset_twist1 : (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. -Qed. - -Lemma uniset_twist2 : (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. -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)). -Proof. -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)). -Proof. -Intros; Apply seq_trans with (union x (union (union y z) t)). -Apply seq_right; Apply seq_left; Trivial. -Apply uniset_twist2. -Qed. - - -(*i theory of minter to do similarly -Require Min. -(* uniset intersection *) -Definition minter := [m1,m2:uniset] - (Charac [a:A](andb (charac m1 a)(charac m2 a))). -i*) - -End defs. - -Unset Implicit Arguments. |