Nicer proofs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10476 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 83 insertions, 83 deletions

diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 35f254e13..e10c3ab40 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -6,16 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** This module proves the decidablitiy of arithmetical statements from
+(** This module proves the decidablity of arithmetical statements from
 the axiom that the order of the real numbers is decidable. *)
 
-(** Assuming a decidable predicate [P n], A series is constructied who's
+(** Assuming a decidable predicate [P n], A series is constructed who's
 [n]th term is 1/2^n if [P n] holds and 0 otherwise.  This sum reaches 2
 only if [P n] holds for all [n], otherwise the sum is less than 2.
 Comparing the sum to 2 decides if [forall n, P n] or [~forall n, P n] *)
 
 (** One can iterate this lemma and use classical logic to decide any
-statement in the arithmetical heirarchy. *)
+statement in the arithmetical hierarchy. *)
 
 (** Contributed by Cezary Kaliszyk and Russell O'Connor *)
 
@@ -28,118 +28,118 @@ Section Arithmetical_dec.
 Variable P : nat -> Prop.
 Hypothesis HP : forall n, {P n} + {~P n}.
 
-Let positive_sums_lemma : (forall (m n : nat) (f : nat -> R), (lt m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
+Let ge_fun_sums_ge_lemma : (forall (m n : nat) (f : nat -> R), (lt m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
 intros m n f mn fpos.
 replace (sum_f_R0 f m) with (sum_f_R0 f m + 0) by ring.
 rewrite (tech2 f m n mn).
-assert (sum_f_R0 f m = sum_f_R0 f m + 0) by ring.
 apply Rplus_le_compat_l.
-induction (n - S m)%nat.
- simpl.
+ induction (n - S m)%nat; simpl in *.
  apply fpos.
-simpl in *.
 replace 0 with (0 + 0) by ring.
 apply (Rplus_le_compat _ _ _ _ IHn0 (fpos (S (m + S n0)%nat))).
 Qed.
 
-Let positive_sums : (forall (m n : nat) (f : nat -> R), (le m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
+Let ge_fun_sums_ge : (forall (m n : nat) (f : nat -> R), (le m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
 intros m n f mn pos.
-elim (le_lt_or_eq _ _ mn).
-intro; apply positive_sums_lemma; assumption.
+ elim (le_lt_or_eq _ _ mn).
+ intro; apply ge_fun_sums_ge_lemma; assumption.
 intro H; rewrite H; auto with *.
 Qed.
 
-Lemma forall_dec : {forall n, P n} + {~forall n, P n}.
-Proof.
-set (f:=fun n => (if HP n then (1/2)^n else 0)%R).
- assert (Hg:Cauchy_crit_series f).
- intros e He.
- assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R).
-  apply GP_infinite.
-  apply Rabs_def1; fourier.
- assert (He':e/2 > 0) by fourier.
- destruct (X _ He') as [N HN].
- clear X.
- exists N.
- intros n m Hn Hm.
- replace e with (e/2 + e/2)%R by field.
- set (g:=(fun n0 : nat => 1 * (1 / 2) ^ n0)) in *.
- assert (R_dist (sum_f_R0 g n) (sum_f_R0 g m) < e / 2 + e / 2).
-  apply Rle_lt_trans with (R_dist (sum_f_R0 g n) 2+R_dist 2 (sum_f_R0 g m))%R.
-   apply R_dist_tri.
-  replace (/(1 - 1/2)) with 2 in HN by field.
-  cut (forall n, (n >= N)%nat -> R_dist (sum_f_R0 g n) 2 < e/2)%R.
-   intros Z.
-   apply Rplus_lt_compat.
-    apply Z; assumption.
-   rewrite R_dist_sym.
+Let f:=fun n => (if HP n then (1/2)^n else 0)%R.
+
+Lemma cauchy_crit_geometric_dec_fun : Cauchy_crit_series f.
+intros e He.
+assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R).
+ apply GP_infinite.
+ apply Rabs_def1; fourier.
+assert (He':e/2 > 0) by fourier.
+destruct (X _ He') as [N HN].
+clear X.
+exists N.
+intros n m Hn Hm.
+replace e with (e/2 + e/2)%R by field.
+set (g:=(fun n0 : nat => 1 * (1 / 2) ^ n0)) in *.
+assert (R_dist (sum_f_R0 g n) (sum_f_R0 g m) < e / 2 + e / 2).
+ apply Rle_lt_trans with (R_dist (sum_f_R0 g n) 2+R_dist 2 (sum_f_R0 g m))%R.
+  apply R_dist_tri.
+ replace (/(1 - 1/2)) with 2 in HN by field.
+ cut (forall n, (n >= N)%nat -> R_dist (sum_f_R0 g n) 2 < e/2)%R.
+  intros Z.
+  apply Rplus_lt_compat.
    apply Z; assumption.
-  clear - HN He.
-  intros n Hn.
-  apply HN.
-  auto.
- eapply Rle_lt_trans;[|apply H].
- clear -positive_sums n.
- cut (forall n m, (m <= n)%nat -> R_dist (sum_f_R0 f n) (sum_f_R0 f m) <= R_dist (sum_f_R0 g n) (sum_f_R0 g m)).
-  intros H.
-  destruct (le_lt_dec m n).
-   apply H; assumption.
   rewrite R_dist_sym.
-  rewrite (R_dist_sym (sum_f_R0 g n)).
-  apply H; auto with *.
- clear n m.
- intros n m Hnm.
- unfold R_dist.
- cut (forall i : nat, (1 / 2) ^ i >= 0). intro RPosPow.
+  apply Z; assumption.
+ clear - HN He.
+ intros n Hn.
+ apply HN.
+ auto.
+eapply Rle_lt_trans;[|apply H].
+clear -ge_fun_sums_ge n.
+cut (forall n m, (m <= n)%nat -> R_dist (sum_f_R0 f n) (sum_f_R0 f m) <= R_dist (sum_f_R0 g n) (sum_f_R0 g m)).
+ intros H.
+ destruct (le_lt_dec m n).
+  apply H; assumption.
+ rewrite R_dist_sym.
+ rewrite (R_dist_sym (sum_f_R0 g n)).
+ apply H; auto with *.
+clear n m.
+intros n m Hnm.
+unfold R_dist.
+cut (forall i : nat, (1 / 2) ^ i >= 0). intro RPosPow.
+rewrite Rabs_pos_eq.
  rewrite Rabs_pos_eq.
-  rewrite Rabs_pos_eq.
-   cut (sum_f_R0 g m - sum_f_R0 f m <=  sum_f_R0 g n - sum_f_R0 f n).
-    intros; fourier.
+  cut (sum_f_R0 g m - sum_f_R0 f m <=  sum_f_R0 g n - sum_f_R0 f n).
+   intros; fourier.
    do 2 rewrite <- minus_sum.
- apply (positive_sums m n (fun i : nat => g i - f i) Hnm).
- intro i.
- unfold f, g.
- elim (HP i); intro; ring_simplify; auto with *.
- cut (sum_f_R0 g m <= sum_f_R0 g n). intro; fourier.
- apply (positive_sums m n g Hnm).
- intro. unfold g.
- ring_simplify.
- apply Rge_le.
- apply RPosPow.
- cut (sum_f_R0 f m <= sum_f_R0 f n). intro; fourier.
- apply (positive_sums m n f Hnm).
+   apply (ge_fun_sums_ge m n (fun i : nat => g i - f i) Hnm).
+   intro i.
+   unfold f, g.
+   elim (HP i); intro; ring_simplify; auto with *.
+  cut (sum_f_R0 g m <= sum_f_R0 g n). 
+   intro; fourier.
+  apply (ge_fun_sums_ge m n g Hnm).
+  intro. unfold g.
+  ring_simplify.
+  apply Rge_le.
+  apply RPosPow.
+ cut (sum_f_R0 f m <= sum_f_R0 f n).
+  intro; fourier.
+ apply (ge_fun_sums_ge m n f Hnm).
  intro; unfold f.
  elim (HP i); intro; simpl.
- apply Rge_le.
- apply RPosPow.
+  apply Rge_le.
+  apply RPosPow.
  auto with *.
- induction i.
- simpl. apply Rle_ge. auto with *.
- simpl. fourier.
+intro i.
+apply Rle_ge.
+apply pow_le.
+fourier.
+Qed.
 
- destruct (cv_cauchy_2 _ Hg).
+Lemma forall_dec : {forall n, P n} + {~forall n, P n}.
+Proof.
+destruct (cv_cauchy_2 _ cauchy_crit_geometric_dec_fun).
  cut (2 <= x <-> forall n : nat, P n).
  intro H.
  elim (Rle_dec 2 x); intro X.
  left; tauto.
  right; tauto.
-
- assert (A:Rabs(1/2) < 1) by (apply Rabs_def1; fourier).
- assert (A0:=(GP_infinite (1/2) A)).
- symmetry.
+assert (A:Rabs(1/2) < 1) by (apply Rabs_def1; fourier).
+assert (A0:=(GP_infinite (1/2) A)).
+symmetry.
  split; intro.
  replace 2 with (/ (1 - (1 / 2))) by field.
  unfold Pser, infinit_sum in A0.
  eapply Rle_cv_lim;[|unfold Un_cv; apply A0 |apply u].
  intros n.
  clear -n H.
- induction n; unfold f;simpl.
+  induction n; unfold f;simpl.
   destruct (HP 0); auto with *.
   elim n; auto.
  apply Rplus_le_compat; auto.
  destruct (HP (S n)); auto with *.
  elim n0; auto.
-
 intros n.
 destruct (HP n); auto.
 elim (RIneq.Rle_not_lt _ _ H).
@@ -173,12 +173,12 @@ assert (Z:  Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
   intros H;
   simpl; unfold g at 2;
   destruct (eq_nat_dec (S a) n).
-   rewrite IHa1.
-    ring.
+    rewrite IHa1.
+     ring.
+    omega.
+   ring_simplify.
+   apply IHa0.
    omega.
-  ring_simplify.
-  apply IHa0.
-  omega.
   elimtype False; omega.
  ring_simplify.
  apply IHa1.