← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Reals/Rlogic.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Reals/Rlogic.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(** * This module proves some logical properties of the axiomatics of Reals
 
10
 
 
11
1. Decidablity of arithmetical statements from
 
12
   the axiom that the order of the real numbers is decidable.
 
13
 
 
14
2. Derivability of the archimedean "axiom"
 
15
*)
 
16
 
 
17
(** 1- Proof of the decidablity of arithmetical statements from
 
18
excluded middle and the axiom that the order of the real numbers is
 
19
decidable. *)
 
20
 
 
21
(** Assuming a decidable predicate [P n], A series is constructed whose
 
22
[n]th term is 1/2^n if [P n] holds and 0 otherwise.  This sum reaches 2
 
23
only if [P n] holds for all [n], otherwise the sum is less than 2.
 
24
Comparing the sum to 2 decides if [forall n, P n] or [~forall n, P n] *)
 
25
 
 
26
(** One can iterate this lemma and use classical logic to decide any
 
27
statement in the arithmetical hierarchy. *)
 
28
 
 
29
(** Contributed by Cezary Kaliszyk and Russell O'Connor *)
 
30
 
 
31
Require Import ConstructiveEpsilon.
 
32
Require Import Rfunctions.
 
33
Require Import PartSum.
 
34
Require Import SeqSeries.
 
35
Require Import RiemannInt.
 
36
Require Import Fourier.
 
37
 
 
38
Section Arithmetical_dec.
 
39
 
 
40
Variable P : nat -> Prop.
 
41
Hypothesis HP : forall n, {P n} + {~P n}.
 
42
 
 
43
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).
 
44
intros m n f mn fpos.
 
45
replace (sum_f_R0 f m) with (sum_f_R0 f m + 0) by ring.
 
46
rewrite (tech2 f m n mn).
 
47
apply Rplus_le_compat_l.
 
48
 induction (n - S m)%nat; simpl in *.
 
49
 apply fpos.
 
50
replace 0 with (0 + 0) by ring.
 
51
apply (Rplus_le_compat _ _ _ _ IHn0 (fpos (S (m + S n0)%nat))).
 
52
Qed.
 
53
 
 
54
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).
 
55
intros m n f mn pos.
 
56
 elim (le_lt_or_eq _ _ mn).
 
57
 intro; apply ge_fun_sums_ge_lemma; assumption.
 
58
intro H; rewrite H; auto with *.
 
59
Qed.
 
60
 
 
61
Let f:=fun n => (if HP n then (1/2)^n else 0)%R.
 
62
 
 
63
Lemma cauchy_crit_geometric_dec_fun : Cauchy_crit_series f.
 
64
intros e He.
 
65
assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R).
 
66
 apply GP_infinite.
 
67
 apply Rabs_def1; fourier.
 
68
assert (He':e/2 > 0) by fourier.
 
69
destruct (X _ He') as [N HN].
 
70
clear X.
 
71
exists N.
 
72
intros n m Hn Hm.
 
73
replace e with (e/2 + e/2)%R by field.
 
74
set (g:=(fun n0 : nat => 1 * (1 / 2) ^ n0)) in *.
 
75
assert (R_dist (sum_f_R0 g n) (sum_f_R0 g m) < e / 2 + e / 2).
 
76
 apply Rle_lt_trans with (R_dist (sum_f_R0 g n) 2+R_dist 2 (sum_f_R0 g m))%R.
 
77
  apply R_dist_tri.
 
78
 replace (/(1 - 1/2)) with 2 in HN by field.
 
79
 cut (forall n, (n >= N)%nat -> R_dist (sum_f_R0 g n) 2 < e/2)%R.
 
80
  intros Z.
 
81
  apply Rplus_lt_compat.
 
82
   apply Z; assumption.
 
83
  rewrite R_dist_sym.
 
84
  apply Z; assumption.
 
85
 clear - HN He.
 
86
 intros n Hn.
 
87
 apply HN.
 
88
 auto.
 
89
eapply Rle_lt_trans;[|apply H].
 
90
clear -ge_fun_sums_ge n.
 
91
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)).
 
92
 intros H.
 
93
 destruct (le_lt_dec m n).
 
94
  apply H; assumption.
 
95
 rewrite R_dist_sym.
 
96
 rewrite (R_dist_sym (sum_f_R0 g n)).
 
97
 apply H; auto with *.
 
98
clear n m.
 
99
intros n m Hnm.
 
