← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/R_Ifp.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/R_Ifp.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
(*i $Id: R_Ifp.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
10
 
 
11
(**********************************************************)
 
12
(** Complements for the reals.Integer and fractional part *)
 
13
(*                                                        *)
 
14
(**********************************************************)
 
15
 
 
16
Require Import Rbase.
 
17
Require Import Omega.
 
18
Open Local Scope R_scope.
 
19
 
 
20
(*********************************************************)
 
21
(** *    Fractional part                                 *)
 
22
(*********************************************************)
 
23
 
 
24
(**********)
 
25
Definition Int_part (r:R) : Z := (up r - 1)%Z.
 
26
 
 
27
(**********)
 
28
Definition frac_part (r:R) : R := r - IZR (Int_part r).
 
29
 
 
30
(**********)
 
31
Lemma tech_up : forall (r:R) (z:Z), r < IZR z -> IZR z <= r + 1 -> z = up r.
 
32
Proof.
 
33
  intros; generalize (archimed r); intro; elim H1; intros; clear H1;
 
34
    unfold Rgt in H2; unfold Rminus in H3;
 
35
      generalize (Rplus_le_compat_l r (IZR (up r) + - r) 1 H3); 
 
36
        intro; clear H3; rewrite (Rplus_comm (IZR (up r)) (- r)) in H1;
 
37
          rewrite <- (Rplus_assoc r (- r) (IZR (up r))) in H1;
 
38
            rewrite (Rplus_opp_r r) in H1; elim (Rplus_ne (IZR (up r))); 
 
39
              intros a b; rewrite b in H1; clear a b; apply (single_z_r_R1 r z (up r));
 
40
                auto with zarith real.
 
41
Qed.
 
42
 
 
43
(**********)
 
44
Lemma up_tech :
 
45
  forall (r:R) (z:Z), IZR z <= r -> r < IZR (z + 1) -> (z + 1)%Z = up r.
 
46
Proof.
 
47
  intros; generalize (Rplus_le_compat_l 1 (IZR z) r H); intro; clear H;
 
48
    rewrite (Rplus_comm 1 (IZR z)) in H1; rewrite (Rplus_comm 1 r) in H1;
 
49
      cut (1 = IZR 1); auto with zarith real.
 
50
  intro; generalize H1; pattern 1 at 1 in |- *; rewrite H; intro; clear H H1;
 
51
    rewrite <- (plus_IZR z 1) in H2; apply (tech_up r (z + 1));
 
52
      auto with zarith real.
 
53
Qed.
 
54
 
 
55
(**********)
 
56
Lemma fp_R0 : frac_part 0 = 0.
 
57
Proof.
 
58
  unfold frac_part in |- *; unfold Int_part in |- *; elim (archimed 0); intros;
 
59
    unfold Rminus in |- *; elim (Rplus_ne (- IZR (up 0 - 1))); 
 
60
      intros a b; rewrite b; clear a b; rewrite <- Z_R_minus; 
 
61
        cut (up 0 = 1%Z).
 
62
  intro; rewrite H1;
 
63
    rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (refl_equal (IZR 1))); 
 
64
      apply Ropp_0. 
 
65
  elim (archimed 0); intros; clear H2; unfold Rgt in H1;
 
66
    rewrite (Rminus_0_r (IZR (up 0))) in H0; generalize (lt_O_IZR (up 0) H1);
 
67
      intro; clear H1; generalize (le_IZR_R1 (up 0) H0); 
 
68
        intro; clear H H0; omega.
 
69
Qed.
 
70
 
 
71
(**********)
 
72
Lemma for_base_fp : forall r:R, IZR (up r) - r > 0 /\ IZR (up r) - r <= 1.
 
73
Proof.
 
74
  intro; split; cut (IZR (up r) > r /\ IZR (up r) - r <= 1).
 
75
  intro; elim H; intros.
 
76
  apply (Rgt_minus (IZR (up r)) r H0).
 
77
  apply archimed.
 
78
  intro; elim H; intros.
 
79
  exact H1.
 
80
  apply archimed.
 
81
Qed.
 
82
 
 
83
(**********)
 
84
Lemma base_fp : forall r:R, frac_part r >= 0 /\ frac_part r < 1.
 
