ErrorValidation.v 104 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
(**
2 3
   This file contains the coq implementation of the error bound validator as
   well as its soundness proof. The function validErrorbound is the Error bound
Heiko Becker's avatar
Heiko Becker committed
4 5 6 7
   validator from the certificate checking process. Under the assumption that a
   valid range arithmetic result has been computed, it can validate error bounds
   encoded in the analysis result. The validator is used in the file
   CertificateChecker.v to build the complete checker.
Heiko Becker's avatar
Heiko Becker committed
8
 **)
9 10 11
From Coq
     Require Import QArith.QArith QArith.Qminmax QArith.Qabs QArith.Qreals
     micromega.Psatz Reals.Reals.
12

13
From Flover
14 15 16
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
     Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
     ErrorBounds.
17

Heiko Becker's avatar
Heiko Becker committed
18
(** Error bound validator **)
19
Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
20 21
         (typeMap:FloverMap.t mType) (* derived types for e *)
         (A:analysisResult) (* encoded result of Flover *)
22
         (dVars:NatSet.t) (* let-bound variables encountered previously *):=
23
  match FloverMap.find e A, FloverMap.find e typeMap with
24
  | Some (intv, err), Some m =>
25
    if (Qleb 0 err) (* encoding soundness: errors are positive *)
26
    then
27
      match e with (* case analysis for the expression *)
='s avatar
= committed
28
      |Var _ v =>
29
       if (NatSet.mem v dVars)
30
       then true (* defined variables are checked at definition point *)
31 32 33
       else Qleb (computeErrorQ (maxAbs intv) m) err
      |Const m n =>
       Qleb (computeErrorQ (maxAbs intv) m) err
='s avatar
= committed
34
      |Unop Neg e1 =>
35
       if (validErrorbound e1 typeMap A dVars)
36
       then
37
         match FloverMap.find e1 A with
38 39 40
         | Some (iv_e1, err1) => Qeq_bool err err1
         | None => false
         end
41
       else false
='s avatar
= committed
42
      |Unop Inv e1 => false
43
      |Binop b e1 e2 =>
44 45
       if ((validErrorbound e1 typeMap A dVars)
             && (validErrorbound e2 typeMap A dVars))
46
       then
47
         match FloverMap.find e1 A, FloverMap.find e2 A with
48 49 50 51 52 53 54
         | Some (ive1, err1), Some (ive2, err2) =>
           let errIve1 := widenIntv ive1 err1 in
           let errIve2 := widenIntv ive2 err2 in
           let upperBoundE1 := maxAbs ive1 in
           let upperBoundE2 := maxAbs ive2 in
           match b with
           | Plus =>
55 56
             let mAbs := (maxAbs (addIntv errIve1 errIve2)) in
             Qleb (err1 + err2 + computeErrorQ mAbs m) err
57
           | Sub =>
58 59
             let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in
             Qleb (err1 + err2 + computeErrorQ mAbs m) err
60
           | Mult =>
61 62 63
             let mAbs := (maxAbs (multIntv errIve1 errIve2)) in
             let eProp := (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) in
             Qleb (eProp + computeErrorQ mAbs m) err
64 65 66 67 68 69 70
           | Div =>
             if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
                 ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
             then
               let upperBoundInvE2 := maxAbs (invertIntv ive2) in
               let minAbsIve2 := minAbs (errIve2) in
               let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
71 72 73
               let mAbs := (maxAbs (divideIntv errIve1 errIve2)) in
               let eProp := (upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) in
               Qleb (eProp + computeErrorQ mAbs m) err
74 75 76
             else false
           end
         | _, _ => false
77 78
         end
       else false
79 80 81 82 83
      | Fma e1 e2 e3 =>
        if ((validErrorbound e1 typeMap A dVars)
              && (validErrorbound e2 typeMap A dVars)
              && (validErrorbound e3 typeMap A dVars))
        then
84
          match FloverMap.find e1 A, FloverMap.find e2 A, FloverMap.find e3 A with
85 86 87 88 89 90 91 92 93
          | Some (ive1, err1), Some (ive2, err2), Some (ive3, err3) =>
            let errIve1 := widenIntv ive1 err1 in
            let errIve2 := widenIntv ive2 err2 in
            let errIve3 := widenIntv ive3 err3 in
            let upperBoundE1 := maxAbs ive1 in
            let upperBoundE2 := maxAbs ive2 in
            let upperBoundE3 := maxAbs ive3 in
            let errIntv_prod := multIntv errIve2 errIve3 in
            let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
