ErrorValidationAA.v 177 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
(**
   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.
 **)
From Coq
     Require Import QArith.QArith QArith.Qminmax QArith.Qabs QArith.Qreals
Nikita Zyuzin's avatar
Nikita Zyuzin committed
11
     micromega.Psatz Recdef Reals.Reals.
12
13
14

From Flover
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
15
16
17
     Infra.RealSimps Infra.Ltacs Commands Environments ErrorAnalysis ErrorValidationAAutil
     ExpressionSemantics IntervalValidation TypeValidator RealRangeValidator ErrorBounds
     ErrorValidation AffineForm AffineArithQ AffineArith.
18

19
20
21
22
23
24
25
(** Error bound validator **)
Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
         (typeMap:FloverMap.t mType) (* derived types for e *)
         (A:analysisResult) (* encoded result of Flover *)
         (dVars:NatSet.t) (* let-bound variables encountered previously *)
         (currNoise: nat) (* current maximal noise term *)
         (errMap:FloverMap.t (affine_form Q)) (* previously seen affine polys *)
26
  : option (FloverMap.t (affine_form Q) * nat) :=
27
28
29
30
31
  (* case analysis for the expression *)
  if FloverMap.mem e errMap then
    (* We have already checked a subexpression *)
    Some (errMap, currNoise)
  else
32
33
34
35
    olet m := FloverMap.find e typeMap in
    olet dRes := FloverMap.find e A in
    let (intv, err) := dRes in
    (* Error bounds are intervals symmetric at 0 --> the bound must be positive here *)
36
37
38
    if negb (Qleb 0 err) then
      None
    else match e with
39
    | Var _ x =>
40
      if NatSet.mem x dVars then
41
        Some (errMap, currNoise) (* defined variable for a previously checked expression *)
42
      else
43
44
        (* Build an affine polynomial *)
        let errNew := computeErrorQ (maxAbs intv) m in
45
        let af := mkErrorPolyQ errNew currNoise in
46
47
48
49
        if Qleb errNew err then
          Some (FloverMap.add e af errMap, (currNoise+1)%nat)
        else
          None
50
    | Expressions.Const m v =>
51
        let errNew := computeErrorQ (maxAbs intv) m in
52
        let af := mkErrorPolyQ errNew currNoise in
53
54
55
56
        if Qleb errNew err then
          Some (FloverMap.add (elt:=affine_form Q) e af errMap, (currNoise+1)%nat)
        else
          None
57
    | Unop Neg e1 =>
58
        olet res := validErrorboundAA e1 typeMap A dVars currNoise errMap in
59
60
        let (newErrorMap, maxNoise) := res in
        olet afPolye1 := FloverMap.find e1 newErrorMap in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
61
        let errPoly := AffineArithQ.negate_aff afPolye1 in
62
63
64
        match FloverMap.find e1 A with
        | Some (iv_e1, err1) =>
          if Qeq_bool err err1 then
Nikita Zyuzin's avatar
Nikita Zyuzin committed
65
            Some (FloverMap.add e errPoly newErrorMap, maxNoise)
66
67
68
69
          else
            None
        | None => None
        end
70
    | Unop Inv e1 => None
71
72
    | Binop b e1 e2 =>
        olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
73
74
75
76
77
78
79
80
81
82
        let (newErrorMap1, maxNoise1) := res1 in
        olet res2 := validErrorboundAA e2 typeMap A dVars maxNoise1 newErrorMap1 in
        let (newErrorMap2, maxNoise2) := res2 in
        (* Error polynomial for e1 *)
        olet afPolye1 := FloverMap.find e1 newErrorMap2 in
        (* Error polynomial for e2 *)
        olet afPolye2 := FloverMap.find e2 newErrorMap2 in
        (* Analysis results for e1, e2 *)
        match FloverMap.find e1 A, FloverMap.find e2 A with
        | Some (ive1, err1), Some (ive2, err2) =>
83
84
85
86
87
88
            let errIve1 := widenIntv ive1 err1 in
            let errIve2 := widenIntv ive2 err2 in
            match b with
            | Plus =>
                let actualRange := (addIntv errIve1 errIve2) in
                let errNew := computeErrorQ (maxAbs actualRange) m in
89
90
                let errPoly := AffineArithQ.plus_aff
                                (AffineArithQ.plus_aff afPolye1 afPolye2)
91
                                (mkErrorPolyQ errNew maxNoise2) in
92
                let errVal := maxAbs (toIntv errPoly) in
93
94
95
96
                if Qleb errVal err then
                  Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
                else
                  None
97
98
99
            | Sub =>
                let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in
                let errNew := computeErrorQ mAbs m in
100
101
                let errPoly := AffineArithQ.plus_aff
                                (AffineArithQ.subtract_aff afPolye1 afPolye2)
102
                                (mkErrorPolyQ errNew maxNoise2) in
103
                let errVal := maxAbs (toIntv errPoly) in
104
105
106
107
                if Qleb errVal err then
                  Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
                else
                  None
108
109
110
            | Mult =>
                let aaRangee1 := fromIntv ive1 maxNoise2 in
                let aaRangee2 := fromIntv ive2 (maxNoise2 + 1) in
111
112
113
114
115
116
117
                (* Differs from intervals and daisy -- subtraction does not change the range *)
                (* but matters for concrete evaluations *)
                let propError := AffineArithQ.subtract_aff
                                   (AffineArithQ.plus_aff
                                      (AffineArithQ.mult_aff aaRangee1 afPolye2 (maxNoise2 + 2))
                                      (AffineArithQ.mult_aff aaRangee2 afPolye1 (maxNoise2 + 3)))
                                   (AffineArithQ.mult_aff afPolye1 afPolye2 (maxNoise2 + 4)) in
118
119
                let mAbs := (maxAbs (multIntv errIve1 errIve2)) in
                let errNew := computeErrorQ mAbs m in
120
                let errPoly := AffineArithQ.plus_aff propError
121
                                        (mkErrorPolyQ errNew (maxNoise2 + 5)) in
122
                let errVal := maxAbs (toIntv errPoly) in
123
124
125
126
                if Qleb errVal err then
                  Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 6)%nat)
                else
                  None
127
            | Div =>
128
129
130
                if ((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
                    ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))) then
                  let aaRangee1 := fromIntv ive1 maxNoise2 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
131
132
133
134
135
                  let aaRangeInve2 := fromIntv (invertIntv ive2) (maxNoise2 + 1) in
                  let minAbsIve2 := minAbs errIve2 in
                  let errMultiplier := fromIntv (invertIntv (multIntv ive2 errIve2))
                                                (maxNoise2 + 2) in
                  let invErrAf2 := AffineArithQ.mult_aff afPolye2 errMultiplier (maxNoise2 + 3) in
136
                  let propError := AffineArithQ.plus_aff