85
Proof.
 
86
  intro; unfold frac_part in |- *; unfold Int_part in |- *; split.
 
87
     (*sup a O*)
 
88
  cut (r - IZR (up r) >= -1).
 
89
  rewrite <- Z_R_minus; simpl in |- *; intro; unfold Rminus in |- *;
 
90
    rewrite Ropp_plus_distr; rewrite <- Rplus_assoc;
 
91
      fold (r - IZR (up r)) in |- *; fold (r - IZR (up r) - -1) in |- *;
 
92
        apply Rge_minus; auto with zarith real.
 
93
  rewrite <- Ropp_minus_distr; apply Ropp_le_ge_contravar; elim (for_base_fp r);
 
94
    auto with zarith real.
 
95
    (*inf a 1*) 
 
96
  cut (r - IZR (up r) < 0).
 
97
  rewrite <- Z_R_minus; simpl in |- *; intro; unfold Rminus in |- *;
 
98
    rewrite Ropp_plus_distr; rewrite <- Rplus_assoc;
 
99
      fold (r - IZR (up r)) in |- *; rewrite Ropp_involutive; 
 
100
        elim (Rplus_ne 1); intros a b; pattern 1 at 2 in |- *; 
 
101
          rewrite <- a; clear a b; rewrite (Rplus_comm (r - IZR (up r)) 1);
 
102
            apply Rplus_lt_compat_l; auto with zarith real.
 
103
  elim (for_base_fp r); intros; rewrite <- Ropp_0; rewrite <- Ropp_minus_distr;
 
104
    apply Ropp_gt_lt_contravar; auto with zarith real.
 
105
Qed.
 
106
 
 
107
(*********************************************************)
 
108
(** *    Properties                                      *)
 
109
(*********************************************************)
 
110
 
 
111
(**********)
 
112
Lemma base_Int_part :
 
113
  forall r:R, IZR (Int_part r) <= r /\ IZR (Int_part r) - r > -1. 
 
114
Proof.
 
115
  intro; unfold Int_part in |- *; elim (archimed r); intros.
 
116
  split; rewrite <- (Z_R_minus (up r) 1); simpl in |- *.
 
117
  generalize (Rle_minus (IZR (up r) - r) 1 H0); intro; unfold Rminus in H1;
 
118
    rewrite (Rplus_assoc (IZR (up r)) (- r) (-1)) in H1;
 
119
      rewrite (Rplus_comm (- r) (-1)) in H1;
 
120
        rewrite <- (Rplus_assoc (IZR (up r)) (-1) (- r)) in H1;
 
121
          fold (IZR (up r) - 1) in H1; fold (IZR (up r) - 1 - r) in H1;
 
122
            apply Rminus_le; auto with zarith real.
 
123
  generalize (Rplus_gt_compat_l (-1) (IZR (up r)) r H); intro;
 
124
    rewrite (Rplus_comm (-1) (IZR (up r))) in H1;
 
125
      generalize (Rplus_gt_compat_l (- r) (IZR (up r) + -1) (-1 + r) H1); 
 
126
        intro; clear H H0 H1; rewrite (Rplus_comm (- r) (IZR (up r) + -1)) in H2;
 
127
          fold (IZR (up r) - 1) in H2; fold (IZR (up r) - 1 - r) in H2;
 
128
            rewrite (Rplus_comm (- r) (-1 + r)) in H2;
 
129
              rewrite (Rplus_assoc (-1) r (- r)) in H2; rewrite (Rplus_opp_r r) in H2;
 
130
                elim (Rplus_ne (-1)); intros a b; rewrite a in H2; 
 
131
                  clear a b; auto with zarith real.  
 
132
Qed.
 
133
 
 
134
(**********)
 
135
Lemma Int_part_INR : forall n:nat, Int_part (INR n) = Z_of_nat n.
 
136
Proof.
 
137
  intros n; unfold Int_part in |- *.
 
138
  cut (up (INR n) = (Z_of_nat n + Z_of_nat 1)%Z).
 
139
  intros H'; rewrite H'; simpl in |- *; ring.
 
140
  apply sym_equal; apply tech_up; auto.
 
141
  replace (Z_of_nat n + Z_of_nat 1)%Z with (Z_of_nat (S n)).
 
