ErrorValidation.v 113 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
132
133
134
135
136
137
138
  simpl in eval_real; inversion eval_real; inversion eval_float; subst.
  rename H2 into E1_v;
    rename H7 into E2_v.
  (* assert ((typeExpression (Var Q m v)) (Var Q m v) = Some m) as tEv. *)
  (* unfold typeExpression. unfold expEqBool. *)
  (* case_eq (mTypeEqBool m m && (v =? v)); intros; auto. *)
  (* apply andb_false_iff in H. destruct H. assert (mTypeEqBool m m = true) by (apply EquivEqBoolEq; auto). *)
  (* congruence. *)
  (* assert (v =? v = true) by (apply beq_nat_true_iff; auto). *)
  (* congruence. *)
139
  simpl in error_valid.
140
  rewrite absenv_var in error_valid; simpl in error_valid; subst.
141
  case_eq (Gamma (Var Q m v)); intros; rewrite H in error_valid; [ | inversion error_valid].
142
143
144
145
146
  
  (* assert (mTypeEqBool m m && (v =? v) = true). *)
  (* apply andb_true_iff; split; [ rewrite EquivEqBoolEq | apply beq_nat_true_iff ]; auto. *)
  
  (* rewrite H in error_valid. *)
147
  rewrite <- andb_lazy_alt in error_valid.
148
149
  andb_to_prop error_valid.
  rename L into error_pos.
150
151
152
  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 *)
153
  induction approxCEnv.
154
  (* empty environment case, contradiction *)
155
  - unfold emptyEnv in *; simpl in *.
156
    congruence.
157
158
159
  - unfold updEnv in *; simpl in *.
    case_eq (v =? x); intros eq_case; rewrite eq_case in *.
    + rewrite Nat.eqb_eq in eq_case; subst.
160
      assert (NatSet.mem x dVars = false) as x_not_bound.
161
162
      * case_eq (NatSet.mem x dVars); intros case_mem; try auto.
        rewrite NatSet.mem_spec in case_mem.
163
164
165
166
167
168
        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.
169
        inversion E1_v; inversion E2_v; subst.
170
171
172
173
174
        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.
175
176
177
        inversion typing_ok; subst.
        rewrite H in H5; inversion H5; subst.
        clear H5 H3.
178
        apply Rmult_le_compat_r.
179
        { apply inj_eps_posR. } 
180
        { rewrite <- maxAbs_impl_RmaxAbs.
181
          apply contained_leq_maxAbs.
182
          unfold contained; simpl.
183
184
          assert ((toRExp (Var Q m x)) = Var R m x) by (simpl; auto).
          rewrite <- H2 in eval_float.
185
          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.
186
187
          rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
          apply valid_bounds_prf; try auto.
188
189
190
191
192
          - 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. }
193
    + apply IHapproxCEnv; try auto.
194
195
      * constructor; auto.
      * constructor; auto.
196
197
198
      * intros v0 m2 (*overVar*) mem_dVars (*isSubExpr*).
          specialize (dVars_sound v0 m2 (*overVar*) mem_dVars (*isSubExpr*)).
        destruct dVars_sound as [vR0 [mR0 iv_sound_val]].
199
        case_eq (v0 =? x); intros case_mem;
200
          rewrite case_mem in iv_sound_val; simpl in iv_sound_val.
201
202
203
204
205
206
        { 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. }
207
        { exists vR0, mR0; split; auto; destruct iv_sound_val as [E1_v0 iv_sound_val]; auto. }
208
209
210
211
212
213
214
215
216
217
218
      * 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 *.
219
220
    case_eq (v =? x); intros eq_case; rewrite eq_case in *.
    + rewrite Nat.eqb_eq in eq_case; subst.
221
222
223
      inversion E1_v; inversion E2_v; subst.
      rewrite absenv_var in *; auto.
    + apply IHapproxCEnv; try auto.
224
225
      * constructor; auto.
      * constructor; auto.
226
227
228
229
      * 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.
230
        { case_eq (NatSet.mem v (NatSet.add x dVars));
231
            intros case_add; rewrite case_add in *; simpl in *; try auto.
232
233
          - rewrite NatSet.mem_spec in case_add.
            rewrite NatSet.add_spec in case_add.
234
            destruct case_add as [v_eq_x | v_dVar]; subst.
235
            + rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto.
236
            + rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars.
237
              inversion case_dVars. }
238
239
        { rewrite absenv_var in bounds_valid. rewrite not_in_add in bounds_valid.
          auto. }
240
241
242
243
244
245
246
247
248
249
250
251
252
      * 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. }
253
      * intros v0 m2 (*overVar*) mem_dVars (*isSubExpr*).
Raphaël Monat's avatar
Raphaël Monat committed
254
        specialize (dVars_sound v0 m2 (*overVar*)).
255
256
        rewrite absenv_var in *; simpl in *.
        rewrite NatSet.mem_spec in mem_dVars.
257
        assert (NatSet.In v0 (NatSet.add x dVars)) as v0_in_add.