Nikita Zyuzin's avatar
Nikita Zyuzin committed
137
138
139
140
                                     (AffineArithQ.subtract_aff
                                        (AffineArithQ.mult_aff afPolye1 aaRangeInve2 (maxNoise2 + 4))
                                        (AffineArithQ.mult_aff aaRangee1 invErrAf2 (maxNoise2 + 5)))
                                     (AffineArithQ.mult_aff afPolye1 invErrAf2 (maxNoise2 + 6)) in
141
142
                  let mAbs := (maxAbs (divideIntv errIve1 errIve2)) in
                  let errNew := computeErrorQ mAbs m in
143
                  let errPoly := AffineArithQ.plus_aff propError
Nikita Zyuzin's avatar
Nikita Zyuzin committed
144
                                          (mkErrorPolyQ  errNew (maxNoise2 + 7)) in
145
146
                  let errVal := maxAbs (toIntv errPoly) in
                  if (Qleb errVal err) then
Nikita Zyuzin's avatar
Nikita Zyuzin committed
147
                    Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 8)%nat)
148
149
150
151
                  else
                    None
                else
                  None
152
            end
153
154
        | _, _ => None
        end
155
156
    | Fma e1 e2 e3 =>
        olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
        let (newErrorMap1, maxNoise1) := res1 in
        olet res2 := validErrorboundAA e2 typeMap A dVars maxNoise1 newErrorMap1 in
        let (newErrorMap2, maxNoise2) := res2 in
        olet res3 := validErrorboundAA e3 typeMap A dVars maxNoise2 newErrorMap2 in
        let (newErrorMap3, maxNoise3) := res3 in
        (* Error polynomial for e1 *)
        olet afPolye1 := FloverMap.find e1 newErrorMap3 in
        (* Error polynomial for e2 *)
        olet afPolye2 := FloverMap.find e2 newErrorMap3 in
        (* Error polynomial for e2 *)
        olet afPolye3 := FloverMap.find e3 newErrorMap3 in
        match FloverMap.find e1 A, FloverMap.find e2 A, FloverMap.find e3 A with
        | Some (ive1, err1), Some (ive2, err2), Some (ive3, err3) =>
          let errIve1 := widenIntv ive1 err1 in
          let errIve2 := widenIntv ive2 err2 in
          let errIve3 := widenIntv ive3 err3 in
Joachim Bard's avatar
Joachim Bard committed
173
174
          let aaRangee1 := fromIntv ive1 maxNoise3 in
          let aaRangee2 := fromIntv ive2 (maxNoise3 + 1) in
175
          let propError := AffineArithQ.plus_aff
Nikita Zyuzin's avatar
Nikita Zyuzin committed
176
177
                             (AffineArithQ.subtract_aff
                                (AffineArithQ.plus_aff
Joachim Bard's avatar
Joachim Bard committed
178
179
180
181
182
                                   (AffineArithQ.mult_aff aaRangee1 afPolye2 (maxNoise3 + 2))
                                   (AffineArithQ.mult_aff aaRangee2 afPolye1 (maxNoise3 + 3)))
                                (AffineArithQ.mult_aff afPolye1 afPolye2 (maxNoise3 + 4)))
                             afPolye3 in
          let mAbs := (maxAbs (addIntv (multIntv errIve1 errIve2) errIve3)) in
183
          let errNew := computeErrorQ mAbs m in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
184
          let errPoly := AffineArithQ.plus_aff propError (mkErrorPolyQ errNew (maxNoise3 + 5)) in
185
186
          let errVal := maxAbs (toIntv errPoly) in
          if Qleb errVal err then
187
            Some (FloverMap.add e errPoly newErrorMap3, (maxNoise3 + 6)%nat)
188
189
190
191
          else
            None
        | _, _, _ => None
        end
192
    | Downcast m e1 =>
193
        olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
194
195
196
197
198
199
200
201
        let (newErrorMap1, maxNoise1) := res1 in
        (* Error polynomial for e1 *)
        olet afPolye1 := FloverMap.find e1 newErrorMap1 in
        olet aRes := FloverMap.find e1 A in
        let (ive1, err1) := aRes in
        let errIve1 := widenIntv ive1 err1 in
        let mAbs := maxAbs errIve1 in
        let newErr := computeErrorQ mAbs m in
202
        let errPoly := AffineArithQ.plus_aff afPolye1
203
                                (mkErrorPolyQ newErr maxNoise1) in
204
205
206
207
208
        let errVal := maxAbs (toIntv errPoly) in
        if Qleb errVal err then
          Some (FloverMap.add e errPoly newErrorMap1, (maxNoise1 + 1)%nat)
        else
          None
209
    end.
210
211

(** Error bound command validator **)
212
213
214
215
Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
         (typeMap: FloverMap.t mType) (* derived types for e *)
         (A: analysisResult) (* encoded result of Flover *)
         (dVars: NatSet.t) (* let-bound variables encountered previously *)
216
         (currNoise: nat) (* current maximal noise term *)
217
         (errMap: FloverMap.t (affine_form Q)) (* previously seen affine polys *)
218
  : option (FloverMap.t (affine_form Q) * nat) :=
219
  match f with
220
  | Let m x e g =>
221
222
223
224
225
226
    olet res1 := validErrorboundAA e typeMap A dVars currNoise errMap in
    let (errMap1, maxNoise1) := res1 in
    olet afPolye := FloverMap.find e errMap1 in
    match FloverMap.find e A, FloverMap.find (Var Q x) A with
    | Some (iv_e, err_e), Some (iv_x, err_x) =>
      if Qeq_bool err_e err_x then
Nikita Zyuzin's avatar
Nikita Zyuzin committed
227
228
229
230
231
        match FloverMap.find (Var Q x) errMap1 with
        | Some _ => None
        | None => validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1
                                      (FloverMap.add (Var Q x) afPolye errMap1)
        end
232
233
234
235
      else
          None
    | _,_ => None
    end
236
  | Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
237
  end.
Heiko Becker's avatar
Heiko Becker committed
238

239
Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap
240
           noise_map noise expr_map :=
241
  forall v__R v__FP m__FP (iv__A: intv) (err__A: error),
242
243
  eval_expr E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
  eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
244
  FloverMap.find e A = Some (iv__A, err__A) ->
245
  exists af err__af,
246
    fresh noise (afQ2R af) /\
247
    (forall n, (n >= noise)%nat -> noise_map n = None) /\
248
249
250
251
    FloverMap.find e expr_map = Some af /\
    (0 <= err__af)%R /\
    toInterval (afQ2R af) = (-err__af, err__af)%R /\
    (err__af <= Q2R err__A)%R /\
252
    af_evals (afQ2R af) (v__R - v__FP)%R noise_map.
253

254
Lemma checked_error_expressions_extension e E1 E2 A Gamma DeltaMap
255
256
257
258
259
      noise_map1 noise_map2 noise1 noise2 expr_map1 expr_map2:
  contained_map noise_map1 noise_map2 ->
  (noise1 <= noise2)%nat ->
  contained_flover_map expr_map1 expr_map2 ->
  (forall n, (n >= noise2)%nat -> noise_map2 n = None) ->