142
  repeat rewrite <- INR_IZR_INZ.
 
143
  apply lt_INR; auto.
 
144
  rewrite Zplus_comm; rewrite <- Znat.inj_plus; simpl in |- *; auto.
 
145
  rewrite plus_IZR; simpl in |- *; auto with real.
 
146
  repeat rewrite <- INR_IZR_INZ; auto with real.
 
147
Qed.
 
148
 
 
149
(**********)
 
150
Lemma fp_nat : forall r:R, frac_part r = 0 ->  exists c : Z, r = IZR c.
 
151
Proof.
 
152
  unfold frac_part in |- *; intros; split with (Int_part r);
 
153
    apply Rminus_diag_uniq; auto with zarith real.
 
154
Qed.
 
155
 
 
156
(**********)
 
157
Lemma R0_fp_O : forall r:R, 0 <> frac_part r -> 0 <> r.
 
158
Proof.
 
159
  red in |- *; intros; rewrite <- H0 in H; generalize fp_R0; intro;
 
160
    auto with zarith real.
 
161
Qed.
 
162
 
 
163
(**********)
 
164
Lemma Rminus_Int_part1 :
 
165
  forall r1 r2:R,
 
166
    frac_part r1 >= frac_part r2 ->
 
167
    Int_part (r1 - r2) = (Int_part r1 - Int_part r2)%Z.
 
168
Proof.
 
169
  intros; elim (base_fp r1); elim (base_fp r2); intros;
 
170
    generalize (Rge_le (frac_part r2) 0 H0); intro; clear H0;
 
171
      generalize (Ropp_le_ge_contravar 0 (frac_part r2) H4); 
 
172
        intro; clear H4; rewrite Ropp_0 in H0;
 
173
          generalize (Rge_le 0 (- frac_part r2) H0); intro; 
 
174
            clear H0; generalize (Rge_le (frac_part r1) 0 H2); 
 
175
              intro; clear H2; generalize (Ropp_lt_gt_contravar (frac_part r2) 1 H1);
 
176
                intro; clear H1; unfold Rgt in H2;
 
177
                  generalize
 
178
                    (sum_inequa_Rle_lt 0 (frac_part r1) 1 (-1) (- frac_part r2) 0 H0 H3 H2 H4);
 
179
                    intro; elim H1; intros; clear H1; elim (Rplus_ne 1); 
 
180
                      intros a b; rewrite a in H6; clear a b H5;
 
181
                        generalize (Rge_minus (frac_part r1) (frac_part r2) H); 
 
182
                          intro; clear H; fold (frac_part r1 - frac_part r2) in H6;
 
183
                            generalize (Rge_le (frac_part r1 - frac_part r2) 0 H1); 
 
184
                              intro; clear H1 H3 H4 H0 H2; unfold frac_part in H6, H;
 
185
                                unfold Rminus in H6, H;
 
186
                                  rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2))) in H;
 
187
                                    rewrite (Ropp_involutive (IZR (Int_part r2))) in H;
 
188
                                      rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)))
 
189
                                        in H;
 
190
                                        rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)))
 
191
                                          in H; rewrite (Rplus_comm (- IZR (Int_part r1)) (- r2)) in H;
 
192
                                            rewrite (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2))) in H;
 
193
                                              rewrite <- (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)))
 
194
                                                in H; rewrite (Rplus_comm (- IZR (Int_part r1)) (IZR (Int_part r2))) in H;
 
195
                                                  fold (r1 - r2) in H; fold (IZR (Int_part r2) - IZR (Int_part r1)) in H;
 
196
                                                    generalize
 
197
                                                      (Rplus_le_compat_l (IZR (Int_part r1) - IZR (Int_part r2)) 0
 
198
                                                        (r1 - r2 + (IZR (Int_part r2) - IZR (Int_part r1))) H); 
 
199
                                                      intro; clear H;
 
200
                                                        rewrite (Rplus_comm (r1 - r2) (IZR (Int_part r2) - IZR (Int_part r1))) in H0;
 
201
                                                          rewrite <-
 
202
                                                            (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2))
 
203
                                                              (IZR (Int_part r2) - IZR (Int_part r1)) (r1 - r2))
 
