ErrorValidation.v 107 KB
Newer Older
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
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
15
     Infra.RealSimps Infra.Ltacs Environments IntervalValidation TypeValidator
Nikita Zyuzin's avatar
Nikita Zyuzin committed
16
     ErrorBounds RealRangeValidator.
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 153 154
Section soundnessProofs.

  Definition eval_Real E1 Gamma (e:expr Q) nR :=
155
    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) nR REAL.
156 157 158

  Arguments eval_Real _ _ _ _/.

159 160
  Definition eval_Fin E2 Gamma DeltaMap (e:expr Q) nF m :=
    eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) nF m.
161 162 163

  Arguments eval_Fin _ _ _ _ _/.

164
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi fVars
165
      dVars Gamma DeltaMap exprTypes:
166
  eval_Real E1 Gamma (Var Q v) nR ->
167
    validTypes (Var Q v) Gamma DeltaMap ->
168
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
169
    validRanges (Var Q v) A E1 (toRTMap (toRExpMap Gamma)) ->
170
    validErrorbound (Var Q v) exprTypes A dVars = true ->
171
    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
172
    FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
173
    exists nF m,
174
    eval_Fin E2 Gamma DeltaMap (Var Q v) nF m.
175
Proof.
176 177
  intros eval_real typing_ok approxCEnv bounds_valid error_valid v_sound A_var.
  apply validRanges_single in bounds_valid.
178
  destruct_smart [find_v [eval_real2 bounds_valid]] bounds_valid.
179
  pose proof (meps_0_deterministic _ eval_real eval_real2); subst.
180 181
  cbn in *.
  inversion eval_real; subst.
182
  Flover_compute; type_conv.
183
  destruct (approxEnv_gives_value approxCEnv H1); try eauto.
184 185 186 187 188 189
  - set_tac.
    case_eq (NatSet.mem v dVars); intros v_case; set_tac.
    left; apply v_sound.
    apply NatSetProps.FM.diff_3; set_tac.
  - destruct typing_ok as [? [tdef ?]].
    exists x, x0. eapply Var_load; eauto.
190 191
    eapply toRExpMap_some; eauto; simpl; auto.
Qed.
192 193

Lemma validErrorboundCorrectVariable:
194
  forall E1 E2 A (v:nat) e nR nF mF nlo nhi fVars dVars Gamma DeltaMap,
195
    eval_Real E1 Gamma (Var Q v) nR ->
196
    eval_Fin E2 Gamma DeltaMap (Var Q v) nF mF ->
197
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
198
    validTypes (Var Q v) (Gamma) DeltaMap ->
199 200
    validRanges (Var Q v) A E1 (toRTMap (toRExpMap Gamma)) ->
    validErrorbound (Var Q v) Gamma A dVars = true ->
201
    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
202
    FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
203 204
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
205
  intros * eval_real eval_float approxCEnv typing_ok bounds_valid error_valid
206 207
                     v_sound A_var.
  apply validRanges_single in bounds_valid.
208 209
  destruct_smart [find_v [eval_real2 bounds_valid]] bounds_valid.
  pose proof (meps_0_deterministic _ eval_real eval_real2); subst.
210
  cbn in *; Flover_compute; type_conv.
211
  inversion eval_real;
212 213 214
    inversion eval_float;
    subst.
  rename H1 into E1_v.
215
  rename L into error_pos.
216
  rename R into error_valid.
217 218 219
  case_eq (v mem dVars); [intros v_dVar | intros v_fVar].
  - rewrite v_dVar in *; simpl in *.
    rewrite NatSet.mem_spec in v_dVar.
220
    eapply approxEnv_dVar_bounded; eauto.
221 222 223
  - rewrite v_fVar in *; simpl in *.
    apply not_in_not_mem in v_fVar.
    assert (v  fVars) as v_in_fVars by set_tac.
224
    pose proof (approxEnv_fVar_bounded approxCEnv E1_v H6 v_in_fVars H5).
225
    eapply Rle_trans; eauto.
226
    canonize_hyps.
