← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/ArithProp.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/ArithProp.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: ArithProp.v 9454 2006-12-15 15:30:59Z bgregoir $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rbasic_fun.
 
13
Require Import Even.
 
14
Require Import Div2.
 
15
Require Import ArithRing.
 
16
 
 
17
Open Local Scope Z_scope.
 
18
Open Local Scope R_scope.
 
19
 
 
20
Lemma minus_neq_O : forall n i:nat, (i < n)%nat -> (n - i)%nat <> 0%nat.
 
21
Proof.
 
22
  intros; red in |- *; intro.
 
23
  cut (forall n m:nat, (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m).
 
24
  intro; assert (H2 := H1 _ _ (lt_le_weak _ _ H) H0); rewrite H2 in H;
 
25
    elim (lt_irrefl _ H).
 
26
  set (R := fun n m:nat => (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m).
 
27
  cut
 
28
    ((forall n m:nat, R n m) ->
 
29
      forall n0 m:nat, (m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m).
 
30
  intro; apply H1.
 
31
  apply nat_double_ind.
 
32
  unfold R in |- *; intros; inversion H2; reflexivity.
 
33
  unfold R in |- *; intros; simpl in H3; assumption.
 
34
  unfold R in |- *; intros; simpl in H4; assert (H5 := le_S_n _ _ H3);
 
35
    assert (H6 := H2 H5 H4); rewrite H6; reflexivity.
 
36
  unfold R in |- *; intros; apply H1; assumption.
 
37
Qed.
 
38
 
 
39
Lemma le_minusni_n : forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat.
 
40
Proof.
 
41
  set (R := fun m n:nat => (n <= m)%nat -> (m - n <= m)%nat).
 
42
  cut
 
43
    ((forall m n:nat, R m n) -> forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat).
 
44
  intro; apply H.
 
45
  apply nat_double_ind.
 
46
  unfold R in |- *; intros; simpl in |- *; apply le_n.
 
47
  unfold R in |- *; intros; simpl in |- *; apply le_n.
 
48
  unfold R in |- *; intros; simpl in |- *; apply le_trans with n.
 
49
  apply H0; apply le_S_n; assumption.
 
50
  apply le_n_Sn.
 
51
  unfold R in |- *; intros; apply H; assumption.
 
52
Qed.
 
53
 
 
54
Lemma lt_minus_O_lt : forall m n:nat, (m < n)%nat -> (0 < n - m)%nat.
 
55
Proof.
 
56
  intros n m; pattern n, m in |- *; apply nat_double_ind;
 
57
    [ intros; rewrite <- minus_n_O; assumption
 
58
      | intros; elim (lt_n_O _ H)
 
59
      | intros; simpl in |- *; apply H; apply lt_S_n; assumption ].
 
60
Qed.
 
61
 
 
62
Lemma even_odd_cor :
 
63
  forall n:nat,  exists p : nat, n = (2 * p)%nat \/ n = S (2 * p).
 
64
Proof.
 
65
  intro.
 
66
  assert (H := even_or_odd n).
 
67
  exists (div2 n).
 
68
  assert (H0 := even_odd_double n).
 
69
  elim H0; intros.
 
70
  elim H1; intros H3 _.
 
71
  elim H2; intros H4 _.
 
72
  replace (2 * div2 n)%nat with (double (div2 n)).
 
73
  elim H; intro.
 
74
  left.
 
75
  apply H3; assumption.
 
76
  right.
 
77
  apply H4; assumption.
 
78
  unfold double in |- *;ring.
 
79
Qed.
 
80
 
 
81
  (* 2m <= 2n => m<=n *)
 
82
Lemma le_double : forall m n:nat, (2 * m <= 2 * n)%nat -> (m <= n)%nat.
 
83
Proof.
 
84
  intros; apply INR_le.
 
85
  assert (H1 := le_INR _ _ H).
 
86
  do 2 rewrite mult_INR in H1.
 
87
  apply Rmult_le_reg_l with (INR 2).
 
88
  replace (INR 2) with 2; [ prove_sup0 | reflexivity ].
 
89
  assumption.
 
90
Qed.
 
91
 
 
92
(** Here, we have the euclidian division *)
 
93
(** This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=kPI *)
 
94
Lemma euclidian_division :
 
95
  forall x y:R,
 
96
    y <> 0 ->
 
97
    exists k : Z, (exists r : R, x = IZR k * y + r /\ 0 <= r < Rabs y).
 
98
Proof.
 
99
  intros.
 
100
  set
 
101
    (k0 :=
 
102
      match Rcase_abs y with
 
103
        | left _ => (1 - up (x / - y))%Z
 
104
        | right _ => (up (x / y) - 1)%Z
 
105
      end).
 
106
  exists k0.
 
107
  exists (x - IZR k0 * y).
 
108
  split.
 
109
  ring.
 
110
  unfold k0 in |- *; case (Rcase_abs y); intro.
 
111
  assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl in |- *;
 
112
    unfold Rminus in |- *.
 
113
  replace (- ((1 + - IZR (up (x / - y))) * y)) with
 
114
    ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ].
 
115
  split.
 
116
  apply Rmult_le_reg_l with (/ - y).
 
117
  apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact r.
 
118
  rewrite Rmult_0_r; rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r;
 
119
    rewrite <- Ropp_inv_permute; [ idtac | assumption ].
 
120
  rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse;
 
121
    rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ].
 
122
  apply Rplus_le_reg_l with (IZR (up (x / - y)) - x / - y).
 
123
  rewrite Rplus_0_r; unfold Rdiv in |- *; pattern (/ - y) at 4 in |- *;
 
124
    rewrite <- Ropp_inv_permute; [ idtac | assumption ].
 
125
  replace
 
126
    (IZR (up (x * / - y)) - x * - / y +
 
127
      (- (x * / y) + - (IZR (up (x * / - y)) - 1))) with 1; 
 
128
    [ idtac | ring ].
 
129
  elim H0; intros _ H1; unfold Rdiv in H1; exact H1.
 
130
  rewrite (Rabs_left _ r); apply Rmult_lt_reg_l with (/ - y).
 
131
  apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact r.
 
132
  rewrite <- Rinv_l_sym.
 
133
  rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r;
 
134
    rewrite <- Ropp_inv_permute; [ idtac | assumption ].
 
135
  rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse;
 
136
    rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ];
 
