ErrorValidation.v 106 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
(**
Heiko Becker's avatar
Heiko Becker committed
2 3 4 5 6 7
   This file contains the coq implementation of the error bound validator as well
   as its soundness proof. The function validErrorbound is the Error bound
   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
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
Heiko Becker's avatar
Heiko Becker committed
10
Require Import Coq.micromega.Psatz Coq.Reals.Reals.
11
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps Daisy.Infra.Ltacs.
12
Require Import Daisy.Environments Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds.
13

Heiko Becker's avatar
Heiko Becker committed
14
(** Error bound validator **)
15
Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analysisResult) (dVars:NatSet.t):=
16
  let (intv, err) := (absenv e) in
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
  let mopt := typeMap e in
  match mopt with
  | None => false
  | Some m =>
    if (Qleb 0 err)
    then
      match e with
      |Var _ _ v =>
       if (NatSet.mem v dVars)
       then true
       else (Qleb (maxAbs intv * (meps m)) err)
      |Const _ n =>
       Qleb (maxAbs intv * (meps m)) err
      |Unop _ _ => false
      |Binop b e1 e2 =>
       if ((validErrorbound e1 typeMap absenv dVars) && (validErrorbound e2 typeMap absenv dVars))
       then
         let (ive1, err1) := absenv e1 in
         let (ive2, err2) := absenv e2 in
         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 =>
           Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (meps m)) err
         | Sub =>
           Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (meps m)) err
         | Mult =>
           Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * (meps m)) err
         | 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
             Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (meps m)) err
           else false
         end
       else false
      |Downcast m1 e1 =>
       let (ive1, err1) := absenv e1 in
       let rec := validErrorbound e1 typeMap absenv dVars in
       let errIve1 := widenIntv ive1 err1 in
       andb rec (Qleb (err1 + maxAbs errIve1 * (meps m1)) err)
      end
    else false
  end.
Heiko Becker's avatar
Heiko Becker committed
66 67


68
(** Error bound command validator **)
='s avatar
= committed
69
Fixpoint validErrorboundCmd (f:cmd Q) (typeMap:exp Q -> option mType) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool :=
70
  match f with
71
  |Let m x e g =>
='s avatar
= committed
72 73
   if ((validErrorbound e typeMap env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q m x)))))
   then validErrorboundCmd g typeMap env (NatSet.add x dVars)
74
   else false
='s avatar
= committed
75
  |Ret e => validErrorbound e typeMap env dVars
76 77
  end.

Heiko Becker's avatar
Heiko Becker committed
78 79 80 81 82
(**
    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.
**)
83 84
Lemma err_always_positive e tmap (absenv:analysisResult) iv err dVars:
  validErrorbound e tmap absenv dVars = true ->
85 86 87
  (iv,err) = absenv e ->
  (0 <= Q2R err)%R.
Proof.
88
  destruct e; intros validErrorbound_e absenv_e;
89
    unfold validErrorbound in validErrorbound_e;
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
    rewrite <- absenv_e in validErrorbound_e; simpl in *.
  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
    + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
    + destruct (tmap (Var Q m n)); inversion validErrorbound_e.
  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
    + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
    + destruct (tmap (Const m q)); inversion validErrorbound_e.
  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
    + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
    + destruct (tmap (Unop u e)); inversion validErrorbound_e.
  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
    + apply Qle_bool_iff, Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
    + destruct (tmap (Binop b e1 e2));inversion validErrorbound_e.
  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
    + apply Qle_bool_iff, Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
    + destruct (tmap (Downcast m e));inversion validErrorbound_e.
106
Qed.
Heiko Becker's avatar
Heiko Becker committed
107

108

109
Lemma validErrorboundCorrectVariable:
110 111
  forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma,
    validType Gamma (Var Q m v) m ->
112
    approxEnv E1 absenv fVars dVars E2 ->
113 114
    eval_exp E1 (toREval (toRExp (Var Q m v))) nR M0 ->
    eval_exp E2 (toRExp (Var Q m v)) nF m ->
115
    validIntervalbounds (Var Q m v) absenv P dVars = true ->