204
                                                            in H0; unfold Rminus in H0; fold (r1 - r2) in H0;
 
205
                                                              rewrite
 
206
                                                                (Rplus_assoc (IZR (Int_part r1)) (- IZR (Int_part r2))
 
207
                                                                  (IZR (Int_part r2) + - IZR (Int_part r1))) in H0;
 
208
                                                                rewrite <-
 
209
                                                                  (Rplus_assoc (- IZR (Int_part r2)) (IZR (Int_part r2))
 
210
                                                                    (- IZR (Int_part r1))) in H0;
 
211
                                                                  rewrite (Rplus_opp_l (IZR (Int_part r2))) in H0;
 
212
                                                                    elim (Rplus_ne (- IZR (Int_part r1))); intros a b; 
 
213
                                                                      rewrite b in H0; clear a b;
 
214
                                                                        elim (Rplus_ne (IZR (Int_part r1) + - IZR (Int_part r2))); 
 
215
                                                                          intros a b; rewrite a in H0; clear a b;
 
216
                                                                            rewrite (Rplus_opp_r (IZR (Int_part r1))) in H0; elim (Rplus_ne (r1 - r2));
 
217
                                                                              intros a b; rewrite b in H0; clear a b;
 
218
                                                                                fold (IZR (Int_part r1) - IZR (Int_part r2)) in H0;
 
219
                                                                                  rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2))) in H6;
 
220
                                                                                    rewrite (Ropp_involutive (IZR (Int_part r2))) in H6;
 
221
                                                                                      rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)))
 
222
                                                                                        in H6;
 
223
                                                                                        rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)))
 
224
                                                                                          in H6; rewrite (Rplus_comm (- IZR (Int_part r1)) (- r2)) in H6;
 
225
                                                                                            rewrite (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2))) in H6;
 
226
                                                                                              rewrite <- (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)))
 
227
                                                                                                in H6;
 
228
                                                                                                rewrite (Rplus_comm (- IZR (Int_part r1)) (IZR (Int_part r2))) in H6;
 
229
                                                                                                  fold (r1 - r2) in H6; fold (IZR (Int_part r2) - IZR (Int_part r1)) in H6;
 
230
                                                                                                    generalize
 
231
                                                                                                      (Rplus_lt_compat_l (IZR (Int_part r1) - IZR (Int_part r2))
 
232
                                                                                                        (r1 - r2 + (IZR (Int_part r2) - IZR (Int_part r1))) 1 H6); 
 
233
                                                                                                      intro; clear H6;
 
234
                                                                                                        rewrite (Rplus_comm (r1 - r2) (IZR (Int_part r2) - IZR (Int_part r1))) in H;
 
235
                                                                                                          rewrite <-
 
236
                                                                                                            (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2))
 
237
                                                                                                              (IZR (Int_part r2) - IZR (Int_part r1)) (r1 - r2))
 
238
                                                                                                            in H;
 
239
                                                                                                            rewrite <- (Ropp_minus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
 
240
                                                                                                              rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H;
 
241
                                                                                                                elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H; 
 
242
                                                                                                                  clear a b; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
 
243
                                                                                                                    rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; 
 
244
                                                                                                                      cut (1 = IZR 1); auto with zarith real.
 
245
  intro; rewrite H1 in H; clear H1;
 
246
    rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H;
 
247
      generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); 
 
248
        intros; clear H H0; unfold Int_part at 1 in |- *; 
 
249
          omega.
 
250
Qed.
 
251
 
 
252
(**********)
 
253
Lemma Rminus_Int_part2 :
 
254
  forall r1 r2:R,
 
255
    frac_part r1 < frac_part r2 ->
 
256
    Int_part (r1 - r2) = (Int_part r1 - Int_part r2 - 1)%Z.
 
257
Proof.
 
258
  intros; elim (base_fp r1); elim (base_fp r2); intros;
 
259
    generalize (Rge_le (frac_part r2) 0 H0); intro; clear H0;
 
260
      generalize (Ropp_le_ge_contravar 0 (frac_part r2) H4); 
 
261
        intro; clear H4; rewrite Ropp_0 in H0;
 
262
          generalize (Rge_le 0 (- frac_part r2) H0); intro; 
 
