diff options
Diffstat (limited to 'theories/Sets')
| -rwxr-xr-x | theories/Sets/Classical_sets.v | 132 | ||||
| -rwxr-xr-x | theories/Sets/Constructive_sets.v | 159 | ||||
| -rwxr-xr-x | theories/Sets/Cpo.v | 109 | ||||
| -rwxr-xr-x | theories/Sets/Ensembles.v | 101 | ||||
| -rwxr-xr-x | theories/Sets/Finite_sets.v | 81 | ||||
| -rwxr-xr-x | theories/Sets/Finite_sets_facts.v | 347 | ||||
| -rwxr-xr-x | theories/Sets/Image.v | 205 | ||||
| -rwxr-xr-x | theories/Sets/Infinite_sets.v | 244 | ||||
| -rwxr-xr-x | theories/Sets/Integers.v | 167 | ||||
| -rwxr-xr-x | theories/Sets/Multiset.v | 191 | ||||
| -rwxr-xr-x | theories/Sets/Partial_Order.v | 100 | ||||
| -rwxr-xr-x | theories/Sets/Permut.v | 91 | ||||
| -rwxr-xr-x | theories/Sets/Powerset.v | 190 | ||||
| -rwxr-xr-x | theories/Sets/Powerset_Classical_facts.v | 342 | ||||
| -rwxr-xr-x | theories/Sets/Powerset_facts.v | 268 | ||||
| -rwxr-xr-x | theories/Sets/Relations_1.v | 67 | ||||
| -rwxr-xr-x | theories/Sets/Relations_1_facts.v | 112 | ||||
| -rwxr-xr-x | theories/Sets/Relations_2.v | 56 | ||||
| -rwxr-xr-x | theories/Sets/Relations_2_facts.v | 153 | ||||
| -rwxr-xr-x | theories/Sets/Relations_3.v | 62 | ||||
| -rwxr-xr-x | theories/Sets/Relations_3_facts.v | 171 | ||||
| -rw-r--r-- | theories/Sets/Uniset.v | 215 | ||||
| -rwxr-xr-x | theories/Sets/intro.tex | 24 |
23 files changed, 3587 insertions, 0 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v new file mode 100755 index 00000000..98cb14e4 --- /dev/null +++ b/theories/Sets/Classical_sets.v @@ -0,0 +1,132 @@ +(************************************************************************) +(* 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.4.2.1 2004/07/16 19:31:17 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 : + forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A. +Proof. +intros A NI. +elim (not_all_ex_not U (fun x:U => ~ In U A x)). +intros x H; apply Inhabited_intro with x. +apply NNPP; auto with sets. +red in |- *; intro. +apply NI; red in |- *. +intros x H'; elim (H x); trivial with sets. +Qed. +Hint Resolve not_included_empty_Inhabited. + +Lemma not_empty_Inhabited : + forall A:Ensemble U, A <> Empty_set U -> Inhabited U A. +Proof. +intros; apply not_included_empty_Inhabited. +red in |- *; auto with sets. +Qed. + +Lemma Inhabited_Setminus : + forall X Y:Ensemble U, + Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X). +Proof. +intros X Y I NI. +elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI). +intros x YX. +apply Inhabited_intro with x. +apply Setminus_intro. +apply not_imply_elim with (In U X x); trivial with sets. +auto with sets. +Qed. +Hint Resolve Inhabited_Setminus. + +Lemma Strict_super_set_contains_new_element : + forall X Y:Ensemble U, + Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X). +Proof. +auto 7 with sets. +Qed. +Hint Resolve Strict_super_set_contains_new_element. + +Lemma Subtract_intro : + forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y. +Proof. +unfold Subtract at 1 in |- *; auto with sets. +Qed. +Hint Resolve Subtract_intro. + +Lemma Subtract_inv : + forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y. +Proof. +intros A x y H'; elim H'; auto with sets. +Qed. + +Lemma Included_Strict_Included : + forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y. +Proof. +intros X Y H'; try assumption. +elim (classic (X = Y)); auto with sets. +Qed. + +Lemma Strict_Included_inv : + forall X Y:Ensemble U, + Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X). +Proof. +intros X Y H'; red in H'. +split; [ tauto | idtac ]. +elim H'; intros H'0 H'1; try exact H'1; clear H'. +apply Strict_super_set_contains_new_element; auto with sets. +Qed. + +Lemma not_SIncl_empty : + forall X:Ensemble U, ~ Strict_Included U X (Empty_set U). +Proof. +intro X; red in |- *; intro H'; try exact H'. +lapply (Strict_Included_inv X (Empty_set U)); auto with sets. +intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0. +intros x H'0; elim H'0. +intro H'3; elim H'3. +Qed. + +Lemma Complement_Complement : + forall A:Ensemble U, Complement U (Complement U A) = A. +Proof. +unfold Complement in |- *; intros; apply Extensionality_Ensembles; + auto with sets. +red in |- *; split; auto with sets. +red in |- *; intros; apply NNPP; auto with sets. +Qed. + +End Ensembles_classical. + +Hint Resolve Strict_super_set_contains_new_element Subtract_intro + not_SIncl_empty: sets v62.
\ No newline at end of file diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v new file mode 100755 index 00000000..a2bc781d --- /dev/null +++ b/theories/Sets/Constructive_sets.v @@ -0,0 +1,159 @@ +(************************************************************************) +(* 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.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*) + +Require Export Ensembles. + +Section Ensembles_facts. +Variable U : Type. + +Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C. +Proof. +intros B C H'; rewrite H'; auto with sets. +Qed. + +Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x. +Proof. +red in |- *; destruct 1. +Qed. +Hint Resolve Noone_in_empty. + +Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A. +Proof. +intro; red in |- *. +intros x H; elim (Noone_in_empty x); auto with sets. +Qed. +Hint Resolve Included_Empty. + +Lemma Add_intro1 : + forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y. +Proof. +unfold Add at 1 in |- *; auto with sets. +Qed. +Hint Resolve Add_intro1. + +Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x. +Proof. +unfold Add at 1 in |- *; auto with sets. +Qed. +Hint Resolve Add_intro2. + +Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x). +Proof. +intros A x. +apply Inhabited_intro with (x := x); auto with sets. +Qed. +Hint Resolve Inhabited_add. + +Lemma Inhabited_not_empty : + forall X:Ensemble U, Inhabited U X -> X <> Empty_set U. +Proof. +intros X H'; elim H'. +intros x H'0; red in |- *; intro H'1. +absurd (In U X x); auto with sets. +rewrite H'1; auto with sets. +Qed. +Hint Resolve Inhabited_not_empty. + +Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U. +Proof. +auto with sets. +Qed. +Hint Resolve Add_not_Empty. + +Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x. +Proof. +intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets. +Qed. +Hint Resolve not_Empty_Add. + +Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y. +Proof. +intros x y H'; elim H'; trivial with sets. +Qed. +Hint Resolve Singleton_inv. + +Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y. +Proof. +intros x y H'; rewrite H'; trivial with sets. +Qed. +Hint Resolve Singleton_intro. + +Lemma Union_inv : + forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x. +Proof. +intros B C x H'; elim H'; auto with sets. +Qed. + +Lemma Add_inv : + forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y. +Proof. +intros A x y H'; elim H'; auto with sets. +Qed. + +Lemma Intersection_inv : + forall (B C:Ensemble U) (x:U), + In U (Intersection U B C) x -> In U B x /\ In U C x. +Proof. +intros B C x H'; elim H'; auto with sets. +Qed. +Hint Resolve Intersection_inv. + +Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y. +Proof. +intros x y z H'; elim H'; auto with sets. +Qed. +Hint Resolve Couple_inv. + +Lemma Setminus_intro : + forall (A B:Ensemble U) (x:U), + In U A x -> ~ In U B x -> In U (Setminus U A B) x. +Proof. +unfold Setminus at 1 in |- *; red in |- *; auto with sets. +Qed. +Hint Resolve Setminus_intro. + +Lemma Strict_Included_intro : + forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y. +Proof. +auto with sets. +Qed. +Hint Resolve Strict_Included_intro. + +Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X. +Proof. +intro X; red in |- *; intro H'; elim H'. +intros H'0 H'1; elim H'1; auto with sets. +Qed. +Hint Resolve Strict_Included_strict. + +End Ensembles_facts. + +Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2 + Intersection_inv Couple_inv Setminus_intro Strict_Included_intro + Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty + not_Empty_Add Inhabited_add Included_Empty: sets v62.
\ No newline at end of file diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v new file mode 100755 index 00000000..9fae12f5 --- /dev/null +++ b/theories/Sets/Cpo.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: Cpo.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*) + +Require Export Ensembles. +Require Export Relations_1. +Require Export Partial_Order. + +Section Bounds. +Variable U : Type. +Variable D : PO U. + +Let C := Carrier_of U D. + +Let R := Rel_of U D. + +Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop := + Upper_Bound_definition : + In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x. + +Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop := + Lower_Bound_definition : + In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x. + +Inductive Lub (B:Ensemble U) (x:U) : Prop := + Lub_definition : + Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x. + +Inductive Glb (B:Ensemble U) (x:U) : Prop := + Glb_definition : + Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x. + +Inductive Bottom (bot:U) : Prop := + Bottom_definition : + In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot. + +Inductive Totally_ordered (B:Ensemble U) : Prop := + Totally_ordered_definition : + (Included U B C -> + forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) -> + Totally_ordered B. + +Definition Compatible : Relation U := + fun x y:U => + In U C x -> + In U C y -> exists z : _, In U C z /\ Upper_Bound (Couple U x y) z. + +Inductive Directed (X:Ensemble U) : Prop := + Definition_of_Directed : + Included U X C -> + Inhabited U X -> + (forall x1 x2:U, + Included U (Couple U x1 x2) X -> + exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) -> + Directed X. + +Inductive Complete : Prop := + Definition_of_Complete : + (exists bot : _, Bottom bot) -> + (forall X:Ensemble U, Directed X -> exists bsup : _, Lub X bsup) -> + Complete. + +Inductive Conditionally_complete : Prop := + Definition_of_Conditionally_complete : + (forall X:Ensemble U, + Included U X C -> + (exists maj : _, Upper_Bound X maj) -> + exists bsup : _, Lub X bsup) -> Conditionally_complete. +End Bounds. +Hint Resolve Totally_ordered_definition Upper_Bound_definition + Lower_Bound_definition Lub_definition Glb_definition Bottom_definition + Definition_of_Complete Definition_of_Complete + Definition_of_Conditionally_complete. + +Section Specific_orders. +Variable U : Type. + +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.
\ No newline at end of file diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v new file mode 100755 index 00000000..05afc298 --- /dev/null +++ b/theories/Sets/Ensembles.v @@ -0,0 +1,101 @@ +(************************************************************************) +(* 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.7.2.1 2004/07/16 19:31:17 herbelin Exp $ i*) + +Section Ensembles. +Variable U : Type. + +Definition Ensemble := U -> Prop. + +Definition In (A:Ensemble) (x:U) : Prop := A x. + +Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x. + +Inductive Empty_set : Ensemble :=. + +Inductive Full_set : Ensemble := + Full_intro : forall x:U, In Full_set x. + +(** NB: The following definition builds-in equality of elements in [U] as + Leibniz equality. + + 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 : forall x:U, In B x -> In (Union B C) x + | Union_intror : forall x:U, In C x -> In (Union B C) x. + +Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x). + +Inductive Intersection (B C:Ensemble) : Ensemble := + Intersection_intro : + forall x:U, In B x -> In C x -> In (Intersection B C) x. + +Inductive Couple (x y:U) : Ensemble := + | Couple_l : In (Couple x y) x + | Couple_r : In (Couple x y) y. + +Inductive Triple (x y z:U) : Ensemble := + | Triple_l : In (Triple x y z) x + | Triple_m : In (Triple x y z) y + | Triple_r : In (Triple x y z) z. + +Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x. + +Definition Setminus (B C:Ensemble) : Ensemble := + fun x:U => In B x /\ ~ In C x. + +Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x). + +Inductive Disjoint (B C:Ensemble) : Prop := + Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C. + +Inductive Inhabited (B:Ensemble) : Prop := + Inhabited_intro : forall x:U, In B x -> Inhabited B. + +Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C. + +Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B. + +(** Extensionality Axiom *) + +Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B. +Hint Resolve Extensionality_Ensembles. + +End Ensembles. + +Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets + v62. + +Hint Resolve Union_introl Union_intror Intersection_intro In_singleton + Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro + Extensionality_Ensembles: sets v62.
\ No newline at end of file diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v new file mode 100755 index 00000000..5a2e4397 --- /dev/null +++ b/theories/Sets/Finite_sets.v @@ -0,0 +1,81 @@ +(************************************************************************) +(* 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.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*) + +Require Import Ensembles. + +Section Ensembles_finis. +Variable U : Type. + +Inductive Finite : Ensemble U -> Prop := + | Empty_is_finite : Finite (Empty_set U) + | Union_is_finite : + forall A:Ensemble U, + Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x). + +Inductive cardinal : Ensemble U -> nat -> Prop := + | card_empty : cardinal (Empty_set U) 0 + | card_add : + forall (A:Ensemble U) (n:nat), + cardinal A n -> forall x:U, ~ In U A x -> cardinal (Add U A x) (S n). + +End Ensembles_finis. + +Hint Resolve Empty_is_finite Union_is_finite: sets v62. +Hint Resolve card_empty card_add: sets v62. + +Require Import Constructive_sets. + +Section Ensembles_finis_facts. +Variable U : Type. + +Lemma cardinal_invert : + forall (X:Ensemble U) (p:nat), + cardinal U X p -> + match p with + | O => X = Empty_set U + | S n => + exists A : _, + (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n) + end. +Proof. +induction 1; simpl in |- *; auto. +exists A; exists x; auto. +Qed. + +Lemma cardinal_elim : + forall (X:Ensemble U) (p:nat), + cardinal U X p -> + match p with + | O => X = Empty_set U + | S n => Inhabited U X + end. +Proof. +intros X p C; elim C; simpl in |- *; trivial with sets. +Qed. + +End Ensembles_finis_facts. diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v new file mode 100755 index 00000000..952965e8 --- /dev/null +++ b/theories/Sets/Finite_sets_facts.v @@ -0,0 +1,347 @@ +(************************************************************************) +(* 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.7.2.1 2004/07/16 19:31:17 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 : + forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n. +Proof. +induction 1 as [| A _ [n H]]. +exists 0; auto with sets. +exists (S n); auto with sets. +Qed. + +Lemma cardinal_finite : + forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X. +Proof. +induction 1; auto with sets. +Qed. + +Theorem Add_preserves_Finite : + forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x). +Proof. +intros X x H'. +elim (classic (In U X x)); intro H'0; auto with sets. +rewrite (Non_disjoint_union U X x); auto with sets. +Qed. +Hint Resolve Add_preserves_Finite. + +Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x). +Proof. +intro x; rewrite <- (Empty_set_zero U (Singleton U x)). +change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets. +Qed. +Hint Resolve Singleton_is_finite. + +Theorem Union_preserves_Finite : + forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y). +Proof. +intros X Y H'; elim H'. +rewrite (Empty_set_zero U Y); auto with sets. +intros A H'0 H'1 x H'2 H'3. +rewrite (Union_commutative U (Add U A x) Y). +rewrite <- (Union_add U Y A x). +rewrite (Union_commutative U Y A); auto with sets. +Qed. + +Lemma Finite_downward_closed : + forall A:Ensemble U, + Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X. +Proof. +intros A H'; elim H'; auto with sets. +intros X H'0. +rewrite (less_than_empty U X H'0); auto with sets. +intros; elim Included_Add with U X A0 x; auto with sets. +destruct 1 as [A' [H5 H6]]. +rewrite H5; auto with sets. +Qed. + +Lemma Intersection_preserves_finite : + forall A:Ensemble U, + Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A). +Proof. +intros A H' X; apply Finite_downward_closed with A; auto with sets. +Qed. + +Lemma cardinalO_empty : + forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U. +Proof. +intros X H; apply (cardinal_invert U X 0); trivial with sets. +Qed. +Hint Resolve cardinalO_empty. + +Lemma inh_card_gt_O : + forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0. +Proof. +induction 1 as [x H']. +intros n H'0. +elim (gt_O_eq n); auto with sets. +intro H'1; generalize H'; generalize H'0. +rewrite <- H'1; intro H'2. +rewrite (cardinalO_empty X); auto with sets. +intro H'3; elim H'3. +Qed. + +Lemma card_soustr_1 : + forall (X:Ensemble U) (n:nat), + cardinal U X n -> + forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n). +Proof. +intros X n H'; elim H'. +intros x H'0; elim H'0. +clear H' n X. +intros X n H' H'0 x H'1 x0 H'2. +elim (classic (In U X x0)). +intro H'4; rewrite (add_soustr_xy U X x x0). +elim (classic (x = x0)). +intro H'5. +absurd (In U X x0); auto with sets. +rewrite <- H'5; auto with sets. +intro H'3; try assumption. +cut (S (pred n) = pred (S n)). +intro H'5; rewrite <- H'5. +apply card_add; auto with sets. +red in |- *; intro H'6; elim H'6. +intros H'7 H'8; try assumption. +elim H'1; auto with sets. +unfold pred at 2 in |- *; symmetry in |- *. +apply S_pred with (m := 0). +change (n > 0) in |- *. +apply inh_card_gt_O with (X := X); auto with sets. +apply Inhabited_intro with (x := x0); auto with sets. +red in |- *; intro H'3. +apply H'1. +elim H'3; auto with sets. +rewrite H'3; auto with sets. +elim (classic (x = x0)). +intro H'3; rewrite <- H'3. +cut (Subtract U (Add U X x) x = X); auto with sets. +intro H'4; rewrite H'4; auto with sets. +intros H'3 H'4; try assumption. +absurd (In U (Add U X x) x0); auto with sets. +red in |- *; intro H'5; try exact H'5. +lapply (Add_inv U X x x0); tauto. +Qed. + +Lemma cardinal_is_functional : + forall (X:Ensemble U) (c1:nat), + cardinal U X c1 -> + forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2. +Proof. +intros X c1 H'; elim H'. +intros Y c2 H'0; elim H'0; auto with sets. +intros A n H'1 H'2 x H'3 H'5. +elim (not_Empty_Add U A x); auto with sets. +clear H' c1 X. +intros X n H' H'0 x H'1 Y c2 H'2. +elim H'2. +intro H'3. +elim (not_Empty_Add U X x); auto with sets. +clear H'2 c2 Y. +intros X0 c2 H'2 H'3 x0 H'4 H'5. +elim (classic (In U X0 x)). +intro H'6; apply f_equal with nat. +apply H'0 with (Y := Subtract U (Add U X0 x0) x). +elimtype (pred (S c2) = c2); auto with sets. +apply card_soustr_1; auto with sets. +rewrite <- H'5. +apply Sub_Add_new; auto with sets. +elim (classic (x = x0)). +intros H'6 H'7; apply f_equal with nat. +apply H'0 with (Y := X0); auto with sets. +apply Simplify_add with (x := x); auto with sets. +pattern x at 2 in |- *; rewrite H'6; auto with sets. +intros H'6 H'7. +absurd (Add U X x = Add U X0 x0); auto with sets. +clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2. +red in |- *; intro H'. +lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets. +clear H'. +intro H'; red in H'. +elim H'; intros H'0 H'1; red in H'0; clear H' H'1. +absurd (In U (Add U X0 x0) x); auto with sets. +lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ]. +Qed. + +Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m. +Proof. +intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm). +elim m; auto with sets. +intros; elim H0; intros; elim H1; intros; elim H2; intros. +elim (not_Empty_Add U x x0 H3). +Qed. + +Lemma cardinal_unicity : + forall (X:Ensemble U) (n:nat), + cardinal U X n -> forall m:nat, cardinal U X m -> n = m. +Proof. +intros; apply cardinal_is_functional with X X; auto with sets. +Qed. + +Lemma card_Add_gen : + forall (A:Ensemble U) (x:U) (n n':nat), + cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n. +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 : + forall (X:Ensemble U) (c1:nat), + cardinal U X c1 -> + forall (Y:Ensemble U) (c2:nat), + cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1. +Proof. +intros X c1 H'; elim H'. +intros Y c2 H'0; elim H'0; auto with sets arith. +intro H'1. +elim (Strict_Included_strict U (Empty_set U)); auto with sets arith. +clear H' c1 X. +intros X n H' H'0 x H'1 Y c2 H'2. +elim H'2. +intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith. +clear H'2 c2 Y. +intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)). +intro H'6; apply gt_n_S. +apply H'0 with (Y := Subtract U (Add U X0 x0) x). +elimtype (pred (S c2) = c2); auto with sets arith. +apply card_soustr_1; auto with sets arith. +apply incl_st_add_soustr; auto with sets arith. +elim (classic (x = x0)). +intros H'6 H'7; apply gt_n_S. +apply H'0 with (Y := X0); auto with sets arith. +apply sincl_add_x with (x := x0). +rewrite <- H'6; auto with sets arith. +pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith. +intros H'6 H'7; red in H'5. +elim H'5; intros H'8 H'9; try exact H'8; clear H'5. +red in H'8. +generalize (H'8 x). +intro H'5; lapply H'5; auto with sets arith. +intro H; elim Add_inv with U X0 x0 x; auto with sets arith. +intro; absurd (In U X0 x); auto with sets arith. +intro; absurd (x = x0); auto with sets arith. +Qed. + +Lemma incl_card_le : + forall (X Y:Ensemble U) (n m:nat), + cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m. +Proof. +intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro. +cut (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 : + forall P:Ensemble U -> Prop, + (forall X:Ensemble U, + Finite U X -> + (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) -> + P (Empty_set U). +Proof. +intros P H'; try assumption. +apply H'; auto with sets. +clear H'; auto with sets. +intros Y H'; try assumption. +red in H'. +elim H'; intros H'0 H'1; try exact H'1; clear H'. +lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ]. +elim H'1; auto with sets. +Qed. + +Hint Unfold not. + +Lemma Generalized_induction_on_finite_sets : + forall P:Ensemble U -> Prop, + (forall X:Ensemble U, + Finite U X -> + (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) -> + forall X:Ensemble U, Finite U X -> P X. +Proof. +intros P H'0 X H'1. +generalize P H'0; clear H'0 P. +elim H'1. +intros P H'0. +apply G_aux; auto with sets. +clear H'1 X. +intros A H' H'0 x H'1 P H'3. +cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets. +generalize H'1. +apply H'0. +intros X K H'5 L Y H'6; apply H'3; auto with sets. +apply Finite_downward_closed with (A := Add U X x); auto with sets. +intros Y0 H'7. +elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x)); + auto with sets. +intros H'2 H'4. +elim (Included_Add U Y0 X x); + [ intro H'14 + | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14 + | idtac ]; auto with sets. +elim (Included_Strict_Included U Y0 X); auto with sets. +intro H'9; apply H'5 with (Y := Y0); auto with sets. +intro H'9; rewrite H'9. +apply H'3; auto with sets. +intros Y1 H'8; elim H'8. +intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets. +elim (Included_Strict_Included U A' X); auto with sets. +intro H'8; apply H'5 with (Y := A'); auto with sets. +rewrite <- H'15; auto with sets. +intro H'8. +elim H'7. +intros H'9 H'10; apply H'10 || elim H'10; try assumption. +generalize H'6. +rewrite <- H'8. +rewrite <- H'15; auto with sets. +Qed. + +End Finite_sets_facts.
\ No newline at end of file diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v new file mode 100755 index 00000000..f58f2f81 --- /dev/null +++ b/theories/Sets/Image.v @@ -0,0 +1,205 @@ +(************************************************************************) +(* 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.6.2.1 2004/07/16 19:31:17 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 : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y. + +Lemma Im_def : + forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x). +Proof. +intros X f x H'; try assumption. +apply Im_intro with (x := x); auto with sets. +Qed. +Hint Resolve Im_def. + +Lemma Im_add : + forall (X:Ensemble U) (x:U) (f:U -> V), + Im (Add _ X x) f = Add _ (Im X f) (f x). +Proof. +intros X x f. +apply Extensionality_Ensembles. +split; red in |- *; intros x0 H'. +elim H'; intros. +rewrite H0. +elim Add_inv with U X x x1; auto with sets. +destruct 1; auto with sets. +elim Add_inv with V (Im X f) (f x) x0; auto with sets. +destruct 1 as [x0 H y H0]. +rewrite H0; auto with sets. +destruct 1; auto with sets. +Qed. + +Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V. +Proof. +intro f; try assumption. +apply Extensionality_Ensembles. +split; auto with sets. +red in |- *. +intros x H'; elim H'. +intros x0 H'0; elim H'0; auto with sets. +Qed. +Hint Resolve image_empty. + +Lemma finite_image : + forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f). +Proof. +intros X f H'; elim H'. +rewrite (image_empty f); auto with sets. +intros A H'0 H'1 x H'2; clear H' X. +rewrite (Im_add A x f); auto with sets. +apply Add_preserves_Finite; auto with sets. +Qed. +Hint Resolve finite_image. + +Lemma Im_inv : + forall (X:Ensemble U) (f:U -> V) (y:V), + In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y. +Proof. +intros X f y H'; elim H'. +intros x H'0 y0 H'1; rewrite H'1. +exists x; auto with sets. +Qed. + +Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y. + +Lemma not_injective_elim : + forall f:U -> V, + ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y). +Proof. +unfold injective in |- *; intros f H. +cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)). +2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y); + trivial with sets. +destruct 1 as [x C]; exists x. +cut (exists y : _, ~ (f x = f y -> x = y)). +2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y); + trivial with sets. +destruct 1 as [y D]; exists y. +apply imply_to_and; trivial with sets. +Qed. + +Lemma cardinal_Im_intro : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p. +Proof. +intros. +apply finite_cardinal; apply finite_image. +apply cardinal_finite with n; trivial with sets. +Qed. + +Lemma In_Image_elim : + forall (A:Ensemble U) (f:U -> V), + injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x. +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 : + forall (A:Ensemble U) (f:U -> V) (n:nat), + injective f -> + cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n. +Proof. +induction 2 as [| A n H'0 H'1 x H'2]; auto with sets. +rewrite (image_empty f). +intros n' CE. +apply cardinal_unicity with V (Empty_set V); auto with sets. +intro n'. +rewrite (Im_add A x f). +intro H'3. +elim cardinal_Im_intro with A f n; trivial with sets. +intros i CI. +lapply (H'1 i); trivial with sets. +cut (~ In _ (Im A f) (f x)). +intros H0 H1. +apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets. +apply card_add; auto with sets. +rewrite <- H1; trivial with sets. +red in |- *; intro; apply H'2. +apply In_Image_elim with f; trivial with sets. +Qed. + +Lemma cardinal_decreases : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n. +Proof. +induction 1 as [| A n H'0 H'1 x H'2]; auto with sets. +rewrite (image_empty f); intros. +cut (n' = 0). +intro E; rewrite E; trivial with sets. +apply cardinal_unicity with V (Empty_set V); auto with sets. +intro n'. +rewrite (Im_add A x f). +elim cardinal_Im_intro with A f n; trivial with sets. +intros p C H'3. +apply le_trans with (S p). +apply card_Add_gen with V (Im A f) (f x); trivial with sets. +apply le_n_S; auto with sets. +Qed. + +Theorem Pigeonhole : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal U A n -> + forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f. +Proof. +unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I. +cut (n' = n). +intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n). +apply injective_preserves_cardinal with (A := A) (f := f) (n := n); + trivial with sets. +Qed. + +Lemma Pigeonhole_principle : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal _ A n -> + forall n':nat, + cardinal _ (Im A f) n' -> + n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y). +Proof. +intros; apply not_injective_elim. +apply Pigeonhole with A n n'; trivial with sets. +Qed. +End Image. +Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v new file mode 100755 index 00000000..c357e26c --- /dev/null +++ b/theories/Sets/Infinite_sets.v @@ -0,0 +1,244 @@ +(************************************************************************) +(* 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.5.2.1 2004/07/16 19:31:17 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. + +Hint Resolve Defn_of_Approximant. + +Section Infinite_sets. +Variable U : Type. + +Lemma make_new_approximant : + forall A X:Ensemble U, + ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X). +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 in |- *; intro H'3; apply H'. +rewrite <- H'3; auto with sets. +Qed. + +Lemma approximants_grow : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, + cardinal U X n -> + Included U X A -> exists Y : _, cardinal U Y (S n) /\ Included U Y A. +Proof. +intros A X H' n H'0; elim H'0; auto with sets. +intro H'1. +cut (Inhabited U (Setminus U A (Empty_set U))). +intro H'2; elim H'2. +intros x H'3. +exists (Add U (Empty_set U) x); auto with sets. +split. +apply card_add; auto with sets. +cut (In U A x). +intro H'4; red in |- *; auto with sets. +intros x0 H'5; elim H'5; auto with sets. +intros x1 H'6; elim H'6; auto with sets. +elim H'3; auto with sets. +apply make_new_approximant; auto with sets. +intros A0 n0 H'1 H'2 x H'3 H'5. +lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets. +intros x0 H'2; try assumption. +elim H'2; intros H'7 H'8; try exact H'8; clear H'2. +elim (make_new_approximant A x0); auto with sets. +intros x1 H'2; try assumption. +exists (Add U x0 x1); auto with sets. +split. +apply card_add; auto with sets. +elim H'2; auto with sets. +red in |- *. +intros x2 H'9; elim H'9; auto with sets. +intros x3 H'10; elim H'10; auto with sets. +elim H'2; auto with sets. +auto with sets. +apply Defn_of_Approximant; auto with sets. +apply cardinal_finite with (n := S n0); auto with sets. +Qed. + +Lemma approximants_grow' : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, + cardinal U X n -> + Approximant U A X -> + exists Y : _, cardinal U Y (S n) /\ Approximant U A Y. +Proof. +intros A X H' n H'0 H'1; try assumption. +elim H'1. +intros H'2 H'3. +elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A). +intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4. +exists x; auto with sets. +split; [ auto with sets | idtac ]. +apply Defn_of_Approximant; auto with sets. +apply cardinal_finite with (n := S n); auto with sets. +apply approximants_grow with (X := X); auto with sets. +Qed. + +Lemma approximant_can_be_any_size : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, exists Y : _, cardinal U Y n /\ Approximant U A Y. +Proof. +intros A H' H'0 n; elim n. +exists (Empty_set U); auto with sets. +intros n0 H'1; elim H'1. +intros x H'2. +apply approximants_grow' with (X := x); tauto. +Qed. + +Variable V : Type. + +Theorem Image_set_continuous : + forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), + Finite V X -> + Included V X (Im U V A f) -> + exists n : _, + (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X). +Proof. +intros A f X H'; elim H'. +intro H'0; exists 0. +exists (Empty_set U); auto with sets. +intros A0 H'0 H'1 x H'2 H'3; try assumption. +lapply H'1; + [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ]; + auto with sets. +intros x0 H'1; try assumption. +exists (S n); try assumption. +elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6; + clear H'4 H'1. +clear E. +generalize H'2. +rewrite <- H'5. +intro H'1; try assumption. +red in H'3. +generalize (H'3 x). +intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ]; + auto with sets. +specialize 5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x); + intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ]; + auto with sets. +intros x1 H'4; try assumption. +apply ex_intro with (x := Add U x0 x1). +split; [ split; [ try assumption | idtac ] | idtac ]. +apply card_add; auto with sets. +red in |- *; intro H'9; try exact H'9. +apply H'1. +elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets. +elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets. +red in |- *; auto with sets. +intros x2 H'4; elim H'4; auto with sets. +intros x3 H'11; elim H'11; auto with sets. +elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets. +apply Im_add; auto with sets. +Qed. + +Theorem Image_set_continuous' : + forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), + Approximant V (Im U V A f) X -> + exists Y : _, Approximant U A Y /\ Im U V Y f = X. +Proof. +intros A f X H'; try assumption. +cut + (exists n : _, + (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)). +intro H'0; elim H'0; intros n E; elim E; clear H'0. +intros x H'0; try assumption. +elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3; + clear H'1 H'0; auto with sets. +exists x. +split; [ idtac | try assumption ]. +apply Defn_of_Approximant; auto with sets. +apply cardinal_finite with (n := n); auto with sets. +apply Image_set_continuous; auto with sets. +elim H'; auto with sets. +elim H'; auto with sets. +Qed. + +Theorem Pigeonhole_bis : + forall (A:Ensemble U) (f:U -> V), + ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f. +Proof. +intros A f H'0 H'1; try assumption. +elim (Image_set_continuous' A f (Im U V A f)); auto with sets. +intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2. +elim (make_new_approximant A x); auto with sets. +intros x0 H'2; elim H'2. +intros H'5 H'6. +elim (finite_cardinal V (Im U V A f)); auto with sets. +intros n E. +elim (finite_cardinal U x); auto with sets. +intros n0 E0. +apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n). +apply card_add; auto with sets. +rewrite (Im_add U V x x0 f); auto with sets. +cut (In V (Im U V x f) (f x0)). +intro H'8. +rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets. +rewrite H'4; auto with sets. +elim (Extension V (Im U V x f) (Im U V A f)); auto with sets. +apply le_lt_n_Sm. +apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f); + auto with sets. +rewrite H'4; auto with sets. +elim H'3; auto with sets. +Qed. + +Theorem Pigeonhole_ter : + forall (A:Ensemble U) (f:U -> V) (n:nat), + injective U V f -> Finite V (Im U V A f) -> Finite U A. +Proof. +intros A f H' H'0 H'1. +apply NNPP. +red in |- *; intro H'2. +elim (Pigeonhole_bis A f); auto with sets. +Qed. + +End Infinite_sets. diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v new file mode 100755 index 00000000..26f29c96 --- /dev/null +++ b/theories/Sets/Integers.v @@ -0,0 +1,167 @@ +(************************************************************************) +(* 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.6.2.1 2004/07/16 19:31:17 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 : forall x:nat, In nat Integers x. +Hint Resolve Integers_defn. + +Lemma le_reflexive : Reflexive nat le. +Proof. +red in |- *; auto with arith. +Qed. + +Lemma le_antisym : Antisymmetric nat le. +Proof. +red in |- *; intros x y H H'; rewrite (le_antisym x y); auto. +Qed. + +Lemma le_trans : Transitive nat le. +Proof. +red in |- *; intros; apply le_trans with y; auto. +Qed. +Hint Resolve le_reflexive le_antisym le_trans. + +Lemma le_Order : Order nat le. +Proof. +auto with sets arith. +Qed. +Hint Resolve le_Order. + +Lemma triv_nat : forall n:nat, In nat Integers n. +Proof. +auto with sets arith. +Qed. +Hint Resolve triv_nat. + +Definition nat_po : PO nat. +apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le); + auto with sets arith. +apply Inhabited_intro with (x := 0); auto with sets arith. +Defined. +Hint Unfold nat_po. + +Lemma le_total_order : Totally_ordered nat nat_po Integers. +Proof. +apply Totally_ordered_definition. +simpl in |- *. +intros H' x y H'0. +specialize 2le_or_lt with (n := x) (m := y); intro H'2; elim H'2. +intro H'1; left; auto with sets arith. +intro H'1; right. +cut (y <= x); auto with sets arith. +Qed. +Hint Resolve le_total_order. + +Lemma Finite_subset_has_lub : + forall X:Ensemble nat, + Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m. +Proof. +intros X H'; elim H'. +exists 0. +apply Upper_Bound_definition; auto with sets arith. +intros y H'0; elim H'0; auto with sets arith. +intros A H'0 H'1 x H'2; try assumption. +elim H'1; intros x0 H'3; clear H'1. +elim le_total_order. +simpl in |- *. +intro H'1; try assumption. +lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith. +generalize (H'4 x0 x). +clear H'4. +clear H'1. +intro H'1; lapply H'1; + [ intro H'4; elim H'4; + [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ] + | clear H'1 ]. +exists x. +apply Upper_Bound_definition; auto with sets arith; simpl in |- *. +intros y H'1; elim H'1. +generalize le_trans. +intro H'4; red in H'4. +intros x1 H'6; try assumption. +apply H'4 with (y := x0); auto with sets arith. +elim H'3; simpl in |- *; auto with sets arith. +intros x1 H'4; elim H'4; auto with sets arith. +exists x0. +apply Upper_Bound_definition; auto with sets arith; simpl in |- *. +intros y H'1; elim H'1. +intros x1 H'4; try assumption. +elim H'3; simpl in |- *; auto with sets arith. +intros x1 H'4; elim H'4; auto with sets arith. +red in |- *. +intros x1 H'1; elim H'1; auto with sets arith. +Qed. + +Lemma Integers_has_no_ub : + ~ (exists m : nat, Upper_Bound nat nat_po Integers m). +Proof. +red in |- *; intro H'; elim H'. +intros x H'0. +elim H'0; intros H'1 H'2. +cut (In nat Integers (S x)). +intro H'3. +specialize 1H'2 with (y := S x); intro H'4; lapply H'4; + [ intro H'5; clear H'4 | try assumption; clear H'4 ]. +simpl in H'5. +absurd (S x <= x); auto with arith. +auto with sets arith. +Qed. + +Lemma Integers_infinite : ~ Finite nat Integers. +Proof. +generalize Integers_has_no_ub. +intro H'; red in |- *; intro H'0; try exact H'0. +apply H'. +apply Finite_subset_has_lub; auto with sets arith. +Qed. + +End Integers_sect. + + + + diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v new file mode 100755 index 00000000..a308282b --- /dev/null +++ b/theories/Sets/Multiset.v @@ -0,0 +1,191 @@ +(************************************************************************) +(* 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.9.2.1 2004/07/16 19:31:17 herbelin Exp $ i*) + +(* G. Huet 1-9-95 *) + +Require Import Permut. + +Set Implicit Arguments. + +Section multiset_defs. + +Variable A : Set. +Variable eqA : A -> A -> Prop. +Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. + +Inductive multiset : Set := + Bag : (A -> nat) -> multiset. + +Definition EmptyBag := Bag (fun a:A => 0). +Definition SingletonBag (a:A) := + Bag (fun a':A => match Aeq_dec a a' with + | left _ => 1 + | right _ => 0 + end). + +Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a. + +(** multiset equality *) +Definition meq (m1 m2:multiset) := + forall a:A, multiplicity m1 a = multiplicity m2 a. + +Hint Unfold meq multiplicity. + +Lemma meq_refl : forall x:multiset, meq x x. +Proof. +destruct x; auto. +Qed. +Hint Resolve meq_refl. + +Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z. +Proof. +unfold meq in |- *. +destruct x; destruct y; destruct z. +intros; rewrite H; auto. +Qed. + +Lemma meq_sym : forall x y:multiset, meq x y -> meq y x. +Proof. +unfold meq in |- *. +destruct x; destruct y; auto. +Qed. +Hint Immediate meq_sym. + +(** multiset union *) +Definition munion (m1 m2:multiset) := + Bag (fun a:A => multiplicity m1 a + multiplicity m2 a). + +Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x). +Proof. +unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. +Qed. +Hint Resolve munion_empty_left. + +Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag). +Proof. +unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. +Qed. + + +Require Import Plus. (* comm. and ass. of plus *) + +Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). +Proof. +unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *. +destruct x; destruct y; auto with arith. +Qed. +Hint Resolve munion_comm. + +Lemma munion_ass : + forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)). +Proof. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z; auto with arith. +Qed. +Hint Resolve munion_ass. + +Lemma meq_left : + forall x y z:multiset, meq x y -> meq (munion x z) (munion y z). +Proof. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto with arith. +Qed. +Hint Resolve meq_left. + +Lemma meq_right : + forall x y z:multiset, meq x y -> meq (munion z x) (munion z y). +Proof. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto. +Qed. +Hint Resolve meq_right. + + +(** Here we should make multiset an abstract datatype, by hiding [Bag], + [munion], [multiplicity]; all further properties are proved abstractly *) + +Lemma munion_rotate : + forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)). +Proof. +intros; apply (op_rotate multiset munion meq); auto. +exact meq_trans. +Qed. + +Lemma meq_congr : + forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t). +Proof. +intros; apply (cong_congr multiset munion meq); auto. +exact meq_trans. +Qed. + +Lemma munion_perm_left : + forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)). +Proof. +intros; apply (perm_left multiset munion meq); auto. +exact meq_trans. +Qed. + +Lemma multiset_twist1 : + forall x y z t:multiset, + meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z). +Proof. +intros; apply (twist multiset munion meq); auto. +exact meq_trans. +Qed. + +Lemma multiset_twist2 : + forall x y z t:multiset, + meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t). +Proof. +intros; apply meq_trans with (munion (munion x (munion y z)) t). +apply meq_sym; apply munion_ass. +apply meq_left; apply munion_perm_left. +Qed. + +(** specific for treesort *) + +Lemma treesort_twist1 : + forall x y z t u:multiset, + meq u (munion y z) -> + meq (munion x (munion u t)) (munion (munion y (munion x t)) z). +Proof. +intros; apply meq_trans with (munion x (munion (munion y z) t)). +apply meq_right; apply meq_left; trivial. +apply multiset_twist1. +Qed. + +Lemma treesort_twist2 : + forall x y z t u:multiset, + meq u (munion y z) -> + meq (munion x (munion u t)) (munion (munion y (munion x z)) t). +Proof. +intros; apply meq_trans with (munion x (munion (munion y z) t)). +apply meq_right; apply meq_left; trivial. +apply multiset_twist2. +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. + +Hint Unfold meq multiplicity: v62 datatypes. +Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right + munion_empty_left: v62 datatypes. +Hint Immediate meq_sym: v62 datatypes.
\ No newline at end of file diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v new file mode 100755 index 00000000..b3e59886 --- /dev/null +++ b/theories/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.6.2.1 2004/07/16 19:31:18 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 := fun x y:U => Rel_of p x y /\ x <> y. + +Inductive covers (y x:U) : Prop := + Definition_of_covers : + Strict_Rel_of x y -> + ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) -> + covers y x. + +End Partial_orders. + +Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62. +Hint Resolve Definition_of_covers: sets v62. + + +Section Partial_order_facts. +Variable U : Type. +Variable D : PO U. + +Lemma Strict_Rel_Transitive_with_Rel : + forall x y z:U, + Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z. +unfold Strict_Rel_of at 1 in |- *. +red in |- *. +elim D; simpl in |- *. +intros C R H' H'0; elim H'0. +intros H'1 H'2 H'3 x y z H'4 H'5; split. +apply H'2 with (y := y); tauto. +red in |- *; intro H'6. +elim H'4; intros H'7 H'8; apply H'8; clear H'4. +apply H'3; auto. +rewrite H'6; tauto. +Qed. + +Lemma Strict_Rel_Transitive_with_Rel_left : + forall x y z:U, + Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z. +unfold Strict_Rel_of at 1 in |- *. +red in |- *. +elim D; simpl in |- *. +intros C R H' H'0; elim H'0. +intros H'1 H'2 H'3 x y z H'4 H'5; split. +apply H'2 with (y := y); tauto. +red in |- *; intro H'6. +elim H'5; intros H'7 H'8; apply H'8; clear H'5. +apply H'3; auto. +rewrite <- H'6; auto. +Qed. + +Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D). +red in |- *. +intros x y z H' H'0. +apply Strict_Rel_Transitive_with_Rel with (y := y); + [ intuition | unfold Strict_Rel_of in H', H'0; intuition ]. +Qed. +End Partial_order_facts.
\ No newline at end of file diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v new file mode 100755 index 00000000..af6151bf --- /dev/null +++ b/theories/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.6.2.1 2004/07/16 19:31:18 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 : forall x y:U, cong (op x y) (op y x). +Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)). + +Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z). +Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y). +Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z. +Hypothesis cong_sym : forall x y:U, cong x y -> cong y x. + +(** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *) + +Lemma cong_congr : + forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t). +Proof. +intros; apply cong_trans with (op y z). +apply cong_left; trivial. +apply cong_right; trivial. +Qed. + +Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)). +Proof. +intros; apply cong_right; apply op_comm. +Qed. + +Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z). +Proof. +intros; apply cong_left; apply op_comm. +Qed. + +Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y). +Proof. +intros. +apply cong_trans with (op x (op y z)). +apply op_ass. +apply cong_trans with (op x (op z y)). +apply cong_right; apply op_comm. +apply cong_sym; apply op_ass. +Qed. + +Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)). +Proof. +intros. +apply cong_trans with (op (op x y) z). +apply cong_sym; apply op_ass. +apply cong_trans with (op (op y x) z). +apply cong_left; apply op_comm. +apply op_ass. +Qed. + +Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)). +Proof. +intros; apply cong_trans with (op (op x y) z). +apply cong_sym; apply op_ass. +apply op_comm. +Qed. + +(* Needed for treesort ... *) +Lemma twist : + forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z). +Proof. +intros. +apply cong_trans with (op x (op (op y t) z)). +apply cong_right; apply perm_right. +apply cong_trans with (op (op x (op y t)) z). +apply cong_sym; apply op_ass. +apply cong_left; apply perm_left. +Qed. + +End Axiomatisation.
\ No newline at end of file diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v new file mode 100755 index 00000000..a7f5e9f4 --- /dev/null +++ b/theories/Sets/Powerset.v @@ -0,0 +1,190 @@ +(************************************************************************) +(* 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.5.2.1 2004/07/16 19:31:18 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 : + forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X. +Hint Resolve Definition_of_Power_set. + +Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X. +intro X; red in |- *. +intros x H'; elim H'. +Qed. +Hint Resolve Empty_set_minimal. + +Theorem Power_set_Inhabited : + forall X:Ensemble U, Inhabited (Ensemble U) (Power_set X). +intro X. +apply Inhabited_intro with (Empty_set U); auto with sets. +Qed. +Hint Resolve Power_set_Inhabited. + +Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U). +auto 6 with sets. +Qed. +Hint Resolve Inclusion_is_an_order. + +Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U). +elim Inclusion_is_an_order; auto with sets. +Qed. +Hint Resolve Inclusion_is_transitive. + +Definition Power_set_PO : Ensemble U -> PO (Ensemble U). +intro A; try assumption. +apply Definition_of_PO with (Power_set A) (Included U); auto with sets. +Defined. +Hint Unfold Power_set_PO. + +Theorem Strict_Rel_is_Strict_Included : + same_relation (Ensemble U) (Strict_Included U) + (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))). +auto with sets. +Qed. +Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included. + +Lemma Strict_inclusion_is_transitive_with_inclusion : + forall x y z:Ensemble U, + Strict_Included U x y -> Included U y z -> Strict_Included U x z. +intros x y z H' H'0; try assumption. +elim Strict_Rel_is_Strict_Included. +unfold contains in |- *. +intros H'1 H'2; try assumption. +apply H'1. +apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets. +Qed. + +Lemma Strict_inclusion_is_transitive_with_inclusion_left : + forall x y z:Ensemble U, + Included U x y -> Strict_Included U y z -> Strict_Included U x z. +intros x y z H' H'0; try assumption. +elim Strict_Rel_is_Strict_Included. +unfold contains in |- *. +intros H'1 H'2; try assumption. +apply H'1. +apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets. +Qed. + +Lemma Strict_inclusion_is_transitive : + Transitive (Ensemble U) (Strict_Included U). +apply cong_transitive_same_relation with + (R := Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))); + auto with sets. +Qed. + +Theorem Empty_set_is_Bottom : + forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U). +intro A; apply Bottom_definition; simpl in |- *; auto with sets. +Qed. +Hint Resolve Empty_set_is_Bottom. + +Theorem Union_minimal : + forall a b X:Ensemble U, + Included U a X -> Included U b X -> Included U (Union U a b) X. +intros a b X H' H'0; red in |- *. +intros x H'1; elim H'1; auto with sets. +Qed. +Hint Resolve Union_minimal. + +Theorem Intersection_maximal : + forall a b X:Ensemble U, + Included U X a -> Included U X b -> Included U X (Intersection U a b). +auto with sets. +Qed. + +Theorem Union_increases_l : forall a b:Ensemble U, Included U a (Union U a b). +auto with sets. +Qed. + +Theorem Union_increases_r : forall a b:Ensemble U, Included U b (Union U a b). +auto with sets. +Qed. + +Theorem Intersection_decreases_l : + forall a b:Ensemble U, Included U (Intersection U a b) a. +intros a b; red in |- *. +intros x H'; elim H'; auto with sets. +Qed. + +Theorem Intersection_decreases_r : + forall a b:Ensemble U, Included U (Intersection U a b) b. +intros a b; red in |- *. +intros x H'; elim H'; auto with sets. +Qed. +Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l + Intersection_decreases_r. + +Theorem Union_is_Lub : + forall A a b:Ensemble U, + Included U a A -> + Included U b A -> + Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b). +intros A a b H' H'0. +apply Lub_definition; simpl in |- *. +apply Upper_Bound_definition; simpl in |- *; auto with sets. +intros y H'1; elim H'1; auto with sets. +intros y H'1; elim H'1; simpl in |- *; auto with sets. +Qed. + +Theorem Intersection_is_Glb : + forall A a b:Ensemble U, + Included U a A -> + Included U b A -> + Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) + (Intersection U a b). +intros A a b H' H'0. +apply Glb_definition; simpl in |- *. +apply Lower_Bound_definition; simpl in |- *; auto with sets. +apply Definition_of_Power_set. +generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a; + auto with sets. +intros y H'1; elim H'1; auto with sets. +intros y H'1; elim H'1; simpl in |- *; auto with sets. +Qed. + +End The_power_set_partial_order. + +Hint Resolve Empty_set_minimal: sets v62. +Hint Resolve Power_set_Inhabited: sets v62. +Hint Resolve Inclusion_is_an_order: sets v62. +Hint Resolve Inclusion_is_transitive: sets v62. +Hint Resolve Union_minimal: sets v62. +Hint Resolve Union_increases_l: sets v62. +Hint Resolve Union_increases_r: sets v62. +Hint Resolve Intersection_decreases_l: sets v62. +Hint Resolve Intersection_decreases_r: sets v62. +Hint Resolve Empty_set_is_Bottom: sets v62. +Hint Resolve Strict_inclusion_is_transitive: sets v62.
\ No newline at end of file diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v new file mode 100755 index 00000000..05c60def --- /dev/null +++ b/theories/Sets/Powerset_Classical_facts.v @@ -0,0 +1,342 @@ +(************************************************************************) +(* 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.5.2.1 2004/07/16 19:31:18 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 : + forall (A B:Ensemble U) (x:U), + ~ In U A x -> + Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B. +Proof. +intros A B x H' H'0; red in |- *. +lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets. +clear H'0; intro H'0; split. +apply incl_add_x with (x := x); tauto. +elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2. +intros x0 H'0. +red in |- *; intro H'2. +elim H'0; clear H'0. +rewrite <- H'2; auto with sets. +Qed. + +Lemma incl_soustr_in : + forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X. +Proof. +intros X x H'; red in |- *. +intros x0 H'0; elim H'0; auto with sets. +Qed. +Hint Resolve incl_soustr_in: sets v62. + +Lemma incl_soustr : + forall (X Y:Ensemble U) (x:U), + Included U X Y -> Included U (Subtract U X x) (Subtract U Y x). +Proof. +intros X Y x H'; red in |- *. +intros x0 H'0; elim H'0. +intros H'1 H'2. +apply Subtract_intro; auto with sets. +Qed. +Hint Resolve incl_soustr: sets v62. + + +Lemma incl_soustr_add_l : + forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X. +Proof. +intros X x; red in |- *. +intros x0 H'; elim H'; auto with sets. +intro H'0; elim H'0; auto with sets. +intros t H'1 H'2; elim H'2; auto with sets. +Qed. +Hint Resolve incl_soustr_add_l: sets v62. + +Lemma incl_soustr_add_r : + forall (X:Ensemble U) (x:U), + ~ In U X x -> Included U X (Subtract U (Add U X x) x). +Proof. +intros X x H'; red in |- *. +intros x0 H'0; try assumption. +apply Subtract_intro; auto with sets. +red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets. +Qed. +Hint Resolve incl_soustr_add_r: sets v62. + +Lemma add_soustr_2 : + forall (X:Ensemble U) (x:U), + In U X x -> Included U X (Add U (Subtract U X x) x). +Proof. +intros X x H'; red in |- *. +intros x0 H'0; try assumption. +elim (classic (x = x0)); intro K; auto with sets. +elim K; auto with sets. +Qed. + +Lemma add_soustr_1 : + forall (X:Ensemble U) (x:U), + In U X x -> Included U (Add U (Subtract U X x) x) X. +Proof. +intros X x H'; red in |- *. +intros x0 H'0; elim H'0; auto with sets. +intros y H'1; elim H'1; auto with sets. +intros t H'1; try assumption. +rewrite <- (Singleton_inv U x t); auto with sets. +Qed. +Hint Resolve add_soustr_1 add_soustr_2: sets v62. + +Lemma add_soustr_xy : + forall (X:Ensemble U) (x y:U), + x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x. +Proof. +intros X x y H'; apply Extensionality_Ensembles. +split; red in |- *. +intros x0 H'0; elim H'0; auto with sets. +intro H'1; elim H'1. +intros u H'2 H'3; try assumption. +apply Add_intro1. +apply Subtract_intro; auto with sets. +intros t H'2 H'3; try assumption. +elim (Singleton_inv U x t); auto with sets. +intros u H'2; try assumption. +elim (Add_inv U (Subtract U X y) x u); auto with sets. +intro H'0; elim H'0; auto with sets. +intro H'0; rewrite <- H'0; auto with sets. +Qed. +Hint Resolve add_soustr_xy: sets v62. + +Lemma incl_st_add_soustr : + forall (X Y:Ensemble U) (x:U), + ~ In U X x -> + Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x). +Proof. +intros X Y x H' H'0; apply sincl_add_x with (x := x); auto with sets. +split. +elim H'0. +intros H'1 H'2. +generalize (Inclusion_is_transitive U). +intro H'4; red in H'4. +apply H'4 with (y := Y); auto with sets. +red in H'0. +elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *) +red in |- *; intro H'0; apply H'2. +rewrite H'0; auto 8 with sets. +Qed. + +Lemma Sub_Add_new : + forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x. +Proof. +auto with sets. +Qed. + +Lemma Simplify_add : + forall (X X0:Ensemble U) (x:U), + ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0. +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 : + forall (X A:Ensemble U) (x:U), + Included U X (Add U A x) -> + Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A). +Proof. +intros X A x H'0; try assumption. +elim (classic (In U X x)). +intro H'1; right; try assumption. +exists (Subtract U X x). +split; auto with sets. +red in H'0. +red in |- *. +intros x0 H'2; try assumption. +lapply (Subtract_inv U X x x0); auto with sets. +intro H'3; elim H'3; intros K K'; clear H'3. +lapply (H'0 x0); auto with sets. +intro H'3; try assumption. +lapply (Add_inv U A x x0); auto with sets. +intro H'4; elim H'4; + [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ]. +elim K'; auto with sets. +intro H'1; left; try assumption. +red in H'0. +red in |- *. +intros x0 H'2; try assumption. +lapply (H'0 x0); auto with sets. +intro H'3; try assumption. +lapply (Add_inv U A x x0); auto with sets. +intro H'4; elim H'4; + [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ]. +absurd (In U X x0); auto with sets. +rewrite <- H'5; auto with sets. +Qed. + +Lemma setcover_inv : + forall A x y:Ensemble U, + covers (Ensemble U) (Power_set_PO U A) y x -> + Strict_Included U x y /\ + (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y). +Proof. +intros A x y H'; elim H'. +unfold Strict_Rel_of in |- *; simpl in |- *. +intros H'0 H'1; split; [ auto with sets | idtac ]. +intros z H'2 H'3; try assumption. +elim (classic (x = z)); auto with sets. +intro H'4; right; try assumption. +elim (classic (z = y)); auto with sets. +intro H'5; try assumption. +elim H'1. +exists z; auto with sets. +Qed. + +Theorem Add_covers : + forall A a:Ensemble U, + Included U a A -> + forall x:U, + In U A x -> + ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a. +Proof. +intros A a H' x H'0 H'1; try assumption. +apply setcover_intro; auto with sets. +red in |- *. +split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets. +apply H'1. +rewrite H'2; auto with sets. +red in |- *; intro H'2; elim H'2; clear H'2. +intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2. +lapply (Strict_Included_inv U a z); auto with sets; clear H'3. +intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5. +intros x0 H'2; elim H'2. +intros H'5 H'6; try assumption. +generalize H'4; intro K. +red in H'4. +elim H'4; intros H'8 H'9; red in H'8; clear H'4. +lapply (H'8 x0); auto with sets. +intro H'7; try assumption. +elim (Add_inv U a x x0); auto with sets. +intro H'15. +cut (Included U (Add U a x) z). +intro H'10; try assumption. +red in K. +elim K; intros H'11 H'12; apply H'12; clear K; auto with sets. +rewrite H'15. +red in |- *. +intros x1 H'10; elim H'10; auto with sets. +intros x2 H'11; elim H'11; auto with sets. +Qed. + +Theorem covers_Add : + forall A a a':Ensemble U, + Included U a A -> + Included U a' A -> + covers (Ensemble U) (Power_set_PO U A) a' a -> + exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x. +Proof. +intros A a a' H' H'0 H'1; try assumption. +elim (setcover_inv A a a'); auto with sets. +intros H'6 H'7. +clear H'1. +elim (Strict_Included_inv U a a'); auto with sets. +intros H'5 H'8; elim H'8. +intros x H'1; elim H'1. +intros H'2 H'3; try assumption. +exists x. +split; [ try assumption | idtac ]. +clear H'8 H'1. +elim (H'7 (Add U a x)); auto with sets. +intro H'1. +absurd (a = Add U a x); auto with sets. +red in |- *; intro H'8; try exact H'8. +apply H'3. +rewrite H'8; auto with sets. +auto with sets. +red in |- *. +intros x0 H'1; elim H'1; auto with sets. +intros x1 H'8; elim H'8; auto with sets. +split; [ idtac | try assumption ]. +red in H'0; auto with sets. +Qed. + +Theorem covers_is_Add : + forall A a a':Ensemble U, + Included U a A -> + Included U a' A -> + (covers (Ensemble U) (Power_set_PO U A) a' a <-> + (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)). +Proof. +intros A a a' H' H'0; split; intro K. +apply covers_Add with (A := A); auto with sets. +elim K. +intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1. +apply Add_covers; intuition. +Qed. + +Theorem Singleton_atomic : + forall (x:U) (A:Ensemble U), + In U A x -> + covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U). +intros x A H'. +rewrite <- (Empty_set_zero' U x). +apply Add_covers; auto with sets. +Qed. + +Lemma less_than_singleton : + forall (X:Ensemble U) (x:U), + Strict_Included U X (Singleton U x) -> X = Empty_set U. +intros X x H'; try assumption. +red in H'. +lapply (Singleton_atomic x (Full_set U)); + [ intro H'2; try exact H'2 | apply Full_intro ]. +elim H'; intros H'0 H'1; try exact H'1; clear H'. +elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x)); + [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets. +elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ]; + auto with sets. +elim H'1; auto with sets. +Qed. + +End Sets_as_an_algebra. + +Hint Resolve incl_soustr_in: sets v62. +Hint Resolve incl_soustr: sets v62. +Hint Resolve incl_soustr_add_l: sets v62. +Hint Resolve incl_soustr_add_r: sets v62. +Hint Resolve add_soustr_1 add_soustr_2: sets v62. +Hint Resolve add_soustr_xy: sets v62.
\ No newline at end of file diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v new file mode 100755 index 00000000..2c71f529 --- /dev/null +++ b/theories/Sets/Powerset_facts.v @@ -0,0 +1,268 @@ +(************************************************************************) +(* 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.8.2.1 2004/07/16 19:31:18 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. +Hint Unfold not. + +Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X. +Proof. +auto 6 with sets. +Qed. +Hint Resolve Empty_set_zero. + +Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. +Proof. +unfold Add at 1 in |- *; auto with sets. +Qed. +Hint Resolve Empty_set_zero'. + +Lemma less_than_empty : + forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U. +Proof. +auto with sets. +Qed. +Hint Resolve less_than_empty. + +Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A. +Proof. +auto with sets. +Qed. + +Theorem Union_associative : + forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C). +Proof. +auto 9 with sets. +Qed. +Hint Resolve Union_associative. + +Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A. +Proof. +auto 7 with sets. +Qed. + +Lemma Union_absorbs : + forall A B:Ensemble U, Included U B A -> Union U A B = A. +Proof. +auto 7 with sets. +Qed. + +Theorem Couple_as_union : + forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y. +Proof. +intros x y; apply Extensionality_Ensembles; split; red in |- *. +intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets). +intros x0 H'; elim H'; auto with sets. +Qed. + +Theorem Triple_as_union : + forall x y z:U, + Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) = + Triple U x y z. +Proof. +intros x y z; apply Extensionality_Ensembles; split; red in |- *. +intros x0 H'; elim H'. +intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets). +intros x1 H'0; elim H'0; auto with sets. +intros x0 H'; elim H'; auto with sets. +Qed. + +Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y. +Proof. +intros x y. +rewrite <- (Couple_as_union x y). +rewrite <- (Union_idempotent (Singleton U x)). +apply Triple_as_union. +Qed. + +Theorem Triple_as_Couple_Singleton : + forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z). +Proof. +intros x y z. +rewrite <- (Triple_as_union x y z). +rewrite <- (Couple_as_union x y); auto with sets. +Qed. + +Theorem Intersection_commutative : + forall A B:Ensemble U, Intersection U A B = Intersection U B A. +Proof. +intros A B. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'; elim H'; auto with sets. +Qed. + +Theorem Distributivity : + forall A B C:Ensemble U, + Intersection U A (Union U B C) = + Union U (Intersection U A B) (Intersection U A C). +Proof. +intros A B C. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'. +elim H'. +intros x0 H'0 H'1; generalize H'0. +elim H'1; auto with sets. +elim H'; intros x0 H'0; elim H'0; auto with sets. +Qed. + +Theorem Distributivity' : + forall A B C:Ensemble U, + Union U A (Intersection U B C) = + Intersection U (Union U A B) (Union U A C). +Proof. +intros A B C. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'. +elim H'; auto with sets. +intros x0 H'0; elim H'0; auto with sets. +elim H'. +intros x0 H'0; elim H'0; auto with sets. +intros x1 H'1 H'2; try exact H'2. +generalize H'1. +elim H'2; auto with sets. +Qed. + +Theorem Union_add : + forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x). +Proof. +unfold Add in |- *; auto with sets. +Qed. +Hint Resolve Union_add. + +Theorem Non_disjoint_union : + forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X. +intros X x H'; unfold Add in |- *. +apply Extensionality_Ensembles; red in |- *. +split; red in |- *; auto with sets. +intros x0 H'0; elim H'0; auto with sets. +intros t H'1; elim H'1; auto with sets. +Qed. + +Theorem Non_disjoint_union' : + forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X. +Proof. +intros X x H'; unfold Subtract in |- *. +apply Extensionality_Ensembles. +split; red in |- *; auto with sets. +intros x0 H'0; elim H'0; auto with sets. +intros x0 H'0; apply Setminus_intro; auto with sets. +red in |- *; intro H'1; elim H'1. +lapply (Singleton_inv U x x0); auto with sets. +intro H'4; apply H'; rewrite H'4; auto with sets. +Qed. + +Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y. +Proof. +intro x; rewrite (Empty_set_zero' x); auto with sets. +Qed. +Hint Resolve singlx. + +Lemma incl_add : + forall (A B:Ensemble U) (x:U), + Included U A B -> Included U (Add U A x) (Add U B x). +Proof. +intros A B x H'; red in |- *; auto with sets. +intros x0 H'0. +lapply (Add_inv U A x x0); auto with sets. +intro H'1; elim H'1; + [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ]; + auto with sets. +Qed. +Hint Resolve incl_add. + +Lemma incl_add_x : + forall (A B:Ensemble U) (x:U), + ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B. +Proof. +unfold Included in |- *. +intros A B x H' H'0 x0 H'1. +lapply (H'0 x0); auto with sets. +intro H'2; lapply (Add_inv U B x x0); auto with sets. +intro H'3; elim H'3; + [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ]. +absurd (In U A x0); auto with sets. +rewrite <- H'4; auto with sets. +Qed. + +Lemma Add_commutative : + forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x. +Proof. +intros A x y. +unfold Add in |- *. +rewrite (Union_associative A (Singleton U x) (Singleton U y)). +rewrite (Union_commutative (Singleton U x) (Singleton U y)). +rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); + auto with sets. +Qed. + +Lemma Add_commutative' : + forall (A:Ensemble U) (x y z:U), + Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y. +Proof. +intros A x y z. +rewrite (Add_commutative (Add U A x) y z). +rewrite (Add_commutative A x z); auto with sets. +Qed. + +Lemma Add_distributes : + forall (A B:Ensemble U) (x y:U), + Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y). +Proof. +intros A B x y H'; try assumption. +rewrite <- (Union_add (Add U A x) B y). +unfold Add at 4 in |- *. +rewrite (Union_commutative A (Singleton U x)). +rewrite Union_associative. +rewrite (Union_absorbs A B H'). +rewrite (Union_commutative (Singleton U x) A). +auto with sets. +Qed. + +Lemma setcover_intro : + forall (U:Type) (A x y:Ensemble U), + Strict_Included U x y -> + ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) -> + covers (Ensemble U) (Power_set_PO U A) y x. +Proof. +intros; apply Definition_of_covers; auto with sets. +Qed. +Hint Resolve setcover_intro. + +End Sets_as_an_algebra. + +Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add + singlx incl_add: sets v62. + diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v new file mode 100755 index 00000000..e33746a9 --- /dev/null +++ b/theories/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.4.2.1 2004/07/16 19:31:18 herbelin Exp $ i*) + +Section Relations_1. + Variable U : Type. + + Definition Relation := U -> U -> Prop. + Variable R : Relation. + + Definition Reflexive : Prop := forall x:U, R x x. + + Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z. + + Definition Symmetric : Prop := forall x y:U, R x y -> R y x. + + Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y. + + Definition contains (R R':Relation) : Prop := + forall x y:U, R' x y -> R x y. + + Definition same_relation (R R':Relation) : Prop := + contains R R' /\ contains R' R. + + Inductive Preorder : Prop := + Definition_of_preorder : Reflexive -> Transitive -> Preorder. + + Inductive Order : Prop := + Definition_of_order : + Reflexive -> Transitive -> Antisymmetric -> Order. + + Inductive Equivalence : Prop := + Definition_of_equivalence : + Reflexive -> Transitive -> Symmetric -> Equivalence. + + Inductive PER : Prop := + Definition_of_PER : Symmetric -> Transitive -> PER. + +End Relations_1. +Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains + same_relation: sets v62. +Hint Resolve Definition_of_preorder Definition_of_order + Definition_of_equivalence Definition_of_PER: sets v62.
\ No newline at end of file diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v new file mode 100755 index 00000000..62688895 --- /dev/null +++ b/theories/Sets/Relations_1_facts.v @@ -0,0 +1,112 @@ +(************************************************************************) +(* 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.7.2.1 2004/07/16 19:31:18 herbelin Exp $ i*) + +Require Export Relations_1. + +Definition Complement (U:Type) (R:Relation U) : Relation U := + fun x y:U => ~ R x y. + +Theorem Rsym_imp_notRsym : + forall (U:Type) (R:Relation U), + Symmetric U R -> Symmetric U (Complement U R). +Proof. +unfold Symmetric, Complement in |- *. +intros U R H' x y H'0; red in |- *; intro H'1; apply H'0; auto with sets. +Qed. + +Theorem Equiv_from_preorder : + forall (U:Type) (R:Relation U), + Preorder U R -> Equivalence U (fun x y:U => R x y /\ R y x). +Proof. +intros U R H'; elim H'; intros H'0 H'1. +apply Definition_of_equivalence. +red in H'0; auto 10 with sets. +2: red in |- *; intros x y h; elim h; intros H'3 H'4; auto 10 with sets. +red in H'1; red in |- *; auto 10 with sets. +intros x y z h; elim h; intros H'3 H'4; clear h. +intro h; elim h; intros H'5 H'6; clear h. +split; apply H'1 with y; auto 10 with sets. +Qed. +Hint Resolve Equiv_from_preorder. + +Theorem Equiv_from_order : + forall (U:Type) (R:Relation U), + Order U R -> Equivalence U (fun x y:U => R x y /\ R y x). +Proof. +intros U R H'; elim H'; auto 10 with sets. +Qed. +Hint Resolve Equiv_from_order. + +Theorem contains_is_preorder : + forall U:Type, Preorder (Relation U) (contains U). +Proof. +auto 10 with sets. +Qed. +Hint Resolve contains_is_preorder. + +Theorem same_relation_is_equivalence : + forall U:Type, Equivalence (Relation U) (same_relation U). +Proof. +unfold same_relation at 1 in |- *; auto 10 with sets. +Qed. +Hint Resolve same_relation_is_equivalence. + +Theorem cong_reflexive_same_relation : + forall (U:Type) (R R':Relation U), + same_relation U R R' -> Reflexive U R -> Reflexive U R'. +Proof. +unfold same_relation in |- *; intuition. +Qed. + +Theorem cong_symmetric_same_relation : + forall (U:Type) (R R':Relation U), + same_relation U R R' -> Symmetric U R -> Symmetric U R'. +Proof. + compute in |- *; intros; elim H; intros; clear H; + apply (H3 y x (H0 x y (H2 x y H1))). +(*Intuition.*) +Qed. + +Theorem cong_antisymmetric_same_relation : + forall (U:Type) (R R':Relation U), + same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'. +Proof. + compute in |- *; intros; elim H; intros; clear H; + apply (H0 x y (H3 x y H1) (H3 y x H2)). +(*Intuition.*) +Qed. + +Theorem cong_transitive_same_relation : + forall (U:Type) (R R':Relation U), + same_relation U R R' -> Transitive U R -> Transitive U R'. +Proof. +intros U R R' H' H'0; red in |- *. +elim H'. +intros H'1 H'2 x y z H'3 H'4; apply H'2. +apply H'0 with y; auto with sets. +Qed.
\ No newline at end of file diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v new file mode 100755 index 00000000..15d3ee2d --- /dev/null +++ b/theories/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.4.2.1 2004/07/16 19:31:18 herbelin Exp $ i*) + +Require Export Relations_1. + +Section Relations_2. +Variable U : Type. +Variable R : Relation U. + +Inductive Rstar : Relation U := + | Rstar_0 : forall x:U, Rstar x x + | Rstar_n : forall x y z:U, R x y -> Rstar y z -> Rstar x z. + +Inductive Rstar1 : Relation U := + | Rstar1_0 : forall x:U, Rstar1 x x + | Rstar1_1 : forall x y:U, R x y -> Rstar1 x y + | Rstar1_n : forall x y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z. + +Inductive Rplus : Relation U := + | Rplus_0 : forall x y:U, R x y -> Rplus x y + | Rplus_n : forall x y z:U, R x y -> Rplus y z -> Rplus x z. + +Definition Strongly_confluent : Prop := + forall x a b:U, R x a -> R x b -> ex (fun z:U => R a z /\ R b z). + +End Relations_2. + +Hint Resolve Rstar_0: sets v62. +Hint Resolve Rstar1_0: sets v62. +Hint Resolve Rstar1_1: sets v62. +Hint Resolve Rplus_0: sets v62.
\ No newline at end of file diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v new file mode 100755 index 00000000..4c729fe7 --- /dev/null +++ b/theories/Sets/Relations_2_facts.v @@ -0,0 +1,153 @@ +(************************************************************************) +(* 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.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*) + +Require Export Relations_1. +Require Export Relations_1_facts. +Require Export Relations_2. + +Theorem Rstar_reflexive : + forall (U:Type) (R:Relation U), Reflexive U (Rstar U R). +Proof. +auto with sets. +Qed. + +Theorem Rplus_contains_R : + forall (U:Type) (R:Relation U), contains U (Rplus U R) R. +Proof. +auto with sets. +Qed. + +Theorem Rstar_contains_R : + forall (U:Type) (R:Relation U), contains U (Rstar U R) R. +Proof. +intros U R; red in |- *; intros x y H'; apply Rstar_n with y; auto with sets. +Qed. + +Theorem Rstar_contains_Rplus : + forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R). +Proof. +intros U R; red in |- *. +intros x y H'; elim H'. +generalize Rstar_contains_R; intro T; red in T; auto with sets. +intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets. +Qed. + +Theorem Rstar_transitive : + forall (U:Type) (R:Relation U), Transitive U (Rstar U R). +Proof. +intros U R; red in |- *. +intros x y z H'; elim H'; auto with sets. +intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto with sets. +Qed. + +Theorem Rstar_cases : + forall (U:Type) (R:Relation U) (x y:U), + Rstar U R x y -> x = y \/ (exists u : _, R x u /\ Rstar U R u y). +Proof. +intros U R x y H'; elim H'; auto with sets. +intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto with sets. +Qed. + +Theorem Rstar_equiv_Rstar1 : + forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R). +Proof. +generalize Rstar_contains_R; intro T; red in T. +intros U R; unfold same_relation, contains in |- *. +split; intros x y H'; elim H'; auto with sets. +generalize Rstar_transitive; intro T1; red in T1. +intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets. +intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets. +Qed. + +Theorem Rsym_imp_Rstarsym : + forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R). +Proof. +intros U R H'; red in |- *. +intros x y H'0; elim H'0; auto with sets. +intros x0 y0 z H'1 H'2 H'3. +generalize Rstar_transitive; intro T1; red in T1. +apply T1 with y0; auto with sets. +apply Rstar_n with x0; auto with sets. +Qed. + +Theorem Sstar_contains_Rstar : + forall (U:Type) (R S:Relation U), + contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R). +Proof. +unfold contains in |- *. +intros U R S H' x y H'0; elim H'0; auto with sets. +generalize Rstar_transitive; intro T1; red in T1. +intros x0 y0 z H'1 H'2 H'3; apply T1 with y0; auto with sets. +Qed. + +Theorem star_monotone : + forall (U:Type) (R S:Relation U), + contains U S R -> contains U (Rstar U S) (Rstar U R). +Proof. +intros U R S H'. +apply Sstar_contains_Rstar; auto with sets. +generalize (Rstar_contains_R U S); auto with sets. +Qed. + +Theorem RstarRplus_RRstar : + forall (U:Type) (R:Relation U) (x y z:U), + Rstar U R x y -> Rplus U R y z -> exists u : _, R x u /\ Rstar U R u z. +Proof. +generalize Rstar_contains_Rplus; intro T; red in T. +generalize Rstar_transitive; intro T1; red in T1. +intros U R x y z H'; elim H'. +intros x0 H'0; elim H'0. +intros x1 y0 H'1; exists y0; auto with sets. +intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets. +intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0. +split; [ try assumption | idtac ]. +apply T1 with z0; auto with sets. +Qed. + +Theorem Lemma1 : + forall (U:Type) (R:Relation U), + Strongly_confluent U R -> + forall x b:U, + Rstar U R x b -> + forall a:U, R x a -> exists z : _, Rstar U R a z /\ R b z. +Proof. +intros U R H' x b H'0; elim H'0. +intros x0 a H'1; exists a; auto with sets. +intros x0 y z H'1 H'2 H'3 a H'4. +red in H'. +specialize 3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7; + [ intro H'8; lapply H'8; + [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ] + | clear H'7 ]; auto with sets. +elim H'9. +intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5. +elim (H'3 t); auto with sets. +intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5. +exists z1; split; [ idtac | assumption ]. +apply Rstar_n with t; auto with sets. +Qed.
\ No newline at end of file diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v new file mode 100755 index 00000000..6a254819 --- /dev/null +++ b/theories/Sets/Relations_3.v @@ -0,0 +1,62 @@ +(************************************************************************) +(* 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.7.2.1 2004/07/16 19:31:18 herbelin Exp $ i*) + +Require Export Relations_1. +Require Export Relations_2. + +Section Relations_3. + Variable U : Type. + Variable R : Relation U. + + Definition coherent (x y:U) : Prop := + exists z : _, Rstar U R x z /\ Rstar U R y z. + + Definition locally_confluent (x:U) : Prop := + forall y z:U, R x y -> R x z -> coherent y z. + + Definition Locally_confluent : Prop := forall x:U, locally_confluent x. + + Definition confluent (x:U) : Prop := + forall y z:U, Rstar U R x y -> Rstar U R x z -> coherent y z. + + Definition Confluent : Prop := forall x:U, confluent x. + + Inductive noetherian : U -> Prop := + definition_of_noetherian : + forall x:U, (forall y:U, R x y -> noetherian y) -> noetherian x. + + Definition Noetherian : Prop := forall x:U, noetherian x. + +End Relations_3. +Hint Unfold coherent: sets v62. +Hint Unfold locally_confluent: sets v62. +Hint Unfold confluent: sets v62. +Hint Unfold Confluent: sets v62. +Hint Resolve definition_of_noetherian: sets v62. +Hint Unfold Noetherian: sets v62. + diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v new file mode 100755 index 00000000..34322dc7 --- /dev/null +++ b/theories/Sets/Relations_3_facts.v @@ -0,0 +1,171 @@ +(************************************************************************) +(* 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.6.2.1 2004/07/16 19:31:18 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 : + forall (U:Type) (R:Relation U) (x y:U), Rstar U R x y -> coherent U R x y. +Proof. +intros U R x y H'; red in |- *. +exists y; auto with sets. +Qed. +Hint Resolve Rstar_imp_coherent. + +Theorem coherent_symmetric : + forall (U:Type) (R:Relation U), Symmetric U (coherent U R). +Proof. +unfold coherent at 1 in |- *. +intros U R; red in |- *. +intros x y H'; elim H'. +intros z H'0; exists z; tauto. +Qed. + +Theorem Strong_confluence : + forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R. +Proof. +intros U R H'; red in |- *. +intro x; red in |- *; intros a b H'0. +unfold coherent at 1 in |- *. +generalize b; clear b. +elim H'0; clear H'0. +intros x0 b H'1; exists b; auto with sets. +intros x0 y z H'1 H'2 H'3 b H'4. +generalize (Lemma1 U R); intro h; lapply h; + [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0; + [ intro H'5; generalize (H'5 y); intro h1; lapply h1; + [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7; + clear h h0 h1 h2 h3 + | clear h h0 h1 ] + | clear h h0 ] + | clear h ]; auto with sets. +generalize (H'3 z0); intro h; lapply h; + [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1 + | clear h ]; auto with sets. +exists z1; split; auto with sets. +apply Rstar_n with z0; auto with sets. +Qed. + +Theorem Strong_confluence_direct : + forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R. +Proof. +intros U R H'; red in |- *. +intro x; red in |- *; intros a b H'0. +unfold coherent at 1 in |- *. +generalize b; clear b. +elim H'0; clear H'0. +intros x0 b H'1; exists b; auto with sets. +intros x0 y z H'1 H'2 H'3 b H'4. +cut (ex (fun t:U => Rstar U R y t /\ R b t)). +intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0. +generalize (H'3 t); intro h; lapply h; + [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1 + | clear h ]; auto with sets. +exists z0; split; [ assumption | idtac ]. +apply Rstar_n with t; auto with sets. +generalize H'1; generalize y; clear H'1. +elim H'4. +intros x1 y0 H'0; exists y0; auto with sets. +intros x1 y0 z0 H'0 H'1 H'5 y1 H'6. +red in H'. +generalize (H' x1 y0 y1); intro h; lapply h; + [ intro H'7; lapply H'7; + [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; + clear h H'7 h0 h1 + | clear h ] + | clear h ]; auto with sets. +generalize (H'5 z1); intro h; lapply h; + [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1 + | clear h ]; auto with sets. +exists t; split; auto with sets. +apply Rstar_n with z1; auto with sets. +Qed. + +Theorem Noetherian_contains_Noetherian : + forall (U:Type) (R R':Relation U), + Noetherian U R -> contains U R R' -> Noetherian U R'. +Proof. +unfold Noetherian at 2 in |- *. +intros U R R' H' H'0 x. +elim (H' x); auto with sets. +Qed. + +Theorem Newman : + forall (U:Type) (R:Relation U), + Noetherian U R -> Locally_confluent U R -> Confluent U R. +Proof. +intros U R H' H'0; red in |- *; intro x. +elim (H' x); unfold confluent in |- *. +intros x0 H'1 H'2 y z H'3 H'4. +generalize (Rstar_cases U R x0 y); intro h; lapply h; + [ intro h0; elim h0; + [ clear h h0; intro h1 + | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6; + clear h h0 h1 h2 ] + | clear h ]; auto with sets. +elim h1; auto with sets. +generalize (Rstar_cases U R x0 z); intro h; lapply h; + [ intro h0; elim h0; + [ clear h h0; intro h1 + | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8; + clear h h0 h1 h2 ] + | clear h ]; auto with sets. +elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets. +unfold Locally_confluent, locally_confluent, coherent in H'0. +generalize (H'0 x0 u v); intro h; lapply h; + [ intro H'9; lapply H'9; + [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11; + clear h H'9 h0 h1 + | clear h ] + | clear h ]; auto with sets. +clear H'0. +unfold coherent at 1 in H'2. +generalize (H'2 u); intro h; lapply h; + [ intro H'0; generalize (H'0 y t); intro h0; lapply h0; + [ intro H'9; lapply H'9; + [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13; + clear h h0 H'9 h1 h2 + | clear h h0 ] + | clear h h0 ] + | clear h ]; auto with sets. +generalize Rstar_transitive; intro T; red in T. +generalize (H'2 v); intro h; lapply h; + [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0; + [ intro H'14; lapply H'14; + [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16; + clear h h0 H'14 h1 h2 + | clear h h0 ] + | clear h h0 ] + | clear h ]; auto with sets. +red in |- *; (exists z1; split); auto with sets. +apply T with y1; auto with sets. +apply T with t; auto with sets. +Qed.
\ No newline at end of file diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v new file mode 100644 index 00000000..10d26f22 --- /dev/null +++ b/theories/Sets/Uniset.v @@ -0,0 +1,215 @@ +(************************************************************************) +(* 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.9.2.1 2004/07/16 19:31:18 herbelin Exp $ i*) + +(** Sets as characteristic functions *) + +(* G. Huet 1-9-95 *) +(* Updated Papageno 12/98 *) + +Require Import Bool. + +Set Implicit Arguments. + +Section defs. + +Variable A : Set. +Variable eqA : A -> A -> Prop. +Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. + +Inductive uniset : Set := + Charac : (A -> bool) -> uniset. + +Definition charac (s:uniset) (a:A) : bool := let (f) := s in f a. + +Definition Emptyset := Charac (fun a:A => false). + +Definition Fullset := Charac (fun a:A => true). + +Definition Singleton (a:A) := + Charac + (fun a':A => + match eqA_dec a a' with + | left h => true + | right h => false + end). + +Definition In (s:uniset) (a:A) : Prop := charac s a = true. +Hint Unfold In. + +(** uniset inclusion *) +Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a). +Hint Unfold incl. + +(** uniset equality *) +Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. +Hint Unfold seq. + +Lemma leb_refl : forall b:bool, leb b b. +Proof. +destruct b; simpl in |- *; auto. +Qed. +Hint Resolve leb_refl. + +Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. +Proof. +unfold incl in |- *; intros s1 s2 E a; elim (E a); auto. +Qed. + +Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1. +Proof. +unfold incl in |- *; intros s1 s2 E a; elim (E a); auto. +Qed. + +Lemma seq_refl : forall x:uniset, seq x x. +Proof. +destruct x; unfold seq in |- *; auto. +Qed. +Hint Resolve seq_refl. + +Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z. +Proof. +unfold seq in |- *. +destruct x; destruct y; destruct z; simpl in |- *; intros. +rewrite H; auto. +Qed. + +Lemma seq_sym : forall x y:uniset, seq x y -> seq y x. +Proof. +unfold seq in |- *. +destruct x; destruct y; simpl in |- *; auto. +Qed. + +(** uniset union *) +Definition union (m1 m2:uniset) := + Charac (fun a:A => orb (charac m1 a) (charac m2 a)). + +Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). +Proof. +unfold seq in |- *; unfold union in |- *; simpl in |- *; auto. +Qed. +Hint Resolve union_empty_left. + +Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset). +Proof. +unfold seq in |- *; unfold union in |- *; simpl in |- *. +intros x a; rewrite (orb_b_false (charac x a)); auto. +Qed. +Hint Resolve union_empty_right. + +Lemma union_comm : forall x y:uniset, seq (union x y) (union y x). +Proof. +unfold seq in |- *; unfold charac in |- *; unfold union in |- *. +destruct x; destruct y; auto with bool. +Qed. +Hint Resolve union_comm. + +Lemma union_ass : + forall x y z:uniset, seq (union (union x y) z) (union x (union y z)). +Proof. +unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +destruct x; destruct y; destruct z; auto with bool. +Qed. +Hint Resolve union_ass. + +Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z). +Proof. +unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto. +Qed. +Hint Resolve seq_left. + +Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y). +Proof. +unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto. +Qed. +Hint 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 Import Permut. + +Lemma union_rotate : + forall x y z:uniset, seq (union x (union y z)) (union z (union x y)). +Proof. +intros; apply (op_rotate uniset union seq); auto. +exact seq_trans. +Qed. + +Lemma seq_congr : + forall x y z t:uniset, seq x y -> seq z t -> seq (union x z) (union y t). +Proof. +intros; apply (cong_congr uniset union seq); auto. +exact seq_trans. +Qed. + +Lemma union_perm_left : + forall x y z:uniset, seq (union x (union y z)) (union y (union x z)). +Proof. +intros; apply (perm_left uniset union seq); auto. +exact seq_trans. +Qed. + +Lemma uniset_twist1 : + forall x y z t:uniset, + seq (union x (union (union y z) t)) (union (union y (union x t)) z). +Proof. +intros; apply (twist uniset union seq); auto. +exact seq_trans. +Qed. + +Lemma uniset_twist2 : + forall x y z t:uniset, + seq (union x (union (union y z) t)) (union (union y (union x z)) t). +Proof. +intros; apply seq_trans with (union (union x (union y z)) t). +apply seq_sym; apply union_ass. +apply seq_left; apply union_perm_left. +Qed. + +(** specific for treesort *) + +Lemma treesort_twist1 : + forall x y z t u:uniset, + seq u (union y z) -> + seq (union x (union u t)) (union (union y (union x t)) z). +Proof. +intros; apply seq_trans with (union x (union (union y z) t)). +apply seq_right; apply seq_left; trivial. +apply uniset_twist1. +Qed. + +Lemma treesort_twist2 : + forall x y z t u:uniset, + seq u (union y z) -> + seq (union x (union u t)) (union (union y (union x z)) t). +Proof. +intros; apply seq_trans with (union x (union (union y z) t)). +apply seq_right; apply seq_left; trivial. +apply uniset_twist2. +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.
\ No newline at end of file diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex new file mode 100755 index 00000000..83c2177f --- /dev/null +++ b/theories/Sets/intro.tex @@ -0,0 +1,24 @@ +\section{Sets}\label{Sets} + +This is a library on sets defined by their characteristic predicate. +It contains the following modules: + +\begin{itemize} +\item {\tt Ensembles.v} +\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v} +\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, + {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v}, \\ + {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v} +\item {\tt Partial\_Order.v}, {\tt Cpo.v} +\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, + {\tt Powerset\_Classical\_facts.v} +\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v} +\item {\tt Image.v} +\item {\tt Infinite\_sets.v} +\item {\tt Integers.v} +\end{itemize} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: |