100
unfold R_dist.
 
101
cut (forall i : nat, (1 / 2) ^ i >= 0). intro RPosPow.
 
102
rewrite Rabs_pos_eq.
 
103
 rewrite Rabs_pos_eq.
 
104
  cut (sum_f_R0 g m - sum_f_R0 f m <=  sum_f_R0 g n - sum_f_R0 f n).
 
105
   intros; fourier.
 
106
   do 2 rewrite <- minus_sum.
 
107
   apply (ge_fun_sums_ge m n (fun i : nat => g i - f i) Hnm).
 
108
   intro i.
 
109
   unfold f, g.
 
110
   elim (HP i); intro; ring_simplify; auto with *.
 
111
  cut (sum_f_R0 g m <= sum_f_R0 g n). 
 
112
   intro; fourier.
 
113
  apply (ge_fun_sums_ge m n g Hnm).
 
114
  intro. unfold g.
 
115
  ring_simplify.
 
116
  apply Rge_le.
 
117
  apply RPosPow.
 
118
 cut (sum_f_R0 f m <= sum_f_R0 f n).
 
119
  intro; fourier.
 
120
 apply (ge_fun_sums_ge m n f Hnm).
 
121
 intro; unfold f.
 
122
 elim (HP i); intro; simpl.
 
123
  apply Rge_le.
 
124
  apply RPosPow.
 
125
 auto with *.
 
126
intro i.
 
127
apply Rle_ge.
 
128
apply pow_le.
 
129
fourier.
 
130
Qed.
 
131
 
 
132
Lemma forall_dec : {forall n, P n} + {~forall n, P n}.
 
133
Proof.
 
134
destruct (cv_cauchy_2 _ cauchy_crit_geometric_dec_fun).
 
135
 cut (2 <= x <-> forall n : nat, P n).
 
136
 intro H.
 
137
 elim (Rle_dec 2 x); intro X.
 
138
 left; tauto.
 
139
 right; tauto.
 
140
assert (A:Rabs(1/2) < 1) by (apply Rabs_def1; fourier).
 
141
assert (A0:=(GP_infinite (1/2) A)).
 
142
symmetry.
 
143
 split; intro.
 
144
 replace 2 with (/ (1 - (1 / 2))) by field.
 
145
 unfold Pser, infinite_sum in A0.
 
146
 eapply Rle_cv_lim;[|unfold Un_cv; apply A0 |apply u].
 
147
 intros n.
 
148
 clear -n H.
 
149
  induction n; unfold f;simpl.
 
150
  destruct (HP 0); auto with *.
 
151
  elim n; auto.
 
152
 apply Rplus_le_compat; auto.
 
153
 destruct (HP (S n)); auto with *.
 
154
 elim n0; auto.
 
155
intros n.
 
156
destruct (HP n); auto.
 
157
elim (RIneq.Rle_not_lt _ _ H).
 
158
assert (B:0< (1/2)^n).
 
159
 apply pow_lt.
 
160
 fourier.
 
161
apply Rle_lt_trans with (2-(1/2)^n);[|fourier].
 
162
replace (/(1-1/2))%R with 2 in A0 by field.
 
163
set (g:= fun m => if (eq_nat_dec m n) then (1/2)^n else 0).
 
