aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-23 11:37:49 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-23 11:37:49 +0000
commitf7cd707fe388f0cfd990664c18a2d09d49890744 (patch)
tree462dc02647b30f18a0f0d1f123347b9f754f9006 /theories
parent98936ab93169591d6e1fc8321cb921397cfd67af (diff)
Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10711 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/Reals/Rlogic.v57
1 files changed, 56 insertions, 1 deletions
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index b8c85458c..8aadf8f5d 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -6,7 +6,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** * This module proves the decidablity of arithmetical statements from
+(** * This module proves some logical properties of the axiomatics of Reals
+
+1. Decidablity of arithmetical statements from
+ the axiom that the order of the real numbers is decidable.
+
+2. Derivability of the archimedean "axiom"
+*)
+
+(** 1- Proof of the decidablity of arithmetical statements from
excluded middle and the axiom that the order of the real numbers is
decidable. *)
@@ -236,3 +244,50 @@ assumption.
Qed.
End Arithmetical_dec.
+
+(** 2- Derivability of the Archimedean axiom *)
+
+(* This is a standard proof (it has been taken from PlanetMath). It is
+formulated negatively so as to avoid the need for classical
+logic. Using a proof of {n | ~P n}+{forall n, P n} (the one above or a
+variant of it that does not need classical axioms) , we can in
+principle also derive [up] and its [specification] *)
+
+Theorem not_not_archimedean :
+ forall r : R, ~ (forall n : nat, (INR n <= r)%R).
+intros r H.
+set (E := fun r => exists n : nat, r = INR n).
+assert (exists x : R, E x) by
+ (exists 0%R; simpl; red; exists 0%nat; reflexivity).
+assert (bound E) by (exists r; intros x (m,H2); rewrite H2; apply H).
+destruct (completeness E) as (M,(H3,H4)); try assumption.
+set (M' := (M + -1)%R).
+assert (H2 : ~ is_upper_bound E M').
+ intro H5.
+ assert (M <= M')%R by (apply H4; exact H5).
+ apply (Rlt_not_le M M').
+ unfold M' in |- *.
+ pattern M at 2 in |- *.
+ rewrite <- Rplus_0_l.
+ pattern (0 + M)%R in |- *.
+ rewrite Rplus_comm.
+ rewrite <- (Rplus_opp_r 1).
+ apply Rplus_lt_compat_l.
+ rewrite Rplus_comm.
+ apply Rlt_plus_1.
+ assumption.
+apply H2.
+intros N (n,H7).
+rewrite H7.
+unfold M' in |- *.
+assert (H5 : (INR (S n) <= M)%R) by (apply H3; exists (S n); reflexivity).
+rewrite S_INR in H5.
+assert (H6 : (INR n + 1 + -1 <= M + -1)%R).
+ apply Rplus_le_compat_r.
+ assumption.
+rewrite Rplus_assoc in H6.
+rewrite Rplus_opp_r in H6.
+rewrite (Rplus_comm (INR n) 0) in H6.
+rewrite Rplus_0_l in H6.
+assumption.
+Qed.