ErrorValidation.v 110 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
  let mopt := typeMap e in
  match mopt with
  | None => false
  | Some m =>
    if (Qleb 0 err)
    then
      match e with
='s avatar
= committed
24
      |Var _ v =>
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
       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
   if ((validErrorbound e typeMap env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q x)))))
='s avatar
= committed
73
   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
    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.
='s avatar
= committed
93
    + destruct (tmap (Var Q n)); inversion validErrorbound_e.
94
95
96
97
98
99
100
101
102
103
104
105
  - 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:
='s avatar
= committed
110
111
  forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma defVars,
    typeCheck (Var Q v) defVars Gamma = true -> 
112
113
    approxEnv E1 defVars absenv fVars dVars E2 ->
    eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Var Q v))) nR M0 ->
='s avatar
= committed
114
115
116
117
    eval_exp E2 defVars (toRExp (Var Q v)) nF m ->
    validIntervalbounds (Var Q v) absenv P dVars = true ->
    validErrorbound (Var Q v) Gamma absenv dVars = true ->
    (forall v1,
118
        NatSet.mem v1 dVars = true ->
119
        exists r, E1 v1 = Some r /\ 
='s avatar
= committed
120
             (Q2R (fst (fst (absenv (Var Q v1)))) <= r <= Q2R (snd (fst (absenv (Var Q v1)))))%R) ->
121
    (forall v1, NatSet.mem v1 fVars= true ->
122
          exists r, E1 v1 = Some r /\
123
                (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) ->
='s avatar
= committed
124
    absenv (Var Q v) = ((nlo, nhi), e) ->
125
126
    (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
127
  intros * typing_ok approxCEnv eval_real eval_float bounds_valid error_valid dVars_sound P_valid absenv_var.
128
  simpl in eval_real; inversion eval_real; inversion eval_float; subst.
129
130
  rename H1 into E1_v;
    rename H6 into E2_v.
131
  simpl in error_valid.
132
  rewrite absenv_var in error_valid; simpl in error_valid; subst.
133
  case_eq (Gamma (Var Q v)); intros; rewrite H in error_valid; [ | inversion error_valid].
134
  rewrite <- andb_lazy_alt in error_valid.
135
136
  andb_to_prop error_valid.
  rename L into error_pos.
137
138
139
  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 *)
140
  induction approxCEnv.
141
  (* empty environment case, contradiction *)
142
  - unfold emptyEnv in *; simpl in *.
143
    congruence.
144
145
146
  - unfold updEnv in *; simpl in *.
    case_eq (v =? x); intros eq_case; rewrite eq_case in *.
    + rewrite Nat.eqb_eq in eq_case; subst.
147
      assert (NatSet.mem x dVars = false) as x_not_bound.
148
149
      * case_eq (NatSet.mem x dVars); intros case_mem; try auto.
        rewrite NatSet.mem_spec in case_mem.
150
151
152
153
154
155
        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.
156
        inversion E1_v; inversion E2_v; subst.
157
158
159
160
161
        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.
162
163
        rewrite H5 in H1; inversion H1; subst.
        rewrite H,H5 in typing_ok; apply EquivEqBoolEq in typing_ok; subst.
164
        clear H5 H3.
165
        apply Rmult_le_compat_r.
166
        { apply inj_eps_posR. } 
167
        { rewrite <- maxAbs_impl_RmaxAbs.
168
          apply contained_leq_maxAbs.
169
          unfold contained; simpl.
170
171
172
          assert ((toRExp (Var Q x)) = Var R x) by (simpl; auto).
          rewrite <- H3 in eval_float.
          pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) defVars bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf.
173
174
          rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
          apply valid_bounds_prf; try auto.
175
176
177
178
179
          - 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. }
180
    + apply IHapproxCEnv; try auto.
181
182
      * constructor; auto.
      * constructor; auto.
183
184
185
      * intros v0 mem_dVars.
          specialize (dVars_sound v0 mem_dVars).
        destruct dVars_sound as [vR0 iv_sound_val].
186
        case_eq (v0 =? x); intros case_mem;
187
          rewrite case_mem in iv_sound_val; simpl in iv_sound_val.
188
189
190
191
192
193
        { 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. }
194
        { exists vR0. split; auto; destruct iv_sound_val as [E1_v0 iv_sound_val]; auto. }
195
196
197
198
199
200
201
202
203
204
205
      * 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 *.
206
207
    case_eq (v =? x); intros eq_case; rewrite eq_case in *.
    + rewrite Nat.eqb_eq in eq_case; subst.
208
209
210
      inversion E1_v; inversion E2_v; subst.
      rewrite absenv_var in *; auto.
    + apply IHapproxCEnv; try auto.
211
212
      * constructor; auto.
      * constructor; auto.