164
assert (Z:  Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
 
165
 intros e He.
 
166
 exists n.
 
167
 intros a Ha.
 
168
 replace (sum_f_R0 g a) with ((1/2)^n).
 
169
  rewrite (R_dist_eq); assumption.
 
170
 symmetry.
 
171
 cut (forall a : nat, ((a >= n)%nat -> sum_f_R0 g a = (1 / 2) ^ n) /\ ((a < n)%nat -> sum_f_R0 g a = 0))%R.
 
172
  intros H0.
 
173
  destruct (H0 a).
 
174
  auto.
 
175
 clear - g.
 
176
 induction a.
 
177
  split;
 
178
   intros H;
 
179
   simpl; unfold g;
 
180
   destruct (eq_nat_dec 0 n); try reflexivity.
 
181
   elim f; auto with *.
 
182
  elimtype False; omega.
 
183
 destruct IHa as [IHa0 IHa1].
 
184
 split;
 
185
  intros H;
 
186
  simpl; unfold g at 2;
 
187
  destruct (eq_nat_dec (S a) n).
 
188
    rewrite IHa1.
 
189
     ring.
 
190
    omega.
 
191
   ring_simplify.
 
192
   apply IHa0.
 
193
   omega.
 
194
  elimtype False; omega.
 
195
 ring_simplify.
 
196
 apply IHa1.
 
197
 omega.
 
198
assert (C:=CV_minus _ _ _ _ A0 Z).
 
199
eapply Rle_cv_lim;[|apply u |apply C].
 
200
clear - n0 B.
 
201
intros m.
 
202
simpl.
 
203
induction m.
 
204
 simpl.
 
205
 unfold f, g.
 
206
 destruct (eq_nat_dec 0 n).
 
207
  destruct (HP 0).
 
208
   elim n0.
 
209
   congruence.
 
210
  clear -n.
 
211
  induction n; simpl; fourier.
 
212
 destruct (HP); simpl; fourier.
 
213
cut (f (S m) <= 1 * ((1 / 2) ^ (S m)) - g (S m)).
 
214
 intros L.
 
215
 eapply Rle_trans.
 
216
  simpl.
 
217
  apply Rplus_le_compat.
 
218
   apply IHm.
 
219
  apply L.
 
220
 simpl; fourier.
 
221
unfold f, g.
 
222
destruct (eq_nat_dec (S m) n).
 
223
 destruct (HP (S m)).
 
224
  elim n0.
 
225
  congruence.
 
226
 rewrite e.
 
227
 fourier.
 
228
destruct (HP (S m)).
 
229
 fourier.
 
230
ring_simplify.
 
231
apply pow_le.
 
232
fourier.
 
233
Qed.
 
234
 
 
235
Lemma sig_forall_dec :  {n | ~P n}+{forall n, P n}.
 
236
destruct forall_dec.
 
237
 right; assumption.
 
238
left.
 
239
apply constructive_indefinite_description_nat; auto.
 
240
 clear - HP.
 
241
 firstorder.
 
242
apply Classical_Pred_Type.not_all_ex_not.
 
243
assumption.
 
244
Qed.
 
245
 
 
246
End Arithmetical_dec.
 
247
 
 
248
(** 2- Derivability of the Archimedean axiom *)
 
249
 
 
250
(* This is a standard proof (it has been taken from PlanetMath). It is
 
251
formulated negatively so as to avoid the need for classical
 
252
logic. Using a proof of {n | ~P n}+{forall n, P n} (the one above or a
 
253
variant of it that does not need classical axioms) , we can in
 
254
principle also derive [up] and its [specification] *)
 
255
 
 
256
Theorem not_not_archimedean :
 
257
  forall r : R, ~ (forall n : nat, (INR n <= r)%R).
 
258
intros r H.
 
259
set (E := fun r => exists n : nat, r = INR n).
 
260
assert (exists x : R, E x) by
 
261
  (exists 0%R; simpl; red; exists 0%nat; reflexivity).
 
262
assert (bound E) by (exists r; intros x (m,H2); rewrite H2; apply H).
 
263
destruct (completeness E) as (M,(H3,H4)); try assumption.
 
264
set (M' := (M + -1)%R).
 
265
assert (H2 : ~ is_upper_bound E M').
 
266
  intro H5.
 
267
  assert (M <= M')%R by (apply H4; exact H5).
 
268
  apply (Rlt_not_le M M').
 
269
    unfold M' in |- *.
 
270
    pattern M at 2 in |- *.
 
271
    rewrite <- Rplus_0_l.
 
272
    pattern (0 + M)%R in |- *.
 
273
    rewrite Rplus_comm.
 
274
    rewrite <- (Rplus_opp_r 1).
 
275
    apply Rplus_lt_compat_l.
 
276
    rewrite Rplus_comm.
 
277
    apply Rlt_plus_1.
 
278
  assumption.
 
279
apply H2.
 
280
intros N (n,H7).
 
281
rewrite H7.
 
282
unfold M' in |- *.
 
283
assert (H5 : (INR (S n) <= M)%R) by (apply H3; exists (S n); reflexivity).
 
284
rewrite S_INR in H5.
 
285
assert (H6 : (INR n + 1 + -1 <= M + -1)%R).
 
286
  apply Rplus_le_compat_r.
 
287
  assumption.
 
288
rewrite Rplus_assoc in H6.
 
289
rewrite Rplus_opp_r in H6.
 
290
rewrite (Rplus_comm (INR n) 0) in H6.
 
291
rewrite Rplus_0_l in H6.
 
292
assumption.
 
293
Qed.