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, 3520 insertions, 0 deletions
diff --git a/theories7/Sets/Classical_sets.v b/theories7/Sets/Classical_sets.v new file mode 100755 index 00000000..a6928ffd --- /dev/null +++ b/theories7/Sets/Classical_sets.v @@ -0,0 +1,133 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..35c88e9d --- /dev/null +++ b/theories7/Sets/Constructive_sets.v @@ -0,0 +1,162 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..2fe46be6 --- /dev/null +++ b/theories7/Sets/Cpo.v @@ -0,0 +1,107 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..c3a044c0 --- /dev/null +++ b/theories7/Sets/Ensembles.v @@ -0,0 +1,108 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..fb53994d --- /dev/null +++ b/theories7/Sets/Finite_sets.v @@ -0,0 +1,74 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..63d4d2ad --- /dev/null +++ b/theories7/Sets/Finite_sets_facts.v @@ -0,0 +1,345 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..0794a3bb --- /dev/null +++ b/theories7/Sets/Image.v @@ -0,0 +1,199 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..bf423753 --- /dev/null +++ b/theories7/Sets/Infinite_sets.v @@ -0,0 +1,232 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..7dee371f --- /dev/null +++ b/theories7/Sets/Integers.v @@ -0,0 +1,166 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..b5d5edf7 --- /dev/null +++ b/theories7/Sets/Multiset.v @@ -0,0 +1,186 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..759cf4e2 --- /dev/null +++ b/theories7/Sets/Partial_Order.v @@ -0,0 +1,100 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..2d0413a8 --- /dev/null +++ b/theories7/Sets/Permut.v @@ -0,0 +1,91 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..b1fa892c --- /dev/null +++ b/theories7/Sets/Powerset.v @@ -0,0 +1,188 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..1a51c562 --- /dev/null +++ b/theories7/Sets/Powerset_Classical_facts.v @@ -0,0 +1,338 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..fbe7d93e --- /dev/null +++ b/theories7/Sets/Powerset_facts.v @@ -0,0 +1,276 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..d4ed823b --- /dev/null +++ b/theories7/Sets/Relations_1.v @@ -0,0 +1,67 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..cf73ce8b --- /dev/null +++ b/theories7/Sets/Relations_1_facts.v @@ -0,0 +1,109 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..92a1236e --- /dev/null +++ b/theories7/Sets/Relations_2.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..b82438eb --- /dev/null +++ b/theories7/Sets/Relations_2_facts.v @@ -0,0 +1,151 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..092fc534 --- /dev/null +++ b/theories7/Sets/Relations_3.v @@ -0,0 +1,63 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..822f550a --- /dev/null +++ b/theories7/Sets/Relations_3_facts.v @@ -0,0 +1,157 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..33880214 --- /dev/null +++ b/theories7/Sets/Uniset.v @@ -0,0 +1,212 @@ +(************************************************************************) +(* 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. |