diff options
Diffstat (limited to 'theories/Sets/Integers.v')
| -rw-r--r-- | theories/Sets/Integers.v | 223 |
1 files changed, 110 insertions, 113 deletions
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index cfadd81c..c969ad9c 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Integers.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Integers.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Finite_sets. Require Export Constructive_sets. @@ -45,120 +45,117 @@ Require Export Partial_Order. Require Export Cpo. Section Integers_sect. - -Inductive Integers : Ensemble nat := + + 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. + 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. + + Lemma le_Order : Order nat le. + Proof. + split; [exact le_reflexive | exact le_trans | exact le_antisym]. + Qed. + + Lemma triv_nat : forall n:nat, In nat Integers n. + Proof. + exact Integers_defn. + Qed. + + 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). + apply Integers_defn. + exact le_Order. + Defined. + + 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. + + 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. + unfold nat_po. simpl. apply triv_nat. + 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. simpl in |- *. apply triv_nat. + 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). elim H'3; simpl in |- *; auto with sets arith. trivial. + intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial. + exists x0. + apply Upper_Bound_definition. + unfold nat_po. simpl. apply triv_nat. + 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; apply triv_nat. + 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. + apply triv_nat. + 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. |