137
      apply Rplus_lt_reg_r with (IZR (up (x / - y)) - 1).
 
138
  replace (IZR (up (x / - y)) - 1 + 1) with (IZR (up (x / - y)));
 
139
    [ idtac | ring ].
 
140
  replace (IZR (up (x / - y)) - 1 + (- (x * / y) + - (IZR (up (x / - y)) - 1)))
 
141
    with (- (x * / y)); [ idtac | ring ].
 
142
  rewrite <- Ropp_mult_distr_r_reverse; rewrite (Ropp_inv_permute _ H); elim H0;
 
143
    unfold Rdiv in |- *; intros H1 _; exact H1.
 
144
  apply Ropp_neq_0_compat; assumption.
 
145
  assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl in |- *;
 
146
    cut (0 < y).
 
147
  intro; unfold Rminus in |- *;
 
148
    replace (- ((IZR (up (x / y)) + -1) * y)) with ((1 - IZR (up (x / y))) * y);
 
149
      [ idtac | ring ].
 
150
  split.
 
151
  apply Rmult_le_reg_l with (/ y).
 
152
  apply Rinv_0_lt_compat; assumption.
 
153
  rewrite Rmult_0_r; rewrite (Rmult_comm (/ y)); rewrite Rmult_plus_distr_r;
 
154
    rewrite Rmult_assoc; rewrite <- Rinv_r_sym;
 
155
      [ rewrite Rmult_1_r | assumption ];
 
156
      apply Rplus_le_reg_l with (IZR (up (x / y)) - x / y); 
 
157
        rewrite Rplus_0_r; unfold Rdiv in |- *;
 
158
          replace
 
159
            (IZR (up (x * / y)) - x * / y + (x * / y + (1 - IZR (up (x * / y))))) with
 
160
            1; [ idtac | ring ]; elim H0; intros _ H2; unfold Rdiv in H2; 
 
161
              exact H2.
 
162
  rewrite (Rabs_right _ r); apply Rmult_lt_reg_l with (/ y).
 
163
  apply Rinv_0_lt_compat; assumption.
 
164
  rewrite <- (Rinv_l_sym _ H); rewrite (Rmult_comm (/ y));
 
165
    rewrite Rmult_plus_distr_r; rewrite Rmult_assoc; rewrite <- Rinv_r_sym;
 
166
      [ rewrite Rmult_1_r | assumption ];
 
167
      apply Rplus_lt_reg_r with (IZR (up (x / y)) - 1);
 
168
        replace (IZR (up (x / y)) - 1 + 1) with (IZR (up (x / y))); 
 
169
          [ idtac | ring ];
 
170
          replace (IZR (up (x / y)) - 1 + (x * / y + (1 - IZR (up (x / y))))) with
 
171
            (x * / y); [ idtac | ring ]; elim H0; unfold Rdiv in |- *; 
 
172
              intros H2 _; exact H2.
 
173
  case (total_order_T 0 y); intro.
 
174
  elim s; intro.
 
175
  assumption.
 
176
  elim H; symmetry  in |- *; exact b.
 
177
  assert (H1 := Rge_le _ _ r); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 r0)).
 
178
Qed.
 
179
 
 
180
Lemma tech8 : forall n i:nat, (n <= S n + i)%nat.
 
181
Proof.
 
182
  intros; induction  i as [| i Hreci].
 
183
  replace (S n + 0)%nat with (S n); [ apply le_n_Sn | ring ].
 
184
  replace (S n + S i)%nat with (S (S n + i)).
 
185
  apply le_S; assumption.
 
186
  apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; do 2 rewrite S_INR; ring.
 
187
Qed.