ErrorValidation.v 115 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 12 13 14
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs
               Coq.QArith.Qreals Coq.micromega.Psatz Coq.Reals.Reals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps
               Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps
               Daisy.Infra.Ltacs Daisy.Environments
               Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds.
15

Heiko Becker's avatar
Heiko Becker committed
16
(** Error bound validator **)
17 18 19 20 21
Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
         (typeMap:exp Q -> option mType) (* derived types for e *)
         (A:analysisResult) (* encoded result of Daisy *)
         (dVars:NatSet.t) (* let-bound variables encountered previously *):=
  let (intv, err) := (A e) in
22 23 24 25
  let mopt := typeMap e in
  match mopt with
  | None => false
  | Some m =>
26
    if (Qleb 0 err) (* encoding soundness: errors are positive *)
27
    then
28
      match e with (* case analysis for the expression *)
='s avatar
= committed
29
      |Var _ v =>
30
       if (NatSet.mem v dVars)
31
       then true (* defined variables are checked at definition point *)
32
       else (Qleb (maxAbs intv * (mTypeToQ m)) err)
33
      |Const _ n =>
34
       Qleb (maxAbs intv * (mTypeToQ m)) err
='s avatar
= committed
35
      |Unop Neg e1 =>
36 37
       if (validErrorbound e1 typeMap A dVars)
       then Qeq_bool err (snd (A e1))
38
       else false
='s avatar
= committed
39
      |Unop Inv e1 => false
40
      |Binop b e1 e2 =>
41 42
       if ((validErrorbound e1 typeMap A dVars)
             && (validErrorbound e2 typeMap A dVars))
43
       then
44 45
         let (ive1, err1) := A e1 in
         let (ive2, err2) := A e2 in
46 47 48 49 50 51
         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 =>
52
           Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
53
         | Sub =>
54
           Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
55
         | Mult =>
56
           Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
57 58 59 60 61 62 63
         | 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
64
             Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err
65 66 67
           else false
         end
       else false
68 69 70 71 72 73 74 75 76 77 78 79 80 81
      | Fma e1 e2 e3 =>
        if ((validErrorbound e1 typeMap A dVars)
              && (validErrorbound e2 typeMap A dVars)
              && (validErrorbound e3 typeMap A dVars))
        then
          let (ive1, err1) := A e1 in
          let (ive2, err2) := A e2 in
          let (ive3, err3) := A e3 in
          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
Nikita Zyuzin's avatar
Nikita Zyuzin committed
82 83 84
          let errIntv_prod := multIntv errIve2 errIve3 in
          let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
          Qleb (err1 + mult_error_bound + (maxAbs (addIntv errIntv_prod errIve1)) * (mTypeToQ m)) err
85
        else false
86
      |Downcast m1 e1 =>
87
       if validErrorbound e1 typeMap A dVars
88
       then
89
         let (ive1, err1) := A e1 in
