From f093a07ab0289c632b3f5600e8ad03bad23c13c5 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 12 Nov 2001 17:59:15 +0000 Subject: suppression d'axiomes dans Rstar, Newman et Integers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2187 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sets/Integers.v | 145 +++++++++++++---------------------------------- 1 file changed, 40 insertions(+), 105 deletions(-) (limited to 'theories/Sets') diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 85d3b1c12..dbfc6b463 100755 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -46,128 +46,67 @@ Require Export Cpo. Section Integers_sect. -Inductive Nat : Type := - mkNat: nat -> Nat. - -Parameter nat_of_Nat: Nat -> nat. - -Axiom nat_of_nat_returns: (n: nat) (nat_of_Nat (mkNat n)) = n. - -Lemma mkNat_injective: (n1, n2: nat) (mkNat n1) == (mkNat n2) -> n1 = n2. -Proof. -Intros n1 n2 H'; Try Assumption. -Rewrite <- (nat_of_nat_returns n1). -Rewrite <- (nat_of_nat_returns n2). -Rewrite H'; Auto with sets arith. -Qed. - -Inductive Integers : (Ensemble Nat) := - Integers_defn: (x: Nat) (In Nat Integers x). +Inductive Integers : (Ensemble nat) := + Integers_defn: (x: nat) (In nat Integers x). Hints Resolve Integers_defn. -Inductive Le_Nat [x, y:Nat]: Prop := - Definition_of_Le_nat: - (n1, n2: nat) x == (mkNat n1) -> y == (mkNat n2) -> (le n1 n2) -> - (Le_Nat x y). - -Lemma Le_Nat_direct: (n1, n2: nat) (le n1 n2) -> (Le_Nat (mkNat n1) (mkNat n2)). +Lemma le_reflexive: (Reflexive nat le). Proof. -Intros n1 n2 H'. -Apply Definition_of_Le_nat with n1 := n1 n2 := n2; Auto with sets arith. +Red; Auto with arith. Qed. -Hints Resolve Le_Nat_direct. -Lemma Le_Nat_Reflexive: (Reflexive Nat Le_Nat). +Lemma le_antisym: (Antisymmetric nat le). Proof. -Red. -Intro x; Elim x; Auto with sets arith. +Red; Intros x y H H';Rewrite (le_antisym x y);Auto. Qed. -Hints Resolve Le_Nat_Reflexive. -Lemma Le_Nat_antisym: (Antisymmetric Nat Le_Nat). +Lemma le_trans: (Transitive nat le). Proof. -Red. -Intros x y H'; Elim H'. -Intros n1 n2 H'0 H'1 H'2 H'3; Elim H'3. -Intros n3 n4 H'4 H'5 H'6. -Cut n1 = n4 /\ n2 = n3. -Intro H'7. -Generalize H'6. -Elim H'7; Intros H'8 H'9; Rewrite <- H'8; Clear H'7. -Rewrite <- H'9. -Intro H'7. -Cut n1 = n2. -Rewrite H'0; Rewrite H'1. -Intro H'10; Rewrite <- H'10; Auto with sets arith. -Apply le_antisym; Auto with sets arith. -Split; Apply mkNat_injective. -Rewrite <- H'5; Rewrite H'0; Auto with sets arith. -Rewrite <- H'4; Rewrite H'1; Auto with sets arith. +Red; Intros; Apply le_trans with y;Auto. Qed. +Hints Resolve le_reflexive le_antisym le_trans. -Hints Resolve Le_Nat_antisym. - -Lemma Le_Nat_trans: (Transitive Nat Le_Nat). -Proof. -Red. -Intros x y z H'; Elim H'. -Intros n1 n2 H'0 H'1 H'2 H'3; Elim H'3. -Intros n3 n4 H'4 H'5 H'6. -Rewrite H'0; Rewrite H'5. -Apply Le_Nat_direct. -Apply le_trans with m := n3; Auto with sets arith. -Cut n2 = n3. -Intro H'7; Rewrite <- H'7; Auto with sets arith. -Apply mkNat_injective. -Rewrite <- H'4; Rewrite <- H'1; Auto with sets arith. -Qed. -Hints Resolve Le_Nat_trans. - -Lemma Le_Nat_Order: (Order Nat Le_Nat). +Lemma le_Order: (Order nat le). Proof. Auto with sets arith. Qed. -Hints Resolve Le_Nat_Order. +Hints Resolve le_Order. -Definition Nat_O := (mkNat O). - -Lemma triv_Nat: (n: nat) (In Nat Integers (mkNat n)). +Lemma triv_nat: (n: nat) (In nat Integers n). Proof. Auto with sets arith. Qed. -Hints Resolve triv_Nat. +Hints Resolve triv_nat. -Definition Nat_po: (PO Nat). -Apply Definition_of_PO with Carrier_of := Integers Rel_of := Le_Nat; Auto with sets arith. -Apply Inhabited_intro with x := Nat_O; Auto with sets arith. +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. +Hints Unfold nat_po. -Lemma Le_Nat_total_order: (Totally_ordered Nat Nat_po Integers). +Lemma le_total_order: (Totally_ordered nat nat_po Integers). Proof. Apply Totally_ordered_definition. Simpl. -Intros H' x; Elim x. -Intros n y; Elim y. -Intros n0 H'0. -Specialize 2 le_or_lt with n := n m := n0; Intro H'2; Elim H'2. +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 n0 n); Auto with sets arith. +Cut (le y x); Auto with sets arith. Qed. -Hints Resolve Le_Nat_total_order. +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)). + (X: (Ensemble nat)) (Finite nat X) -> + (EXT m: nat | (Upper_Bound nat nat_po X m)). Proof. Intros X H'; Elim H'. -Exists Nat_O. +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_Nat_total_order. +Elim le_total_order. Simpl. Intro H'1; Try Assumption. LApply H'1; [Intro H'4; Idtac | Try Assumption]; Auto with sets arith. @@ -181,7 +120,7 @@ Intro H'1; LApply H'1; Exists x. Apply Upper_Bound_definition; Auto with sets arith; Simpl. Intros y H'1; Elim H'1. -Generalize Le_Nat_trans. +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. @@ -197,30 +136,21 @@ 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)). +Lemma Integers_has_no_ub: ~ (EXT m:nat | (Upper_Bound nat nat_po Integers m)). Proof. Red; Intro H'; Elim H'. -Intro x; Elim x. -Intros n H'0; Elim H'0. -Intros H'1 H'2; Try Assumption. -Cut (In Nat Integers (mkNat (S n))). -Intro H'3; Try Assumption. -Specialize 1 H'2 with y := (mkNat (S n)); Intro H'4; LApply H'4; +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. -Elim H'5. -Intros n1 n2 H'4 H'6; Try Assumption. -Specialize 2 mkNat_injective with n1 := (S n) n2 := n1; Intro H'8; LApply H'8; - [Intro H'9; Rewrite <- H'9; Clear H'8 | Clear H'8]; Auto with sets arith. -Specialize 2 mkNat_injective with n1 := n n2 := n2; Intro H'8; LApply H'8; - [Intro H'10; Rewrite <- H'10; Clear H'8 | Clear H'8]; Auto with sets arith. -Intro H'7; Try Assumption. -Specialize 1 le_Sn_n with n := n; Intro H'8; Elim H'8. -Auto with sets arith. +Absurd (le (S x) x); Auto with arith. Auto with sets arith. Qed. -Lemma Integers_infinite: ~ (Finite Nat Integers). +Lemma Integers_infinite: ~ (Finite nat Integers). Proof. Generalize Integers_has_no_ub. Intro H'; Red; Intro H'0; Try Exact H'0. @@ -229,3 +159,8 @@ Apply Finite_subset_has_lub; Auto with sets arith. Qed. End Integers_sect. + + + + + -- cgit v1.2.3