263
            clear H0; generalize (Rge_le (frac_part r1) 0 H2); 
 
264
              intro; clear H2; generalize (Ropp_lt_gt_contravar (frac_part r2) 1 H1);
 
265
                intro; clear H1; unfold Rgt in H2;
 
266
                  generalize
 
267
                    (sum_inequa_Rle_lt 0 (frac_part r1) 1 (-1) (- frac_part r2) 0 H0 H3 H2 H4);
 
268
                    intro; elim H1; intros; clear H1; elim (Rplus_ne (-1)); 
 
269
                      intros a b; rewrite b in H5; clear a b H6;
 
270
                        generalize (Rlt_minus (frac_part r1) (frac_part r2) H); 
 
271
                          intro; clear H; fold (frac_part r1 - frac_part r2) in H5; 
 
272
                            clear H3 H4 H0 H2; unfold frac_part in H5, H1; unfold Rminus in H5, H1;
 
273
                              rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2))) in H5;
 
274
                                rewrite (Ropp_involutive (IZR (Int_part r2))) in H5;
 
275
                                  rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)))
 
276
                                    in H5;
 
277
                                    rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)))
 
278
                                      in H5; rewrite (Rplus_comm (- IZR (Int_part r1)) (- r2)) in H5;
 
279
                                        rewrite (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2))) in H5;
 
280
                                          rewrite <- (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)))
 
281
                                            in H5;
 
282
                                            rewrite (Rplus_comm (- IZR (Int_part r1)) (IZR (Int_part r2))) in H5;
 
283
                                              fold (r1 - r2) in H5; fold (IZR (Int_part r2) - IZR (Int_part r1)) in H5;
 
284
                                                generalize
 
285
                                                  (Rplus_lt_compat_l (IZR (Int_part r1) - IZR (Int_part r2)) (-1)
 
286
                                                    (r1 - r2 + (IZR (Int_part r2) - IZR (Int_part r1))) H5); 
 
287
                                                  intro; clear H5;
 
288
                                                    rewrite (Rplus_comm (r1 - r2) (IZR (Int_part r2) - IZR (Int_part r1))) in H;
 
289
                                                      rewrite <-
 
290
                                                        (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2))
 
291
                                                          (IZR (Int_part r2) - IZR (Int_part r1)) (r1 - r2))
 
292
                                                        in H; unfold Rminus in H; fold (r1 - r2) in H;
 
293
                                                          rewrite
 
294
                                                            (Rplus_assoc (IZR (Int_part r1)) (- IZR (Int_part r2))
 
295
                                                              (IZR (Int_part r2) + - IZR (Int_part r1))) in H;
 
296
                                                            rewrite <-
 
297
                                                              (Rplus_assoc (- IZR (Int_part r2)) (IZR (Int_part r2))
 
298
                                                                (- IZR (Int_part r1))) in H;
 
299
                                                              rewrite (Rplus_opp_l (IZR (Int_part r2))) in H;
 
300
                                                                elim (Rplus_ne (- IZR (Int_part r1))); intros a b; 
 
301
                                                                  rewrite b in H; clear a b; rewrite (Rplus_opp_r (IZR (Int_part r1))) in H;
 
302
                                                                    elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H; 
 
303
                                                                      clear a b; fold (IZR (Int_part r1) - IZR (Int_part r2)) in H;
 
304
                                                                        fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H;
 
305
                                                                          rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2))) in H1;
 
306
                                                                            rewrite (Ropp_involutive (IZR (Int_part r2))) in H1;
 
307
                                                                              rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)))
 
308
                                                                                in H1;
 
309
                                                                                rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)))
 
310
                                                                                  in H1; rewrite (Rplus_comm (- IZR (Int_part r1)) (- r2)) in H1;
 
311
                                                                                    rewrite (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
 
312
                                                                                      rewrite <- (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)))
 
313
                                                                                        in H1;
 