90 91 92 93
         let errIve1 := widenIntv ive1 err1 in
         (Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
       else
         false
94 95 96
      end
    else false
  end.
Heiko Becker's avatar
Heiko Becker committed
97

98
(** Error bound command validator **)
99 100 101 102 103
Fixpoint validErrorboundCmd (f:cmd Q) (* analyzed cmd with let's *)
         (typeMap:exp Q -> option mType) (* inferred types *)
         (A:analysisResult) (* Daisy's encoded result *)
         (dVars:NatSet.t) (* defined variables *)
         : bool :=
104
  match f with
105
  |Let m x e g =>
106 107
   if ((validErrorbound e typeMap A dVars) && (Qeq_bool (snd (A e)) (snd (A (Var Q x)))))
   then validErrorboundCmd g typeMap A (NatSet.add x dVars)
108
   else false
109
  |Ret e => validErrorbound e typeMap A dVars
110 111
  end.

112 113 114
(* Hide mTypeToQ from simplification since it will blow up the goal buffer *)
Arguments mTypeToQ _ :simpl nomatch.

Heiko Becker's avatar
Heiko Becker committed
115 116 117 118 119
(**
    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.
**)
120 121
Lemma err_always_positive e tmap (absenv:analysisResult) iv err dVars:
  validErrorbound e tmap absenv dVars = true ->
122 123 124
  (iv,err) = absenv e ->
  (0 <= Q2R err)%R.
Proof.
125
  destruct e; intros validErrorbound_e absenv_e;
126
    unfold validErrorbound in validErrorbound_e;
127 128 129 130 131
    rewrite <- absenv_e in validErrorbound_e; simpl in *;
  repeat match goal with
  | [H: context [match ?E with | Some _ => _ |None => _ end] |- _ ] => destruct (E) eqn:?; try congruence
  | [H: context [if ?c then _ else _ ] |- _] => destruct (c) eqn:?; try congruence end;
    canonize_hyps; auto.
132
Qed.
Heiko Becker's avatar
Heiko Becker committed
133

134
Lemma validErrorboundCorrectVariable_eval:
135 136 137 138
  forall E1 E2 absenv (v:nat) e nR nlo nhi P fVars dVars Gamma expTypes,
    eval_exp E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
    typeCheck (Var Q v) Gamma expTypes = true ->
    approxEnv E1 Gamma absenv fVars dVars E2 ->
='s avatar
= committed
139
    validIntervalbounds (Var Q v) absenv P dVars = true ->
140 141
    validErrorbound (Var Q v) expTypes absenv dVars = true ->
    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
='s avatar
= committed
142
    (forall v1,
143
        NatSet.mem v1 dVars = true ->
='s avatar
= committed
144
        exists r, E1 v1 = Some r /\
='s avatar
= committed
145
             (Q2R (fst (fst (absenv (Var Q v1)))) <= r <= Q2R (snd (fst (absenv (Var Q v1)))))%R) ->
146
    (forall v1, NatSet.mem v1 fVars= true ->
147
          exists r, E1 v1 = Some r /\
148
                (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) ->
149 150 151
    (forall v1 : NatSet.elt,
        NatSet.mem v1 (NatSet.union fVars dVars) = true ->
        exists m0 : mType, Gamma v1 = Some m0) ->
='s avatar
= committed
152
    absenv (Var Q v) = ((nlo, nhi), e) ->
153
    exists nF m,
154
    eval_exp E2 Gamma (toRExp (Var Q v)) nF m.
155
Proof.
156 157
  intros * eval_real typing_ok approxCEnv bounds_valid error_valid v_sound
                     dVars_sound P_valid types_valid absenv_var.
158 159 160 161 162 163 164 165 166 167 168 169
  eapply validIntervalbounds_sound in bounds_valid; eauto.
  destruct bounds_valid as [nR2 [eval_real2 bounds_valid]].
  assert (nR2 = nR) by (eapply meps_0_deterministic; eauto);
    subst.
  simpl in eval_real; inversion eval_real; subst.
  rename H1 into E1_v.
  simpl in *.
  assert (exists m, Gamma v = Some m) as v_has_type.
  { destruct (expTypes (Var Q v)); try congruence.
    case_eq (Gamma v); intros * gamma_v;
      rewrite gamma_v in *; eauto. }
  destruct v_has_type as [m type_v].
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
  destruct (approxEnv_gives_value approxCEnv E1_v); try eauto.
  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:
  forall E1 E2 absenv (v:nat) e nR nF mF nlo nhi P fVars dVars Gamma expTypes,
    eval_exp E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
    eval_exp E2 Gamma (toRExp (Var Q v)) nF mF ->
    typeCheck (Var Q v) Gamma expTypes = true ->
    approxEnv E1 Gamma absenv fVars dVars E2 ->
    validIntervalbounds (Var Q v) absenv P dVars = true ->
    validErrorbound (Var Q v) expTypes absenv dVars = true ->
    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
    (forall v1,
        NatSet.mem v1 dVars = true ->
        exists r, E1 v1 = Some r /\
             (Q2R (fst (fst (absenv (Var Q v1)))) <= r <= Q2R (snd (fst (absenv (Var Q v1)))))%R) ->
    (forall v1, NatSet.mem v1 fVars= true ->
          exists r, E1 v1 = Some r /\
                (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) ->
    (forall v1 : NatSet.elt,
        NatSet.mem v1 (NatSet.union fVars dVars) = true ->
        exists m0 : mType, Gamma v1 = Some m0) ->
    absenv (Var Q v) = ((nlo, nhi), e) ->
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
  intros * eval_real eval_float typing_ok approxCEnv bounds_valid error_valid
                     v_sound dVars_sound P_valid types_valid absenv_var.
  eapply validIntervalbounds_sound in bounds_valid; eauto.
  destruct bounds_valid as [nR2 [eval_real2 bounds_valid]].
  assert (nR2 = nR) by (eapply meps_0_deterministic; eauto);
    subst.
  simpl in *;
    inversion eval_real;
    inversion eval_float;
    subst.
  rename H1 into E1_v.
  simpl in *.
211 212 213
  rewrite absenv_var in error_valid; simpl in error_valid.
  case_eq (expTypes (Var Q v));
    intros * expType_v; rewrite expType_v in *; try congruence.
214 215 216 217
  match goal with
  | [ H: Gamma v = Some _ |- _] => rewrite H in *
  end; simpl in *.
  type_conv.
218 219
  andb_to_prop error_valid.
  rename L into error_pos.
220
  rename R into error_valid.
221 222 223
  case_eq (v mem dVars); [intros v_dVar | intros v_fVar].
  - rewrite v_dVar in *; simpl in *.
    rewrite NatSet.mem_spec in v_dVar.
224 225
    eapply approxEnv_dVar_bounded; eauto.
    rewrite absenv_var; auto.
226 227 228
  - rewrite v_fVar in *; simpl in *.
    apply not_in_not_mem in v_fVar.
    assert (v  fVars) as v_in_fVars by set_tac.
229
    pose proof (approxEnv_fVar_bounded approxCEnv E1_v H6 v_in_fVars H5).
230 231 232 233 234 235 236 237 238 239 240
    eapply Rle_trans.
    apply H.
    canonize_hyps.
    rewrite Q2R_mult in error_valid.
    rewrite <- maxAbs_impl_RmaxAbs in error_valid.
    eapply Rle_trans; eauto.
    eapply Rmult_le_compat_r.
    + apply mTypeToQ_pos_R.
    + rewrite absenv_var in *; simpl in *.
      destruct bounds_valid as [valid_lo valid_hi].
      apply RmaxAbs; eauto.
241
Qed.
242

243
Lemma validErrorboundCorrectConstant_eval E1 E2 absenv m n nR e nlo nhi dVars Gamma defVars:
244
    eval_exp E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 ->
='s avatar
= committed
245
    typeCheck (Const m n) defVars Gamma = true ->
246
    validErrorbound (Const m n) Gamma absenv dVars = true ->
247
    (Q2R nlo <= nR <= Q2R nhi)%R ->
248
    absenv (Const m n) = ((nlo,nhi),e) ->
249
    exists nF m',
250
      eval_exp E2 defVars (toRExp (Const m n)) nF m'.
251
Proof.
252
  intros eval_real subexpr_ok error_valid intv_valid absenv_const.
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
  repeat eexists.
  econstructor.
  rewrite Rabs_eq_Qabs.
  apply Qle_Rle.
  rewrite Qabs_pos; try lra.
  apply mTypeToQ_pos_Q. lra.
Qed.

Lemma validErrorboundCorrectConstant E1 E2 absenv m n nR nF e nlo nhi dVars Gamma defVars:
    eval_exp E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 ->
    eval_exp E2 defVars (toRExp (Const m n)) nF m ->
    typeCheck (Const m n) defVars Gamma = true ->
    validErrorbound (Const m n) Gamma absenv dVars = true ->
    (Q2R nlo <= nR <= Q2R nhi)%R ->
    absenv (Const m n) = ((nlo,nhi),e) ->
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
  intros eval_real eval_float subexpr_ok error_valid intv_valid absenv_const.
Heiko Becker's avatar
Heiko Becker committed
271
  eapply Rle_trans.
272
  simpl in eval_real,eval_float.
Heiko Becker's avatar
Heiko Becker committed
273
  eapply const_abs_err_bounded; eauto.
274
  unfold validErrorbound in error_valid.
Heiko Becker's avatar
Heiko Becker committed
275
  rewrite absenv_const in *; simpl in *.
276
  case_eq (Gamma (Const m n)); intros * type_const;
277
    rewrite type_const in error_valid; try congruence.
278 279
  andb_to_prop error_valid.
  rename R into error_valid.
Heiko Becker's avatar
Heiko Becker committed
280
  inversion eval_real; subst.
281 282
  simpl in *; rewrite Q2R0_is_0 in *.
  rewrite delta_0_deterministic in intv_valid; auto.
283 284
  apply Qle_bool_iff in error_valid.
  apply Qle_Rle in error_valid.
Heiko Becker's avatar
Heiko Becker committed
285
  destruct intv_valid.
286
  eapply Rle_trans.
Heiko Becker's avatar
Heiko Becker committed
287
  - eapply Rmult_le_compat_r.
288
    apply mTypeToQ_pos_R.
Heiko Becker's avatar
Heiko Becker committed
289
    apply RmaxAbs; eauto.
Heiko Becker's avatar
Heiko Becker committed
290
  - rewrite Q2R_mult in error_valid.
Heiko Becker's avatar
Heiko Becker committed
291
    rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto.
292
    inversion subexpr_ok; subst.
293 294
    rewrite type_const in *.
    apply mTypeEq_compat_eq in H3; subst; auto.
295
Qed.
296

297
Lemma validErrorboundCorrectAddition E1 E2 absenv
298
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
299
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars:
300 301 302 303
  m = join m1 m2 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR M0 ->
304 305 306
  eval_exp E2 defVars (toRExp e1) nF1 m1 ->
  eval_exp E2 defVars (toRExp e2) nF2 m2 ->
  eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
='s avatar
= committed
307
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
308
           (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
='s avatar
= committed
309
  typeCheck (Binop Plus e1 e2) defVars Gamma = true ->
310
  validErrorbound (Binop Plus e1 e2) Gamma absenv dVars = true ->
311 312
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
313 314 315 316 317 318 319
  absenv e1 = ((e1lo,e1hi),err1) ->
  absenv e2 = ((e2lo, e2hi),err2) ->
  absenv (Binop Plus e1 e2) = ((alo,ahi),e)->
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
320
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
321
         subexpr_ok valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_add
322
         err1_bounded err2_bounded.
323
  eapply Rle_trans.
324 325 326
  eapply
    (add_abs_err_bounded e1 e2);
    try eauto.
327 328
  unfold validErrorbound in valid_error.
  rewrite absenv_add,absenv_e1,absenv_e2 in valid_error.
329
  case_eq (Gamma (Binop Plus e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ].
330 331 332 333
  simpl in subexpr_ok; rewrite H in subexpr_ok.
  case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ].
  case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ].
  andb_to_prop subexpr_ok.
334
  apply mTypeEq_compat_eq in L0; subst.
335 336 337 338
  pose proof (typingSoundnessExp _ _ R0 e1_float).
  pose proof (typingSoundnessExp _ _ R e2_float).
  rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst.
  clear H2 H3 H0 H1.
339
  andb_to_prop valid_error.
340
  rename R2 into valid_error.
341 342 343
  eapply Rle_trans.
  apply Rplus_le_compat_l.
  eapply Rmult_le_compat_r.
344
  apply mTypeToQ_pos_R.
345 346 347
  Focus 2.
  rewrite Qle_bool_iff in valid_error.
  apply Qle_Rle in valid_error.
348 349 350 351 352 353 354
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite Q2R_mult in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite <- Rabs_eq_Qabs in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
  apply valid_error.
355
  clear L R.
356 357 358 359 360 361 362
  remember (addIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
  iv_assert iv iv_unf.
  destruct iv_unf as [ivl [ivh iv_unf]].
  rewrite iv_unf.
  rewrite <- maxAbs_impl_RmaxAbs.
  assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
  assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
363
  rewrite <- H0, <- H1.
364
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
365
  pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded).
366
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
367 368 369
  pose proof (distance_gives_iv (a:=nR2) _ (Q2R e2lo, Q2R e2hi) contained_intv2 err2_bounded).
  pose proof (IntervalArith.interval_addition_valid _ _ H2 H3).
  simpl in *.
370
  destruct H4.
371 372 373 374 375 376 377 378
  subst; simpl in *.
  apply RmaxAbs; simpl.
  - rewrite Q2R_min4.
    repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus; auto.
  - rewrite Q2R_max4.
    repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus; auto.
379
Qed.
Heiko Becker's avatar
Heiko Becker committed
380

381
Lemma validErrorboundCorrectSubtraction E1 E2 absenv
382
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
383
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
384 385 386 387
  m = join m1 m2 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 ->
388 389 390
  eval_exp E2 defVars (toRExp e1) nF1 m1->
  eval_exp E2 defVars (toRExp e2) nF2 m2 ->
  eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
='s avatar
= committed
391
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
392
           (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
='s avatar
= committed
393
  typeCheck (Binop Sub e1 e2) defVars Gamma = true ->
394
  validErrorbound (Binop Sub e1 e2) Gamma absenv dVars = true ->
395 396
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
397 398 399 400 401 402 403
  absenv e1 = ((e1lo,e1hi),err1) ->
  absenv e2 = ((e2lo, e2hi),err2) ->
  absenv (Binop Sub e1 e2) = ((alo,ahi),e)->
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
404
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
405
         subexpr_ok valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_sub
406 407
         err1_bounded err2_bounded.
  eapply Rle_trans.
408 409 410
  eapply (subtract_abs_err_bounded e1 e2); try eauto.
  unfold validErrorbound in valid_error.
  rewrite absenv_sub,absenv_e1,absenv_e2 in valid_error.
411
  case_eq (Gamma (Binop Sub e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ].
412 413 414 415
  simpl in subexpr_ok; rewrite H in subexpr_ok.
  case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ].
  case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ].
  andb_to_prop subexpr_ok.
416
  apply mTypeEq_compat_eq in L0; subst.
417 418 419 420
  pose proof (typingSoundnessExp _ _ R0 e1_float).
  pose proof (typingSoundnessExp _ _ R e2_float).
  rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst.
  clear H2 H3 H0 H1.
421
  andb_to_prop valid_error.
422
  rename R2 into valid_error.
423 424 425 426 427 428 429 430 431 432 433
  apply Qle_bool_iff in valid_error.
  apply Qle_Rle in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite Q2R_mult in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite <- Rabs_eq_Qabs in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
  eapply Rle_trans.
  apply Rplus_le_compat_l.
  eapply Rmult_le_compat_r.
434
  apply mTypeToQ_pos_R.
435 436
  Focus 2.
  apply valid_error.
437 438 439 440 441 442 443
  remember (subtractIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
  iv_assert iv iv_unf.
  destruct iv_unf as [ivl [ivh iv_unf]].
  rewrite iv_unf.
  rewrite <- maxAbs_impl_RmaxAbs.
  assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
  assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
444
  rewrite <- H0, <- H1.
445
    assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
446
  pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded).
447
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
448 449 450
  pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded).
  pose proof (IntervalArith.interval_subtraction_valid _ _ H2 H3).
  simpl in *.
451
  destruct H4.
452 453 454 455 456 457 458 459 460 461 462 463 464 465
  subst; simpl in *.
  apply RmaxAbs; simpl.
  - rewrite Q2R_min4.
    repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus;
      repeat rewrite Q2R_opp;
      repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus; auto.
  - rewrite Q2R_max4.
    repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus;
      repeat rewrite Q2R_opp;
      repeat rewrite Q2R_plus;
      repeat rewrite Q2R_minus; auto.
466 467
Qed.

468
Lemma validErrorboundCorrectMult E1 E2 absenv
469
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
470
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
471 472 473 474
  m = join m1 m2 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR M0 ->
475 476 477
  eval_exp E2 defVars (toRExp e1) nF1 m1 ->
  eval_exp E2 defVars (toRExp e2) nF2 m2 ->
  eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
='s avatar
= committed
478
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
479
           (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m ->
='s avatar
= committed
480
  typeCheck (Binop Mult e1 e2) defVars Gamma = true ->
481
  validErrorbound (Binop Mult e1 e2) Gamma absenv dVars = true ->
482 483
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
484 485 486 487 488 489 490
  absenv e1 = ((e1lo,e1hi),err1) ->
  absenv e2 = ((e2lo, e2hi),err2) ->
  absenv (Binop Mult e1 e2) = ((alo,ahi),e)->
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
491
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
492
         subexpr_ok valid_error valid_e1 valid_e2 absenv_e1 absenv_e2 absenv_mult
493 494
         err1_bounded err2_bounded.
  eapply Rle_trans.
495
  eapply (mult_abs_err_bounded e1 e2); eauto.
496 497
  unfold validErrorbound in valid_error.
  rewrite absenv_mult,absenv_e1,absenv_e2 in valid_error.
498
  case_eq (Gamma (Binop Mult e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ].
499 500 501 502
  simpl in subexpr_ok; rewrite H in subexpr_ok.
  case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ].
  case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ].
  andb_to_prop subexpr_ok.
503
  apply mTypeEq_compat_eq in L0; subst.
504 505 506 507
  pose proof (typingSoundnessExp _ _ R0 e1_float).
  pose proof (typingSoundnessExp _ _ R e2_float).
  rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst.
  clear H2 H3 H0 H1.
508
  andb_to_prop valid_error.
509
  rename R2 into valid_error.
510 511
  assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma absenv dVars); eauto).
  assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma absenv dVars); eauto).
