ErrorValidationAA.v 180 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
     Infra.RealSimps Infra.Ltacs Environments ErrorAnalysis ErrorValidationAAutil
16
     ExpressionSemantics IntervalValidation TypeValidator RealRangeValidator ErrorBounds
17
     ErrorValidation AffineForm AffineArithQ AffineArith AffineValidation.
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
    | Let _ _ _ _ => None
210
    end.
211 212

(** Error bound command validator **)
213
(*
214 215 216 217
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 *)
218
         (currNoise: nat) (* current maximal noise term *)
219
         (errMap: FloverMap.t (affine_form Q)) (* previously seen affine polys *)
220
  : option (FloverMap.t (affine_form Q) * nat) :=
221
  match f with
222
  | Let m x e g =>
223 224 225 226 227 228
    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
229 230 231 232 233
        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
234 235 236 237
      else
          None
    | _,_ => None
    end
238
  | Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
239
  end.
240
 *)
241

242 243 244 245 246
(* Notation for the universal case of the soundness statement, to help reason
   about memoization cases. This allows us to show several monotonicity lemmas
   that simplify the soundness proofs. This definition is just an extract from
   the full soundness statement, for elaboration on the used assumptions and the
   goal, find that statement below *)
247
Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap
248
           noise_map noise expr_map :=
249
  forall v__R v__FP m__FP (iv__A: intv) (err__A: error),
250 251
  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 ->
252
  FloverMap.find e A = Some (iv__A, err__A) ->
253
  exists af err__af,
254
    fresh noise (afQ2R af) /\
255
    (forall n, (n >= noise)%nat -> noise_map n = None) /\
256 257 258 259
    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 /\
260
    af_evals (afQ2R af) (v__R - v__FP)%R noise_map.
261

262
Lemma checked_error_expressions_extension e E1 E2 A Gamma DeltaMap
263 264 265 266 267
      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) ->
268 269
  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.
270 271 272 273 274 275 276 277 278
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.

279
Lemma checked_error_expressions_flover_map_add_compat e e' af E1 E2 A Gamma DeltaMap
280 281
      noise_map noise expr_map:
  Q_orderedExps.exprCompare e' e <> Eq ->
282 283
  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
284 285 286 287 288 289 290 291 292 293 294
                            (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.

295 296
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.
297

298 299 300 301
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.
302
Proof.
303 304
  intros H Hdvars.
  unfold dVars_contained in Hdvars |-*.
305 306
  intros v Hvin.
  specialize (Hdvars v Hvin).
307
  eapply flover_map_in_extension; eauto.
308 309
Qed.

310 311 312 313 314 315 316 317 318
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
319
  | Let _ _ _ _ => False (* FIXME *)
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 415 416 417 418 419 420 421
  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.
422 423
  - simpl in *. destruct Hcont; contradiction.
  - simpl in *. destruct Hcont; contradiction.
424 425
Qed.

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 485 486 487 488 489 490 491 492 493 494 495
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.
496
    destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
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 523 524 525 526 527 528 529 530 531 532 533
    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).
534
    destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
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 655 656 657 658 659 660 661 662 663 664 665
    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).
666
    destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
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 749 750 751 752 753 754 755 756 757 758 759
    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.
760
    destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788
    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.
789 790 791 792 793
  - destruct (FloverMap.mem (elt:=affine_form Q) (Let m n e1 e2) expr_map1) eqn:Hmem.
    + inversion Hvalidbounds; subst.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    + Flover_compute. destruct (negb (Qleb 0 e)) eqn:?; congruence.
794 795
Qed.

796 797 798 799 800
(* The soundness statements starts off with assumption that the checking
   function succeeds and then also maintains several invariants. We require
   these invariants because of the checker function dependency on the current
   noise index and its memoization of the previosly computed polynomials. We
   explain these invariants in-line below. *)