314
                                                                                        rewrite (Rplus_comm (- IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
 
315
                                                                                          fold (r1 - r2) in H1; fold (IZR (Int_part r2) - IZR (Int_part r1)) in H1;
 
316
                                                                                            generalize
 
317
                                                                                              (Rplus_lt_compat_l (IZR (Int_part r1) - IZR (Int_part r2))
 
318
                                                                                                (r1 - r2 + (IZR (Int_part r2) - IZR (Int_part r1))) 0 H1); 
 
319
                                                                                              intro; clear H1;
 
320
                                                                                                rewrite (Rplus_comm (r1 - r2) (IZR (Int_part r2) - IZR (Int_part r1))) in H0;
 
321
                                                                                                  rewrite <-
 
322
                                                                                                    (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2))
 
323
                                                                                                      (IZR (Int_part r2) - IZR (Int_part r1)) (r1 - r2))
 
324
                                                                                                    in H0;
 
325
                                                                                                    rewrite <- (Ropp_minus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
 
326
                                                                                                      rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H0;
 
327
                                                                                                        elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H0; 
 
328
                                                                                                          clear a b; rewrite <- (Rplus_opp_l 1) in H0;
 
329
                                                                                                            rewrite <- (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2)) (-1) 1)
 
330
                                                                                                              in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0;
 
331
                                                                                                                rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
 
332
                                                                                                                  rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; 
 
333
                                                                                                                    cut (1 = IZR 1); auto with zarith real.
 
334
  intro; rewrite H1 in H; rewrite H1 in H0; clear H1;
 
335
    rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H;
 
336
      rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0;
 
337
        rewrite <- (plus_IZR (Int_part r1 - Int_part r2 - 1) 1) in H0;
 
338
          generalize (Rlt_le (IZR (Int_part r1 - Int_part r2 - 1)) (r1 - r2) H); 
 
339
            intro; clear H;
 
340
              generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0); 
 
341
                intros; clear H0 H1; unfold Int_part at 1 in |- *; 
 
342
                  omega.
 
343
Qed.
 
344
 
 
345
(**********)
 
346
Lemma Rminus_fp1 :
 
347
  forall r1 r2:R,
 
348
    frac_part r1 >= frac_part r2 ->
 
349
    frac_part (r1 - r2) = frac_part r1 - frac_part r2.
 
350
Proof.
 
351
  intros; unfold frac_part in |- *; generalize (Rminus_Int_part1 r1 r2 H);
 
352
    intro; rewrite H0; rewrite <- (Z_R_minus (Int_part r1) (Int_part r2));
 
353
      unfold Rminus in |- *;
 
354
        rewrite (Ropp_plus_distr (IZR (Int_part r1)) (- IZR (Int_part r2)));
 
355
          rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2)));
 
356
            rewrite (Ropp_involutive (IZR (Int_part r2)));
 
357
              rewrite (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)));
 
358
                rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)));
 
359
                  rewrite <- (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2)));
 
360
                    rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)));
 
361
                      rewrite (Rplus_comm (- r2) (- IZR (Int_part r1))); 
 
362
                        auto with zarith real.
 
363
Qed.
 
364
 
 
365
(**********)
 
366
Lemma Rminus_fp2 :
 
367
  forall r1 r2:R,
 
368
    frac_part r1 < frac_part r2 ->
 
369
    frac_part (r1 - r2) = frac_part r1 - frac_part r2 + 1.
 
370
Proof.
 
371
  intros; unfold frac_part in |- *; generalize (Rminus_Int_part2 r1 r2 H);
 
372
    intro; rewrite H0; rewrite <- (Z_R_minus (Int_part r1 - Int_part r2) 1);
 
373
      rewrite <- (Z_R_minus (Int_part r1) (Int_part r2)); 
 
374
        unfold Rminus in |- *;
 
375
          rewrite
 
376
            (Ropp_plus_distr (IZR (Int_part r1) + - IZR (Int_part r2)) (- IZR 1))
 
377
            ; rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2)));
 
378
              rewrite (Ropp_involutive (IZR 1));
 
379
                rewrite (Ropp_involutive (IZR (Int_part r2)));
 
380
                  rewrite (Ropp_plus_distr (IZR (Int_part r1)));
 
381
                    rewrite (Ropp_involutive (IZR (Int_part r2))); simpl in |- *;
 
382
                      rewrite <-
 
383
                        (Rplus_assoc (r1 + - r2) (- IZR (Int_part r1) + IZR (Int_part r2)) 1)
 
384
                        ; rewrite (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)));
 
385
                          rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)));
 
386
                            rewrite <- (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2)));
 