512
  clear R1 L1.
513 514 515 516 517 518 519 520 521 522 523
  apply Qle_bool_iff in valid_error.
  apply Qle_Rle in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite Q2R_mult in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite <- Rabs_eq_Qabs in valid_error.
  repeat rewrite Q2R_plus in valid_error.
  repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
  eapply Rle_trans.
  Focus 2.
  apply valid_error.
524 525
  apply Rplus_le_compat.
  - unfold Rabs in err1_bounded.
526 527 528 529
    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
530
        by (apply contained_leq_maxAbs_val; auto).
531 532
    assert (nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R
      as upperBound_nR2
533
        by (apply contained_leq_maxAbs_val; auto).
534 535
    assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
      as upperBound_Ropp_nR1
536
        by (apply contained_leq_maxAbs_neg_val; auto).
537 538
    assert (- nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R
      as upperBound_Ropp_nR2
539
        by (apply contained_leq_maxAbs_neg_val; auto).
540 541 542 543 544 545 546 547
    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).
548 549
    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).
550 551 552 553 554 555
    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.
Heiko Becker's avatar
Heiko Becker committed
556 557
    clear e1_real e1_float e2_real e2_float eval_real eval_float valid_error
      absenv_e1 absenv_e2.
558
    (* Large case distinction for
Heiko Becker's avatar
Heiko Becker committed
559 560
         a) different cases of the value of Rabs (...) and
         b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *)
