ErrorValidation.v 108 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

Heiko Becker's avatar
Heiko Becker committed
152
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi P 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 157
    approxEnv E1 Gamma A fVars dVars E2 ->
    validIntervalbounds (Var Q v) A P dVars = true ->
158
    validErrorbound (Var Q v) exprTypes A dVars = true ->
159
    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
160 161 162
    dVars_range_valid dVars E1 A ->
    fVars_P_sound fVars E1 P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
163
    FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
164
    exists nF m,
165
    eval_expr E2 Gamma (toRExp (Var Q v)) nF m.
166
Proof.
Heiko Becker's avatar
Heiko Becker committed
167 168
  intros eval_real typing_ok approxCEnv bounds_valid error_valid v_sound
                     dVars_sound P_valid types_valid A_var.
169
  eapply validIntervalbounds_sound in bounds_valid; eauto.
170 171 172 173
  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.
174
  Flover_compute; type_conv.
175
  destruct (approxEnv_gives_value approxCEnv H1); try eauto.
176 177 178 179 180 181 182
  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:
183
  forall E1 E2 A (v:nat) e nR nF mF nlo nhi P fVars dVars Gamma exprTypes,
184
    eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
185 186
    eval_expr E2 Gamma (toRExp (Var Q v)) nF mF ->
    typeCheck (Var Q v) Gamma exprTypes = true ->
Heiko Becker's avatar
Heiko Becker committed
187 188
    approxEnv E1 Gamma A fVars dVars E2 ->
    validIntervalbounds (Var Q v) A P dVars = true ->
189
    validErrorbound (Var Q v) exprTypes A dVars = true ->
190
    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
191 192 193
    dVars_range_valid dVars E1 A ->
    fVars_P_sound fVars E1 P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
194
    FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
195 196 197
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
  intros * eval_real eval_float typing_ok approxCEnv bounds_valid error_valid
Heiko Becker's avatar
Heiko Becker committed
198
                     v_sound dVars_sound P_valid types_valid A_var.
199
  eapply validIntervalbounds_sound in bounds_valid; eauto.
200 201
  destruct_smart [find_v [eval_real2 bounds_valid]] bounds_valid.
  pose proof (meps_0_deterministic _ eval_real eval_real2); subst.
202
  cbn in *; Flover_compute; type_conv.
203
  inversion eval_real;
204 205 206
    inversion eval_float;
    subst.
  rename H1 into E1_v.
207
  rename L into error_pos.
208
  rename R into error_valid.
209 210 211
  case_eq (v mem dVars); [intros v_dVar | intros v_fVar].
  - rewrite v_dVar in *; simpl in *.
    rewrite NatSet.mem_spec in v_dVar.
212
    eapply approxEnv_dVar_bounded; eauto.
213 214 215
  - rewrite v_fVar in *; simpl in *.
    apply not_in_not_mem in v_fVar.
    assert (v  fVars) as v_in_fVars by set_tac.
216
    pose proof (approxEnv_fVar_bounded approxCEnv E1_v H6 v_in_fVars H5).
217
    eapply Rle_trans; eauto.
218
    canonize_hyps.
219
    repeat destr_factorize.
220
    rewrite computeErrorQ_computeErrorR in error_valid.
221
    eapply Rle_trans; eauto.
222 223 224 225
    rewrite <- maxAbs_impl_RmaxAbs.
    apply computeErrorR_up.
    apply contained_leq_maxAbs.
    simpl in *; auto.
226
Qed.
227

228
Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR  Gamma:
229
    eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR REAL ->
230
    exists nF m',
231
      eval_expr E2 Gamma (toRExp (Const m n)) nF m'.
232
Proof.
233
  intros eval_real .
234
  repeat eexists.
235 236 237
  eapply Const_dist'; eauto.
  instantiate (1:= 0%R).
  rewrite Rabs_R0. auto using mTypeToR_pos_R.
238 239
Qed.

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

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

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

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

Heiko Becker's avatar
Heiko Becker committed
929
Lemma validErrorboundCorrectDiv E1 E2 A
930
      (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
931
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
932
  m = join m1 m2 ->
933 934 935
  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 ->
936 937 938
  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
939 940 941
           (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
942
  validErrorbound (Binop Div e1 e2) Gamma A dVars = true ->
943 944 945
  (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) ->
946 947 948
  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)->
949 950 951 952
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
953
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
954
         subexprr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real A_e1
Heiko Becker's avatar
Heiko Becker committed
955
         A_e2 A_div err1_bounded err2_bounded.
956
  cbn in *; Flover_compute; type_conv; subst.
957
  eapply Rle_trans.
958
  eapply (div_abs_err_bounded e1 e2); eauto.
Heiko Becker's avatar
Heiko Becker committed
959 960 961 962
  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.
963
  rename L0 into no_div_zero_float.
964
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
965
  pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded).
966
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
967
  pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded).
Heiko Becker's avatar
Heiko Becker committed
968 969 970 971 972 973
  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.
974 975 976 977 978
  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.
979 980
    rewrite <- maxAbs_impl_RmaxAbs_iv in valid_error.
    repeat rewrite <- minAbs_impl_RminAbs_iv in valid_error.
981 982 983 984 985 986 987
    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).