258
        { rewrite NatSet.add_spec. right; auto. }
259
        { rewrite <- NatSet.mem_spec in v0_in_add.
260
261
262
          specialize (dVars_sound v0_in_add).
          destruct dVars_sound as [vR0 [mR0 [val_def iv_sound_val]]].
          exists vR0, mR0; split; auto.
263
          unfold updEnv in val_def; simpl in val_def.
264
265
          case_eq (v0 =? x); intros case_mem;
            rewrite case_mem in val_def; simpl in val_def.
266
267
          - rewrite Nat.eqb_eq in case_mem; subst.
            apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars.
268
            rewrite <- NatSet.mem_spec in mem_dVars.
269
            rewrite mem_dVars in *; congruence.
270
          - auto. }
271
      * rewrite absenv_var in bounds_valid.
272
273
274
275
276
277
278
279
280
281
        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.
282

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

318
Lemma validErrorboundCorrectAddition E1 E2 absenv
319
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
320
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma:
321
322
323
324
325
326
327
  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 ->
328
329
  validType Gamma (Binop Plus e1 e2) m ->
  validErrorbound (Binop Plus e1 e2) Gamma absenv dVars = true ->
330
331
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
  (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
332
333
334
335
336
337
338
  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.
339
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
340
         subexpr_ok valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_add
341
         err1_bounded err2_bounded.
342
  eapply Rle_trans.
343
344
345
  eapply
    (add_abs_err_bounded e1 e2);
    try eauto.
346
347
  unfold validErrorbound in valid_error.
  rewrite absenv_add,absenv_e1,absenv_e2 in valid_error.
348
349
350
351
352
353
354
355
  (* assert (typeExpression (Binop Plus e1 e2) (Binop Plus e1 e2) = Some m) as type_add. *)
  (* { simpl typeExpression; repeat rewrite expEqBool_refl; simpl. *)
  (*   pose proof (typeExpressionIsSound _ e1_float) as type_e1. *)
  (*   pose proof (typeExpressionIsSound _ e2_float) as type_e2. *)
  (*   rewrite type_e1,type_e2. *)
  (*   rewrite mIsJoin; auto. } *)
  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.
356
  andb_to_prop valid_error.
357
  rename R0 into valid_error.
358
359
360
  eapply Rle_trans.
  apply Rplus_le_compat_l.
  eapply Rmult_le_compat_r.
361
  apply inj_eps_posR.
362
363
364
  Focus 2.
  rewrite Qle_bool_iff in valid_error.
  apply Qle_Rle in valid_error.
365
366
367
368
369
370
371
  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.
372
  clear L R.
373
374
375
376
377
378
379
  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).
380
  rewrite <- H0, <- H1.
381
382
383
384
  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
  pose proof (distance_gives_iv (a:=nR1) _ contained_intv1 err1_bounded).
  assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
  pose proof (distance_gives_iv (a:=nR2) _ contained_intv2 err2_bounded).
385
386
387
  pose proof (IntervalArith.interval_addition_valid H2 H3).
  unfold IntervalArith.contained in H4.
  destruct H4.
388
389
390
391
392
393
394
395
  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.
396
Qed.
Heiko Becker's avatar
Heiko Becker committed
397

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

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

1005
Lemma validErrorboundCorrectDiv E1 E2 absenv
1006
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
1007
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma:
1008
1009
1010
1011
1012
1013
  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 Div e1 e2))) nR M0 ->
  eval_exp E2 (toRExp e1) nF1 m1 ->
  eval_exp E2 (toRExp e2) nF2 m2 ->
1014
1015
1016
  eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Div (Var Q m1 1) (Var Q m2 2))) nF m -> 
  validType Gamma (Binop Div e1 e2) m ->
  validErrorbound (Binop Div e1 e2) Gamma absenv dVars = true ->
1017
1018
1019
  (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) ->
1020
1021
1022
1023
1024
1025
1026
  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.
1027
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
1028
         subexpr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real absenv_e1
1029
         absenv_e2 absenv_div err1_bounded err2_bounded.
1030
  eapply Rle_trans.
1031
  eapply (div_abs_err_bounded e1 e2); eauto.
1032
1033
  unfold validErrorbound in valid_error.
  rewrite absenv_div,absenv_e1,absenv_e2 in valid_error.
1034
1035
  case_eq (Gamma (Binop Div 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.
1036
  rename H into type_binop.
1037
  andb_to_prop valid_error.
1038
1039
  assert (validErrorbound e1 Gamma absenv dVars = true) as valid_err_e1 by auto;
    assert (validErrorbound e2 Gamma absenv dVars = true) as valid_err_e2 by auto.
1040
1041
  clear L1 R.
  rename R1 into valid_error.
1042
  rename L0 into no_div_zero_float.
1043
1044
1045
1046
  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).
1047
1048
  assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma absenv); eauto).
  assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma absenv); eauto).
1049
1050
1051
1052
1053
1054
1055
  apply Qle_bool_iff in