116
    validErrorbound (Var Q m v) Gamma absenv dVars = true ->
Raphaël Monat's avatar
Raphaël Monat committed
117
    (forall v1 m1,
118
        NatSet.mem v1 dVars = true ->
119 120
        exists r mv1,
          E1 v1 = Some (r, M0) /\ Gamma (Var Q mv1 v1) = Some m1 /\
121 122 123 124
          (Q2R (fst (fst (absenv (Var Q m1 v1)))) <= r <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) ->
    (forall v1, NatSet.mem v1 fVars= true ->
          exists r, E1 v1 = Some (r, M0) /\
                (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) ->
125
    absenv (Var Q m v) = ((nlo, nhi), e) ->
126 127
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
128
  intros * typing_ok approxCEnv eval_real eval_float bounds_valid error_valid dVars_sound P_valid absenv_var.
129 130 131
  simpl in eval_real; inversion eval_real; inversion eval_float; subst.
  rename H2 into E1_v;
    rename H7 into E2_v.
132
  simpl in error_valid.
133
  rewrite absenv_var in error_valid; simpl in error_valid; subst.
134
  case_eq (Gamma (Var Q m v)); intros; rewrite H in error_valid; [ | inversion error_valid].
135
  rewrite <- andb_lazy_alt in error_valid.
136 137
  andb_to_prop error_valid.
  rename L into error_pos.
138 139 140
  rename R into error_valid.
  (* induction on the approximation relation to do a case distinction on whether
     we argue currently about a free or a let bound variable *)
141
  induction approxCEnv.
142
  (* empty environment case, contradiction *)
143
  - unfold emptyEnv in *; simpl in *.
144
    congruence.
145 146 147
  - unfold updEnv in *; simpl in *.
    case_eq (v =? x); intros eq_case; rewrite eq_case in *.
    + rewrite Nat.eqb_eq in eq_case; subst.
148
      assert (NatSet.mem x dVars = false) as x_not_bound.
149 150
      * case_eq (NatSet.mem x dVars); intros case_mem; try auto.
        rewrite NatSet.mem_spec in case_mem.
151 152 153 154 155 156
        assert (NatSet.In x (NatSet.union fVars dVars))
          as x_in_union by (rewrite NatSet.union_spec; auto).
        rewrite <- NatSet.mem_spec in x_in_union.
        rewrite x_in_union in *.
        congruence.
      * rewrite x_not_bound in error_valid.
157
        inversion E1_v; inversion E2_v; subst.
158 159 160 161 162
        eapply Rle_trans; try eauto.
        apply Qle_bool_iff in error_valid.
        apply Qle_Rle in error_valid.
        eapply Rle_trans; eauto.
        rewrite Q2R_mult.
163 164 165
        inversion typing_ok; subst.
        rewrite H in H5; inversion H5; subst.
        clear H5 H3.
166
        apply Rmult_le_compat_r.
167
        { apply inj_eps_posR. } 
168
        { rewrite <- maxAbs_impl_RmaxAbs.
169
          apply contained_leq_maxAbs.
170
          unfold contained; simpl.
171 172
          assert ((toRExp (Var Q m x)) = Var R m x) by (simpl; auto).
          rewrite <- H2 in eval_float.
173
          pose proof (validIntervalbounds_sound A P (E:=fun y : nat => if y =? x then Some (nR, M0) else E1 y) (vR:=nR) typing_ok bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf.
174 175
          rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
          apply valid_bounds_prf; try auto.
176 177 178 179 180
          - intros v v_mem_diff.
            rewrite NatSet.diff_spec, NatSet.singleton_spec in v_mem_diff.
            destruct v_mem_diff as [v_eq v_no_dVar].
            subst.
            rewrite NatSet.add_spec; auto. }
181
    + apply IHapproxCEnv; try auto.
182 183
      * constructor; auto.
      * constructor; auto.
='s avatar
= committed
184 185
      * intros v0 m2 mem_dVars.
          specialize (dVars_sound v0 m2 mem_dVars).
186
        destruct dVars_sound as [vR0 [mR0 iv_sound_val]].
187
        case_eq (v0 =? x); intros case_mem;
188
          rewrite case_mem in iv_sound_val; simpl in iv_sound_val.
189 190 191 192 193 194
        { rewrite Nat.eqb_eq in case_mem; subst.
          rewrite NatSet.mem_spec in mem_dVars.
          assert (NatSet.In x (NatSet.union fVars dVars))
            as x_in_union by (rewrite NatSet.union_spec; auto).
          rewrite <- NatSet.mem_spec in x_in_union;
            rewrite x_in_union in *; congruence. }
195
        { exists vR0, mR0; split; auto; destruct iv_sound_val as [E1_v0 iv_sound_val]; auto. }
196 197 198 199 200 201 202 203 204 205 206
      * intros v0 v0_fVar.
        assert (NatSet.mem v0 (NatSet.add x fVars) = true)
          as v0_in_add by (rewrite NatSet.mem_spec, NatSet.add_spec; rewrite NatSet.mem_spec in v0_fVar; auto).
        specialize (P_valid v0 v0_in_add).
        case_eq (v0 =? x); intros case_v0; rewrite case_v0 in *; try auto.
        rewrite Nat.eqb_eq in case_v0; subst.
        assert (NatSet.mem x (NatSet.union fVars dVars) = true)
          as x_in_union
            by (rewrite NatSet.mem_spec, NatSet.union_spec; rewrite NatSet.mem_spec in v0_fVar; auto).
        rewrite x_in_union in *; congruence.
  - unfold updEnv in E1_v, E2_v; simpl in *.
207 208
    case_eq (v =? x); intros eq_case; rewrite eq_case in *.
    + rewrite Nat.eqb_eq in eq_case; subst.
209 210 211
      inversion E1_v; inversion E2_v; subst.
      rewrite absenv_var in *; auto.
    + apply IHapproxCEnv; try auto.
212 213
      * constructor; auto.
      * constructor; auto.
214 215 216 217
      * rewrite absenv_var.
        case_eq (NatSet.mem v dVars);
        intros case_dVars; rewrite case_dVars in *; simpl in *; try auto.
        assert (NatSet.mem v (NatSet.add x dVars) = false) as not_in_add.
218
        { case_eq (NatSet.mem v (NatSet.add x dVars));
219
            intros case_add; rewrite case_add in *; simpl in *; try auto.
220 221
          - rewrite NatSet.mem_spec in case_add.
            rewrite NatSet.add_spec in case_add.
222
            destruct case_add as [v_eq_x | v_dVar]; subst.
223
            + rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto.
224
            + rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars.
225
              inversion case_dVars. }
226 227
        { rewrite absenv_var in bounds_valid. rewrite not_in_add in bounds_valid.
          auto. }
228 229 230 231 232 233 234 235 236 237 238 239 240
      * rewrite absenv_var in bounds_valid; simpl in *.
        case_eq (NatSet.mem v dVars);
        intros case_dVars; rewrite case_dVars in *; simpl in *; try auto.
        assert (NatSet.mem v (NatSet.add x dVars) = false) as not_in_add.
        { case_eq (NatSet.mem v (NatSet.add x dVars));
            intros case_add; rewrite case_add in *; simpl in *; try auto.
          - rewrite NatSet.mem_spec in case_add.
            rewrite NatSet.add_spec in case_add.
            destruct case_add as [v_eq_x | v_dVar]; subst.
            + rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto.
            + rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars.
              inversion case_dVars. }
        { rewrite not_in_add in error_valid; auto. }
='s avatar
= committed
241 242
      * intros v0 m2 mem_dVars.
        specialize (dVars_sound v0 m2).
243 244
        rewrite absenv_var in *; simpl in *.
        rewrite NatSet.mem_spec in mem_dVars.
245
        assert (NatSet.In v0 (NatSet.add x dVars)) as v0_in_add.
246
        { rewrite NatSet.add_spec. right; auto. }
247
        { rewrite <- NatSet.mem_spec in v0_in_add.
248 249 250
          specialize (dVars_sound v0_in_add).
          destruct dVars_sound as [vR0 [mR0 [val_def iv_sound_val]]].
          exists vR0, mR0; split; auto.
251
          unfold updEnv in val_def; simpl in val_def.
252 253
          case_eq (v0 =? x); intros case_mem;
            rewrite case_mem in val_def; simpl in val_def.
254 255
          - rewrite Nat.eqb_eq in case_mem; subst.
            apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars.
256
            rewrite <- NatSet.mem_spec in mem_dVars.
257
            rewrite mem_dVars in *; congruence.
258
          - auto. }
259
      * rewrite absenv_var in bounds_valid.
260 261 262 263 264 265 266 267 268 269
        intros v0 v0_fVar.
        specialize (P_valid v0 v0_fVar).
        unfold updEnv in P_valid; simpl in *.
        case_eq (v0 =? x); intros case_v0; rewrite case_v0 in *; try auto.
        rewrite Nat.eqb_eq in case_v0; subst.
        assert (NatSet.mem x (NatSet.union fVars dVars) = true)
          as x_in_union
            by (rewrite NatSet.mem_spec, NatSet.union_spec; rewrite NatSet.mem_spec in v0_fVar; auto).
        rewrite x_in_union in *; congruence.
Qed.
270

271
Lemma validErrorboundCorrectConstant:
272
  forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars m Gamma,
273 274
    eval_exp E1 (toREval (toRExp (Const m n))) nR M0 ->
    eval_exp E2 (toRExp (Const m n)) nF m ->
275 276
    validType Gamma (Const m n) m ->
    validErrorbound (Const m n) Gamma absenv dVars = true ->
277
    (Q2R nlo <= nR <= Q2R nhi)%R ->
278
    absenv (Const m n) = ((nlo,nhi),e) ->
279 280
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
281
  intros *  eval_real eval_float subexpr_ok error_valid intv_valid absenv_const.
Heiko Becker's avatar
Heiko Becker committed
282
  eapply Rle_trans.
283
  simpl in eval_real,eval_float.
Heiko Becker's avatar
Heiko Becker committed
284
  eapply const_abs_err_bounded; eauto.
285
  unfold validErrorbound in error_valid.
Heiko Becker's avatar
Heiko Becker committed
286
  rewrite absenv_const in *; simpl in *.
287
  case_eq (Gamma (Const m n)); intros; rewrite H in error_valid; [ | inversion error_valid ].
288 289
  andb_to_prop error_valid.
  rename R into error_valid.
Heiko Becker's avatar
Heiko Becker committed
290
  inversion eval_real; subst.
291
  simpl in H3; rewrite Q2R0_is_0 in H3.
Heiko Becker's avatar
Heiko Becker committed
292
  rewrite delta_0_deterministic in *; auto.
293 294
  apply Qle_bool_iff in error_valid.
  apply Qle_Rle in error_valid.
Heiko Becker's avatar
Heiko Becker committed
295
  destruct intv_valid.
296
  eapply Rle_trans.
Heiko Becker's avatar
Heiko Becker committed
297
  - eapply Rmult_le_compat_r.
298
    apply inj_eps_posR.
Heiko Becker's avatar
Heiko Becker committed
299
    apply RmaxAbs; eauto.
Heiko Becker's avatar
Heiko Becker committed
300
  - rewrite Q2R_mult in error_valid.
Heiko Becker's avatar
Heiko Becker committed
301
    rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto.
302 303
    inversion subexpr_ok; subst.
    rewrite H in H6; inversion H6; subst; auto.
304
Qed.
305

306
Lemma validErrorboundCorrectAddition E1 E2 absenv
307
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
308
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma:
309 310 311 312 313 314 315
  m = computeJoin m1 m2 ->
  eval_exp E1 (toREval (toRExp e1)) nR1 M0 ->
  eval_exp E1 (toREval (toRExp e2)) nR2 M0 ->
  eval_exp E1 (toREval (toRExp (Binop Plus e1 e2))) nR M0 ->
  eval_exp E2 (toRExp e1) nF1 m1 ->
  eval_exp E2 (toRExp e2) nF2 m2 ->
  eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Plus (Var Q m1 1) (Var Q m2 2))) nF m ->
316 317
  validType Gamma (Binop Plus e1 e2) m ->
  validErrorbound (Binop Plus e1 e2) Gamma absenv dVars = true ->
318 319
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
320 321 322 323 324 325 326
  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.
327
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
328
         subexpr_ok valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_add
329
         err1_bounded err2_bounded.
330
  eapply Rle_trans.
331 332 333
  eapply
    (add_abs_err_bounded e1 e2);
    try eauto.
334 335
  unfold validErrorbound in valid_error.
  rewrite absenv_add,absenv_e1,absenv_e2 in valid_error.
336 337
  case_eq (Gamma (Binop Plus e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ].
  inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6.
338
  andb_to_prop valid_error.
339
  rename R0 into valid_error.
340 341 342
  eapply Rle_trans.
  apply Rplus_le_compat_l.
  eapply Rmult_le_compat_r.
343
  apply inj_eps_posR.
344 345 346
  Focus 2.
  rewrite Qle_bool_iff in valid_error.
  apply Qle_Rle in valid_error.
347 348 349 350 351 352 353
  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.
354
  clear L R.
355 356 357 358 359 360 361
  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).
362
  rewrite <- H0, <- H1.
363 364 365 366
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
  pose proof (distance_gives_iv (a:=nR1) _ contained_intv1 err1_bounded).
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
  pose proof (distance_gives_iv (a:=nR2) _ contained_intv2 err2_bounded).
367 368 369
  pose proof (IntervalArith.interval_addition_valid H2 H3).
  unfold IntervalArith.contained in H4.
  destruct H4.
370 371 372 373 374 375 376 377
  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.
378
Qed.
Heiko Becker's avatar
Heiko Becker committed
379

380
Lemma validErrorboundCorrectSubtraction E1 E2 absenv
381
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
382
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma:
383 384 385 386 387 388 389
  m = computeJoin m1 m2 ->
  eval_exp E1 (toREval (toRExp e1)) nR1 M0 ->
  eval_exp E1 (toREval (toRExp e2)) nR2 M0 ->
  eval_exp E1 (toREval (toRExp (Binop Sub e1 e2))) nR M0 ->
  eval_exp E2 (toRExp e1) nF1 m1->
  eval_exp E2 (toRExp e2) nF2 m2 ->
  eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Sub (Var Q m1 1) (Var Q m2 2))) nF m ->