988 989 990 991
    eapply Rle_trans.
    Focus 2.
    apply valid_error.
    apply Rplus_le_compat.
992
    (* Error Propagation proof *)
Heiko Becker's avatar
Heiko Becker committed
993 994
    + clear A_e1 A_e2 valid_error eval_float eval_real e1_float
            e1_real e2_float e2_real A_div
995
            E1 E2 alo ahi nR nF e L.
996
      unfold widenInterval in *.
Heiko Becker's avatar
Heiko Becker committed
997 998 999 1000
      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).
1001
      pose proof (interval_inversion_valid (Q2R e2lo,Q2R e2hi) no_div_zero_real_R valid_bounds_e2) as valid_bounds_inv_e2.
1002
      clear no_div_zero_real_R.
1003 1004 1005
      (* Before doing case distinction, prove bounds that will be used many times: *)
      assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
        as upperBound_nR1
1006
          by (apply contained_leq_maxAbs_val; auto).
1007
      assert (/ nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R
1008
        as upperBound_nR2
1009
          by (apply contained_leq_maxAbs_val; auto).
1010 1011
      assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
        as upperBound_Ropp_nR1
1012
          by (apply contained_leq_maxAbs_neg_val; auto).
1013
      assert (- / nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R
1014
        as upperBound_Ropp_nR2
1015
          by (apply contained_leq_maxAbs_neg_val; auto).
1016 1017 1018 1019 1020 1021
      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).
1022
      unfold invertInterval in *; simpl in upperBound_nR2, upperBound_Ropp_nR2.
Heiko Becker's avatar
Heiko Becker committed
1023
      (* Case distinction for the divisor range
1024
         positive or negative in float and real valued execution *)
1025
      destruct no_div_zero_real as [ real_iv_neg | real_iv_pos];
1026
        destruct no_div_zero_float as [float_iv_neg | float_iv_pos].
1027
      (* The range of the divisor lies in the range from -infinity until 0 *)
1028
      * unfold widenIntv in *; simpl in *.
1029 1030 1031
        rewrite <- Q2R_plus in float_iv_neg.
        rewrite <- Q2R0_is_0 in float_iv_neg.
        rewrite <- Q2R0_is_0 in real_iv_neg.
Heiko Becker's avatar
Heiko Becker committed
1032
        pose proof (err_prop_inversion_neg float_iv_neg real_iv_neg err2_bounded valid_bounds_e2 H0 err2_pos) as err_prop_inv.
Heiko Becker's avatar
Heiko Becker committed
1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051
        rewrite Q2R_plus in float_iv_neg.
        rewrite Q2R0_is_0 in float_iv_neg.
        rewrite Q2R0_is_0 in real_iv_neg.
        rewrite Q2R_minus, Q2R_plus.
        repeat rewrite minAbs_negative_iv_is_hi; try lra.
        unfold Rdiv.
        repeat rewrite Q2R1.
        rewrite Rmult_1_l.
        (* Prove inequality to 0 in Q *)
        assert (e2lo == 0 -> False)
               by (rewrite <- Q2R0_is_0 in real_iv_neg; apply Rlt_Qlt in real_iv_neg;
                   assert (e2lo < 0) by (apply (Qle_lt_trans _ e2hi); try auto; apply Rle_Qle; lra);
                   lra).
        assert (e2hi == 0 -> False)
          by (rewrite <- Q2R0_is_0 in real_iv_neg; apply Rlt_Qlt in real_iv_neg; lra).
        rewrite Rabs_case_inverted in err1_bounded, err2_bounded.
        assert (nF1 <= Q2R err1 + nR1)%R as ub_nF1 by lra.
        assert (nR1 - Q2R err1 <= nF1)%R as lb_nF1 by lra.
        destruct err2_bounded as [[nR2_sub_pos err2_bounded] | [nR2_sub_neg err2_bounded]].
Heiko Becker's avatar
Heiko Becker committed
1052
        (* Positive case for abs (nR2 - nF2) <= err2 *)
Heiko Becker's avatar
Heiko Becker committed
1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068
        { rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, Ropp_involutive.
          apply Rgt_lt in nR2_sub_pos.
          assert (nF2 < nR2)%R as nF2_le_nR2 by lra.
          apply Ropp_lt_contravar in nF2_le_nR2.
          apply Rinv_lt_contravar in nF2_le_nR2; [ | apply Rmult_0_lt_preserving; try lra].
          repeat (rewrite <- Ropp_inv_permute in nF2_le_nR2; try lra).
          apply Ropp_lt_contravar in nF2_le_nR2.
          repeat rewrite Ropp_involutive in nF2_le_nR2.
          assert (/ nR2 - / nF2 < 0)%R as abs_inv_neg by lra.
          rewrite Rabs_left in err_prop_inv; try lra.
          rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded, err_prop_inv.
          assert (/nF2 <= /nR2 + Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R as error_prop_inv_up by lra.
          assert (/nR2 - Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) <= /nF2)%R as error_prop_inv_down by lra.
          (* Next do a case distinction for the absolute value*)
          unfold Rabs.
          destruct Rcase_abs.
Heiko Becker's avatar
Heiko Becker committed
1069
          (* Case 1: Absolute value negative *)
Heiko Becker's avatar
Heiko Becker committed
1070 1071 1072