summaryrefslogtreecommitdiff
path: root/theories7/Sets/Integers.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories7/Sets/Integers.v')
-rwxr-xr-xtheories7/Sets/Integers.v166
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.
-
-
-
-
-