260
261
  checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1 ->
  checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2.
262
263
264
265
266
267
268
269
270
Proof.
  intros cont contf Hnoise Hvalidmap checked1.
  unfold checked_error_expressions in checked1 |-*.
  intros.
  specialize (checked1 v__R v__FP m__FP iv__A err__A) as (af & err__af & checked1); auto.
  exists af, err__af.
  intuition; eauto using fresh_monotonic, af_evals_map_extension.
Qed.

271
Lemma checked_error_expressions_flover_map_add_compat e e' af E1 E2 A Gamma DeltaMap
272
273
      noise_map noise expr_map:
  Q_orderedExps.exprCompare e' e <> Eq ->
274
275
  checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map noise expr_map ->
  checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map noise
276
277
278
279
280
281
282
283
284
285
286
                            (FloverMap.add e' af expr_map).
Proof.
  intros Hneq checked1.
  unfold checked_error_expressions in checked1 |-*.
  intros.
  specialize (checked1 v__R v__FP m__FP iv__A err__A) as (af' & err__af' & checked1); auto.
  exists af', err__af'.
  intuition.
  rewrite FloverMapFacts.P.F.add_neq_o; auto.
Qed.

287
288
Definition dVars_contained  dVars (expr_map: FloverMap.t (affine_form Q)): Prop :=
  forall v, NatSet.In v dVars -> FloverMap.In (Var Q v) expr_map.
289

290
291
292
293
Lemma dVars_contained_extension dVars expr_map1 expr_map2:
  contained_flover_map expr_map1 expr_map2 ->
  dVars_contained dVars expr_map1 ->
  dVars_contained dVars expr_map2.
294
Proof.
295
296
  intros H Hdvars.
  unfold dVars_contained in Hdvars |-*.
297
298
  intros v Hvin.
  specialize (Hdvars v Hvin).
299
  eapply flover_map_in_extension; eauto.
300
301
Qed.

302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
Fixpoint contained_subexpr (e: expr Q) (expr_map: FloverMap.t (affine_form Q)): Prop :=
  match e with
  | Var _ x => True
  | Expressions.Const m v => True
  | Unop u e' => contained_subexpr e' expr_map
  | Binop b e1 e2 => contained_subexpr e1 expr_map /\ contained_subexpr e2 expr_map
  | Fma e1 e2 e3 => contained_subexpr e1 expr_map /\ contained_subexpr e2 expr_map /\
                   contained_subexpr e3 expr_map
  | Downcast m e' => contained_subexpr e' expr_map
  end /\ FloverMap.In e expr_map.

Lemma contained_subexpr_map_extension e expr_map1 expr_map2:
  contained_flover_map expr_map1 expr_map2 ->
  contained_subexpr e expr_map1 ->
  contained_subexpr e expr_map2.
Proof.
  intros Hcontf Hconte.
  induction e; cbn in *; intuition; eauto using flover_map_in_extension.
Qed.

Lemma contained_subexpr_add_compat e e' a expr_map:
  contained_subexpr e expr_map ->
  contained_subexpr e (FloverMap.add e' a expr_map).
Proof.
  intros Hcont.
  induction e; cbn in *; intuition; rewrite FloverMapFacts.P.F.add_in_iff; now right.
Qed.

Lemma contained_subexpr_eq_compat e e' expr_map:
  Q_orderedExps.exprCompare e e' = Eq ->
  contained_subexpr e expr_map ->
  contained_subexpr e' expr_map.
Proof.
  intros Hexpeq Hcont.
  functional induction (Q_orderedExps.exprCompare e e'); try congruence.
  - apply nat_compare_eq in Hexpeq.
    subst; auto.
  - cbn in Hcont |-*.
    split; auto.
    destruct Hcont as [_ Hcont].
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e3.
  - cbn in e3.
    apply Ndec.Pcompare_Peqb in e6.
    rewrite e6 in e3.
    rewrite andb_true_l in e3.
    apply Ndec.Ncompare_Neqb in Hexpeq.
    now rewrite Hexpeq in e3.
  - cbn in Hcont |-*.
    destruct Hcont as [Hsubcont Hcont].
    specialize (IHc Hexpeq Hsubcont).
    split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e5.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2) & Hcont).
    specialize (IHc e6 Hsubcont1).
    specialize (IHc0 Hexpeq Hsubcont2).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e6.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2) & Hcont).
    specialize (IHc e6 Hsubcont1).
    specialize (IHc0 Hexpeq Hsubcont2).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e6.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2) & Hcont).
    specialize (IHc e6 Hsubcont1).
    specialize (IHc0 Hexpeq Hsubcont2).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e6.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2) & Hcont).
    specialize (IHc e6 Hsubcont1).
    specialize (IHc0 Hexpeq Hsubcont2).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e6.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2 & Hsubcont3) & Hcont).
    specialize (IHc e3 Hsubcont1).
    specialize (IHc0 e4 Hsubcont2).
    specialize (IHc1 Hexpeq Hsubcont3).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    rewrite e4.
    now rewrite e3.
  - cbn in Hcont |-*.
    destruct Hcont as [Hsubcont Hcont].
    specialize (IHc Hexpeq Hsubcont).
    split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e5.
  - cbn in e5.
    apply Ndec.Pcompare_Peqb in e8.
    rewrite e8 in e5.
    rewrite andb_true_l in e5.
    apply Ndec.Ncompare_Neqb in Hexpeq.
    now rewrite Hexpeq in e5.
Qed.

