ErrorValidation.v 114 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
(** Error bound command validator **)
='s avatar
= committed
68
Fixpoint validErrorboundCmd (f:cmd Q) (typeMap:exp Q -> option mType) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool :=
69
  match f with
70
  |Let m x e g =>
='s avatar
= committed
71
72
   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)
73
   else false
='s avatar
= committed
74
  |Ret e => validErrorbound e typeMap env dVars
75
76
  end.

77
78
79
80
81
82
83
84
85
86
87

(* (** Error bound command validator **) *)
(* Fixpoint validErrorboundCmd (f:cmd Q) (typeMap:exp Q -> option mType) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool := *)
(*   match f with *)
(*   |Let m x e g => *)
(*    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) *)
(*    else false *)
(*   |Ret e => validErrorbound e typeMap env dVars *)
(*   end. *)

Heiko Becker's avatar
Heiko Becker committed
88
89
90
91
92
(**
    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.
**)
93
94
Lemma err_always_positive e tmap (absenv:analysisResult) iv err dVars:
  validErrorbound e tmap absenv dVars = true ->
95
96
97
  (iv,err) = absenv e ->
  (0 <= Q2R err)%R.
Proof.
98
  destruct e; intros validErrorbound_e absenv_e;
99
    unfold validErrorbound in validErrorbound_e;
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
    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.
116
Qed.
Heiko Becker's avatar
Heiko Becker committed
117

118
119


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

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

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

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

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

1017
Lemma validErrorboundCorrectDiv E1 E2 absenv
1018
      (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
1019
      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma:
1020
1021
1022
1023
1024
1025
  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 ->
1026
1027
1028
  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 ->
1029
1030
1031
  (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) ->
1032
1033
1034
1035
1036
1037
1038
  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.
1039
  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
1040
         subexpr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real absenv_e1
1041
         absenv_e2 absenv_div err1_bounded err2_bounded.
1042
  eapply Rle_trans.
1043
  eapply (div_abs_err_bounded e1 e2); eauto.
1044
1045
  unfold validErrorbound in valid_error.
  rewrite absenv_div,absenv_e1,absenv_e2 in valid_error.
1046
1047
  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.
1048
  rename H into type_binop.
1049
  andb_to_prop valid_error.
1050
1051
  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.
1052
1053
  clear L1 R.
  rename R1 into valid_error.
1054
  rename L0 into no_div_zero_float.
1055
1056
1057
1058
  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).
1059
1060
  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).
1061
1062
1063
1064
1065
1066
1067
  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.
  rewrite Q2R_div in valid_error.
  - rewrite Q2R_mult in valid_error.
    repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
1068
1069
    rewrite <- maxAbs_impl_RmaxAbs_iv in valid_error.
    repeat rewrite <- minAbs_impl_RminAbs_iv in valid_error.
1070
1071
1072
1073
1074
1075
1076
    apply le_neq_bool_to_lt_prop in no_div_zero_float; apply le_neq_bool_to_lt_prop in no_div_zero_real.
    assert ((IVhi (Q2R e2lo,Q2R e2hi) < 0)%R \/ (0 < IVlo (Q2R e2lo,Q2R e2hi))%R) as no_div_zero_real_R
          by (simpl; rewrite <- Q2R0_is_0; simpl in no_div_zero_real;
              destruct no_div_zero_real as [ndiv | ndiv]; apply Qlt_Rlt in ndiv; auto).
    apply Q_case_div_to_R_case_div in no_div_zero_float; apply Q_case_div_to_R_case_div in no_div_zero_real.
    assert (Q2R e2lo = 0 -> False)%R by (apply (lt_or_gt_neq_zero_lo _ (Q2R e2hi)); try auto; lra).
    assert (Q2R e2hi = 0 -> False)%R by (apply (lt_or_gt_neq_zero_hi (Q2R e2lo)); try auto; lra).
1077
1078
1079
1080
    eapply Rle_trans.
    Focus 2.
    apply valid_error.
    apply Rplus_le_compat.
1081
    (* Error Propagation proof *)
Heiko Becker's avatar
Heiko Becker committed
1082
    + clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float