diff options
Diffstat (limited to 'theories7/Sets/Integers.v')
| -rwxr-xr-x | theories7/Sets/Integers.v | 166 |
1 files changed, 0 insertions, 166 deletions
diff --git a/theories7/Sets/Integers.v b/theories7/Sets/Integers.v deleted file mode 100755 index 7dee371f..00000000 --- a/theories7/Sets/Integers.v +++ /dev/null @@ -1,166 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id: Integers.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Finite_sets. -Require Export Constructive_sets. -Require Export Classical_Type. -Require Export Classical_sets. -Require Export Powerset. -Require Export Powerset_facts. -Require Export Powerset_Classical_facts. -Require Export Gt. -Require Export Lt. -Require Export Le. -Require Export Finite_sets_facts. -Require Export Image. -Require Export Infinite_sets. -Require Export Compare_dec. -Require Export Relations_1. -Require Export Partial_Order. -Require Export Cpo. - -Section Integers_sect. - -Inductive Integers : (Ensemble nat) := - Integers_defn: (x: nat) (In nat Integers x). -Hints Resolve Integers_defn. - -Lemma le_reflexive: (Reflexive nat le). -Proof. -Red; Auto with arith. -Qed. - -Lemma le_antisym: (Antisymmetric nat le). -Proof. -Red; Intros x y H H';Rewrite (le_antisym x y);Auto. -Qed. - -Lemma le_trans: (Transitive nat le). -Proof. -Red; Intros; Apply le_trans with y;Auto. -Qed. -Hints Resolve le_reflexive le_antisym le_trans. - -Lemma le_Order: (Order nat le). -Proof. -Auto with sets arith. -Qed. -Hints Resolve le_Order. - -Lemma triv_nat: (n: nat) (In nat Integers n). -Proof. -Auto with sets arith. -Qed. -Hints Resolve triv_nat. - -Definition nat_po: (PO nat). -Apply Definition_of_PO with Carrier_of := Integers Rel_of := le; Auto with sets arith. -Apply Inhabited_intro with x := O; Auto with sets arith. -Defined. -Hints Unfold nat_po. - -Lemma le_total_order: (Totally_ordered nat nat_po Integers). -Proof. -Apply Totally_ordered_definition. -Simpl. -Intros H' x y H'0. -Specialize 2 le_or_lt with n := x m := y; Intro H'2; Elim H'2. -Intro H'1; Left; Auto with sets arith. -Intro H'1; Right. -Cut (le y x); Auto with sets arith. -Qed. -Hints Resolve le_total_order. - -Lemma Finite_subset_has_lub: - (X: (Ensemble nat)) (Finite nat X) -> - (EXT m: nat | (Upper_Bound nat nat_po X m)). -Proof. -Intros X H'; Elim H'. -Exists O. -Apply Upper_Bound_definition; Auto with sets arith. -Intros y H'0; Elim H'0; Auto with sets arith. -Intros A H'0 H'1 x H'2; Try Assumption. -Elim H'1; Intros x0 H'3; Clear H'1. -Elim le_total_order. -Simpl. -Intro H'1; Try Assumption. -LApply H'1; [Intro H'4; Idtac | Try Assumption]; Auto with sets arith. -Generalize (H'4 x0 x). -Clear H'4. -Clear H'1. -Intro H'1; LApply H'1; - [Intro H'4; Elim H'4; - [Intro H'5; Try Exact H'5; Clear H'4 H'1 | Intro H'5; Clear H'4 H'1] | - Clear H'1]. -Exists x. -Apply Upper_Bound_definition; Auto with sets arith; Simpl. -Intros y H'1; Elim H'1. -Generalize le_trans. -Intro H'4; Red in H'4. -Intros x1 H'6; Try Assumption. -Apply H'4 with y := x0; Auto with sets arith. -Elim H'3; Simpl; Auto with sets arith. -Intros x1 H'4; Elim H'4; Auto with sets arith. -Exists x0. -Apply Upper_Bound_definition; Auto with sets arith; Simpl. -Intros y H'1; Elim H'1. -Intros x1 H'4; Try Assumption. -Elim H'3; Simpl; Auto with sets arith. -Intros x1 H'4; Elim H'4; Auto with sets arith. -Red. -Intros x1 H'1; Elim H'1; Auto with sets arith. -Qed. - -Lemma Integers_has_no_ub: ~ (EXT m:nat | (Upper_Bound nat nat_po Integers m)). -Proof. -Red; Intro H'; Elim H'. -Intros x H'0. -Elim H'0; Intros H'1 H'2. -Cut (In nat Integers (S x)). -Intro H'3. -Specialize 1 H'2 with y := (S x); Intro H'4; LApply H'4; - [Intro H'5; Clear H'4 | Try Assumption; Clear H'4]. -Simpl in H'5. -Absurd (le (S x) x); Auto with arith. -Auto with sets arith. -Qed. - -Lemma Integers_infinite: ~ (Finite nat Integers). -Proof. -Generalize Integers_has_no_ub. -Intro H'; Red; Intro H'0; Try Exact H'0. -Apply H'. -Apply Finite_subset_has_lub; Auto with sets arith. -Qed. - -End Integers_sect. - - - - - |