Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Fcalc_bracket.v 16.1 KB
 Guillaume Melquiond committed Mar 01, 2010 1 2 3 4 5 ``````Require Import Fcore. Section Fcalc_bracket. Variable d u : R. `````` 6 ``````Hypothesis Hdu : (d < u)%R. `````` Guillaume Melquiond committed Mar 01, 2010 7 `````` `````` 8 ``````Inductive location := loc_Exact | loc_Inexact : comparison -> location. `````` Guillaume Melquiond committed Mar 01, 2010 9 10 11 12 `````` Variable x : R. Inductive inbetween : location -> Prop := `````` 13 14 `````` | inbetween_Exact : x = d -> inbetween loc_Exact | inbetween_Inexact l : (d < x < u)%R -> Rcompare x ((d + u) / 2)%R = l -> inbetween (loc_Inexact l). `````` Guillaume Melquiond committed Mar 01, 2010 15 `````` `````` Guillaume Melquiond committed Mar 05, 2010 16 17 ``````Section Fcalc_bracket_any. `````` Guillaume Melquiond committed Mar 01, 2010 18 19 20 21 ``````Variable l : location. Theorem inbetween_bounds : inbetween l -> `````` 22 `````` (d <= x < u)%R. `````` Guillaume Melquiond committed Mar 01, 2010 23 ``````Proof. `````` 24 ``````intros [Hx|l' Hx Hl] ; clear l. `````` Guillaume Melquiond committed Mar 01, 2010 25 26 27 28 ``````rewrite Hx. split. apply Rle_refl. exact Hdu. `````` 29 ``````now split ; try apply Rlt_le. `````` Guillaume Melquiond committed Mar 01, 2010 30 31 ``````Qed. `````` 32 ``````Theorem inbetween_bounds_not_Eq : `````` Guillaume Melquiond committed Mar 01, 2010 33 `````` inbetween l -> `````` 34 `````` l <> loc_Exact -> `````` Guillaume Melquiond committed Mar 01, 2010 35 36 `````` (d < x < u)%R. Proof. `````` 37 38 39 ``````intros [Hx|l' Hx Hl] H. now elim H. exact Hx. `````` Guillaume Melquiond committed Mar 01, 2010 40 41 ``````Qed. `````` Guillaume Melquiond committed Mar 05, 2010 42 43 ``````End Fcalc_bracket_any. `````` 44 45 46 47 ``````Theorem inbetween_distance_inexact : forall l, inbetween (loc_Inexact l) -> Rcompare (x - d) (u - x) = l. `````` Guillaume Melquiond committed Mar 05, 2010 48 ``````Proof. `````` 49 50 51 ``````intros l Hl. inversion_clear Hl as [|l' Hl' Hx]. now rewrite Rcompare_middle. `````` Guillaume Melquiond committed Mar 05, 2010 52 53 ``````Qed. `````` 54 55 56 57 ``````Theorem inbetween_distance_inexact_abs : forall l, inbetween (loc_Inexact l) -> Rcompare (Rabs (d - x)) (Rabs (u - x)) = l. `````` Guillaume Melquiond committed Mar 05, 2010 58 ``````Proof. `````` 59 60 61 ``````intros l Hl. rewrite Rabs_left1. rewrite Rabs_pos_eq. `````` Guillaume Melquiond committed Mar 05, 2010 62 ``````rewrite Ropp_minus_distr. `````` 63 64 65 66 67 68 ``````now apply inbetween_distance_inexact. apply Rle_0_minus. apply Rlt_le. apply (inbetween_bounds _ Hl). apply Rle_minus. apply (inbetween_bounds _ Hl). `````` Guillaume Melquiond committed Mar 05, 2010 69 70 ``````Qed. `````` Guillaume Melquiond committed Mar 01, 2010 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 ``````End Fcalc_bracket. Section Fcalc_bracket_step. Variable start step : R. Variable nb_steps : Z. Variable Hstep : (0 < step)%R. Lemma ordered_steps : forall k, (start + Z2R k * step < start + Z2R (k + 1) * step)%R. Proof. intros k. apply Rplus_lt_compat_l. apply Rmult_lt_compat_r. exact Hstep. apply Z2R_lt. apply Zlt_succ. Qed. `````` Guillaume Melquiond committed May 17, 2010 91 ``````Lemma middle_range : `````` 92 93 94 95 96 97 98 `````` forall k, ((start + (start + Z2R k * step)) / 2 = start + (Z2R k / 2 * step))%R. Proof. intros k. field. Qed. `````` Guillaume Melquiond committed Mar 01, 2010 99 100 ``````Hypothesis (Hnb_steps : (1 < nb_steps)%Z). `````` 101 102 ``````Lemma inbetween_step_not_Eq : forall x k l l', `````` Guillaume Melquiond committed Mar 01, 2010 103 `````` inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l -> `````` 104 105 106 `````` (0 < k < nb_steps)%Z -> Rcompare x (start + (Z2R nb_steps / 2 * step))%R = l' -> inbetween start (start + Z2R nb_steps * step) x (loc_Inexact l'). `````` Guillaume Melquiond committed Mar 01, 2010 107 ``````Proof. `````` 108 ``````intros x k l l' Hx Hk Hl'. `````` Guillaume Melquiond committed Mar 01, 2010 109 110 ``````constructor. (* . *) `````` 111 112 113 ``````assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx). split. apply Rlt_le_trans with (2 := proj1 Hx'). `````` Guillaume Melquiond committed Mar 01, 2010 114 115 116 117 118 ``````rewrite <- (Rplus_0_r start) at 1. apply Rplus_lt_compat_l. apply Rmult_lt_0_compat. now apply (Z2R_lt 0). exact Hstep. `````` 119 ``````apply Rlt_le_trans with (1 := proj2 Hx'). `````` Guillaume Melquiond committed Mar 01, 2010 120 121 122 ``````apply Rplus_le_compat_l. apply Rmult_le_compat_r. now apply Rlt_le. `````` 123 124 125 ``````apply Z2R_le. omega. (* . *) `````` Guillaume Melquiond committed May 17, 2010 126 ``````now rewrite middle_range. `````` 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 ``````Qed. Theorem inbetween_step_Lo : forall x k l, inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l -> (0 < k)%Z -> (2 * k + 1 < nb_steps)%Z -> inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt). Proof. intros x k l Hx Hk1 Hk2. apply inbetween_step_not_Eq with (1 := Hx). omega. apply Rcompare_Lt. assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx). apply Rlt_le_trans with (1 := proj2 Hx'). apply Rcompare_not_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_not_Lt. `````` Guillaume Melquiond committed Mar 01, 2010 144 145 146 147 ``````change 2%R with (Z2R 2). rewrite <- mult_Z2R. apply Z2R_le. omega. `````` 148 ``````exact Hstep. `````` Guillaume Melquiond committed Mar 01, 2010 149 150 151 152 153 154 ``````Qed. Theorem inbetween_step_Hi : forall x k l, inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l -> (nb_steps < 2 * k)%Z -> (k < nb_steps)%Z -> `````` 155 `````` inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Gt). `````` Guillaume Melquiond committed Mar 01, 2010 156 157 ``````Proof. intros x k l Hx Hk1 Hk2. `````` 158 159 160 161 162 163 164 165 ``````apply inbetween_step_not_Eq with (1 := Hx). omega. apply Rcompare_Gt. assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx). apply Rlt_le_trans with (2 := proj1 Hx'). apply Rcompare_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_Lt. `````` Guillaume Melquiond committed Mar 01, 2010 166 167 168 ``````change 2%R with (Z2R 2). rewrite <- mult_Z2R. apply Z2R_lt. `````` 169 170 ``````omega. exact Hstep. `````` Guillaume Melquiond committed Mar 01, 2010 171 172 ``````Qed. `````` 173 ``````Theorem inbetween_step_Lo_not_Eq : `````` Guillaume Melquiond committed Mar 01, 2010 174 175 `````` forall x l, inbetween start (start + step) x l -> `````` 176 177 `````` l <> loc_Exact -> inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt). `````` Guillaume Melquiond committed Mar 01, 2010 178 179 ``````Proof. intros x l Hx Hl. `````` 180 ``````assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl). `````` Guillaume Melquiond committed Mar 01, 2010 181 182 ``````constructor. (* . *) `````` 183 184 185 186 ``````split. apply Hx'. apply Rlt_trans with (1 := proj2 Hx'). apply Rplus_lt_compat_l. `````` Guillaume Melquiond committed Mar 01, 2010 187 ``````rewrite <- (Rmult_1_l step) at 1. `````` 188 189 190 191 192 193 ``````apply Rmult_lt_compat_r. exact Hstep. now apply (Z2R_lt 1). (* . *) apply Rcompare_Lt. apply Rlt_le_trans with (1 := proj2 Hx'). `````` Guillaume Melquiond committed May 17, 2010 194 ``````rewrite middle_range. `````` 195 196 197 198 199 200 201 202 ``````apply Rcompare_not_Lt_inv. rewrite <- (Rmult_1_l step) at 2. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. rewrite Rmult_1_r. apply Rcompare_not_Lt. apply (Z2R_le 2). now apply (Zlt_le_succ 1). exact Hstep. `````` Guillaume Melquiond committed Mar 01, 2010 203 204 205 206 207 ``````Qed. Lemma middle_odd : forall k, (2 * k + 1 = nb_steps)%Z -> `````` 208 `````` (((start + Z2R k * step) + (start + Z2R (k + 1) * step))/2 = start + Z2R nb_steps /2 * step)%R. `````` Guillaume Melquiond committed Mar 01, 2010 209 210 ``````Proof. intros k Hk. `````` Guillaume Melquiond committed Apr 12, 2010 211 212 213 ``````rewrite <- Hk. rewrite 2!plus_Z2R, mult_Z2R. simpl. field. `````` Guillaume Melquiond committed Mar 01, 2010 214 215 ``````Qed. `````` 216 ``````Theorem inbetween_step_any_Mi_odd : `````` Guillaume Melquiond committed Mar 01, 2010 217 `````` forall x k l, `````` 218 `````` inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x (loc_Inexact l) -> `````` Guillaume Melquiond committed Mar 01, 2010 219 `````` (2 * k + 1 = nb_steps)%Z -> `````` 220 `````` inbetween start (start + Z2R nb_steps * step) x (loc_Inexact l). `````` Guillaume Melquiond committed Mar 01, 2010 221 ``````Proof. `````` 222 223 ``````intros x k l Hx Hk. apply inbetween_step_not_Eq with (1 := Hx). `````` Guillaume Melquiond committed Mar 01, 2010 224 ``````omega. `````` 225 226 ``````inversion_clear Hx as [|l' _ Hl]. now rewrite (middle_odd _ Hk) in Hl. `````` Guillaume Melquiond committed Mar 01, 2010 227 228 ``````Qed. `````` 229 ``````Theorem inbetween_step_Lo_Mi_Eq_odd : `````` Guillaume Melquiond committed Mar 01, 2010 230 `````` forall x k, `````` 231 `````` inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x loc_Exact -> `````` Guillaume Melquiond committed Mar 01, 2010 232 `````` (2 * k + 1 = nb_steps)%Z -> `````` 233 `````` inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt). `````` Guillaume Melquiond committed Mar 01, 2010 234 235 ``````Proof. intros x k Hx Hk. `````` 236 ``````apply inbetween_step_not_Eq with (1 := Hx). `````` Guillaume Melquiond committed Mar 01, 2010 237 ``````omega. `````` 238 239 240 241 242 243 244 245 246 247 ``````inversion_clear Hx as [Hl|]. rewrite Hl. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. apply Rcompare_Lt. change 2%R with (Z2R 2). rewrite <- mult_Z2R. apply Z2R_lt. rewrite <- Hk. apply Zlt_succ. exact Hstep. `````` Guillaume Melquiond committed Mar 01, 2010 248 249 250 251 252 ``````Qed. Theorem inbetween_step_Hi_Mi_even : forall x k l, inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l -> `````` 253 `````` l <> loc_Exact -> `````` Guillaume Melquiond committed Mar 01, 2010 254 `````` (2 * k = nb_steps)%Z -> `````` 255 `````` inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Gt). `````` Guillaume Melquiond committed Mar 01, 2010 256 257 ``````Proof. intros x k l Hx Hl Hk. `````` 258 ``````apply inbetween_step_not_Eq with (1 := Hx). `````` Guillaume Melquiond committed Mar 01, 2010 259 ``````omega. `````` 260 261 262 263 264 265 266 267 268 269 270 271 ``````apply Rcompare_Gt. assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl). apply Rle_lt_trans with (2 := proj1 Hx'). apply Rcompare_not_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. change 2%R with (Z2R 2). rewrite <- mult_Z2R. apply Rcompare_not_Lt. apply Z2R_le. rewrite Hk. apply Zle_refl. exact Hstep. `````` Guillaume Melquiond committed Mar 01, 2010 272 273 274 275 ``````Qed. Theorem inbetween_step_Mi_Mi_even : forall x k, `````` 276 `````` inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x loc_Exact -> `````` Guillaume Melquiond committed Mar 01, 2010 277 `````` (2 * k = nb_steps)%Z -> `````` 278 `````` inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Eq). `````` Guillaume Melquiond committed Mar 01, 2010 279 280 ``````Proof. intros x k Hx Hk. `````` 281 282 283 284 285 ``````apply inbetween_step_not_Eq with (1 := Hx). omega. apply Rcompare_Eq. inversion_clear Hx as [Hx'|]. rewrite Hx', <- Hk, mult_Z2R. `````` Guillaume Melquiond committed Mar 01, 2010 286 ``````simpl (Z2R 2). `````` 287 ``````field. `````` Guillaume Melquiond committed Mar 01, 2010 288 289 290 291 ``````Qed. Definition new_location_even k l := if Zeq_bool k 0 then `````` 292 `````` match l with loc_Exact => l | _ => loc_Inexact Lt end `````` Guillaume Melquiond committed Mar 01, 2010 293 `````` else `````` 294 `````` loc_Inexact `````` Guillaume Melquiond committed Mar 01, 2010 295 `````` match Zcompare (2 * k) nb_steps with `````` 296 297 298 `````` | Lt => Lt | Eq => match l with loc_Exact => Eq | _ => Gt end | Gt => Gt `````` Guillaume Melquiond committed Mar 01, 2010 299 300 301 `````` end. Theorem new_location_even_correct : `````` Guillaume Melquiond committed May 11, 2010 302 `````` Zeven nb_steps = true -> `````` Guillaume Melquiond committed Mar 01, 2010 303 304 305 306 307 308 309 310 311 312 `````` forall x k l, (0 <= k < nb_steps)%Z -> inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l -> inbetween start (start + Z2R nb_steps * step) x (new_location_even k l). Proof. intros He x k l Hk Hx. unfold new_location_even. destruct (Zeq_bool_spec k 0) as [Hk0|Hk0]. (* k = 0 *) rewrite Hk0 in Hx. rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx. `````` 313 314 ``````set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end). assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)). `````` Guillaume Melquiond committed Mar 01, 2010 315 316 317 318 319 ``````unfold l' ; case l ; try (now left) ; right ; now split. destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2. constructor. rewrite H1 in Hx. now inversion_clear Hx. `````` 320 ``````now apply inbetween_step_Lo_not_Eq with (2 := H1). `````` Guillaume Melquiond committed Mar 01, 2010 321 322 323 324 ``````(* k <> 0 *) destruct (Zcompare_spec (2 * k) nb_steps) as [Hk1|Hk1|Hk1]. (* . 2 * k < nb_steps *) apply inbetween_step_Lo with (1 := Hx). `````` 325 ``````omega. `````` Guillaume Melquiond committed May 11, 2010 326 327 ``````destruct (Zeven_ex nb_steps). rewrite He in H. `````` Guillaume Melquiond committed Mar 01, 2010 328 329 ``````omega. (* . 2 * k = nb_steps *) `````` 330 331 ``````set (l' := match l with loc_Exact => Eq | _ => Gt end). assert ((l = loc_Exact /\ l' = Eq) \/ (l <> loc_Exact /\ l' = Gt)). `````` Guillaume Melquiond committed Mar 01, 2010 332 333 334 335 336 337 338 339 340 341 342 343 344 ``````unfold l' ; case l ; try (now left) ; right ; now split. destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2. rewrite H1 in Hx. now apply inbetween_step_Mi_Mi_even with (1 := Hx). now apply inbetween_step_Hi_Mi_even with (1 := Hx). (* . 2 * k > nb_steps *) apply inbetween_step_Hi with (1 := Hx). exact Hk1. apply Hk. Qed. Definition new_location_odd k l := if Zeq_bool k 0 then `````` 345 `````` match l with loc_Exact => l | _ => loc_Inexact Lt end `````` Guillaume Melquiond committed Mar 01, 2010 346 `````` else `````` 347 `````` loc_Inexact `````` Guillaume Melquiond committed Mar 01, 2010 348 `````` match Zcompare (2 * k + 1) nb_steps with `````` 349 350 351 `````` | Lt => Lt | Eq => match l with loc_Inexact l => l | loc_Exact => Lt end | Gt => Gt `````` Guillaume Melquiond committed Mar 01, 2010 352 353 354 `````` end. Theorem new_location_odd_correct : `````` Guillaume Melquiond committed May 11, 2010 355 `````` Zeven nb_steps = false -> `````` Guillaume Melquiond committed Mar 01, 2010 356 357 358 359 360 361 362 363 364 365 `````` forall x k l, (0 <= k < nb_steps)%Z -> inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l -> inbetween start (start + Z2R nb_steps * step) x (new_location_odd k l). Proof. intros Ho x k l Hk Hx. unfold new_location_odd. destruct (Zeq_bool_spec k 0) as [Hk0|Hk0]. (* k = 0 *) rewrite Hk0 in Hx. rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx. `````` 366 367 ``````set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end). assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)). `````` Guillaume Melquiond committed Mar 01, 2010 368 369 370 371 372 ``````unfold l' ; case l ; try (now left) ; right ; now split. destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2. constructor. rewrite H1 in Hx. now inversion_clear Hx. `````` 373 ``````now apply inbetween_step_Lo_not_Eq with (2 := H1). `````` Guillaume Melquiond committed Mar 01, 2010 374 375 376 377 ``````(* k <> 0 *) destruct (Zcompare_spec (2 * k + 1) nb_steps) as [Hk1|Hk1|Hk1]. (* . 2 * k + 1 < nb_steps *) apply inbetween_step_Lo with (1 := Hx) (3 := Hk1). `````` 378 ``````omega. `````` Guillaume Melquiond committed Mar 01, 2010 379 380 ``````(* . 2 * k + 1 = nb_steps *) destruct l. `````` 381 382 ``````apply inbetween_step_Lo_Mi_Eq_odd with (1 := Hx) (2 := Hk1). apply inbetween_step_any_Mi_odd with (1 := Hx) (2 := Hk1). `````` Guillaume Melquiond committed Mar 01, 2010 383 384 ``````(* . 2 * k + 1 > nb_steps *) apply inbetween_step_Hi with (1 := Hx). `````` Guillaume Melquiond committed May 11, 2010 385 386 ``````destruct (Zeven_ex nb_steps). rewrite Ho in H. `````` Guillaume Melquiond committed Mar 01, 2010 387 388 389 390 ``````omega. apply Hk. Qed. `````` Guillaume Melquiond committed Mar 02, 2010 391 ``````Definition new_location := `````` Guillaume Melquiond committed May 11, 2010 392 `````` if Zeven nb_steps then new_location_even else new_location_odd. `````` Guillaume Melquiond committed Mar 02, 2010 393 394 395 396 397 398 399 400 401 402 403 404 405 406 `````` Theorem new_location_correct : forall x k l, (0 <= k < nb_steps)%Z -> inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l -> inbetween start (start + Z2R nb_steps * step) x (new_location k l). Proof. intros x k l Hk Hx. unfold new_location. generalize (refl_equal nb_steps) (Zle_lt_trans _ _ _ (proj1 Hk) (proj2 Hk)). pattern nb_steps at 2 3 5 ; case nb_steps. now intros _. (* . *) intros [p|p|] Hp _. apply new_location_odd_correct with (2 := Hk) (3 := Hx). `````` Guillaume Melquiond committed May 11, 2010 407 ``````now rewrite Hp. `````` Guillaume Melquiond committed Mar 02, 2010 408 ``````apply new_location_even_correct with (2 := Hk) (3 := Hx). `````` Guillaume Melquiond committed May 11, 2010 409 ``````now rewrite Hp. `````` Guillaume Melquiond committed Mar 02, 2010 410 411 412 413 414 ``````now rewrite Hp in Hnb_steps. (* . *) now intros p _. Qed. `````` Guillaume Melquiond committed Mar 01, 2010 415 416 ``````End Fcalc_bracket_step. `````` Guillaume Melquiond committed May 17, 2010 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 ``````Section Fcalc_bracket_scale. Lemma inbetween_mult_aux : forall x d s, ((x * s + d * s) / 2 = (x + d) / 2 * s)%R. Proof. intros x d s. field. Qed. Theorem inbetween_mult_compat : forall x d u l s, (0 < s)%R -> inbetween x d u l -> inbetween (x * s) (d * s) (u * s) l. Proof. `````` 433 434 435 ``````intros x d u l s Hs [Hx|l' Hx Hl] ; constructor. now rewrite Hx. now split ; apply Rmult_lt_compat_r. `````` Guillaume Melquiond committed May 17, 2010 436 ``````rewrite inbetween_mult_aux. `````` 437 ``````now rewrite Rcompare_mult_r. `````` Guillaume Melquiond committed May 17, 2010 438 439 440 441 442 443 444 445 ``````Qed. Theorem inbetween_mult_reg : forall x d u l s, (0 < s)%R -> inbetween (x * s) (d * s) (u * s) l -> inbetween x d u l. Proof. `````` 446 447 ``````intros x d u l s Hs [Hx|l' Hx Hl] ; constructor. apply Rmult_eq_reg_r with (1 := Hx). `````` Guillaume Melquiond committed May 17, 2010 448 ``````now apply Rgt_not_eq. `````` 449 450 451 ``````now split ; apply Rmult_lt_reg_r with s. rewrite <- Rcompare_mult_r with (1 := Hs). now rewrite inbetween_mult_aux in Hl. `````` Guillaume Melquiond committed May 17, 2010 452 453 454 455 ``````Qed. End Fcalc_bracket_scale. `````` Guillaume Melquiond committed Mar 01, 2010 456 457 458 ``````Section Fcalc_bracket_generic. Variable beta : radix. `````` Guillaume Melquiond committed Mar 04, 2010 459 ``````Notation bpow e := (bpow beta e). `````` Guillaume Melquiond committed Mar 01, 2010 460 461 462 463 464 `````` Variable fexp : Z -> Z. Hypothesis prop_exp : valid_exp fexp. Notation format := (generic_format beta fexp). `````` Guillaume Melquiond committed Mar 02, 2010 465 466 467 ``````Definition inbetween_float m e x l := inbetween (F2R (Float beta m e)) (F2R (Float beta (m + 1) e)) x l. `````` Guillaume Melquiond committed Aug 19, 2010 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 ``````Theorem inbetween_float_bounds : forall x m e l, inbetween_float m e x l -> (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R. Proof. intros x m e l [Hx|l' Hx Hl]. rewrite Hx. split. apply Rle_refl. apply F2R_lt_compat. apply Zlt_succ. split. now apply Rlt_le. apply Hx. Qed. `````` Guillaume Melquiond committed May 17, 2010 484 485 486 ``````Definition inbetween_int m x l := inbetween (Z2R m) (Z2R (m + 1)) x l. `````` Guillaume Melquiond committed Mar 02, 2010 487 ``````Theorem inbetween_float_new_location : `````` Guillaume Melquiond committed May 17, 2010 488 489 `````` forall x m e l k, (0 < k)%Z -> `````` Guillaume Melquiond committed Mar 02, 2010 490 `````` inbetween_float m e x l -> `````` Guillaume Melquiond committed May 17, 2010 491 `````` inbetween_float (Zdiv m (Zpower (radix_val beta) k)) (e + k) x (new_location (Zpower (radix_val beta) k) (Zmod m (Zpower (radix_val beta) k)) l). `````` Guillaume Melquiond committed Mar 02, 2010 492 ``````Proof. `````` Guillaume Melquiond committed May 17, 2010 493 ``````intros x m e l k Hk Hx. `````` Guillaume Melquiond committed Mar 02, 2010 494 ``````unfold inbetween_float in *. `````` Guillaume Melquiond committed May 17, 2010 495 496 497 498 499 500 501 502 ``````assert (Hr: forall m, F2R (Float beta m (e + k)) = F2R (Float beta (m * Zpower (radix_val beta) k) e)). clear -Hk. intros m. rewrite (F2R_change_exp beta e). apply (f_equal (fun r => F2R (Float beta (m * Zpower _ r) e))). ring. omega. assert (Hp: (Zpower (radix_val beta) k > 0)%Z). apply Zlt_gt. `````` Guillaume Melquiond committed Aug 19, 2010 503 ``````now apply Zpower_gt_0. `````` Guillaume Melquiond committed Mar 02, 2010 504 505 506 507 508 509 510 ``````(* . *) rewrite 2!Hr. rewrite Zmult_plus_distr_l, Zmult_1_l. unfold F2R at 2. simpl. rewrite plus_Z2R, Rmult_plus_distr_r. apply new_location_correct. apply bpow_gt_0. `````` Guillaume Melquiond committed May 17, 2010 511 512 ``````now apply Zpower_gt_1. now apply Z_mod_lt. `````` Guillaume Melquiond committed Mar 02, 2010 513 514 ``````rewrite <- 2!Rmult_plus_distr_r, <- 2!plus_Z2R. rewrite Zmult_comm, Zplus_assoc. `````` Guillaume Melquiond committed May 17, 2010 515 516 517 518 519 520 521 522 523 524 525 526 ``````now rewrite <- Z_div_mod_eq. Qed. Theorem inbetween_float_new_location_single : forall x m e l, inbetween_float m e x l -> inbetween_float (Zdiv m (radix_val beta)) (e + 1) x (new_location (radix_val beta) (Zmod m (radix_val beta)) l). Proof. intros x m e l Hx. replace (radix_val beta) with (Zpower (radix_val beta) 1). now apply inbetween_float_new_location. apply Zmult_1_r. `````` Guillaume Melquiond committed Mar 02, 2010 527 528 ``````Qed. `````` Guillaume Melquiond committed May 17, 2010 529 530 ``````Theorem inbetween_float_rounding : forall rnd choice, `````` Guillaume Melquiond committed Aug 20, 2010 531 `````` ( forall x m e l, inbetween_int m x l -> Zrnd rnd x e = choice m e l ) -> `````` Guillaume Melquiond committed May 17, 2010 532 533 534 `````` forall x m l, let e := canonic_exponent beta fexp x in inbetween_float m e x l -> `````` Guillaume Melquiond committed Aug 20, 2010 535 `````` rounding beta fexp rnd x = F2R (Float beta (choice m e l) e). `````` Guillaume Melquiond committed May 17, 2010 536 537 538 539 540 541 542 543 544 545 ``````Proof. intros rnd choice Hc x m l e Hl. unfold rounding, F2R. simpl. apply (f_equal (fun m => (Z2R m * bpow e)%R)). apply Hc. apply inbetween_mult_reg with (bpow e). apply bpow_gt_0. now rewrite scaled_mantissa_bpow. Qed. `````` Guillaume Melquiond committed Mar 04, 2010 546 ``````Theorem inbetween_float_DN : `````` 547 548 `````` forall x m l, let e := canonic_exponent beta fexp x in `````` Guillaume Melquiond committed Mar 04, 2010 549 `````` inbetween_float m e x l -> `````` Guillaume Melquiond committed May 17, 2010 550 `````` rounding beta fexp ZrndDN x = F2R (Float beta m e). `````` Guillaume Melquiond committed Mar 04, 2010 551 ``````Proof. `````` Guillaume Melquiond committed Aug 20, 2010 552 553 554 ``````apply inbetween_float_rounding with (choice := fun m e l => m). intros x m e l Hl. refine (Zfloor_imp m _ _). `````` 555 ``````apply inbetween_bounds with (2 := Hl). `````` Guillaume Melquiond committed May 17, 2010 556 ``````apply Z2R_lt. `````` Guillaume Melquiond committed Mar 04, 2010 557 558 559 560 561 562 563 ``````apply Zlt_succ. Qed. Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m. Definition round_UP l := match l with `````` 564 `````` | loc_Exact => false `````` Guillaume Melquiond committed Mar 04, 2010 565 566 567 568 `````` | _ => true end. Theorem inbetween_float_UP : `````` 569 570 `````` forall x m l, let e := canonic_exponent beta fexp x in `````` Guillaume Melquiond committed Mar 04, 2010 571 `````` inbetween_float m e x l -> `````` Guillaume Melquiond committed May 17, 2010 572 `````` rounding beta fexp ZrndUP x = F2R (Float beta (cond_incr (round_UP l) m) e). `````` Guillaume Melquiond committed Mar 04, 2010 573 ``````Proof. `````` Guillaume Melquiond committed Aug 20, 2010 574 575 ``````apply inbetween_float_rounding with (choice := fun m e l => cond_incr (round_UP l) m). intros x m e l Hl. `````` 576 ``````assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)). `````` Guillaume Melquiond committed May 17, 2010 577 578 ``````case l ; try (now left) ; now right ; split. destruct Hl' as [Hl'|(Hl1, Hl2)]. `````` 579 ``````(* Exact *) `````` Guillaume Melquiond committed May 17, 2010 580 581 582 ``````rewrite Hl'. destruct Hl ; try easy. rewrite H. `````` Guillaume Melquiond committed Aug 20, 2010 583 ``````exact (Zceil_Z2R _). `````` 584 ``````(* not Exact *) `````` Guillaume Melquiond committed May 17, 2010 585 ``````rewrite Hl2. `````` 586 587 588 ``````simpl. apply Zceil_imp. ring_simplify (m + 1 - 1)%Z. `````` Guillaume Melquiond committed May 17, 2010 589 ``````refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))). `````` 590 ``````apply inbetween_bounds_not_Eq with (2 := Hl1) (1 := Hl). `````` Guillaume Melquiond committed Mar 04, 2010 591 592 593 594 ``````Qed. Definition round_NE (p : bool) l := match l with `````` 595 596 597 598 `````` | loc_Exact => false | loc_Inexact Lt => false | loc_Inexact Eq => if p then false else true | loc_Inexact Gt => true `````` Guillaume Melquiond committed Mar 04, 2010 599 600 601 `````` end. Theorem inbetween_float_NE : `````` 602 `````` forall x m l, `````` 603 `````` let e := canonic_exponent beta fexp x in `````` Guillaume Melquiond committed Mar 04, 2010 604 `````` inbetween_float m e x l -> `````` 605 `````` rounding beta fexp ZrndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e). `````` Guillaume Melquiond committed Mar 04, 2010 606 ``````Proof. `````` Guillaume Melquiond committed Aug 20, 2010 607 608 ``````apply inbetween_float_rounding with (choice := fun m e l => cond_incr (round_NE (Zeven m) l) m). intros x m e l Hl. `````` 609 610 611 612 613 ``````inversion_clear Hl as [Hx|l' Hx Hl']. (* Exact *) rewrite Hx. now rewrite Zrnd_Z2R. (* not Exact *) `````` Guillaume Melquiond committed Aug 20, 2010 614 ``````unfold Zrnd, ZrndNE, ZrndN, Znearest, mkZrounding2. `````` 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 ``````assert (Hm: Zfloor x = m). apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). rewrite Zceil_floor_neq. rewrite Hm. replace (Rcompare (x - Z2R m) (/2)) with l'. now case l'. rewrite <- Hl'. rewrite plus_Z2R. rewrite <- (Rcompare_plus_r (- Z2R m) x). apply f_equal. simpl (Z2R 1). field. rewrite Hm. now apply Rlt_not_eq. `````` Guillaume Melquiond committed Mar 04, 2010 630 631 ``````Qed. `````` Guillaume Melquiond committed Mar 01, 2010 632 ``End Fcalc_bracket_generic.``