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

1 files changed, 40 insertions, 105 deletions

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.
+
+
+
+
+