227
    repeat destr_factorize.
228
    rewrite computeErrorQ_computeErrorR in error_valid.
229
    eapply Rle_trans; eauto.
230 231
    eapply toRExpMap_some in Heqo; eauto; simpl in *.
    assert (m = mF) by congruence; subst.
232 233 234 235
    rewrite <- maxAbs_impl_RmaxAbs.
    apply computeErrorR_up.
    apply contained_leq_maxAbs.
    simpl in *; auto.
236
Qed.
237

238 239 240 241
Lemma validErrorboundCorrectConstant_eval E2 m n Gamma DeltaMap:
    (forall (e' : expr R) (m' : mType),
        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    validTypes (Const m n) Gamma DeltaMap ->
242
    exists nF m',
243
      eval_Fin E2 Gamma DeltaMap (Const m n) nF m'.
244
Proof.
245 246
  intros deltas_matched typing_ok.
  simpl in typing_ok.
247
  destruct typing_ok as [? [type_def [? ?]]]; subst.
248
  specialize (deltas_matched (Const x (Q2R n)) x) as (delta & delta_matched & delta_bound).
249
  repeat eexists.
250
  eapply Const_dist' with (delta := delta); eauto.
251
Qed.
252

253
Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma DeltaMap:
254
    eval_Real E1 Gamma (Const m n) nR ->
255 256
    eval_Fin E2 Gamma DeltaMap (Const m n) nF m ->
    validTypes (Const m n) Gamma DeltaMap ->
257
    validErrorbound (Const m n) Gamma A dVars = true ->
258
    (Q2R nlo <= nR <= Q2R nhi)%R ->
259
    FloverMap.find (Const m n) A = Some ((nlo,nhi),e) ->
260 261
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
262
  intros eval_real eval_float subexprr_ok error_valid intv_valid A_const.
263
  unfold eval_Real in *.
264
  cbn in *; Flover_compute; type_conv.
Heiko Becker's avatar
Heiko Becker committed
265 266
  eapply Rle_trans.
  eapply const_abs_err_bounded; eauto.
267
  rename R into error_valid.
Heiko Becker's avatar
Heiko Becker committed
268
  inversion eval_real; subst.
269 270 271 272 273 274 275
  canonize_hyps.
  eapply Rle_trans; eauto.
  rewrite computeErrorQ_computeErrorR.
  rewrite <- maxAbs_impl_RmaxAbs.
  apply computeErrorR_up.
  apply contained_leq_maxAbs.
  simpl in *; auto.
276
Qed.
277

Heiko Becker's avatar
Heiko Becker committed
278
Lemma validErrorboundCorrectAddition E1 E2 A
279
      (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
280
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma DeltaMap:
281 282 283
  eval_Real E1 Gamma e1 nR1 ->
  eval_Real E1 Gamma e2 nR2 ->
  eval_Real E1 Gamma (Binop Plus e1 e2) nR ->
284 285
  eval_Fin E2 Gamma DeltaMap e1 nF1 m1 ->
  eval_Fin E2 Gamma DeltaMap e2 nF2 m2 ->
286
  eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
287 288 289
            (updDefVars (Binop Plus (Var R 1) (Var R 2)) m
                        (updDefVars (Var Rdefinitions.R 2) m2
                                    (updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
290 291 292 293 294 295
            (fun (x : expr Rdefinitions.R) (_ : mType) =>
               if
                 R_orderedExps.eq_dec x (Binop Plus (Var Rdefinitions.R 1) (Var Rdefinitions.R 2))
               then Some delta0
               else None)
            (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
Heiko Becker's avatar
Heiko Becker committed
296
  validErrorbound (Binop Plus e1 e2) Gamma A dVars = true ->
297 298
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
299 300 301
  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)->
302
  FloverMap.find (Binop Plus e1 e2) Gamma = Some m ->
303 304 305 306
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
307
  intros e1_real e2_real eval_real e1_float e2_float eval_float
308 309
         valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
         Gamma_Plus err1_bounded err2_bounded.
310
  cbn in *; Flover_compute; type_conv.
311
  eapply Rle_trans.
312 313 314
  eapply
    (add_abs_err_bounded e1 e2);
    try eauto.
315
  repeat destr_factorize.
316
  rename R0 into valid_error.
317 318 319 320
  canonize_hyps.
  eapply Rle_trans; eauto.
  repeat rewrite Q2R_plus.
  repeat apply Rplus_le_compat_l.
321 322
  clear L R.
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
323 324
  pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded)
       as contained_widen1.
325
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
326 327 328
  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).
329
  subst.
330 331 332 333
  rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
  apply computeErrorR_up.
  apply contained_leq_maxAbs.
  simpl in *; split.
334 335
  - rewrite Q2R_min4.
    repeat rewrite Q2R_plus;
336
      repeat rewrite Q2R_minus; lra.
337 338
  - rewrite Q2R_max4.
    repeat rewrite Q2R_plus;
339
      repeat rewrite Q2R_minus; lra.
340
Qed.
Heiko Becker's avatar
Heiko Becker committed
341

Heiko Becker's avatar
Heiko Becker committed
342
Lemma validErrorboundCorrectSubtraction E1 E2 A
343
      (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
344
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma DeltaMap:
345 346 347
  eval_Real E1 Gamma e1 nR1 ->
  eval_Real E1 Gamma e2 nR2 ->
  eval_Real E1 Gamma (Binop Sub e1 e2) nR ->
348 349
  eval_Fin E2 Gamma DeltaMap e1 nF1 m1->
  eval_Fin E2 Gamma DeltaMap e2 nF2 m2 ->
350
  eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
351 352 353
            (updDefVars (Binop Sub (Var R 1) (Var R 2)) m
                        (updDefVars (Var Rdefinitions.R 2) m2
                                    (updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
354 355
            DeltaMap
            (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
Heiko Becker's avatar
Heiko Becker committed
356
  validErrorbound (Binop Sub e1 e2) Gamma A dVars = true ->
357 358
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
359 360 361
  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)->
362
  FloverMap.find (Binop Sub e1 e2) Gamma = Some m ->
363 364 365 366
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
367 368
  intros e1_real e2_real eval_real e1_float e2_float eval_float
         valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub Gamma_sub
369
         err1_bounded err2_bounded.
370
  cbn in *; Flover_compute; type_conv.
371
  eapply Rle_trans.
372
  eapply (subtract_abs_err_bounded e1 e2); try eauto.
373
  repeat destr_factorize.
374 375
  rename R0 into valid_error.
  canonize_hyps.
376 377 378
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite Q2R_mult in valid_error.
  repeat rewrite Q2R_plus in valid_error.
379 380
  eapply Rle_trans; eauto.
  repeat apply Rplus_le_compat_l.
381
  rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
382 383 384
  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.
385
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
386 387 388
  pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded)
       as contained_widen2.
  pose proof (IntervalArith.interval_subtraction_valid _ _ contained_widen1 contained_widen2).
389 390 391
  apply computeErrorR_up.
  apply contained_leq_maxAbs.
  simpl in *; split.
392 393 394 395 396
  - rewrite Q2R_min4.
    repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus;
      repeat rewrite Q2R_opp;
      repeat rewrite Q2R_plus;
397
      repeat rewrite Q2R_minus; lra.
398 399 400 401 402
  - rewrite Q2R_max4.
    repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus;
      repeat rewrite Q2R_opp;
      repeat rewrite Q2R_plus;
403
      repeat rewrite Q2R_minus; lra.
404 405
Qed.

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

Heiko Becker's avatar
Heiko Becker committed
938
Lemma validErrorboundCorrectDiv E1 E2 A
939
      (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
940
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma DeltaMap:
941 942 943
  eval_Real E1 Gamma e1 nR1 ->
  eval_Real E1 Gamma e2 nR2 ->
  eval_Real E1 Gamma (Binop Div e1 e2) nR ->
944 945
  eval_Fin E2 Gamma DeltaMap e1 nF1 m1->
  eval_Fin E2 Gamma DeltaMap e2 nF2 m2 ->
946
  eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
947 948 949
            (updDefVars (Binop Div (Var R 1) (Var R 2)) m
                        (updDefVars (Var Rdefinitions.R 2) m2
                                    (updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
950 951
            DeltaMap
            (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m ->
Heiko Becker's avatar
Heiko Becker committed
952
  validErrorbound (Binop Div e1 e2) Gamma A dVars = true ->
953 954 955
  (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) ->
956 957 958
  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)->
959
  FloverMap.find (Binop Div e1 e2) Gamma = Some m ->
960 961 962 963
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
964 965
  intros e1_real e2_real eval_real e1_float e2_float eval_float valid_error
         valid_intv1 valid_intv2 no_div_zero_real A_e1 A_e2 A_sub Gamma_sub
966
         err1_bounded err2_bounded.
967 968
  cbn in *; Flover_compute; type_conv.
  canonize_hyps.
969
  eapply Rle_trans.
970
  eapply (div_abs_err_bounded e1 e2); eauto.
971
  rename L0 into no_div_zero_float.
972
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
973
  pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded).
974
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
975
  pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded).
Heiko Becker's avatar
Heiko Becker committed
976 977 978 979 980 981
  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.
982 983 984 985 986
  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.
987 988
    rewrite <- maxAbs_impl_RmaxAbs_iv in valid_error.
    repeat rewrite <- minAbs_impl_RminAbs_iv in valid_error.
989 990 991 992 993 994 995
    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).
996
    eapply Rle_trans; eauto.
997
    apply Rplus_le_compat.
998
    (* Error Propagation proof *)
Heiko Becker's avatar
Heiko Becker committed
999
    + clear A_e1 A_e2 valid_error eval_float eval_real e1_float
1000
            e1_real e2_float e2_real A_sub E1 E2 alo ahi nR nF e L.
1001
      unfold widenInterval in *.
Heiko Becker's avatar
Heiko Becker committed
1002 1003 1004 1005
      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).
1006
      pose proof (interval_inversion_valid (Q2R e2lo,Q2R e2hi) no_div_zero_real_R valid_intv2) as valid_bounds_inv_e2.
1007
      clear no_div_zero_real_R.
1008 1009 1010
      (* Before doing case distinction, prove bounds that will be used many times: *)
      assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
        as upperBound_nR1
1011
          by (apply contained_leq_maxAbs_val; auto).
1012
      assert (/ nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R
1013
        as upperBound_nR2
1014
          by (apply contained_leq_maxAbs_val; auto).
1015 1016
      assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
        as upperBound_Ropp_nR1
1017
          by (apply contained_leq_maxAbs_neg_val; auto).
1018
      assert (- / nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R
1019
        as upperBound_Ropp_nR2
1020
          by (apply contained_leq_maxAbs_neg_val; auto).
1021 1022 1023 1024 1025 1026
      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).
1027
      unfold invertInterval in *; simpl in upperBound_nR2, upperBound_Ropp_nR2.
Heiko Becker's avatar
Heiko Becker committed
1028
      (* Case distinction for the divisor range
1029
         positive or negative in float and real valued execution *)
1030
      destruct no_div_zero_real as [ real_iv_neg | real_iv_pos];
1031
        destruct no_div_zero_float as [float_iv_neg | float_iv_pos].
1032
      (* The range of the divisor lies in the range from -infinity until 0 *)
1033
      * unfold widenIntv in *; simpl in *.
1034 1035 1036
        rewrite <- Q2R_plus in float_iv_neg.
        rewrite <- Q2R0_is_0 in float_iv_neg.
        rewrite <- Q2R0_is_0 in real_iv_neg.
1037
        pose proof (err_prop_inversion_neg float_iv_neg real_iv_neg err2_bounded valid_intv2 H0 err2_pos) as err_prop_inv.
Heiko Becker's avatar
Heiko Becker committed
1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056
        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]].