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