561 562 563 564 565 566 567 568 569 570 571 572 573 574 575
    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.
576
          apply H1.
577 578 579 580
          destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
581
            apply H0.
582 583 584 585 586
            lra.
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            rewrite Rmult_comm.
            eapply Rmult_le_compat_neg_l. hnf. left; auto.
587
            assert (nR1 <= nF1)%R by lra.
588
            apply H2.
589 590 591 592 593 594 595 596
            lra.
        }
        {
          eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          assert (nR2 < nF2)%R by lra.
597
          apply Rlt_le in H2; apply H2.
598 599 600 601
          destruct (Rle_lt_dec 0 nR2).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
602
            apply H0.
603 604 605 606 607 608 609
            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.
610
            apply Rlt_le in H2; apply H2.
611 612 613 614 615 616 617 618 619 620
            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.
621
          apply H2.
622 623 624 625
          destruct (Rle_lt_dec 0 (- nR2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
626
            apply H0.
627 628 629 630 631 632 633
            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.
634
            apply Rlt_le in H2; apply H2.
635 636 637 638 639 640 641 642 643 644 645 646
            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.
647
          apply H1.
648 649 650 651 652
          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.
653
            apply H2.
654 655 656 657 658 659
            lra.
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            rewrite Rmult_comm.
            eapply Rmult_le_compat_neg_l.
            hnf. left; auto.
660 661 662
            apply Ropp_le_ge_contravar in H0.
            apply Rge_le in H0.
            apply H0.
663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678
            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.
679
          apply H1.
680 681 682 683
          destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
684
            apply H0.
685 686 687 688 689 690
            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.
691
            apply H2.
692 693 694 695 696 697 698 699
            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.
700 701 702 703
          apply Ropp_le_ge_contravar in H2.
          repeat rewrite Ropp_involutive in H2.
          apply Rge_le in H2.
          apply H2.
704 705 706 707
          destruct (Rle_lt_dec 0 (nR2 - Q2R err2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
708
            apply H0.
709 710 711 712 713 714 715
            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.
716
            apply Rlt_le in H2; apply H2.
717 718 719 720 721 722 723 724 725 726
            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.
727
          apply H2.
728 729 730 731
          destruct (Rle_lt_dec 0 (- nR2 + Q2R err2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
732
            apply H0.
733 734 735 736 737 738 739
            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.
740
            apply Rlt_le in H2; apply H2.
741 742 743 744 745 746 747 748 749 750 751 752
            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.
753
          apply H1.
754 755 756 757 758
          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.
759
            apply H2.
760 761 762 763 764 765
            lra.
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            rewrite Rmult_comm.
            eapply Rmult_le_compat_neg_l.
            hnf. left; auto.
766 767 768
            apply Ropp_le_ge_contravar in H0.
            apply Rge_le in H0.
            apply H0.
769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784
            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.
785
          apply H1.
786 787 788 789
          destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
790
            apply H0.
791 792 793 794 795 796
            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.
797 798 799 800
            apply Ropp_le_ge_contravar in H2.
            repeat rewrite Ropp_involutive in H2.
            apply Rge_le in H2.
            apply H2.
801 802 803 804 805 806 807 808
            lra.
        }
        {
          eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_neg_l.
          hnf. left; auto.
          assert (nR2 < nF2)%R by lra.
809
          apply Rlt_le in H2; apply H2.
810 811 812 813
          destruct (Rle_lt_dec 0 nR2).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
814
            apply H0.
815 816 817 818 819 820 821
            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.
822 823 824 825
            apply Ropp_le_ge_contravar in H2.
            repeat rewrite Ropp_involutive in H2.
            apply Rge_le in H2.
            apply H2.
826 827 828 829 830 831 832 833 834 835
            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.
836
          apply H2.
837 838 839 840
          destruct (Rle_lt_dec 0 (- nR2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
841
            apply H0.
842 843 844 845 846 847 848
            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.
849 850 851 852
            apply Ropp_le_ge_contravar in H2.
            repeat rewrite Ropp_involutive in H2.
            apply Rge_le in H2.
            apply H2.
853 854 855 856 857 858 859 860
            lra.
        }
        {
          rewrite Ropp_mult_distr_l.
          eapply Rle_trans.
          eapply Rplus_le_compat_l.
          eapply Rmult_le_compat_l.
          lra.
861
          apply H1.
862 863 864 865 866
          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.
867
            apply H2.
868 869 870 871 872
            lra.
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            rewrite Rmult_comm.
            eapply Rmult_le_compat_neg_l; try lra.
873 874 875
            apply Ropp_le_ge_contravar in H0.
            apply Rge_le in H0.
            apply H0.
876 877
            lra.
        }
Heiko Becker's avatar
Heiko Becker committed
878
    (* All positive *)
879 880 881 882 883 884 885 886 887 888 889
    + 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.
890
          apply H1.
891 892 893 894
          destruct (Rle_lt_dec 0 (Q2R err2 + nR2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.
895
            apply H0.
896 897 898 899 900 901
            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.
902
            apply H2.
903 904
            lra.
        }
905 906 907 908 909 910
        {
          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.
911
          apply H2.
912 913 914 915
          destruct (Rle_lt_dec 0 (nR2 - Q2R err2)).
          - eapply Rle_trans.
            eapply Rplus_le_compat_l.
            eapply Rmult_le_compat_r; auto.