390 391
  validType Gamma (Binop Sub e1 e2) m ->
  validErrorbound (Binop Sub e1 e2) Gamma absenv dVars = true ->
392 393
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
394 395 396 397 398 399 400
  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.
401
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
402
         subexpr_ok valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_sub
403 404
         err1_bounded err2_bounded.
  eapply Rle_trans.
405 406 407
  eapply (subtract_abs_err_bounded e1 e2); try eauto.
  unfold validErrorbound in valid_error.
  rewrite absenv_sub,absenv_e1,absenv_e2 in valid_error.
408 409
  case_eq (Gamma (Binop Sub e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ].
  inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6.
410
  andb_to_prop valid_error.
411
  rename R0 into valid_error.
412 413 414 415 416 417 418 419 420 421 422
  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.
423
  apply inj_eps_posR.
424 425
  Focus 2.
  apply valid_error.
426 427 428 429 430 431 432
  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).
433
  rewrite <- H0, <- H1.
434 435 436 437
    assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
  pose proof (distance_gives_iv (a:=nR1) _ contained_intv1 err1_bounded).
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
  pose proof (distance_gives_iv (a:=nR2) _ contained_intv2 err2_bounded).
438 439 440
  pose proof (IntervalArith.interval_subtraction_valid H2 H3).
  unfold IntervalArith.contained in H4.
  destruct H4.
441 442 443 444 445 446 447 448 449 450 451 452 453 454
  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.
455 456
Qed.

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