415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
Lemma validErrorboundAA_contained_subexpr e Gamma A dVars noise1 noise2 expr_map1 expr_map2:
  (forall e', FloverMap.In e' expr_map1 ->
         contained_subexpr e' expr_map1) ->
  (forall n, NatSet.In n dVars -> FloverMap.In (Var Q n) expr_map1) ->
  validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
  contained_subexpr e expr_map2 /\
  contained_flover_map expr_map1 expr_map2 /\
  (forall e', ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
   contained_subexpr e' expr_map2).
Proof.
  revert noise1 noise2 expr_map1 expr_map2.
  induction e; intros * Hchecked Hdvars Hvalidbounds; cbn in Hvalidbounds.
  - destruct (FloverMap.mem (Var Q n) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    Flover_compute.
    destruct negb; [congruence|].
    destruct NatSet.mem eqn:Hmemvar.
    + inversion Hvalidbounds; subst; clear Hvalidbounds.
      intuition.
    + destruct Qleb; [|congruence].
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      repeat split.
      * cbn.
        intuition.
        apply flover_map_in_add.
      * apply contained_flover_map_extension.
        now rewrite <- mem_false_find_none.
      * intros e' Hnin1 Hin.
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition.
        apply flover_map_in_add.
  - destruct (FloverMap.mem (Expressions.Const m v) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    Flover_compute.
    destruct negb; [congruence|].
    destruct Qleb; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    repeat split.
    + cbn.
      intuition.
      apply flover_map_in_add.
    + apply contained_flover_map_extension.
      now rewrite <- mem_false_find_none.
    + intros e' Hnin1 Hin.
      apply flover_map_el_eq_extension in Hin; auto.
      specialize Hin as [Heq Hexpreq].
      eapply contained_subexpr_eq_compat; eauto.
      cbn.
      intuition.
      apply flover_map_in_add.
  - destruct (FloverMap.mem (Unop u e) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct p.
485
    destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
    destruct u; [|congruence].
    destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
      as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
      simpl in Hvalidbounds; try congruence.
    destruct (FloverMap.find e subexpr_map) as [subaf|] eqn: Hsubaf;
      simpl in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e A) as [(subiv, suberr)|] eqn: Hsuba;
      simpl in Hvalidbounds; [|congruence].
    destruct (Qeq_bool e0 suberr) eqn: Heq__err; simpl in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    specialize IHe as (IHsubexpr & IHcont & IHechecked); eauto.
    split; [|split].
    + cbn.
      intuition; [|apply flover_map_in_add].
      now eapply contained_subexpr_add_compat.
    + etransitivity; try apply contained_flover_map_add_compat; eauto.
      apply contained_flover_map_extension.
      now rewrite <- mem_false_find_none.
    + intros e' Hnin1 Hin.
      destruct (flover_map_in_dec e' subexpr_map) as [Hsubin|Hsubnin];
        [apply contained_subexpr_add_compat; auto|].
      apply flover_map_el_eq_extension in Hin; auto.
      specialize Hin as [Heq Hexpreq].
      eapply contained_subexpr_eq_compat; eauto.
      cbn.
      intuition.
      * apply contained_subexpr_add_compat; auto.
      * apply flover_map_in_add.
  - destruct (FloverMap.mem (Binop b e1 e2) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct p as (? & err__A).
523
    destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
    destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
      as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
      cbn in Hvalidbounds; try congruence.
    destruct (validErrorboundAA e2 Gamma A dVars subnoise1 subexpr_map1)
      as [(subexpr_map2, subnoise2)|] eqn: Hvalidsubexpr2;
      cbn in Hvalidbounds; try congruence.
    destruct (FloverMap.find e1 subexpr_map2) as [subaf1|] eqn: Hsubaf1;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e2 subexpr_map2) as [subaf2|] eqn: Hsubaf2;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e1 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A1 & err__A1).
    destruct (FloverMap.find e2 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A2 & err__A2).
    clear H0err.
    specialize IHe1 as (IHsubexpr1 & IHcont1 & IHchecked1); eauto.
    specialize (IHe2 subnoise1 subnoise2 subexpr_map1 subexpr_map2)
      as (IHsubexpr2 & IHcont2 & IHechecked2); eauto.
    {
      intros e' Hin.
      destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
      - eapply contained_subexpr_map_extension with (expr_map1 := expr_map1); eauto.
      - now apply IHchecked1.
    }
    {
      intros * ?.
      eapply flover_map_in_extension; try apply Hdvars; eauto.
    }
    rewrite mem_false_find_none in Hmem.
    destruct b.
    4: destruct (Qleb (snd iv__A2 + err__A2) 0 && negb (Qeq_bool (snd iv__A2 + err__A2) 0)
              || Qleb 0 (fst iv__A2 - err__A2) && negb (Qeq_bool (fst iv__A2 - err__A2) 0)); [|congruence].
    all: destruct Qleb; cbn in Hvalidbounds; [|congruence].
    all: inversion Hvalidbounds; subst; clear Hvalidbounds.
    + split; [|split].
      * cbn.
        intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
        apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
      * epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
        etransitivity; [exact G|].
        apply contained_flover_map_add_compat.
        etransitivity; [|exact IHcont2].
        assumption.
      * intros e' Hnin1 Hin.
        destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
          [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto|].
        destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
          [apply contained_subexpr_add_compat; auto|].
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
        apply contained_subexpr_add_compat.
        eapply contained_subexpr_map_extension; eauto.
    + split; [|split].
      * cbn.
        intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
        apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
      * epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
        etransitivity; [exact G|].
        apply contained_flover_map_add_compat.
        etransitivity; [|exact IHcont2].
        assumption.
      * intros e' Hnin1 Hin.
        destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
          [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto|].
        destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
          [apply contained_subexpr_add_compat; auto|].
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
        apply contained_subexpr_add_compat.
        eapply contained_subexpr_map_extension; eauto.
    + split; [|split].
      * cbn.
        intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
        apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
      * epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
        etransitivity; [exact G|].
        apply contained_flover_map_add_compat.
        etransitivity; [|exact IHcont2].
        assumption.
      * intros e' Hnin1 Hin.
        destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
          [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto|].
        destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
          [apply contained_subexpr_add_compat; auto|].
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
        apply contained_subexpr_add_compat.
        eapply contained_subexpr_map_extension; eauto.
    + split; [|split].
      * cbn.
        intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
        apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
      * epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
        etransitivity; [exact G|].
        apply contained_flover_map_add_compat.
        etransitivity; [|exact IHcont2].
        assumption.
      * intros e' Hnin1 Hin.
        destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
          [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto|].
        destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
          [apply contained_subexpr_add_compat; auto|].
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
        apply contained_subexpr_add_compat.
        eapply contained_subexpr_map_extension; eauto.
  - destruct (FloverMap.mem (Fma e1 e2 e3) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct p as (? & err__A).
655
    destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
    destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
      as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
      cbn in Hvalidbounds; try congruence.
    destruct (validErrorboundAA e2 Gamma A dVars subnoise1 subexpr_map1)
      as [(subexpr_map2, subnoise2)|] eqn: Hvalidsubexpr2;
      cbn in Hvalidbounds; try congruence.
    destruct (validErrorboundAA e3 Gamma A dVars subnoise2 subexpr_map2)
      as [(subexpr_map3, subnoise3)|] eqn: Hvalidsubexpr3;
      cbn in Hvalidbounds; try congruence.
    destruct (FloverMap.find e1 subexpr_map3) as [subaf1|] eqn: Hsubaf1;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e2 subexpr_map3) as [subaf2|] eqn: Hsubaf2;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e3 subexpr_map3) as [subaf3|] eqn: Hsubaf3;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e1 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A1 & err__A1).
    destruct (FloverMap.find e2 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A2 & err__A2).
    destruct (FloverMap.find e3 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A3 & err__A3).
    clear H0err.
    specialize IHe1 as (IHsubexpr1 & IHcont1 & IHchecked1); eauto.
    specialize (IHe2 subnoise1 subnoise2 subexpr_map1 subexpr_map2)
      as (IHsubexpr2 & IHcont2 & IHchecked2); eauto.
    {
      intros e' Hin.
      destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
      - eapply contained_subexpr_map_extension with (expr_map1 := expr_map1); eauto.
      - now apply IHchecked1.
    }
    {
      intros * ?.
      eapply flover_map_in_extension; try apply Hdvars; eauto.
    }
    specialize (IHe3 subnoise2 subnoise3 subexpr_map2 subexpr_map3)
      as (IHsubexpr3 & IHcont3 & IHechecked3); eauto.
    {
      intros e' Hin.
      destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
      - eapply contained_subexpr_map_extension with (expr_map1 := expr_map1); eauto.
        etransitivity; eauto.
      - destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1].
        + apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
        + now apply IHchecked2.
    }
    {
      intros * ?.
      eapply flover_map_in_extension; try apply Hdvars; eauto.
      etransitivity; eauto.
    }
    rewrite mem_false_find_none in Hmem.
    destruct Qleb; cbn in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    split; [|split].
    + cbn.
      intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
      * apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
        etransitivity; eauto.
      * apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map2); auto.
    + epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
      etransitivity; [exact G|].
      apply contained_flover_map_add_compat.
      etransitivity; [|exact IHcont3].
      etransitivity; [|exact IHcont2].
      assumption.
    + intros e' Hnin1 Hin.
      destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
        [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto;
         eapply contained_subexpr_map_extension; eauto|].
      destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
        [apply contained_subexpr_add_compat; auto; eapply contained_subexpr_map_extension; eauto|].
      destruct (flover_map_in_dec e' subexpr_map3) as [Hsubin3|Hsubnin3];
        [apply contained_subexpr_add_compat; auto|].
      apply flover_map_el_eq_extension in Hin; auto.
      specialize Hin as [Heq Hexpreq].
      eapply contained_subexpr_eq_compat; eauto.
      cbn.
      intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
      all: apply contained_subexpr_add_compat.
      all: eapply contained_subexpr_map_extension; eauto.
      eapply contained_subexpr_map_extension; eauto.
  - destruct (FloverMap.mem (Downcast m e) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct p.
749
    destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
    destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
      as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
      cbn in Hvalidbounds; try congruence.
    destruct (FloverMap.find e subexpr_map) as [subaf|] eqn: Hsubaf;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e A) as [(subiv, suberr)|] eqn: Hsuba;
      cbn in Hvalidbounds; [|congruence].
    clear H0err.
    destruct Qleb; cbn in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    specialize IHe as (IHsubexpr & IHcont & IHechecked); eauto.
    split; [|split].
    + cbn.
      intuition; [|apply flover_map_in_add].
      now eapply contained_subexpr_add_compat.
    + etransitivity; try apply contained_flover_map_add_compat; eauto.
      apply contained_flover_map_extension.
      now rewrite <- mem_false_find_none.
    + intros e' Hnin1 Hin.
      destruct (flover_map_in_dec e' subexpr_map) as [Hsubin|Hsubnin];
        [apply contained_subexpr_add_compat; auto|].
      apply flover_map_el_eq_extension in Hin; auto.
      specialize Hin as [Heq Hexpreq].
      eapply contained_subexpr_eq_compat; eauto.
      cbn.
      intuition.
      * apply contained_subexpr_add_compat; auto.
      * apply flover_map_in_add.
Qed.

780
781
Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars :=
  forall (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
782
    (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
783
784
785
786
    (iv__A : intv) (err__A : error),
    (forall (e' : expr R) (m' : mType),
        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
787
    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
788
789
790
    validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
    validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
    NatSet.Subset (usedVars e -- dVars) fVars ->
791
    validTypes e Gamma ->
792
    FloverMap.find e A = Some (iv__A, err__A) ->
793
794
    (0 < noise1)%nat ->
    (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
795
    dVars_contained dVars expr_map1 ->
796
    (forall e' : FloverMap.key,
797
798
        FloverMap.In e' expr_map1 ->
        NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
799
        (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
800
        exists (v__FP' : R) (m__FP' : mType),
801
          eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
802
    (forall e' : FloverMap.key,
803
        FloverMap.In e' expr_map1 ->
804
        checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
805
    ((exists (v__FP : R) (m__FP : mType),
806
         eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
807
     (forall e' : FloverMap.key,
808
809
         ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
         NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
810
         (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
811
         exists (v__FP' : R) (m__FP' : mType),
812
           eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP')) /\
813
    (forall (v__FP : R) (m__FP : mType),
814
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
815
        exists (af : affine_form Q) (err__af : R) (noise_map2 : noise_mapping),
816
          contained_flover_map expr_map1 expr_map2 /\
817
818
819
820
821
822
823
824
825
826
          (noise1 <= noise2)%nat /\
          fresh noise2 (afQ2R af) /\
          contained_map noise_map1 noise_map2 /\
          (forall n0 : nat, (n0 >= noise2)%nat -> noise_map2 n0 = None) /\
          FloverMap.find (elt:=affine_form Q) e expr_map2 = Some af /\
          (0 <= err__af)%R /\
          toInterval (afQ2R af) = ((- err__af)%R, err__af) /\
          (err__af <= Q2R err__A)%R /\
          af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\
          (forall e' : FloverMap.key,
827
              ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
828
              checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)).
829
830
831
832
833

Lemma validErrorboundAA_sound_var n E1 E2 A Gamma DeltaMap fVars dVars:
  validErrorboundAA_sound_statement (Var Q n) E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
  unfold validErrorboundAA_sound_statement.
834
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
835
836
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
                     Hcheckedex Hcheckedall;
837
  inversion Heval__R; subst.
838
839
840
841
842
843
844
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (Var Q n) expr_map1) eqn: Hmem; cbn in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
845
    specialize (Hcheckedex _ Hmem) as (Hvars & Hcert' & Hcheckedex).
846
    repeat split.
847
    1-4: congruence.
848
849
850
851
852
    intros v__FP m__FP Heval__FP.
    unfold checked_error_expressions in Hcheckedall.
    specialize (Hcheckedall v__R v__FP m__FP iv__A err__A) as (af & err__af & Hcheckedall); auto.
    exists af, err__af, noise_map1.
    intuition.
853
854
855
856
857
858
859
860
861
862
863
  }
  destruct (Htypecheck) as (m & Hetype & _ & Hvalidexec).
  rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
  pose proof Hrange as Hrange'.
  destruct Hrange as [_ [tmpiv [tmperr [tmpvR [Hres__A' [Heval1' Hcontained]]]]]].
  rewrite Hcert in Hres__A'.
  replace tmpiv with iv__A in * by congruence.
  replace tmperr with err__A in * by congruence; clear Hres__A' tmperr tmpiv.
  eapply meps_0_deterministic in Heval1'; try exact Heval__R.
  replace tmpvR with v__R in * by congruence; clear Heval1' tmpvR.
864
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
865
866
867
868
  cbn in Htypecheck.
  destruct (NatSet.mem n dVars) eqn: Hmem__n; cbn in Hvalidbounds.
  - inversion Hvalidbounds; subst; clear Hvalidbounds.
    apply NatSetProps.FM.mem_2 in Hmem__n.
869
870
871
    specialize (Hdvars n Hmem__n).
    rewrite <- FloverMapFacts.P.F.not_mem_in_iff in Hmem.
    congruence.
872
873
  - destruct (Qleb (computeErrorQ (maxAbs iv__A) m) err__A) eqn: Herrle; cbn in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
874
    rewrite mem_false_find_none in Hmem.
875
876
877
878
    apply not_in_not_mem in Hmem__n.
    assert (n  fVars) as Hmem__n' by (set_tac; set_tac).
    assert (exists v, E2 n = Some v) as [v__fp Hv__fp]
        by (eapply approxEnv_gives_value; eauto; set_tac).
879
880
    split.
    + assert (exists (v__FP : R) (m__FP : mType),
881
                 eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Var Q n)) v__FP m__FP).
882
      {
883
884
885
        exists v__fp, m.
        constructor; auto.
        eapply toRExpMap_some with (e:=Var Q n); eauto.
886
      }
887
888
889
      split; auto.
      intros e' Hnin Hin.
      destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq].
890
891
      split; [|split; [|now rewrite Hexpeq]].
      1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq;
892
        try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
893
894
      1: now apply subset_diff_to_subset_union.
      erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
895
    + intros v__FP m__FP Heval__FP.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
896
      rewrite Qle_bool_iff in Herrle.
897
898
      apply Qle_Rle in Herrle.
      inversion Heval__FP; subst.
899
900
901
902
903
904
      eapply toRExpMap_some with (e:=Var Q n) in Hetype; eauto.
      cbn in Hetype.
      replace m with m__FP in * by congruence; clear H2.
      replace v__fp with v__FP in * by congruence; clear H3.
      assert (exists q, af_evals (afQ2R (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1))
                            (v__R - v__FP)%R (updMap noise_map1 noise1 q)) as [q Hevals].
905
906
907
908
      {
        rewrite afQ2R_mkErrorPolyQ.
        rewrite computeErrorQ_computeErrorR.
        apply af_evals_mkErrorPolyR_updMap; auto using computeErrorR_pos.
909
910
        pose proof (approxEnv_fVar_bounded Henv H1 Hv__fp Hmem__n' Hetype) as H.
        eapply Rle_trans; try exact H.
911
912
913
914
915
916
917
918
919
        rewrite <- maxAbs_impl_RmaxAbs_iv.
        destruct iv__A as [liv__A hiv__A].
        apply computeErrorR_up.
        apply contained_leq_maxAbs.
        now cbn.
      }
      exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
      (Q2R (computeErrorQ (maxAbs iv__A) m__FP)), (updMap noise_map1 noise1 q).
      rewrite computeErrorQ_computeErrorR in Herrle |-*.
920
      {
921
        repeat split; try auto.
922
        - now apply contained_flover_map_extension.
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
        - lia.
        - rewrite afQ2R_mkErrorPolyQ.
          apply mkErrorPolyR_fresh_compat; lia.
        - apply contained_map_extension; auto.
        - intros n' Hn'.
          unfold updMap.
          destruct (n' =? noise1) eqn: Hneq.
          + apply beq_nat_true in Hneq.
            lia.
          + apply Hnoise_map1.
            lia.
        - rewrite FloverMapFacts.P.F.add_eq_o; try auto.
          apply Q_orderedExps.exprCompare_refl.
        - apply computeErrorR_pos.
        - rewrite afQ2R_mkErrorPolyQ.
          rewrite computeErrorQ_computeErrorR.
          rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
        - intros e' Hnin Hin.
          unfold checked_error_expressions.
          pose proof (flover_map_el_eq_extension Hnin Hin) as [Hexeq Hreq].
          rewrite Hreq.
          intros.
          exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
          (Q2R (computeErrorQ (maxAbs iv__A) m__FP)).
          rewrite computeErrorQ_computeErrorR.
948
          {
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
            repeat split; try auto.
            - rewrite afQ2R_mkErrorPolyQ.
              apply mkErrorPolyR_fresh_compat; lia.
            - intros n' Hn'.
              unfold updMap.
              destruct (n' =? noise1) eqn: Hneq.
              + apply beq_nat_true in Hneq.
                lia.
              + apply Hnoise_map1.
                lia.
            - rewrite FloverMapFacts.P.F.add_eq_o; auto.
            - apply computeErrorR_pos.
            - rewrite afQ2R_mkErrorPolyQ.
              rewrite computeErrorQ_computeErrorR.
              rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
            - erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
              now match goal with
                  | [H1: FloverMap.find e' A = Some (iv__A0, err__A0),
                         H2: FloverMap.find e' A = Some (iv__A, err__A) |- _] => rewrite H1 in H2; inversion H2
                  end.
969
970
971
            - erewrite meps_0_deterministic with (v1 := v__R0) (v2 := v__R); eauto.
              erewrite eval_expr_functional with (v1 := v__FP0) (v2 := v__FP); eauto.
              erewrite Gamma_det; eauto.
972
          }
973
      }
974
975
976
977
978
979
Qed.

Lemma validErrorboundAA_sound_const v m E1 E2 A Gamma DeltaMap fVars dVars:
  validErrorboundAA_sound_statement (Expressions.Const m v) E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
  unfold validErrorboundAA_sound_statement.
980
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
981
982
983
984
985
986
987
988
989
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
                     Hcheckedex Hcheckedall;
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (Expressions.Const m v) expr_map1) eqn: Hmem; cbn in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
990
    specialize (Hcheckedex _ Hmem) as (Hvars & Hcert' & Hcheckedex).
991
    repeat split.
992
    1-4: congruence.
993
994
995
996
997
    intros v__FP m__FP Heval__FP.
    unfold checked_error_expressions in Hcheckedall.
    specialize (Hcheckedall v__R v__FP m__FP iv__A err__A) as (af & err__af & Hcheckedall); auto.
    exists af, err__af, noise_map1.
    intuition.
998
  }
999
1000
1001
  destruct (Htypecheck) as (m__e & Hetype & _ & Hvalidexec).
  rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
1002
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
1003
1004
1005
  destruct (Qleb (computeErrorQ (maxAbs iv__A) m) err__A) eqn: Herrle; cbn in Hvalidbounds; [|congruence].
  inversion Hvalidbounds; subst; clear Hvalidbounds.
  rewrite mem_false_find_none in Hmem.
1006
1007
  split.
  - assert (exists (v__FP : R) (m__FP : mType),
1008
               eval_expr E2 (toRExpMap Gamma) DeltaMap
1009
1010
1011
1012
1013
                             (toRExp (Expressions.Const m v)) v__FP m__FP).
    {
      specialize (Hdeltamap (toRExp (Expressions.Const m v)) m)
        as (delta' & Hdelta & Hdelta').
      exists (perturb (Q2R v) m delta'), m.
1014
      eapply Const_dist' with (delta := delta'); auto.
1015
1016
1017
1018
    }
    split; auto.
    intros e' Hnin Hin.
    destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq].
1019
1020
    split; [|split; [|now rewrite Hexpeq]].
    1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq;
1021
      try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1022
1023
    1: now apply subset_diff_to_subset_union.
    erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
1024
  - rewrite Qle_bool_iff in Herrle.
1025
    apply Qle_Rle in Herrle.
1026
    intros * Heval__FP.
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
    inversion Heval__R; subst.
    inversion Heval__FP; subst.
    cbn in Htypecheck.
    cbn in Hrange.
    destruct Hrange as (_ & tmpiv & tmperr & tmpvR & Hres__A' & Heval1' & Hcontained).
    rewrite Hcert in Hres__A'.
    replace tmpiv with iv__A in * by congruence.
    replace tmperr with err__A in * by congruence; clear Hres__A' tmperr tmpiv.
    pose proof Heval__R as Heval__R'.
    eapply meps_0_deterministic in Heval__R'; try exact Heval1'.
    cbn in Heval__R'.
    replace tmpvR with (Q2R v) in * by congruence; clear Heval1' Heval__R' tmpvR.
    cbn in Heval__R, Heval__FP.
    assert (exists q, af_evals (afQ2R (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1)) (Q2R v - perturb (Q2R v) m__FP delta0)%R (updMap noise_map1 noise1 q)) as [q Hevals].
    {
      rewrite afQ2R_mkErrorPolyQ.
      rewrite computeErrorQ_computeErrorR.
      apply af_evals_mkErrorPolyR_updMap; auto using computeErrorR_pos.
      rewrite <- maxAbs_impl_RmaxAbs_iv.
      destruct iv__A as [liv__A hiv__A].
      cbn in Hcontained |-*.
      pose proof (@const_abs_err_bounded (Q2R v) (Q2R v) (perturb (Q2R v) m__FP delta0)
1049
                                         E1 E2 m__FP _ _ Heval__R Heval__FP) as H'.
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
      apply (Rle_trans _ _ _ H').
      apply computeErrorR_up.
      apply contained_leq_maxAbs.
      now cbn.
    }
    assert (forall n : nat, (n >= noise1 + 1)%nat -> updMap noise_map1 noise1 q n = None).
    {
      intros n' Hn'.
      unfold updMap.
      destruct (n' =? noise1) eqn: Hneq.
      * apply beq_nat_true in Hneq.
        lia.
      * apply Hnoise_map1.
        lia.
    }
    exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
    (Q2R (computeErrorQ (maxAbs iv__A) m__FP)), (updMap noise_map1 noise1 q).
    rewrite computeErrorQ_computeErrorR in Herrle |-*.
    repeat split; auto.
1069
    + now apply contained_flover_map_extension.
1070
1071
1072
1073
1074
1075
    + lia.
    + rewrite afQ2R_mkErrorPolyQ.
      apply mkErrorPolyR_fresh_compat; lia.
    + apply contained_map_extension; auto.
    + rewrite FloverMapFacts.P.F.add_eq_o; try auto.
      apply Q_orderedExps.exprCompare_refl.
1076
    + apply computeErrorR_pos.
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
    + rewrite afQ2R_mkErrorPolyQ.
      rewrite computeErrorQ_computeErrorR.
      rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
    + intros e' Hnin Hin.
      unfold checked_error_expressions.
      pose proof (flover_map_el_eq_extension Hnin Hin) as [Hexeq Hreq].
      rewrite Hreq.
      intros.
      exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
      (Q2R (computeErrorQ (maxAbs iv__A) m__FP)).
      rewrite computeErrorQ_computeErrorR.
      repeat split; try auto.
1089
1090
      * rewrite afQ2R_mkErrorPolyQ.
        apply mkErrorPolyR_fresh_compat; lia.
1091
1092
      * rewrite FloverMapFacts.P.F.add_eq_o; auto.
      * apply computeErrorR_pos.
1093
1094
1095
      * rewrite afQ2R_mkErrorPolyQ.
        rewrite computeErrorQ_computeErrorR.
        rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
1096
1097
1098
1099
1100
      * erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
        now match goal with
            | [H1: FloverMap.find e' A = Some (iv__A0, err__A0),
                   H2: FloverMap.find e' A = Some (iv__A, err__A) |- _] => rewrite H1 in H2; inversion H2
            end.
1101
      * erewrite meps_0_deterministic
1102
          with (v1 := v__R) (v2 := (perturb (Q2R v) REAL delta)); eauto.
1103
        erewrite eval_expr_functional
1104
          with (v1 := v__FP) (v2 := (perturb (Q2R v) m__FP delta0)); eauto.
1105
        erewrite Gamma_det; eauto.
1106
1107
1108
1109
1110
1111
1112
1113
Qed.

Lemma validErrorboundAA_sound_unop u e E1 E2 A Gamma DeltaMap fVars dVars:
  validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars ->
  validErrorboundAA_sound_statement (Unop u e) E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
  intros IHe.
  unfold validErrorboundAA_sound_statement in IHe |-*.
1114
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
1115
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
1116
                     Hcheckedex Hcheckedall.
1117
1118
1119
1120
1121
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (elt:=affine_form Q) (Unop u e) expr_map1) eqn: Hmem;
    simpl in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
1122
    inversion Hvalidbounds; subst; clear Hvalidbounds.
1123
1124
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
1125
    specialize (Hcheckedex _ Hmem) as (Hvars & ? & Hcheckedex).
1126
    repeat split.
1127
    1-4: congruence.
1128
1129
1130
1131
1132
    intros v__FP m__FP Heval__FP.
    unfold checked_error_expressions in Hcheckedall.
    specialize (Hcheckedall v__R v__FP m__FP iv__A err__A) as (af & err__af & Hcheckedall); auto.
    exists af, err__af, noise_map1.
    intuition.
1133
1134
1135
1136
  }
  destruct Htypecheck as (m__e & Hetype & (Htypecheck__e & ?) & Hvalidexec).
  rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; simpl in Hvalidbounds.
1137
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
  destruct u; [|congruence].
  destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
    as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
    simpl in Hvalidbounds; try congruence.
  destruct (FloverMap.find e subexpr_map) as [subaf|] eqn: Hsubaf;
    simpl in Hvalidbounds; [|congruence].
  destruct (FloverMap.find e A) as [(subiv, suberr)|] eqn: Hsuba;
    simpl in Hvalidbounds; [|congruence].
  destruct (Qeq_bool err__A suberr) eqn: Heq__err; simpl in Hvalidbounds; [|congruence].
  inversion Hvalidbounds; subst; clear Hvalidbounds.
1148
  inversion Heval__R; subst.
1149
1150
1151
  unfold isCompat in H2.
  destruct m; cbn in H2; try congruence; clear H2.
  pose proof H3 as H3det.
1152
  specialize (IHe expr_map1 subexpr_map noise_map1 noise1 noise2 v1 subiv suberr).
1153
  specialize IHe as (IHevex & IHevall); eauto;
1154
1155
1156
1157
    [destruct Hrange; auto|].
  split.
  - destruct IHevex as ((nF & m & IHeval) & IHcheckedex).
    assert (exists (v__FP : R) (m__FP : mType),
1158
               eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Unop Neg e)) v__FP m__FP).
1159
1160
    {
      exists (evalUnop Neg nF); exists m__e.
1161
      eapply Unop_neg'; eauto.
1162
1163
1164
      { eapply toRExpMap_some with (e:=Unop Neg e); eauto. }
      { destruct H as [? [? ?]].
        assert (x = m).
1165
        { eapply validTypes_exec; eauto. }
1166
1167
1168
1169
1170
        subst; auto. }
    }
    split; auto.
    intros e' Hnin Hin.
    destruct (flover_map_in_dec e' subexpr_map) as [Hin1|Hnin1].
1171
    + edestruct IHcheckedex as (? & ? & ?); eauto.
1172
    + destruct (flover_map_el_eq_extension Hnin1 Hin) as [Heq Hexpeq]; auto.
1173
1174
      split; [|split; [|now rewrite Hexpeq]].
      1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq;
1175
        try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1176
1177
      1: now apply subset_diff_to_subset_union.
      erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
1178
1179
1180
1181
  - intros v__FP m__FP Heval__FPdet.
    inversion Heval__FPdet; subst.
    pose proof H5 as H5det.
    specialize (IHevall v0 m)
1182
      as (ihaf & iherr__af & ihnoise_map & IHcontf & IHnoise & IHfresh & IHcontn & IHnoise_map &
1183
1184
1185
1186
1187
1188
1189
          IHsub__A & IHerrpos & IHiv__err & IHerr & IHevals & IHchecked); auto.
    replace subaf with ihaf by congruence.
    apply Qeq_bool_eq in Heq__err.
    apply Qeq_eqR in Heq__err.
    rename v0 into nF.
    exists (AffineArithQ.negate_aff ihaf), iherr__af, ihnoise_map.
    repeat split; auto.
1190
1191
1192
1193
1194
    + pose proof contained_flover_map_extension as H'.
      rewrite mem_false_find_none in Hmem.
      specialize (H' _ expr_map1 _ (AffineArithQ.negate_aff ihaf) Hmem).
      etransitivity; try eassumption.
      now apply contained_flover_map_add_compat.
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
    + rewrite afQ2R_negate_aff.
      unfold negate_aff.
      now apply mult_aff_const_fresh_compat.
    + rewrite FloverMapFacts.P.F.add_eq_o; try auto.
      apply Q_orderedExps.exprCompare_refl.
    + rewrite afQ2R_negate_aff.
      rewrite toInterval_negate_aff.
      rewrite IHiv__err.
      cbn.
      f_equal; lra.
    + now rewrite Heq__err.
    + rewrite Rsub_eq_Ropp_Rplus in IHevals.
      cbn.
      field_rewrite (- v1 - - nF = - (v1 - nF))%R.
      rewrite afQ2R_negate_aff.
      now apply negate_aff_sound.
    + intros e' Hnin Hin.
1212
      {
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
        destruct (FloverMapFacts.O.MO.eq_dec (Unop Neg e) e') as [Heqexp|Heqexp].
        - unfold checked_error_expressions.
          pose proof (expr_compare_eq_eval_compat _ _ Heqexp) as Hreq.
          rewrite <- Hreq.
          intros.
          exists (AffineArithQ.negate_aff ihaf), iherr__af.
          repeat split; try auto.
          + rewrite afQ2R_negate_aff.
            unfold negate_aff.
            now apply mult_aff_const_fresh_compat.
          + rewrite FloverMapFacts.P.F.add_eq_o; try auto.
          + rewrite afQ2R_negate_aff.
            rewrite toInterval_negate_aff.
            rewrite IHiv__err.
            cbn.
            f_equal; lra.
          + erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
            match goal with
            | [H1: FloverMap.find e' A = Some (iv__A0, err__A0),
                   H2: FloverMap.find e' A = Some (iv__A, err__A) |- _] => rewrite H1 in H2; inversion H2
            end.
            now rewrite Heq__err.
1235
          + erewrite meps_0_deterministic
1236
              with (v1 := v__R) (v2 := (evalUnop Neg v1)); eauto.
1237
            erewrite eval_expr_functional
1238
              with (v1 := v__FP) (v2 := (evalUnop Neg nF)); eauto;
1239
              [|erewrite Gamma_det; eauto].
1240
1241
1242
1243
1244
1245
1246
1247
1248
            rewrite Rsub_eq_Ropp_Rplus in IHevals.
            cbn.
            field_rewrite (- v1 - - nF = - (v1 - nF))%R.
            rewrite afQ2R_negate_aff.
            now apply negate_aff_sound.
        - destruct (FloverMapFacts.P.F.In_dec subexpr_map e') as [Hsubin|Hsubnin].
          + apply checked_error_expressions_flover_map_add_compat; auto.
          + pose proof (flover_map_el_eq_extension Hsubnin Hin) as [Hexeq Hreq].
            congruence.
1249
      }
1250
1251
Qed.

1252
Lemma validErrorboundAA_sound_plus e1 e2 E1 E2 A Gamma DeltaMap fVars dVars:
1253
1254
  validErrorboundAA_sound_statement e1 E1 E2 A Gamma DeltaMap fVars dVars ->
  validErrorboundAA_sound_statement e2 E1 E2 A Gamma DeltaMap fVars dVars ->
1255
  validErrorboundAA_sound_statement (Binop Plus e1 e2) E1 E2 A Gamma DeltaMap fVars dVars.
1256
1257
1258
Proof.
  intros IHe1 IHe2.
  unfold validErrorboundAA_sound_statement in IHe1, IHe2 |-*.
1259
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
1260
1261
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
                     Hcheckedex Hcheckedall;
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1262
1263
1264
1265
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (Binop Plus e1 e2) expr_map1) eqn: Hmem; cbn in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
1266
    inversion Hvalidbounds; subst; clear Hvalidbounds.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1267
1268
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
1269
    specialize (Hcheckedex _ Hmem) as (Hvars & ? & Hcheckedex).
1270
    repeat split.
1271
    1-4: congruence.
1272
1273
1274
1275
1276
    intros v__FP m__FP Heval__FP.
    unfold checked_error_expressions in Hcheckedall.
    specialize (Hcheckedall v__R v__FP m__FP iv__A err__A) as (af & err__af & Hcheckedall); auto.
    exists af, err__af, noise_map1.
    intuition.
Nikita Zyuzin's avatar
Nikita Zyuzin committed