801 802
Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars :=
  forall (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
803
    (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
804
    (iv__A : intv) (err__A : error),
805 806
    (forall (v : R) (m' : mType),
        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
807
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
808
    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
809 810
    validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
    validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
811 812
    (* WAS: usedVars *)
    NatSet.Subset (freeVars e -- dVars) fVars ->
813
    validTypes e Gamma ->
814
    FloverMap.find e A = Some (iv__A, err__A) ->
815 816
    (* Starting noise index is greater than 0 and the noise mapping doesn't
       map it and anything above to a noise value *)
817 818
    (0 < noise1)%nat ->
    (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
819 820
    (* If a var is a dVar, we know it's in expr_map and invoke the corresponding
     preconditions (described below) *)
821
    dVars_contained dVars expr_map1 ->
822 823 824
    (* Precondition:
       Memoization for the existential case of the goal: if we checked the expression
       already, we know that there is an execution and certificate results for it *)
825
    (forall e' : FloverMap.key,
826
        FloverMap.In e' expr_map1 ->
827
        (* Assumption needed for Cmd_sound proof *)
828 829
        (* WAS: usedVars *)
        NatSet.Subset (freeVars e') (NatSet.union fVars dVars) /\
830
        (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
831
        exists (v__FP' : R) (m__FP' : mType),
832
          eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
833 834 835 836 837 838
    (* Precondition:
       Memoization for the universal case of the goal -- note that
       `checked_error_expressions` track only that case: if we checked
       the expression already, then, if we provide the execution in
       finite precision and the certificate results, we will know that
       the execution's error is bounded *)
839
    (forall e' : FloverMap.key,
840
        FloverMap.In e' expr_map1 ->
841
        checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
842
    (* THE EXESTENTIAL CASE OF THE GOAL *)
843
    ((exists (v__FP : R) (m__FP : mType),
844
         eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
845 846 847
     (* Invariant of the existential case:
        our given expr_map1 is updated only with the expressions for which
        the existential part holds *)
848
     (forall e' : FloverMap.key,
849
         ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
850 851
         (* WAS: usedVars *)
         NatSet.Subset (freeVars e') (NatSet.union fVars dVars) /\
852
         (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
853
         exists (v__FP' : R) (m__FP' : mType),
854
           eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP')) /\
855
    (* UNIVERSAL CASE OF THE GOAL *)
856
    (forall (v__FP : R) (m__FP : mType),
857
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
858 859 860
        (* For the given evaluation we can find a polynomial and an
           error bound with a monotonic extension of noise_map1 to
           noise_map2 *)
861
        exists (af : affine_form Q) (err__af : R) (noise_map2 : noise_mapping),
862 863
          (* Invariant: the checker function only adds new polynomials
             to the expr_map, never removes something from it *)
864
          contained_flover_map expr_map1 expr_map2 /\
865 866
          (* Noise index invariants: the checker function returns new
             noise that is not used in already produced polynomials *)
867 868
          (noise1 <= noise2)%nat /\
          fresh noise2 (afQ2R af) /\
869
          (* Invariant: noise_map is incrementally updated *)
870 871 872
          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 /\
873 874 875 876 877
          (* To show that the error is bounded by the polynomial, we say that
             the polynomial's range is bounded by err__af, which has a value
             less or equal to the certificate error, and that the polynomial
             captures any difference between real and finite-precision
             evaluations *)
878 879 880 881
          (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 /\
882 883 884
          (* Invariant of the universal case:
             our given expr_map1 is updated only with the expressions for which
             the universal part (the conclusion directly above) holds *)
885
          (forall e' : FloverMap.key,
886
              ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
887
              checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)).
888 889 890 891 892

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.
893
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
894 895
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
                     Hcheckedex Hcheckedall;
896
  inversion Heval__R; subst.
897 898 899 900 901 902 903
  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).
904
    specialize (Hcheckedex _ Hmem) as (Hvars & Hcert' & Hcheckedex).
905
    repeat split.
906
    1-4: congruence.
907 908 909 910 911
    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.
912 913 914 915 916 917 918 919 920 921 922
  }
  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.
923
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
924 925 926 927
  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.
928 929 930
    specialize (Hdvars n Hmem__n).
    rewrite <- FloverMapFacts.P.F.not_mem_in_iff in Hmem.
    congruence.
931 932
  - destruct (Qleb (computeErrorQ (maxAbs iv__A) m) err__A) eqn: Herrle; cbn in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
933
    rewrite mem_false_find_none in Hmem.
934 935 936 937
    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).
938 939
    split.
    + assert (exists (v__FP : R) (m__FP : mType),
940
                 eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Var Q n)) v__FP m__FP).
941
      {
942 943 944
        exists v__fp, m.
        constructor; auto.
        eapply toRExpMap_some with (e:=Var Q n); eauto.
945
      }
946 947 948
      split; auto.
      intros e' Hnin Hin.
      destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq].
949
      split; [|split; [|now rewrite Hexpeq]].
950 951 952 953
      * rewrite freeVars_eq_compat;
          try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
        simpl. set_tac. subst; auto.
      * erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
954
    + intros v__FP m__FP Heval__FP.
955
      rewrite Qle_bool_iff in Herrle.
956 957
      apply Qle_Rle in Herrle.
      inversion Heval__FP; subst.
958 959 960 961 962 963
      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].
964 965 966 967
      {
        rewrite afQ2R_mkErrorPolyQ.
        rewrite computeErrorQ_computeErrorR.
        apply af_evals_mkErrorPolyR_updMap; auto using computeErrorR_pos.
968 969
        pose proof (approxEnv_fVar_bounded Henv H1 Hv__fp Hmem__n' Hetype) as H.
        eapply Rle_trans; try exact H.
970 971 972 973 974 975 976 977 978
        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 |-*.
979
      {
980
        repeat split; try auto.
981
        - now apply contained_flover_map_extension.
982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006
        - 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.
1007
          {
1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027
            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.
1028 1029 1030
            - 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.
1031
          }
1032
      }
1033 1034 1035 1036 1037 1038
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.
1039
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
1040 1041 1042 1043 1044 1045 1046 1047 1048
                     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).
1049
    specialize (Hcheckedex _ Hmem) as (Hvars & Hcert' & Hcheckedex).
1050
    repeat split.
1051
    1-4: congruence.
1052 1053 1054 1055 1056
    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.
1057
  }
1058 1059 1060
  destruct (Htypecheck) as (m__e & Hetype & _ & Hvalidexec).
  rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
1061
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
1062 1063 1064
  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.
1065 1066
  split.
  - assert (exists (v__FP : R) (m__FP : mType),
1067
               eval_expr E2 (toRExpMap Gamma) DeltaMap
1068 1069
                             (toRExp (Expressions.Const m v)) v__FP m__FP).
    {
1070
      specialize (Hdeltamap (Q2R v) m)
1071 1072
        as (delta' & Hdelta & Hdelta').
      exists (perturb (Q2R v) m delta'), m.
1073
      eapply Const_dist' with (delta := delta'); auto.
1074 1075 1076 1077
    }
    split; auto.
    intros e' Hnin Hin.
    destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq].
1078
    split; [|split; [|now rewrite Hexpeq]].
1079 1080 1081 1082
      * rewrite freeVars_eq_compat;
          try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
        simpl. set_tac.
      * erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
1083
  - rewrite Qle_bool_iff in Herrle.
1084
    apply Qle_Rle in Herrle.
1085
    intros * Heval__FP.
1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107
    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)
1108
                                         E1 E2 m__FP _ _ Heval__R Heval__FP) as H'.
1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127
      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.
1128
    + now apply contained_flover_map_extension.
1129 1130 1131 1132 1133 1134
    + 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.
1135
    + apply computeErrorR_pos.
1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147
    + 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.
1148 1149
      * rewrite afQ2R_mkErrorPolyQ.
        apply mkErrorPolyR_fresh_compat; lia.
1150 1151
      * rewrite FloverMapFacts.P.F.add_eq_o; auto.
      * apply computeErrorR_pos.
1152 1153 1154
      * rewrite afQ2R_mkErrorPolyQ.
        rewrite computeErrorQ_computeErrorR.
        rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
1155 1156 1157 1158 1159
      * 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.
1160
      * erewrite meps_0_deterministic
1161
          with (v1 := v__R) (v2 := (perturb (Q2R v) REAL delta)); eauto.
1162
        erewrite eval_expr_functional
1163
          with (v1 := v__FP) (v2 := (perturb (Q2R v) m__FP delta0)); eauto.
1164
        erewrite Gamma_det; eauto.
1165 1166 1167 1168 1169 1170 1171 1172
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 |-*.
1173
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
1174
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
1175
                     Hcheckedex Hcheckedall.
1176 1177 1178 1179 1180
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (elt:=affine_form Q) (Unop u e) expr_map1) eqn: Hmem;
    simpl in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
1181
    inversion Hvalidbounds; subst; clear Hvalidbounds.
1182 1183
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
1184
    specialize (Hcheckedex _ Hmem) as (Hvars & ? & Hcheckedex).
1185
    repeat split.
1186
    1-4: congruence.
1187 1188 1189 1190 1191
    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.
1192 1193 1194 1195
  }
  destruct Htypecheck as (m__e & Hetype & (Htypecheck__e & ?) & Hvalidexec).
  rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; simpl in Hvalidbounds.
1196
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
1197 1198 1199 1200 1201 1202 1203 1204 1205 1206
  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.
1207
  inversion Heval__R; subst.
1208 1209 1210
  unfold isCompat in H2.
  destruct m; cbn in H2; try congruence; clear H2.
  pose proof H3 as H3det.
1211
  specialize (IHe expr_map1 subexpr_map noise_map1 noise1 noise2 v1 subiv suberr).
1212
  specialize IHe as (IHevex & IHevall); eauto;
1213 1214 1215 1216
    [destruct Hrange; auto|].
  split.
  - destruct IHevex as ((nF & m & IHeval) & IHcheckedex).
    assert (exists (v__FP : R) (m__FP : mType),
1217
               eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Unop Neg e)) v__FP m__FP).
1218 1219
    {
      exists (evalUnop Neg nF); exists m__e.
1220
      eapply Unop_neg'; eauto.
1221 1222 1223
      { eapply toRExpMap_some with (e:=Unop Neg e); eauto. }
      { destruct H as [? [? ?]].
        assert (x = m).
1224
        { eapply validTypes_exec; eauto. }
1225 1226 1227 1228 1229
        subst; auto. }
    }
    split; auto.
    intros e' Hnin Hin.
    destruct (flover_map_in_dec e' subexpr_map) as [Hin1|Hnin1].
1230
    + edestruct IHcheckedex as (? & ? & ?); eauto.
1231
    + destruct (flover_map_el_eq_extension Hnin1 Hin) as [Heq Hexpeq]; auto.
1232
      split; [|split; [|now rewrite Hexpeq]].
1233 1234 1235 1236
      * rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
          try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
        now apply subset_diff_to_subset_union.
      * erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
1237 1238 1239 1240
  - intros v__FP m__FP Heval__FPdet.
    inversion Heval__FPdet; subst.
    pose proof H5 as H5det.
    specialize (IHevall v0 m)
1241
      as (ihaf & iherr__af & ihnoise_map & IHcontf & IHnoise & IHfresh & IHcontn & IHnoise_map &
1242 1243 1244 1245 1246 1247 1248
          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.
1249 1250 1251 1252 1253
    + 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.
1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270
    + 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.
1271
      {
1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293
        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.
1294
          + erewrite meps_0_deterministic
1295
              with (v1 := v__R) (v2 := (evalUnop Neg v1)); eauto.
1296
            erewrite eval_expr_functional
1297
              with (v1 := v__FP) (v2 := (evalUnop Neg nF)); eauto;
1298
              [|erewrite Gamma_det; eauto].
1299 1300 1301 1302 1303 1304 1305 1306 1307
            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.
1308
      }
1309 1310
Qed.

1311
Lemma validErrorboundAA_sound_plus e1 e2 E1 E2 A Gamma DeltaMap fVars dVars:
1312 1313
  validErrorboundAA_sound_statement e1 E1 E2 A Gamma DeltaMap fVars dVars ->
  validErrorboundAA_sound_statement e2 E1 E2 A Gamma DeltaMap fVars dVars ->
1314
  validErrorboundAA_sound_statement (Binop Plus e1 e2) E1 E2 A Gamma DeltaMap fVars dVars.
1315 1316 1317
Proof.
  intros IHe1 IHe2.
  unfold validErrorboundAA_sound_statement in IHe1, IHe2 |-*.
1318
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
1319 1320
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
                     Hcheckedex Hcheckedall;
1321 1322 1323 1324
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (Binop Plus e1 e2) expr_map1) eqn: Hmem; cbn in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
1325
    inversion Hvalidbounds; subst; clear Hvalidbounds.
1326 1327
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
1328
    specialize (Hcheckedex _ Hmem) as (Hvars & ? & Hcheckedex).
1329
    repeat split.
1330
    1-4: congruence.
1331 1332 1333 1334 1335
    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.
1336 1337 1338 1339 1340
  }
  cbn in Htypecheck.
  destruct (Htypecheck) as (m__e & find_t & (Htypecheck1 & Htypecheck2 & Hjoin) & valid_exec).
  rewrite find_t in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
1341
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366
  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].
  cbn in Hrange.
  destruct Hrange as [[Hdivvalid Hsubranges] [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'.
  replace tmpvR with v__R in * by congruence; clear Heval1' Heval__R' tmpvR.
  destruct Hsubranges as [Hrange1 Hrange2].
  pose proof (validRanges_single _ _ _ _ Hrange1)
    as [iv1 [err1 [vR1 [Hres__A1 [Heval1 Hcontained1]]]]].
  pose proof (validRanges_single _ _ _ _ Hrange2)
    as [iv2 [err2 [vR2 [Hres__A2 [Heval2 Hcontained2]]]]].
  rewrite Hres__A1, Hres__A2 in Hvalidbounds.
  specialize (IHe1 expr_map1 subexpr_map1 noise_map1 noise1 subnoise1 vR1 iv1 err1).
1367
  specialize IHe1 as (((nF1 & m1 & IHevex1) & IHchecked1) & IHevall1); eauto;
1368
    [clear - Hsubset; set_tac; set_tac|].
1369 1370 1371 1372 1373 1374 1375 1376 1377 1378
  destruct (Qleb (maxAbs (toIntv
                            (AffineArithQ.plus_aff (AffineArithQ.plus_aff subaf1 subaf2)
                                                   (mkErrorPolyQ
                                                      (computeErrorQ
                                                         (maxAbs (addIntv (widenIntv iv1 err1) (widenIntv iv2 err2))) m__e)
                                                      subnoise2)))) err__A) eqn: Herrle; [|congruence].
  clear Hdivvalid.
  rewrite Qle_bool_iff in Herrle.
  apply Qle_Rle in Herrle.
  inversion Hvalidbounds; subst; clear Hvalidbounds.
1379
  split.
1380
  * specialize (IHevall1 nF1 m1 IHevex1)
1381
      as (ihaf1 & iherr__af1 & ihnoise_map1 & IHcontf1 & IHnoise1 & IHfresh1 & IHcontn1 &
1382 1383 1384
          IHnoise_map1 & IHsub__A1 & IHerrpos1 & IHiv__err1 & IH__err1 & IHevals1 & IHcheckedall1).
    specialize (IHe2 subexpr_map1 subexpr_map2 ihnoise_map1 subnoise1 subnoise2
                     vR2 iv2 err2).
1385
    specialize IHe2 as (((nF2 & m2 & IHevex2) & IHchecked2) & IHevall2);
1386
      eauto.
1387 1388
    1: clear - Hsubset; set_tac; set_tac.
    1: lia.
1389
    1: eapply dVars_contained_extension; eauto.
1390 1391
    {
      intros e' Hin.
1392 1393 1394
      destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
      - specialize (Hcheckedex _ Hin1).
        intuition.
1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410
      - eapply IHchecked1; eauto.
    }
    {
      intros.
      destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
      - eapply checked_error_expressions_extension; try apply Hcheckedall; auto.
      - eapply checked_error_expressions_extension; try apply IHcheckedall1; auto; reflexivity.
    }
    destruct Hjoin as (m1' & m2' & Hgamma1 & Hgamma2 & join_exists).
    assert (m1' = m1) as Htmp.
    { eapply validTypes_exec with (e:=e1); eauto; eapply eval_det_eval_nondet; eauto. }
    rewrite Htmp in *; clear Htmp.
    assert (m2' = m2) as Htmp.
    { eapply validTypes_exec with (e:=e2); eauto; eapply eval_det_eval_nondet; eauto. }
    rewrite Htmp in *; clear Htmp.
    assert (exists (v__FP : R) (m__FP : mType),
1411
               eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Plus e1 e2)) v__FP m__FP) as H.
1412
    {
1413
      specialize (Hdeltamap (evalBinop Plus nF1 nF2) m__e)
1414 1415
        as (delta' & Hdelta & Hdelta').
      eexists; exists m__e.
1416
      eapply Binop_dist' with (delta := delta'); eauto.
1417 1418 1419 1420
      - congruence.
      - eapply toRExpMap_some; eauto.
        auto.
    }
1421 1422 1423 1424 1425
    pose proof H as H'.
    specialize H' as (? & ? & Heval).
    cbn in Heval.
    inversion Heval; subst.
    specialize (IHevall2 _ _ H10) as (? & ? & ? & ? & ?).
1426 1427
    split; auto.
    intros e' Hnin Hin.