387
                              rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)));
 
388
                                rewrite (Rplus_comm (- r2) (- IZR (Int_part r1))); 
 
389
                                  auto with zarith real.
 
390
Qed.
 
391
 
 
392
(**********)
 
393
Lemma plus_Int_part1 :
 
394
  forall r1 r2:R,
 
395
    frac_part r1 + frac_part r2 >= 1 ->
 
396
    Int_part (r1 + r2) = (Int_part r1 + Int_part r2 + 1)%Z.
 
397
Proof.
 
398
  intros; generalize (Rge_le (frac_part r1 + frac_part r2) 1 H); intro; clear H;
 
399
    elim (base_fp r1); elim (base_fp r2); intros; clear H H2;
 
400
      generalize (Rplus_lt_compat_l (frac_part r2) (frac_part r1) 1 H3); 
 
401
        intro; clear H3; generalize (Rplus_lt_compat_l 1 (frac_part r2) 1 H1); 
 
402
          intro; clear H1; rewrite (Rplus_comm 1 (frac_part r2)) in H2;
 
403
            generalize
 
404
              (Rlt_trans (frac_part r2 + frac_part r1) (frac_part r2 + 1) 2 H H2); 
 
405
              intro; clear H H2; rewrite (Rplus_comm (frac_part r2) (frac_part r1)) in H1;
 
406
                unfold frac_part in H0, H1; unfold Rminus in H0, H1;
 
407
                  rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)))
 
408
                    in H1; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H1;
 
409
                      rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2)
 
410
                        in H1;
 
411
                        rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H1;
 
412
                          rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)))
 
413
                            in H1;
 
414
                            rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
 
415
                              rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)))
 
416
                                in H0; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H0;
 
417
                                  rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2)
 
418
                                    in H0;
 
419
                                    rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H0;
 
420
                                      rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)))
 
421
                                        in H0;
 
422
                                        rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
 
423
                                          generalize
 
424
                                            (Rplus_le_compat_l (IZR (Int_part r1) + IZR (Int_part r2)) 1
 
425
                                              (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) H0); 
 
426
                                            intro; clear H0;
 
427
                                              generalize
 
428
                                                (Rplus_lt_compat_l (IZR (Int_part r1) + IZR (Int_part r2))
 
429
                                                  (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) 2 H1); 
 
430
                                                intro; clear H1;
 
431
                                                  rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))))
 
432
                                                    in H;
 
433
                                                    rewrite <-
 
434
                                                      (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2))
 
435
                                                        (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2))
 
436
                                                      in H; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H;
 
437
                                                        elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H; 
 
438
                                                          clear a b;
 
439
                                                            rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))))
 
440
                                                              in H0;
 
441
                                                              rewrite <-
 
442
                                                                (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2))
 
443
                                                                  (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2))
 
444
                                                                in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0;
 
445
                                                                  elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H0; 
 
446
                                                                    clear a b;
 
447
                                                                      rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0;
 
448
                                                                        cut (1 = IZR 1); auto with zarith real.
 
449
  intro; rewrite H1 in H0; rewrite H1 in H; clear H1;
 
450
    rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H;
 
451
      rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0;
 
452
        rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H;
 
453
          rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0;
 
454
            rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0;
 
455
              generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0); 
 
456
                intro; clear H H0; unfold Int_part at 1 in |- *; omega.
 
457
Qed.
 
458
 
 
459
(**********)
 
460
Lemma plus_Int_part2 :
 
461
  forall r1 r2:R,
 
462
    frac_part r1 + frac_part r2 < 1 ->
 
463
    Int_part (r1 + r2) = (Int_part r1 + Int_part r2)%Z.
 
464
Proof.
 
465
  intros; elim (base_fp r1); elim (base_fp r2); intros; clear H1 H3;
 
466
    generalize (Rge_le (frac_part r2) 0 H0); intro; clear H0;
 
467
      generalize (Rge_le (frac_part r1) 0 H2); intro; clear H2;
 
468
        generalize (Rplus_le_compat_l (frac_part r1) 0 (frac_part r2) H1); 
 
469
          intro; clear H1; elim (Rplus_ne (frac_part r1)); intros a b; 
 
470
            rewrite a in H2; clear a b;
 