94 95
            let mAbs := (maxAbs (addIntv errIve1 errIntv_prod)) in
            Qleb (err1 + mult_error_bound + computeErrorQ mAbs m) err
96 97
          | _, _, _ => false
          end
98
        else false
99
      |Downcast m1 e1 =>
100
       if validErrorbound e1 typeMap A dVars
101
       then
102
         match FloverMap.find e1 A with
103 104
         | Some (ive1, err1) =>
          let errIve1 := widenIntv ive1 err1 in
105 106
          let mAbs := maxAbs errIve1 in
          Qleb (err1 + computeErrorQ mAbs m1) err
107 108
         | None => false
         end
109 110
       else
         false
111 112
      end
    else false
113
  | _, _ => false
114
  end.
Heiko Becker's avatar
Heiko Becker committed
115

116
(** Error bound command validator **)
117
Fixpoint validErrorboundCmd (f:cmd Q) (* analyzed cmd with let's *)
118
         typeMap (* inferred types *)
119
         (A:analysisResult) (* Flover's encoded result *)
120 121
         (dVars:NatSet.t) (* defined variables *)
         : bool :=
122
  match f with
123
  |Let m x e g =>
124
   match FloverMap.find e A, FloverMap.find (Var Q x) A with
125 126 127 128 129 130
     | Some (iv_e, err_e), Some (iv_x, err_x) =>
       if ((validErrorbound e typeMap A dVars) && (Qeq_bool err_e err_x))
       then validErrorboundCmd g typeMap A (NatSet.add x dVars)
       else false
     | _,_ => false
   end
131
  |Ret e => validErrorbound e typeMap A dVars
132 133
  end.

134 135 136
(* Hide mTypeToQ from simplification since it will blow up the goal buffer *)
Arguments mTypeToQ _ :simpl nomatch.

Heiko Becker's avatar
Heiko Becker committed
137 138 139 140 141
(**
    Since errors are intervals with 0 as center, we encode them as single values.
    This lemma enables us to deduce from each run of the validator the invariant
    that when it succeeds, the errors must be positive.
**)
Heiko Becker's avatar
Heiko Becker committed
142
Lemma err_always_positive e tmap (A:analysisResult) dVars iv err:
Heiko Becker's avatar
Heiko Becker committed
143
  validErrorbound e tmap A dVars = true ->
144
    FloverMap.find e A = Some (iv,err) ->
Heiko Becker's avatar
Heiko Becker committed
145
    (0 <= Q2R err)%R.
146
Proof.
Heiko Becker's avatar
Heiko Becker committed
147
  destruct e; cbn; intros;
148
    Flover_compute; canonize_hyps;
Heiko Becker's avatar
Heiko Becker committed
149
      auto.
150
Qed.
Heiko Becker's avatar
Heiko Becker committed
151

152
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi fVars
153
      dVars Gamma exprTypes:
154
    eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
155
    typeCheck (Var Q v) Gamma exprTypes = true ->
Heiko Becker's avatar
Heiko Becker committed
156
    approxEnv E1 Gamma A fVars dVars E2 ->
157
    validRanges (Var Q v) A E1 Gamma ->
158
    validErrorbound (Var Q v) exprTypes A dVars = true ->
159
    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
160
    FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
161
    exists nF m,
162
    eval_expr E2 Gamma (toRExp (Var Q v)) nF m.
163
Proof.
164 165
  intros eval_real typing_ok approxCEnv bounds_valid error_valid v_sound A_var.
  apply validRanges_single in bounds_valid.
166 167 168 169
  destruct_smart [find_v [eval_real2 bounds_valid]] bounds_valid.
  pose proof (meps_0_deterministic _ eval_real eval_real2).  subst.
  cbn in *.
  inversion eval_real; subst.
170
  Flover_compute; type_conv.
171
  destruct (approxEnv_gives_value approxCEnv H1); try eauto.
172 173 174 175 176 177 178
  set_tac.
  case_eq (NatSet.mem v dVars); intros v_case; set_tac.
  left; apply v_sound.
  apply NatSetProps.FM.diff_3; set_tac.
Qed.

Lemma validErrorboundCorrectVariable:
179
  forall E1 E2 A (v:nat) e nR nF mF nlo nhi fVars dVars Gamma exprTypes,
180
    eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
181 182
    eval_expr E2 Gamma (toRExp (Var Q v)) nF mF ->
    typeCheck (Var Q v) Gamma exprTypes = true ->
Heiko Becker's avatar
Heiko Becker committed
183
    approxEnv E1 Gamma A fVars dVars E2 ->
184
    validRanges (Var Q v) A E1 Gamma ->
185
    validErrorbound (Var Q v) exprTypes A dVars = true ->
186
    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
187
    FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
188 189 190
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
  intros * eval_real eval_float typing_ok approxCEnv bounds_valid error_valid
191 192
                     v_sound A_var.
  apply validRanges_single in bounds_valid.
193 194
  destruct_smart [find_v [eval_real2 bounds_valid]] bounds_valid.
  pose proof (meps_0_deterministic _ eval_real eval_real2); subst.
195
  cbn in *; Flover_compute; type_conv.
196
  inversion eval_real;
197 198 199
    inversion eval_float;
    subst.
  rename H1 into E1_v.
200
  rename L into error_pos.
201
  rename R into error_valid.
202 203 204
  case_eq (v mem dVars); [intros v_dVar | intros v_fVar].
  - rewrite v_dVar in *; simpl in *.
    rewrite NatSet.mem_spec in v_dVar.
205
    eapply approxEnv_dVar_bounded; eauto.
206 207 208
  - rewrite v_fVar in *; simpl in *.
    apply not_in_not_mem in v_fVar.
    assert (v  fVars) as v_in_fVars by set_tac.
209
    pose proof (approxEnv_fVar_bounded approxCEnv E1_v H6 v_in_fVars H5).
210
    eapply Rle_trans; eauto.
211
    canonize_hyps.
212
    repeat destr_factorize.
213
    rewrite computeErrorQ_computeErrorR in error_valid.
214
    eapply Rle_trans; eauto.
215 216 217 218
    rewrite <- maxAbs_impl_RmaxAbs.
    apply computeErrorR_up.
    apply contained_leq_maxAbs.
    simpl in *; auto.
219
Qed.
220

221
Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR  Gamma:
222
    eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR REAL ->
223
    exists nF m',
224
      eval_expr E2 Gamma (toRExp (Const m n)) nF m'.
225
Proof.
226
  intros eval_real .
227
  repeat eexists.
228 229 230
  eapply Const_dist'; eauto.
  instantiate (1:= 0%R).
  rewrite Rabs_R0. auto using mTypeToR_pos_R.
231 232
Qed.

Heiko Becker's avatar
Heiko Becker committed
233
Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma defVars:
234
    eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR REAL ->
235
    eval_expr E2 defVars (toRExp (Const m n)) nF m ->
236
    typeCheck (Const m n) defVars Gamma = true ->
Heiko Becker's avatar
Heiko Becker committed
237
    validErrorbound (Const m n) Gamma A dVars = true ->
238
    (Q2R nlo <= nR <= Q2R nhi)%R ->
239
    FloverMap.find (Const m n) A = Some ((nlo,nhi),e) ->
240 241
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
242
  intros eval_real eval_float subexprr_ok error_valid intv_valid A_const.
243
  cbn in *; Flover_compute; type_conv.
Heiko Becker's avatar
Heiko Becker committed
244 245
  eapply Rle_trans.
  eapply const_abs_err_bounded; eauto.
246
  rename R into error_valid.
Heiko Becker's avatar
Heiko Becker committed
247
  inversion eval_real; subst.
248 249 250 251 252 253 254
  canonize_hyps.
  eapply Rle_trans; eauto.
  rewrite computeErrorQ_computeErrorR.
  rewrite <- maxAbs_impl_RmaxAbs.
  apply computeErrorR_up.
  apply contained_leq_maxAbs.
  simpl in *; auto.
255
Qed.
256

Heiko Becker's avatar
Heiko Becker committed
257
Lemma validErrorboundCorrectAddition E1 E2 A
258
      (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
259
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars:
260
  m = join m1 m2 ->
261 262 263
  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
  eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR REAL ->
264 265 266
  eval_expr E2 defVars (toRExp e1) nF1 m1 ->
  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
  eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
='s avatar
= committed
267
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
268
           (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
='s avatar
= committed
269
  typeCheck (Binop Plus e1 e2) defVars Gamma = true ->
Heiko Becker's avatar
Heiko Becker committed
270
  validErrorbound (Binop Plus e1 e2) Gamma A dVars = true ->
271 272
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
273 274 275
  FloverMap.find e1 A = Some ((e1lo,e1hi),err1) ->
  FloverMap.find e2 A = Some ((e2lo, e2hi),err2) ->
  FloverMap.find (Binop Plus e1 e2) A = Some ((alo,ahi),e)->
276 277 278 279
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
280
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
281
         subexprr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
282
         err1_bounded err2_bounded.
283
  cbn in *; Flover_compute; type_conv.
284
  eapply Rle_trans.
285 286 287
  eapply
    (add_abs_err_bounded e1 e2);
    try eauto.
288 289
  pose proof (typingSoundnessExp _ _ R2 e1_float).
  pose proof (typingSoundnessExp _ _ R1 e2_float).
290
  repeat destr_factorize.
291
  rename R0 into valid_error.
292 293 294 295 296
  eapply Rle_trans.
  apply Rplus_le_compat_l.
  Focus 2.
  rewrite Qle_bool_iff in valid_error.
  apply Qle_Rle in valid_error.
297
  repeat rewrite Q2R_plus in valid_error.
298
  eauto.
299 300
  clear L R.
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
301 302
  pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded)
       as contained_widen1.
303
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
304 305 306
  pose proof (distance_gives_iv (a:=nR2) _ (Q2R e2lo, Q2R e2hi) contained_intv2 err2_bounded)
       as contained_widen2.
  pose proof (IntervalArith.interval_addition_valid _ _ contained_widen1 contained_widen2).
307 308 309 310
  rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
  apply computeErrorR_up.
  apply contained_leq_maxAbs.
  simpl in *; split.
311 312
  - rewrite Q2R_min4.
    repeat rewrite Q2R_plus;
313
      repeat rewrite Q2R_minus; lra.
314 315
  - rewrite Q2R_max4.
    repeat rewrite Q2R_plus;
316
      repeat rewrite Q2R_minus; lra.
317
Qed.
Heiko Becker's avatar
Heiko Becker committed
318

Heiko Becker's avatar
Heiko Becker committed
319
Lemma validErrorboundCorrectSubtraction E1 E2 A
320
      (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
321
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
322
  m = join m1 m2 ->
323 324 325
  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
  eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR REAL ->
326 327 328
  eval_expr E2 defVars (toRExp e1) nF1 m1->
  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
  eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
='s avatar
= committed
329
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
330
           (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
='s avatar
= committed
331
  typeCheck (Binop Sub e1 e2) defVars Gamma = true ->
Heiko Becker's avatar
Heiko Becker committed
332
  validErrorbound (Binop Sub e1 e2) Gamma A dVars = true ->
333 334
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
335 336 337
  FloverMap.find e1 A = Some ((e1lo,e1hi),err1) ->
  FloverMap.find e2 A = Some ((e2lo, e2hi),err2) ->
  FloverMap.find (Binop Sub e1 e2) A = Some ((alo,ahi),e)->
338 339 340 341
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
342
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
343
         subexprr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub
344
         err1_bounded err2_bounded.
345
  cbn in *; Flover_compute; type_conv.
346
  eapply Rle_trans.
347
  eapply (subtract_abs_err_bounded e1 e2); try eauto.
348 349
  pose proof (typingSoundnessExp _ _ R2 e1_float).
  pose proof (typingSoundnessExp _ _ R1 e2_float).
350
  repeat destr_factorize.
351 352
  rename R0 into valid_error.
  canonize_hyps.
353 354 355 356 357 358 359
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite Q2R_mult in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  eapply Rle_trans.
  apply Rplus_le_compat_l.
  Focus 2.
  apply valid_error.
360
  rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
361 362 363
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
  pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded)
       as contained_widen1.
364
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
365 366 367
  pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded)
       as contained_widen2.
  pose proof (IntervalArith.interval_subtraction_valid _ _ contained_widen1 contained_widen2).
368 369 370
  apply computeErrorR_up.
  apply contained_leq_maxAbs.
  simpl in *; split.
371 372 373 374 375
  - rewrite Q2R_min4.
    repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus;
      repeat rewrite Q2R_opp;
      repeat rewrite Q2R_plus;
376
      repeat rewrite Q2R_minus; lra.
377 378 379 380 381
  - rewrite Q2R_max4.
    repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus;
      repeat rewrite Q2R_opp;
      repeat rewrite Q2R_plus;
382
      repeat rewrite Q2R_minus; lra.
383 384
Qed.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850
Lemma multiplicationErrorBounded e1lo e1hi e2lo e2hi nR1 nF1 nR2 nF2 err1 err2 :
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
  (Rabs (nR1 - nF1) <= Q2R err1)%R ->
  (Rabs (nR2 - nF2) <= Q2R err2)%R ->
  (0 <= Q2R err1)%R ->
  (0 <= Q2R err2)%R ->
  (Rabs (nR1 * nR2 - nF1 * nF2) <=
   RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 +
   Q2R err1 * Q2R err2)%R.
Proof.
  intros valid_e1 valid_e2 err1_bounded err2_bounded err1_pos err2_pos.
  unfold Rabs in err1_bounded.
  unfold Rabs in err2_bounded.
  (* Before doing case distinction, prove bounds that will be used many times: *)
  assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
    as upperBound_nR1
      by (apply contained_leq_maxAbs_val; auto).
  assert (nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R
    as upperBound_nR2
      by (apply contained_leq_maxAbs_val; auto).
  assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
    as upperBound_Ropp_nR1
      by (apply contained_leq_maxAbs_neg_val; auto).
  assert (- nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R
    as upperBound_Ropp_nR2
      by (apply contained_leq_maxAbs_neg_val; auto).
  assert (nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R
    as bound_nR1 by (apply Rmult_le_compat_r; auto).
  assert (- nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R
    as bound_neg_nR1 by (apply Rmult_le_compat_r; auto).
  assert (nR2 * Q2R err1 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R
    as bound_nR2 by (apply Rmult_le_compat_r; auto).
  assert (- nR2 * Q2R err1 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R
    as bound_neg_nR2 by (apply Rmult_le_compat_r; auto).
  assert (- (Q2R err1 * Q2R err2) <= Q2R err1 * Q2R err2)%R as err_neg_bound
      by  (rewrite Ropp_mult_distr_l; apply Rmult_le_compat_r; lra).
  assert (0 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R
    as zero_up_nR1 by lra.
  assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R
    as nR1_to_sum by lra.
  assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 <=  RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + Q2R err1 * Q2R err2)%R
    as sum_to_errsum by lra.
  (* Large case distinction for
         a) different cases of the value of Rabs (...) and
         b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *)
  destruct Rcase_abs in err1_bounded; destruct Rcase_abs in err2_bounded.
  + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded.
    rewrite Ropp_plus_distr in err1_bounded, err2_bounded.
    rewrite Ropp_involutive in err1_bounded, err2_bounded.
    assert (nF1 <= Q2R err1 + nR1)%R by lra.
    assert (nF2 <= Q2R err2 + nR2)%R by lra.
    unfold Rabs.
    destruct Rcase_abs.
    * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr.
      rewrite Ropp_involutive.
      destruct (Rle_lt_dec 0 nF1).
      { (* Upper Bound ... *)
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l; auto.
        apply H0.
        destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l. hnf. left; auto.
          assert (nR1 <= nF1)%R by lra.
          apply H1.
          lra.
      }
      {
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_neg_l.
        hnf. left; auto.
        assert (nR2 < nF2)%R by lra.
        apply Rlt_le in H1; apply H1.
        destruct (Rle_lt_dec 0 nR2).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          assert (nR1 < nF1)%R by lra.
          apply Rlt_le in H1; apply H1.
          lra.
      }
    * rewrite Rsub_eq_Ropp_Rplus.
      destruct (Rle_lt_dec 0 nF1).
      {
        rewrite Ropp_mult_distr_r.
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l; auto.
        assert (- nF2 <= - nR2)%R by lra.
        apply H1.
        destruct (Rle_lt_dec 0 (- nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          assert (nR1 < nF1)%R by lra.
          apply Rlt_le in H1; apply H1.
          lra.
      }
      {
        rewrite Ropp_mult_distr_l.
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l.
        rewrite <- (Ropp_involutive 0).
        apply Ropp_ge_le_contravar.
        apply Rle_ge.
        rewrite Ropp_0.
        hnf. left; auto.
        apply H0.
        destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          assert (- nF1 <= -nR1)%R by lra.
          apply H1.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          apply Ropp_le_ge_contravar in H.
          apply Rge_le in H.
          apply H.
          lra.
      }
  + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded.
    rewrite Ropp_plus_distr in err1_bounded.
    rewrite Ropp_involutive in err1_bounded.
    assert (nF1 <= Q2R err1 + nR1)%R by lra.
    assert (nF2 <= Q2R err2 + nR2)%R by lra.
    unfold Rabs.
    destruct Rcase_abs.
    * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr.
      rewrite Ropp_involutive.
      destruct (Rle_lt_dec 0 nF1).
      { (* Upper Bound ... *)
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l; auto.
        apply H0.
        destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l. hnf. left; auto.
          assert (nR1 <= nF1)%R by lra.
          apply H1.
          lra.
      }
      {
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_neg_l.
        hnf. left; auto.
        assert (- nF2 <= - (nR2 - Q2R err2))%R by lra.
        apply Ropp_le_ge_contravar in H1.
        repeat rewrite Ropp_involutive in H1.
        apply Rge_le in H1.
        apply H1.
        destruct (Rle_lt_dec 0 (nR2 - Q2R err2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          assert (nR1 < nF1)%R by lra.
          apply Rlt_le in H1; apply H1.
          lra.
      }
    * rewrite Rsub_eq_Ropp_Rplus.
      destruct (Rle_lt_dec 0 nF1).
      {
        rewrite Ropp_mult_distr_r.
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l; auto.
        assert (- nF2 <= - nR2 + Q2R err2)%R by lra.
        apply H1.
        destruct (Rle_lt_dec 0 (- nR2 + Q2R err2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          assert (nR1 < nF1)%R by lra.
          apply Rlt_le in H1; apply H1.
          lra.
      }
      {
        rewrite Ropp_mult_distr_l.
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l.
        rewrite <- (Ropp_involutive 0).
        apply Ropp_ge_le_contravar.
        apply Rle_ge.
        rewrite Ropp_0.
        hnf. left; auto.
        apply H0.
        destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          assert (- nF1 <= -nR1)%R by lra.
          apply H1.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          apply Ropp_le_ge_contravar in H.
          apply Rge_le in H.
          apply H.
          lra.
      }
  + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded.
    rewrite Ropp_plus_distr in err2_bounded.
    rewrite Ropp_involutive in err2_bounded.
    assert (nF1 <= Q2R err1 + nR1)%R by lra.
    assert (nF2 <= Q2R err2 + nR2)%R by lra.
    unfold Rabs.
    destruct Rcase_abs.
    * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr.
      rewrite Ropp_involutive.
      destruct (Rle_lt_dec 0 nF1).
      { (* Upper Bound ... *)
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l; auto.
        apply H0.
        destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l. hnf. left; auto.
          assert (- nF1 <= - (nR1 - Q2R err1))%R by lra.
          apply Ropp_le_ge_contravar in H1.
          repeat rewrite Ropp_involutive in H1.
          apply Rge_le in H1.
          apply H1.
          lra.
      }
      {
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_neg_l.
        hnf. left; auto.
        assert (nR2 < nF2)%R by lra.
        apply Rlt_le in H1; apply H1.
        destruct (Rle_lt_dec 0 nR2).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          assert (- nF1 <= - (nR1 - Q2R err1))%R by lra.
          apply Ropp_le_ge_contravar in H1.
          repeat rewrite Ropp_involutive in H1.
          apply Rge_le in H1.
          apply H1.
          lra.
      }
    * rewrite Rsub_eq_Ropp_Rplus.
      destruct (Rle_lt_dec 0 nF1).
      {
        rewrite Ropp_mult_distr_r.
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l; auto.
        assert (- nF2 <= - nR2)%R by lra.
        apply H1.
        destruct (Rle_lt_dec 0 (- nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          assert (- nF1 <= - (nR1 - Q2R err1))%R by lra.
          apply Ropp_le_ge_contravar in H1.
          repeat rewrite Ropp_involutive in H1.
          apply Rge_le in H1.
          apply H1.
          lra.
      }
      {
        rewrite Ropp_mult_distr_l.
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l.
        lra.
        apply H0.
        destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          assert (- nF1 <= - (nR1 - Q2R err1))%R by lra.
          apply H1.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l; try lra.
          apply Ropp_le_ge_contravar in H.
          apply Rge_le in H.
          apply H.
          lra.
      }
  (* All positive *)
  + assert (nF1 <= Q2R err1 + nR1)%R by lra.
    assert (nF2 <= Q2R err2 + nR2)%R by lra.
    unfold Rabs.
    destruct Rcase_abs.
    * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr.
      rewrite Ropp_involutive.
      destruct (Rle_lt_dec 0 nF1).
      { (* Upper Bound ... *)
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l; auto.
        apply H0.
        destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l. hnf. left; auto.
          assert (nR1 - Q2R err1 <= nF1)%R by lra.
          apply H1.
          lra.
      }
      {
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_neg_l.
        hnf. left; auto.
        assert (nR2 - Q2R err2 <= nF2)%R by lra.
        apply H1.
        destruct (Rle_lt_dec 0 (nR2 - Q2R err2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          lra.
          assert (nR1 - Q2R err1 <= nF1)%R by lra.
          apply H1.
          lra.
      }
    * rewrite Rsub_eq_Ropp_Rplus.
      destruct (Rle_lt_dec 0 nF1).
      {
        rewrite Ropp_mult_distr_r.
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l; auto.
        assert (- nF2 <= Q2R err2 - nR2)%R by lra.
        apply H1.
        destruct (Rle_lt_dec 0 (Q2R err2 - nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          apply H.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          lra.
          assert (nR1 - Q2R err1 <= nF1)%R by lra.
          apply H1.
          lra.
      }
      {
        rewrite Ropp_mult_distr_l.
        eapply Rle_trans.
        eapply Rplus_le_compat_l.
        eapply Rmult_le_compat_l.
        rewrite <- (Ropp_involutive 0).
        apply Ropp_ge_le_contravar.
        apply Rle_ge.
        rewrite Ropp_0.
        lra.
        apply H0.
        destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_r; auto.
          assert (- nF1 <= Q2R err1 - nR1)%R by lra.
          apply H1.
          lra.
        - eapply Rle_trans.
          eapply Rplus_le_compat_l.
          rewrite Rmult_comm.
          eapply Rmult_le_compat_neg_l.
          lra.
          apply Ropp_le_ge_contravar in H.
          apply Rge_le in H.
          apply H.
          lra.
      }
Qed.

Heiko Becker's avatar
Heiko Becker committed
851
Lemma validErrorboundCorrectMult E1 E2 A
852
      (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
853
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
854
  m = join m1 m2 ->
855 856 857
  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
  eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR REAL ->
858 859 860
  eval_expr E2 defVars (toRExp e1) nF1 m1 ->
  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
  eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
='s avatar
= committed
861
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
862
           (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m ->
='s avatar
= committed
863
  typeCheck (Binop Mult e1 e2) defVars Gamma = true ->
Heiko Becker's avatar
Heiko Becker committed
864
  validErrorbound (Binop Mult e1 e2) Gamma A dVars = true ->
865 866
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
867 868 869
  FloverMap.find e1 A = Some ((e1lo,e1hi),err1) ->
  FloverMap.find e2 A = Some ((e2lo, e2hi),err2) ->
  FloverMap.find (Binop Mult e1 e2) A = Some ((alo,ahi),e)->
870 871 872 873
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
874
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
875
         subexprr_ok valid_error valid_e1 valid_e2 A_e1 A_e2 A_mult
876
         err1_bounded err2_bounded.
877
  cbn in *; Flover_compute; type_conv; subst.
878
  eapply Rle_trans.
879
  eapply (mult_abs_err_bounded e1 e2); eauto.
Heiko Becker's avatar
Heiko Becker committed
880 881 882 883 884 885 886 887 888 889 890 891
  pose proof (typingSoundnessExp _ _ R2 e1_float).
  pose proof (typingSoundnessExp _ _ R1 e2_float).
  rewrite H in Heqo0; rewrite H0 in Heqo1; inversion Heqo0; inversion Heqo1; subst.
  clear H H0.
  rename R0 into valid_error.
  assert (0 <= Q2R err1)%R as err1_pos.
  { pose proof (err_always_positive e1 Gamma A dVars);
      eauto. }
  assert (0 <= Q2R err2)%R as err2_pos.
  { pose proof (err_always_positive e2 Gamma A dVars); eauto. }
  clear R2 R1.
  canonize_hyps.
892 893 894 895 896 897
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite Q2R_mult in valid_error.
  repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
  eapply Rle_trans.
  Focus 2.
  apply valid_error.
898
  apply Rplus_le_compat.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
899
  - eauto using multiplicationErrorBounded.
900 901 902
  - rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
    apply computeErrorR_up.
    apply contained_leq_maxAbs.
903
    assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
904 905
    pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded)
      as cont_err1.
906
    assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
907 908 909 910 911
    pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded)
      as cont_err2.
    pose proof (IntervalArith.interval_multiplication_valid _ _ cont_err1 cont_err2)
      as valid_mult.
    simpl in *; split.
912 913 914
    + rewrite Q2R_min4.
      repeat rewrite Q2R_mult;
        repeat rewrite Q2R_minus;
915
        repeat rewrite Q2R_plus. lra.
916 917 918
    + rewrite Q2R_max4.
      repeat rewrite Q2R_mult;
        repeat rewrite Q2R_minus;
919
        repeat rewrite Q2R_plus; lra.
920 921
Qed.

Heiko Becker's avatar
Heiko Becker committed
922
Lemma validErrorboundCorrectDiv E1 E2 A
923
      (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
924
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
925
  m = join m1 m2 ->
926 927 928
  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
  eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR REAL ->
929 930 931
  eval_expr E2 defVars (toRExp e1) nF1 m1 ->
  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
  eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
='s avatar
= committed
932 933 934
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
           (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m ->
  typeCheck (Binop Div e1 e2) defVars Gamma = true ->
Heiko Becker's avatar
Heiko Becker committed
935
  validErrorbound (Binop Div e1 e2) Gamma A dVars = true ->
936 937 938
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
  (Qleb e2hi 0 && negb (Qeq_bool e2hi 0) || Qleb 0 e2lo && negb (Qeq_bool e2lo 0) = true) ->
939 940 941
  FloverMap.find e1 A = Some ((e1lo,e1hi),err1) ->
  FloverMap.find e2 A = Some ((e2lo, e2hi),err2) ->
  FloverMap.find (Binop Div e1 e2) A = Some ((alo,ahi),e)->
942 943 944 945
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
946
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
947
         subexprr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real A_e1
Heiko Becker's avatar
Heiko Becker committed
948
         A_e2 A_div err1_bounded err2_bounded.
949
  cbn in *; Flover_compute; type_conv; subst.
950
  eapply Rle_trans.
951
  eapply (div_abs_err_bounded e1 e2); eauto.
Heiko Becker's avatar
Heiko Becker committed
952 953 954 955
  pose proof (typingSoundnessExp _ _ R2 e1_float).
  pose proof (typingSoundnessExp _ _ R0 e2_float).
  rewrite H in Heqo0; rewrite H0 in Heqo1; inversion Heqo0; inversion Heqo1; subst.
  clear H H0.
956
  rename L0 into no_div_zero_float.
957
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
958
  pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded).
959
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
960
  pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded).
Heiko Becker's avatar
Heiko Becker committed
961 962 963 964 965 966
  assert (0 <= Q2R err1)%R as err1_pos.
  { pose proof (err_always_positive e1 Gamma A); eauto. }
  assert (0 <= Q2R err2)%R as err2_pos.
  { pose proof (err_always_positive e2 Gamma A); eauto. }
  canonize_hyps.
  rename R1 into valid_error.
967 968 969 970 971
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite Q2R_mult in valid_error.
  rewrite Q2R_div in valid_error.
  - rewrite Q2R_mult in valid_error.
    repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
972 973
    rewrite <- maxAbs_impl_RmaxAbs_iv in valid_error.
    repeat rewrite <- minAbs_impl_RminAbs_iv in valid_error.
974 975 976 977 978 979 980
    apply le_neq_bool_to_lt_prop in no_div_zero_float; apply le_neq_bool_to_lt_prop in no_div_zero_real.
    assert ((IVhi (Q2R e2lo,Q2R e2hi) < 0)%R \/ (0 < IVlo (Q2R e2lo,Q2R e2hi))%R) as no_div_zero_real_R
          by (simpl; rewrite <- Q2R0_is_0; simpl in no_div_zero_real;
              destruct no_div_zero_real as [ndiv | ndiv]; apply Qlt_Rlt in ndiv; auto).
    apply Q_case_div_to_R_case_div in no_div_zero_float; apply Q_case_div_to_R_case_div in no_div_zero_real.
    assert (Q2R e2lo = 0 -> False)%R by (apply (lt_or_gt_neq_zero_lo _ (Q2R e2hi)); try auto; lra).
    assert (Q2R e2hi = 0 -> False)%R by (apply (lt_or_gt_neq_zero_hi (Q2R e2lo)); try auto; lra).
981 982 983 984
    eapply Rle_trans.
    Focus 2.
    apply valid_error.
    apply Rplus_le_compat.
985
    (* Error Propagation proof *)
Heiko Becker's avatar
Heiko Becker committed
986 987
    + clear A_e1 A_e2 valid_error eval_float eval_real e1_float
            e1_real e2_float e2_real A_div
988
            E1 E2 alo ahi nR nF e L.
989
      unfold widenInterval in *.
Heiko Becker's avatar
Heiko Becker committed
990 991 992 993
      simpl in *.
      rewrite Q2R_plus, Q2R_minus in no_div_zero_float.
      assert (Q2R e2lo - Q2R err2 = 0 -> False)%R by (apply (lt_or_gt_neq_zero_lo _ (Q2R e2hi + Q2R err2)); try auto; lra).
      assert (Q2R e2hi + Q2R err2 = 0 -> False)%R by (apply (lt_or_gt_neq_zero_hi (Q2R e2lo - Q2R err2)); try auto; lra).
994
      pose proof (interval_inversion_valid (Q2R e2lo,Q2R e2hi) no_div_zero_real_R valid_bounds_e2) as valid_bounds_inv_e2.
995
      clear no_div_zero_real_R.
996 997 998
      (* Before doing case distinction, prove bounds that will be used many times: *)
      assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
        as upperBound_nR1
999
          by (apply contained_leq_maxAbs_val; auto).
1000
      assert (/ nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R