213
214
215
216
      * 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.
217
        { case_eq (NatSet.mem v (NatSet.add x dVars));
218
            intros case_add; rewrite case_add in *; simpl in *; try auto.
219
220
          - rewrite NatSet.mem_spec in case_add.
            rewrite NatSet.add_spec in case_add.
221
            destruct case_add as [v_eq_x | v_dVar]; subst.
222
            + rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto.
223
            + rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars.
224
              inversion case_dVars. }
225
226
        { rewrite absenv_var in bounds_valid. rewrite not_in_add in bounds_valid.
          auto. }
227
228
229
230
231
232
233
234
235
236
237
238
239
      * 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. }
240
241
      * intros v0 mem_dVars.
        specialize (dVars_sound v0).
242
243
        rewrite absenv_var in *; simpl in *.
        rewrite NatSet.mem_spec in mem_dVars.
244
        assert (NatSet.In v0 (NatSet.add x dVars)) as v0_in_add.
245
        { rewrite NatSet.add_spec. right; auto. }
246
        { rewrite <- NatSet.mem_spec in v0_in_add.
247
          specialize (dVars_sound v0_in_add).
248
249
          destruct dVars_sound as [vR0 [val_def iv_sound_val]].
          exists vR0; split; auto.
250
          unfold updEnv in val_def; simpl in val_def.
251
252
          case_eq (v0 =? x); intros case_mem;
            rewrite case_mem in val_def; simpl in val_def.
253
254
          - rewrite Nat.eqb_eq in case_mem; subst.
            apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars.
255
            rewrite <- NatSet.mem_spec in mem_dVars.
256
            rewrite mem_dVars in *; congruence.
257
          - auto. }
258
      * rewrite absenv_var in bounds_valid.
259
260
261
262
263
264
265
266
267
268
        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.
269

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

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

389
Lemma validErrorboundCorrectSubtraction E1 E2 absenv
390
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
391
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
392
  m = computeJoin m1 m2 ->
393
394
395
396
397
398
399
400
401
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 ->
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 ->
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 ->
  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))
           (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n)
           (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
  typeCheck (Binop Sub e1 e2) defVars Gamma = true -> 
402
  validErrorbound (Binop Sub e1 e2) Gamma absenv dVars = true ->
403
404
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
405
406
407
408
409
410
411
  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.
412
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
413
         subexpr_ok valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_sub
414
415
         err1_bounded err2_bounded.
  eapply Rle_trans.
416
417
418
  eapply (subtract_abs_err_bounded e1 e2); try eauto.
  unfold validErrorbound in valid_error.
  rewrite absenv_sub,absenv_e1,absenv_e2 in valid_error.
419
  case_eq (Gamma (Binop Sub e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ].
420
421
422
423
424
425
426
427
428
  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.
  apply EquivEqBoolEq in L0; subst.
  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.
429
  andb_to_prop valid_error.
430
  rename R2 into valid_error.
431
432
433
434
435
436
437
438
439
440
441
  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.
442
  apply inj_eps_posR.
443
444
  Focus 2.
  apply valid_error.
445
446
447
448
449
450
451
  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).
452
  rewrite <- H0, <- H1.
453
454
455
456
    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).
457
458
459
  pose proof (IntervalArith.interval_subtraction_valid H2 H3).
  unfold IntervalArith.contained in H4.
  destruct H4.
460
461
462
463
464
465
466
467
468
469
470
471
472
473
  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.
474
475
Qed.

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

1016
Lemma validErrorboundCorrectDiv E1 E2 absenv
1017
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
1018
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
1019
  m = computeJoin m1 m2 ->
1020
1021
1022
1023
1024
1025
1026
1027
1028
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 ->
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 ->
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Div e1 e2))) nR M0 ->
  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))
           (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n)
           (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m -> 
  typeCheck (Binop Div e1 e2) defVars Gamma = true -> 
1029
  validErrorbound (Binop Div e1 e2) Gamma absenv dVars = true ->
1030
1031
1032
  (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) ->
1033
1034
1035
1036
1037
1038
1039
  absenv e1 = ((e1lo,e1hi),err1) ->
  absenv e2 = ((e2lo, e2hi),err2) ->
  absenv (Binop Div e1 e2) = ((alo,ahi),e)->
  (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
  (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
  (Rabs (nR - nF) <= (Q2R e))%R.
Proof.
1040
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
1041
         subexpr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real absenv_e1
1042
         absenv_e2 absenv_div err1_bounded err2_bounded.
1043
  eapply Rle_trans.
1044
  eapply (div_abs_err_bounded e1 e2); eauto.
1045
1046
  unfold validErrorbound in valid_error.
  rewrite absenv_div,absenv_e1,absenv_e2 in valid_error.
1047