471
              generalize (Rle_trans 0 (frac_part r1) (frac_part r1 + frac_part r2) H0 H2);
 
472
                intro; clear H0 H2; unfold frac_part in H, H1; unfold Rminus in H, H1;
 
473
                  rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)))
 
474
                    in H1; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H1;
 
475
                      rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2)
 
476
                        in H1;
 
477
                        rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H1;
 
478
                          rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)))
 
479
                            in H1;
 
480
                            rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
 
481
                              rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)))
 
482
                                in H; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H;
 
483
                                  rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2) in H;
 
484
                                    rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H;
 
485
                                      rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)))
 
486
                                        in H;
 
487
                                        rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
 
488
                                          generalize
 
489
                                            (Rplus_le_compat_l (IZR (Int_part r1) + IZR (Int_part r2)) 0
 
490
                                              (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) H1); 
 
491
                                            intro; clear H1;
 
492
                                              generalize
 
493
                                                (Rplus_lt_compat_l (IZR (Int_part r1) + IZR (Int_part r2))
 
494
                                                  (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) 1 H); 
 
495
                                                intro; clear H;
 
496
                                                  rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))))
 
497
                                                    in H1;
 
498
                                                    rewrite <-
 
499
                                                      (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2))
 
500
                                                        (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2))
 
501
                                                      in H1; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H1;
 
502
                                                        elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H1; 
 
503
                                                          clear a b;
 
504
                                                            rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))))
 
505
                                                              in H0;
 
506
                                                              rewrite <-
 
507
                                                                (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2))
 
508
                                                                  (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2))
 
509
                                                                in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0;
 
510
                                                                  elim (Rplus_ne (IZR (Int_part r1) + IZR (Int_part r2))); 
 
511
                                                                    intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2));
 
512
                                                                      intros a b; rewrite b in H0; clear a b; cut (1 = IZR 1);
 
513
                                                                        auto with zarith real.
 
514
  intro; rewrite H in H1; clear H;
 
515
    rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0;
 
516
      rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1;
 
517
        rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1;
 
518
          generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1); 
 
519
            intro; clear H0 H1; unfold Int_part at 1 in |- *; 
 
520
              omega.
 
521
Qed.
 
522
 
 
523
(**********)
 
524
Lemma plus_frac_part1 :
 
525
  forall r1 r2:R,
 
526
    frac_part r1 + frac_part r2 >= 1 ->
 
527
    frac_part (r1 + r2) = frac_part r1 + frac_part r2 - 1.
 
528
Proof.
 
529
  intros; unfold frac_part in |- *; generalize (plus_Int_part1 r1 r2 H); intro;
 
530
    rewrite H0; rewrite (plus_IZR (Int_part r1 + Int_part r2) 1);
 
531
      rewrite (plus_IZR (Int_part r1) (Int_part r2)); simpl in |- *;
 
532
        unfold Rminus at 3 4 in |- *;
 
533
          rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)));
 
534
            rewrite (Rplus_comm r2 (- IZR (Int_part r2)));
 
535
              rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2);
 
536
                rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2);
 
537
                  rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)));
 
538
                    rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2)));
 
539
                      unfold Rminus in |- *;
 
540
                        rewrite
 
541
                          (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-1))
 
542
                          ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1);
 
543
                            trivial with zarith real.
 
544
Qed.
 
545
 
 
546
(**********)
 
547
Lemma plus_frac_part2 :
 
548
  forall r1 r2:R,
 
549
    frac_part r1 + frac_part r2 < 1 ->
 
550
    frac_part (r1 + r2) = frac_part r1 + frac_part r2.
 
551
Proof.
 
552
  intros; unfold frac_part in |- *; generalize (plus_Int_part2 r1 r2 H); intro;
 
553
    rewrite H0; rewrite (plus_IZR (Int_part r1) (Int_part r2));
 
554
      unfold Rminus at 2 3 in |- *;
 
555
        rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)));
 
556
          rewrite (Rplus_comm r2 (- IZR (Int_part r2)));
 
557
            rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2);
 
558
              rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2);
 
559
                rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)));
 
560
                  rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2)));
 
561
                    unfold Rminus in |- *; trivial with zarith real.
 
562
Qed.