AffineValidation.v 115 KB
Newer Older
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
2
Require Import Recdef.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
3
Require Import Flover.AffineForm Flover.AffineArithQ Flover.AffineArith.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
4
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
5
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing Flover.ssaPrgs.
6
Require Import Flover.IntervalValidation Flover.RealRangeArith.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
7

8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
Lemma usedVars_eq_compat e1 e2:
  Q_orderedExps.eq e1 e2 ->
  NatSet.eq (usedVars e1) (usedVars e2).
Proof.
  intros Heq.
  unfold Q_orderedExps.eq in Heq.
  functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
  - apply Nat.compare_eq in Heq.
    now rewrite Heq.
  - now set_tac.
  - simpl.
    reflexivity.
  - set_tac.
  - specialize (IHc e6).
    specialize (IHc0 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    simpl.
    now rewrite IHc, IHc0.
  - specialize (IHc e6).
    specialize (IHc0 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    simpl.
    now rewrite IHc, IHc0.
  - specialize (IHc e6).
    specialize (IHc0 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    simpl.
    now rewrite IHc, IHc0.
  - specialize (IHc e6).
    specialize (IHc0 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    simpl.
    now rewrite IHc, IHc0.
  - specialize (IHc e3).
    specialize (IHc0 e4).
    specialize (IHc1 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    apply NatSet.eq_leibniz in IHc1.
    simpl.
    now rewrite IHc, IHc0, IHc1.
  - simpl.
    now apply IHc.
  - simpl in e5.
    rewrite andb_false_iff in e5.
    destruct e5.
    + apply Ndec.Pcompare_Peqb in e8.
      congruence.
60 61
    + apply Nat.compare_eq in Heq; subst.
      rewrite Nat.eqb_refl in H; congruence.
62 63 64 65 66 67 68 69 70 71
Qed.

Lemma usedVars_toREval_toRExp_compat e:
  usedVars (toREval (toRExp e)) = usedVars e.
Proof.
  induction e; simpl; set_tac.
  - now rewrite IHe1, IHe2.
  - now rewrite IHe1, IHe2, IHe3.
Qed.

72
Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma fBits:
73
  Q_orderedExps.eq e1 e2 ->
74 75
  validRanges e1 A E Gamma fBits ->
  validRanges e2 A E Gamma fBits.
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
Proof.
  intros Heq.
  unfold Q_orderedExps.eq in Heq.
  functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
  - simpl.
    intros [_ validr1].
    repeat split; auto.
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    apply Nat.compare_eq in Heq.
    rewrite <- Heq.
    intuition.
  - intros [_ validr1].
    repeat split; auto.
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    intuition.
    + rewrite <- Hfind.
      symmetry.
      apply FloverMapFacts.P.F.find_o.
      unfold Q_orderedExps.exprCompare.
      rewrite e3; auto.
    + erewrite expr_compare_eq_eval_compat; eauto.
      rewrite Q_orderedExps.exprCompare_eq_sym.
      simpl.
      rewrite e3; auto.
  - simpl in e3.
    rewrite andb_false_iff in e3.
    destruct e3.
    + apply Ndec.Pcompare_Peqb in e6.
      congruence.
107 108
    + apply Nat.compare_eq in Heq; subst.
      rewrite Nat.eqb_refl in H; congruence.
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
  - intros valid1; destruct valid1 as [validsub1 validr1].
    specialize (IHc Heq validsub1).
    split; auto.
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    intuition.
    + rewrite <- Hfind.
      symmetry.
      apply FloverMapFacts.P.F.find_o.
      simpl.
      rewrite e5; auto.
    + erewrite expr_compare_eq_eval_compat; eauto.
      rewrite Q_orderedExps.exprCompare_eq_sym.
      simpl.
      rewrite e5; auto.
  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
    specialize (IHc e6 validsub1).
    specialize (IHc0 Heq validsub1').
    repeat split; auto; try congruence.
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    intuition.
    + rewrite <- Hfind.
      symmetry.
      apply FloverMapFacts.P.F.find_o.
      simpl.
      rewrite e6; auto.
    + erewrite expr_compare_eq_eval_compat; eauto.
      rewrite Q_orderedExps.exprCompare_eq_sym.
      simpl.
      rewrite Heq, e6; auto.
  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
    specialize (IHc e6 validsub1).
    specialize (IHc0 Heq validsub1').
    repeat split; auto; try congruence.
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    intuition.
    + rewrite <- Hfind.
      symmetry.
      apply FloverMapFacts.P.F.find_o.
      simpl.
      rewrite e6; auto.
    + erewrite expr_compare_eq_eval_compat; eauto.
      rewrite Q_orderedExps.exprCompare_eq_sym.
      simpl.
      rewrite Heq, e6; auto.
  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
    specialize (IHc e6 validsub1).
    specialize (IHc0 Heq validsub1').
    repeat split; auto; try congruence.
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    intuition.
    + rewrite <- Hfind.
      symmetry.
      apply FloverMapFacts.P.F.find_o.
      simpl.
      rewrite e6; auto.
    + erewrite expr_compare_eq_eval_compat; eauto.
      rewrite Q_orderedExps.exprCompare_eq_sym.
      simpl.
      rewrite Heq, e6; auto.
  - intros valid1; destruct valid1 as [[Hdiv [validsub1 validsub1']] validr1].
    specialize (IHc e6 validsub1).
    specialize (IHc0 Heq validsub1').
    repeat split; auto.
    {
      intros Hrefl; specialize (Hdiv Hrefl).
      intros iv2 err Hfind.
      erewrite FloverMapFacts.P.F.find_o with (y := e12) in Hfind.
      eapply Hdiv; eauto.
      now rewrite Q_orderedExps.exprCompare_eq_sym.
    }
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    intuition.
    + rewrite <- Hfind.
      symmetry.
      apply FloverMapFacts.P.F.find_o.
      simpl.
      rewrite e6; auto.
    + erewrite expr_compare_eq_eval_compat; eauto.
      rewrite Q_orderedExps.exprCompare_eq_sym.
      simpl.
      rewrite Heq, e6; auto.
  - intros valid1; destruct valid1 as [[validsub1 [validsub1' validsub1'']] validr1].
    specialize (IHc e3 validsub1).
    specialize (IHc0 e4 validsub1').
    specialize (IHc1 Heq validsub1'').
    repeat split; auto; try congruence.
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    intuition.
    + rewrite <- Hfind.
      symmetry.
      apply FloverMapFacts.P.F.find_o.
      simpl.
      rewrite e3, e4, Heq; auto.
    + erewrite expr_compare_eq_eval_compat; eauto.
      rewrite Q_orderedExps.exprCompare_eq_sym.
      simpl.
      rewrite Heq, e3, e4; auto.
  - intros valid1; destruct valid1 as [validsub1 validr1].
    specialize (IHc Heq validsub1).
    split; auto.
    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
    exists iv, err, vR.
    intuition.
    + rewrite <- Hfind.
      symmetry.
      apply FloverMapFacts.P.F.find_o.
      simpl.
      rewrite e5; auto.
    + erewrite expr_compare_eq_eval_compat; eauto.
      rewrite Q_orderedExps.exprCompare_eq_sym.
      simpl.
      rewrite e5; auto.
  - simpl in e5.
    rewrite andb_false_iff in e5.
    destruct e5.
    + apply Ndec.Pcompare_Peqb in e8.
      congruence.
232 233
    + apply Nat.compare_eq in Heq; subst.
      rewrite Nat.eqb_refl in *; congruence.
234 235
Qed.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
236
Definition updateExpMapIncr e new_af noise (emap: expressionsAffine) intv incr :=
Nikita Zyuzin's avatar
Nikita Zyuzin committed
237 238 239 240 241 242 243 244 245 246 247
  let new_iv := toIntv new_af in
  if isSupersetIntv new_iv intv then
    Some (FloverMap.add e new_af emap, (noise + incr)%nat)
  else None.

Definition updateExpMap e af noise emap intv :=
  updateExpMapIncr e af noise emap intv 0.

Definition updateExpMapSucc e af noise emap intv :=
  updateExpMapIncr e af noise emap intv 1.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
248 249 250 251
Definition nozeroiv iv :=
  ((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
            ((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))).

252
Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
253
           (exprsAf: expressionsAffine) (currentMaxNoise: nat): option (expressionsAffine * nat) :=
254 255 256 257 258 259 260
  match FloverMap.find e exprsAf with
  | Some _ =>
    (* expression has already been checked; we do not want to introduce *)
    (*      a new affine polynomial for the same expression *)
    Some (exprsAf, currentMaxNoise)
  | None =>
    (* We see it for the first time; update the expressions map *)
261 262
    olet ares := FloverMap.find e A in
    let (intv, _) := ares in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
263
    match e with
Nikita Zyuzin's avatar
Nikita Zyuzin committed
264
    | Var _ v =>
265 266 267 268 269 270 271
      if NatSet.mem v validVars then
        Some (exprsAf, currentMaxNoise)
      else
        let af := fromIntv (P v) currentMaxNoise in
        if isSupersetIntv (toIntv af) intv then
          Some (FloverMap.add e af exprsAf, (currentMaxNoise + 1)%nat)
        else None
Nikita Zyuzin's avatar
Nikita Zyuzin committed
272
    | Const _ c => if isSupersetIntv (c, c) intv then
Nikita Zyuzin's avatar
Nikita Zyuzin committed
273
                    let af := fromIntv (c,c) currentMaxNoise in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
274 275 276
                    Some (FloverMap.add e af exprsAf, currentMaxNoise)
                  else None
    | Unop o e' =>
Nikita Zyuzin's avatar
Nikita Zyuzin committed
277
      olet valid := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
278 279
      let (exprsAf', n') := valid in
      olet af := FloverMap.find e' exprsAf' in
280
      match o with
Nikita Zyuzin's avatar
Nikita Zyuzin committed
281
      | Neg =>
Nikita Zyuzin's avatar
Nikita Zyuzin committed
282
        updateExpMap e (AffineArithQ.negate_aff af) n' exprsAf' intv
Nikita Zyuzin's avatar
Nikita Zyuzin committed
283
      | Inv =>
Nikita Zyuzin's avatar
Nikita Zyuzin committed
284 285 286 287 288
        let iv := toIntv af in
        if nozeroiv iv
        then
          updateExpMapSucc e (AffineArithQ.inverse_aff af n') n' exprsAf' intv
        else None
Nikita Zyuzin's avatar
Nikita Zyuzin committed
289 290
      end
    | Binop o e1 e2 =>
Nikita Zyuzin's avatar
Nikita Zyuzin committed
291
      olet valid1 := validAffineBounds e1 A P validVars exprsAf currentMaxNoise in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
292 293
      let (exprsAf1, n1) := valid1 in
      olet af1 := FloverMap.find e1 exprsAf1 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
294
      olet valid2 := validAffineBounds e2 A P validVars exprsAf1 n1 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
295 296 297 298
      let (exprsAf2, n2) := valid2 in
      olet af2 := FloverMap.find e2 exprsAf2 in
      match o with
      | Plus =>
299
        updateExpMap e (AffineArithQ.plus_aff af1 af2) n2 exprsAf2 intv
Nikita Zyuzin's avatar
Nikita Zyuzin committed
300
      | Sub =>
301
        updateExpMap e (AffineArithQ.subtract_aff af1 af2) n2 exprsAf2 intv
Nikita Zyuzin's avatar
Nikita Zyuzin committed
302
      | Mult =>
303
        updateExpMapSucc e (AffineArithQ.mult_aff af1 af2 n2) n2 exprsAf2 intv
Nikita Zyuzin's avatar
Nikita Zyuzin committed
304
      | Div =>
305 306
          olet ares2 := FloverMap.find e2 A in
          let (aiv2, _) := ares2 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
307
          let iv2 := toIntv af2 in
308
          if nozeroiv iv2 && nozeroiv aiv2
Nikita Zyuzin's avatar
Nikita Zyuzin committed
309
          then
310
            updateExpMapIncr e (AffineArithQ.divide_aff af1 af2 n2) n2 exprsAf2 intv 2
Nikita Zyuzin's avatar
Nikita Zyuzin committed
311 312 313
          else None
      end
    | Fma e1 e2 e3 =>
Nikita Zyuzin's avatar
Nikita Zyuzin committed
314
      olet valid1 := validAffineBounds e1 A P validVars exprsAf currentMaxNoise in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
315 316
      let (exprsAf1, n1) := valid1 in
      olet af1 := FloverMap.find e1 exprsAf1 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
317
      olet valid2 := validAffineBounds e2 A P validVars exprsAf1 n1 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
318 319
      let (exprsAf2, n2) := valid2 in
      olet af2 := FloverMap.find e2 exprsAf2 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
320
      olet valid3 := validAffineBounds e3 A P validVars exprsAf2 n2 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
321 322
      let (exprsAf3, n3) := valid3 in
      olet af3 := FloverMap.find e3 exprsAf3 in
323
        updateExpMapSucc e (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 n3)) n3 exprsAf3 intv
324
    | Downcast _ e' =>
Nikita Zyuzin's avatar
Nikita Zyuzin committed
325
      olet valid' := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
326 327 328 329 330
      let (exprsAf', n') := valid' in
      olet asubres := FloverMap.find e' A in
      let (iv, _) := asubres in
      olet af' := FloverMap.find e' exprsAf' in
      if (isSupersetIntv intv iv) && (isSupersetIntv iv intv) then
331
        Some (FloverMap.add e af' exprsAf', n')
Nikita Zyuzin's avatar
Nikita Zyuzin committed
332
      else None
333
    end
Nikita Zyuzin's avatar
Nikita Zyuzin committed
334
  end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
335

Nikita Zyuzin's avatar
Nikita Zyuzin committed
336 337 338 339 340
Fixpoint afQ2R (af: affine_form Q): affine_form R := match af with
| AffineForm.Const c => AffineForm.Const (Q2R c)
| Noise n v af' => Noise n (Q2R v) (afQ2R af')
end.

341 342 343 344 345 346
Lemma afQ2R_const v:
  afQ2R (AffineForm.Const v) = AffineForm.Const (Q2R v).
Proof.
  trivial.
Qed.

347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
Lemma afQ2R_get_const a:
  get_const (afQ2R a) = Q2R (get_const a).
Proof.
  induction a; auto.
Qed.

Lemma afQ2R_radius a:
  radius (afQ2R a) = Q2R (AffineArithQ.radius a).
Proof.
  induction a; try (simpl; lra).
  simpl.
  rewrite Q2R_plus.
  rewrite Rabs_eq_Qabs.
  now f_equal.
Qed.

363 364 365 366 367 368 369
Lemma afQ2R_get_max_index a:
  get_max_index (afQ2R a) = get_max_index a.
Proof.
  unfold get_max_index.
  functional induction (get_max_index_aux 0 a); try auto;simpl; rewrite e0; auto.
Qed.

370 371 372 373 374 375 376 377 378 379
Lemma to_interval_to_intv a:
  (Q2R (fst (toIntv a)), Q2R (snd (toIntv a))) = toInterval (afQ2R a).
Proof.
  unfold toIntv, toInterval.
  unfold mkInterval, mkIntv.
  simpl fst; simpl snd.
  rewrite afQ2R_get_const.
  rewrite afQ2R_radius.
  f_equal; try apply Q2R_minus; try apply Q2R_plus.
Qed.
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

Lemma afQ2R_plus_aff af1 af2:
  afQ2R (AffineArithQ.plus_aff af1 af2) = plus_aff (afQ2R af1) (afQ2R af2).
Proof.
  unfold AffineArithQ.plus_aff, plus_aff.
  remember (af1, af2) as a12.
  assert (fst a12 = af1 /\ snd a12 = af2) as Havals by now rewrite Heqa12.
  destruct Havals as [Heqa1 Heqa2].
  rewrite <- Heqa1, <- Heqa2.
  clear Heqa1 Heqa2 Heqa12 af1 af2.
  functional induction (AffineArithQ.plus_aff_tuple a12); simpl; rewrite plus_aff_tuple_equation.
  - f_equal; apply Q2R_plus.
  - f_equal.
    assumption.
  - f_equal.
    assumption.
  - rewrite e2.
    f_equal; try apply Q2R_plus.
    assumption.
  - rewrite e2.
    rewrite e3.
    f_equal; try apply Q2R_plus.
    assumption.
  - rewrite e2.
    rewrite e3.
    f_equal; try apply Q2R_plus.
    assumption.
Qed.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
409 410
Lemma afQ2R_mult_aff_aux af1 af2:
  afQ2R (AffineArithQ.mult_aff_aux (af1, af2)) = mult_aff_aux (afQ2R af1, afQ2R af2).
411 412 413 414 415 416 417
Proof.
  unfold AffineArithQ.mult_aff, mult_aff.
  remember (af1, af2) as a12.
  assert (fst a12 = af1 /\ snd a12 = af2) as Havals by now rewrite Heqa12.
  destruct Havals as [Heqa1 Heqa2].
  rewrite <- Heqa1, <- Heqa2.
  clear Heqa1 Heqa2 Heqa12 af1 af2.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
418 419 420 421 422 423
  functional induction (AffineArithQ.mult_aff_aux a12); simpl in *;
    rewrite mult_aff_aux_equation;
    try (f_equal; try apply Q2R_mult; assumption).
  {
    rewrite e2.
    f_equal; try assumption.
424
    simpl.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
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
    rewrite Q2R_plus; do 2 rewrite Q2R_mult.
    do 2 rewrite afQ2R_get_const.
    reflexivity.
  }
  all: rewrite e2; rewrite e3.
  all: f_equal; try assumption.
  all: simpl.
  all: rewrite Q2R_mult.
  all: rewrite afQ2R_get_const.
  all: reflexivity.
Qed.

Lemma afQ2R_mult_aff af1 af2 n:
  afQ2R (AffineArithQ.mult_aff af1 af2 n) = mult_aff (afQ2R af1) (afQ2R af2) n.
Proof.
  unfold AffineArithQ.mult_aff, mult_aff.
  destruct (Qeq_bool (AffineArithQ.radius af1) 0) eqn: Heq.
  - rewrite orb_true_l.
    rewrite Qeq_bool_iff in Heq.
    apply Qeq_eqR in Heq.
    rewrite <- afQ2R_radius in Heq.
    rewrite Q2R0_is_0 in Heq.
    destruct Req_dec_sum as [Heq' | Heq']; rewrite Heq in Heq'; try lra.
    apply afQ2R_mult_aff_aux.
  - rename Heq into Heq1.
    destruct (Qeq_bool (AffineArithQ.radius af2) 0) eqn: Heq2.
    + rewrite orb_true_r.
      rewrite Qeq_bool_iff in Heq2.
      apply Qeq_eqR in Heq2.
      rewrite <- afQ2R_radius in Heq2.
      rewrite Q2R0_is_0 in Heq2.
      destruct Req_dec_sum as [Heq' | Heq']; rewrite Heq2 in Heq'; try lra.
      apply afQ2R_mult_aff_aux.
    + apply RMicromega.Qeq_false in Heq1.
      apply RMicromega.Qeq_false in Heq2.
      rewrite Q2R0_is_0 in Heq1.
      rewrite Q2R0_is_0 in Heq2.
      rewrite <- afQ2R_radius in Heq1.
      rewrite <- afQ2R_radius in Heq2.
464
      simpl.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
465 466
      destruct Req_dec_sum as [Heq' | Heq'];
        try (apply Rmult_integral in Heq'; destruct Heq'; try lra).
467
      f_equal.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
468 469
      * rewrite Q2R_mult.
        do 2 rewrite afQ2R_radius.
470
        reflexivity.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
471 472
      * apply afQ2R_mult_aff_aux.
Qed.
473

Nikita Zyuzin's avatar
Nikita Zyuzin committed
474 475 476
Lemma afQ2R_negate_aff af:
  afQ2R (AffineArithQ.negate_aff af) = negate_aff (afQ2R af).
Proof.
477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500
  unfold AffineArithQ.negate_aff.
  unfold AffineArithQ.mult_aff_const.
  rewrite afQ2R_mult_aff.
  simpl.
  unfold negate_aff.
  unfold mult_aff_const.
  f_equal.
  - f_equal.
    rewrite Q2R_opp.
    lra.
  - f_equal.
    unfold get_max_index.
    functional induction (get_max_index_aux 0 af); try auto; simpl; now rewrite e0.
Qed.

Lemma afQ2R_subtract_aff af1 af2:
  afQ2R (AffineArithQ.subtract_aff af1 af2) = subtract_aff (afQ2R af1) (afQ2R af2).
Proof.
  unfold AffineArithQ.subtract_aff.
  rewrite afQ2R_plus_aff.
  rewrite afQ2R_negate_aff.
  reflexivity.
Qed.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
501
Lemma afQ2R_inverse_aff af n:
502
  above_zero (afQ2R af) \/ below_zero (afQ2R af) ->
Nikita Zyuzin's avatar
Nikita Zyuzin committed
503 504
  afQ2R (AffineArithQ.inverse_aff af n) = inverse_aff (afQ2R af) n.
Proof.
505
  intros above_below.
506 507
  unfold AffineArithQ.inverse_aff.
  unfold inverse_aff.
508 509 510
  unfold above_zero, below_zero in above_below.
  unfold ivhi, IVhi, ivlo, IVlo in *.
  rewrite <- to_interval_to_intv in above_below.
511
  rewrite <- to_interval_to_intv.
512 513 514 515 516 517 518 519 520 521 522 523 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
  simpl fst in above_below |-*.
  simpl snd in above_below |-*.
  assert (AffineArithQ.radius af >= 0) by eauto using AffineArithQ.radius_nonneg.
  assert (get_const af - AffineArithQ.radius af <= get_const af + AffineArithQ.radius af) as Hrel by lra.
  replace 0%R with (Q2R 0) in above_below by lra.
  destruct above_below as [Heq | Heq]; apply Rlt_Qlt in Heq.
  - assert (get_const af + AffineArithQ.radius af > 0) as Hposhi by lra.
    destruct (Qlt_bool (get_const af + AffineArithQ.radius af) 0) eqn: H'';
      try rewrite Qlt_bool_iff in H''; try lra.
    apply Qlt_Rlt in Hposhi.
    destruct (Rlt_dec (Q2R (get_const af + AffineArithQ.radius af)) 0); try lra.
    apply Rlt_Qlt in Hposhi.
    assert (~ get_const af - AffineArithQ.radius af == 0) as minus_nonzero by lra.
    assert (~ get_const af + AffineArithQ.radius af == 0) as plus_nonzero by lra.
    assert (~ -(get_const af - AffineArithQ.radius af) == 0) as minus_nonzero' by lra.
    assert (~ -(get_const af + AffineArithQ.radius af) == 0) as plus_nonzero' by lra.
    assert (~ maxAbs (get_const af - AffineArithQ.radius af, get_const af + AffineArithQ.radius af) *
            maxAbs (get_const af - AffineArithQ.radius af, get_const af + AffineArithQ.radius af) == 0) as ?.
    {
      unfold maxAbs.
      unfold minAbs.
      simpl fst.
      simpl snd.
      try rewrite Qabs.Qabs_pos; try lra.
      try rewrite Qabs.Qabs_pos; try lra.
      try rewrite Q.max_r; try lra.
      try rewrite Q.min_l; try lra.
      unfold not.
      intros H'.
      apply Qmult_integral in H'; lra.
    }
    assert (~ maxAbs (get_const af - AffineArithQ.radius af, get_const af + AffineArithQ.radius af) == 0) as ?.
    {
      unfold maxAbs.
      unfold minAbs.
      simpl fst.
      simpl snd.
      try rewrite Qabs.Qabs_pos; try lra.
      try rewrite Qabs.Qabs_pos; try lra.
      try rewrite Q.max_r; try lra.
    }
    assert (~ minAbs (get_const af - AffineArithQ.radius af, get_const af + AffineArithQ.radius af) == 0) as ?.
    {
      unfold maxAbs.
      unfold minAbs.
      simpl fst.
      simpl snd.
      try rewrite Qabs.Qabs_pos; try lra.
      try rewrite Qabs.Qabs_pos; try lra.
      try rewrite Q.max_r; try lra.
      try rewrite Q.min_l; try lra.
    }
    simpl.
    f_equal; unfold toIntv; simpl;
      repeat rewrite minAbs_impl_RminAbs; repeat rewrite maxAbs_impl_RmaxAbs;
      replace 1%R with (Q2R (1%Q)) by lra;
      replace 2%R with (Q2R (2#1)) by lra;
      repeat (repeat rewrite <- Q2R_plus; repeat rewrite <- Q2R_mult; repeat rewrite <- Q2R_div;
              repeat rewrite <- Q2R_minus; repeat rewrite <- Q2R_opp); try lra.
      unfold mult_aff_const, plus_aff_const.
      unfold AffineArithQ.mult_aff_const, AffineArithQ.plus_aff_const.
      repeat rewrite <- afQ2R_const.
      rewrite <- afQ2R_mult_aff.
      rewrite <- afQ2R_plus_aff.
      repeat f_equal.
      now rewrite afQ2R_get_max_index.
  - rewrite <- Qlt_bool_iff in Heq.
    rewrite Heq.
    rewrite Qlt_bool_iff in Heq.
581 582
    apply Qlt_Rlt in Heq.
    destruct (Rlt_dec (Q2R (get_const af + AffineArithQ.radius af)) 0); try lra.
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
    apply Rlt_Qlt in Heq.
    assert (get_const af - AffineArithQ.radius af < 0) as minus_neg by lra.
    assert (~ get_const af - AffineArithQ.radius af == 0) as minus_nonzero by lra.
    assert (~ get_const af + AffineArithQ.radius af == 0) as plus_nonzero by lra.
    assert (~ -(get_const af - AffineArithQ.radius af) == 0) as minus_nonzero' by lra.
    assert (~ -(get_const af + AffineArithQ.radius af) == 0) as plus_nonzero' by lra.
    assert (~ maxAbs (get_const af - AffineArithQ.radius af, get_const af + AffineArithQ.radius af) *
            maxAbs (get_const af - AffineArithQ.radius af, get_const af + AffineArithQ.radius af) == 0) as ?.
    {
      unfold maxAbs.
      unfold minAbs.
      simpl fst.
      simpl snd.
      try rewrite Qabs.Qabs_neg; try lra.
      try rewrite Qabs.Qabs_neg; try lra.
      try rewrite Q.max_l; try lra.
      try rewrite Q.min_r; try lra.
      unfold not.
      intros H'.
      apply Qmult_integral in H'; lra.
    }
    assert (~ maxAbs (get_const af - AffineArithQ.radius af, get_const af + AffineArithQ.radius af) == 0) as ?.
    {
      unfold maxAbs.
      unfold minAbs.
      simpl fst.
      simpl snd.
      try rewrite Qabs.Qabs_neg; try lra.
      try rewrite Qabs.Qabs_neg; try lra.
      rewrite Q.max_l; try lra.
    }
    assert (~ minAbs (get_const af - AffineArithQ.radius af, get_const af + AffineArithQ.radius af) == 0) as ?.
    {
      unfold maxAbs.
      unfold minAbs.
      simpl fst.
      simpl snd.
      try rewrite Qabs.Qabs_neg; try lra.
      try rewrite Qabs.Qabs_neg; try lra.
      try rewrite Q.max_l; try lra.
      try rewrite Q.min_r; try lra.
    }
625
    simpl.
626 627 628 629 630 631 632 633 634 635 636 637 638 639
    f_equal; unfold toIntv; simpl;
      repeat rewrite minAbs_impl_RminAbs; repeat rewrite maxAbs_impl_RmaxAbs;
      replace 1%R with (Q2R (1%Q)) by lra;
      replace 2%R with (Q2R (2#1)) by lra;
      repeat (repeat rewrite <- Q2R_plus; repeat rewrite <- Q2R_mult; repeat rewrite <- Q2R_div;
              repeat rewrite <- Q2R_minus; repeat rewrite <- Q2R_opp); try lra.
      unfold mult_aff_const, plus_aff_const.
      unfold AffineArithQ.mult_aff_const, AffineArithQ.plus_aff_const.
      repeat rewrite <- afQ2R_const.
      rewrite <- afQ2R_mult_aff.
      rewrite <- afQ2R_plus_aff.
      repeat f_equal.
      now rewrite afQ2R_get_max_index.
Qed.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
640

641
Lemma afQ2R_divide_aff af1 af2 n:
642
  above_zero (afQ2R af2) \/ below_zero (afQ2R af2) ->
643
  afQ2R (AffineArithQ.divide_aff af1 af2 n) = divide_aff (afQ2R af1) (afQ2R af2) n.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
644
Proof.
645
  intros.
646 647
  unfold AffineArithQ.divide_aff.
  rewrite afQ2R_mult_aff.
648
  rewrite afQ2R_inverse_aff; auto.
649
Qed.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
650

Nikita Zyuzin's avatar
Nikita Zyuzin committed
651
Lemma afQ2R_fresh n a:
Nikita Zyuzin's avatar
Nikita Zyuzin committed
652
  fresh n a <-> fresh n (afQ2R a).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
653
Proof.
654
  split; induction a; intros *.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
655 656 657 658 659 660 661
  all: try (unfold fresh, get_max_index; rewrite get_max_index_aux_equation; now simpl).
  all: intros A.
  all: remember A as A' eqn:tmp; clear tmp.
  all: apply fresh_noise_gt in A.
  all: apply fresh_noise_compat in A'.
  all: specialize (IHa A').
  all: apply fresh_noise; assumption.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
662 663
Qed.

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
Lemma nozero_above_below af:
  nozeroiv (toIntv af) = true ->
  above_zero (afQ2R af) \/ below_zero (afQ2R af).
Proof.
  intros noz % orb_prop.
  destruct noz as [below | above].
  - right.
    unfold below_zero.
    apply andb_prop in below as [below notz].
    rewrite negb_true_iff in notz.
    apply Qeq_bool_neq in notz.
    rewrite Qle_bool_iff in below.
    assert (IVhi (toInterval (afQ2R af)) = Q2R (ivhi (toIntv af))) as Heq
        by (rewrite <- to_interval_to_intv; trivial).
    rewrite Heq.
    assert (ivhi (toIntv af) < 0) as Hlt by lra.
    apply Qlt_Rlt in Hlt.
    lra.
  - left.
    unfold above_zero.
    apply andb_prop in above as [above notz].
    rewrite negb_true_iff in notz.
    apply Qeq_bool_neq in notz.
    rewrite Qle_bool_iff in above.
    assert (IVlo (toInterval (afQ2R af)) = Q2R (ivlo (toIntv af))) as Heq
        by (rewrite <- to_interval_to_intv; trivial).
    rewrite Heq.
    assert (ivlo (toIntv af) > 0) as Hlt by lra.
    apply Qlt_Rlt in Hlt.
    lra.
Qed.

696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714
Lemma subset_union s1 s2 s3:
  NatSet.Subset (s1 -- s3) s2 ->
  NatSet.Subset s1 (NatSet.union s2 s3).
Proof.
  intros diff.
  hnf in diff |-*.
  intros a Hin1.
  specialize (diff a).
  destruct (NatSet.mem a s3) eqn: Hmem.
  - rewrite NatSet.mem_spec in Hmem.
    rewrite NatSet.union_spec.
    now right.
  - apply not_in_not_mem in Hmem.
    rewrite NatSet.union_spec.
    left.
    apply diff.
    set_tac.
Qed.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
715 716 717
Definition affine_dVars_range_valid (dVars: NatSet.t) (E: env) (A: analysisResult) noise exprAfs map1: Prop :=
  forall v, NatSet.In v dVars ->
       exists af vR iv err,
718 719 720
         isSupersetIntv (toIntv af) iv = true /\
         FloverMap.find (elt:=affine_form Q) (Var Q v) exprAfs = Some af /\
         fresh noise af /\
Nikita Zyuzin's avatar
Nikita Zyuzin committed
721
         (forall n, (n >= noise)%nat -> map1 n = None) /\
722 723
         FloverMap.find (Var Q v) A = Some (iv, err) /\
         E v = Some vR /\
Nikita Zyuzin's avatar
Nikita Zyuzin committed
724
         af_evals (afQ2R af) vR map1.
725

726 727
Definition affine_fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
  forall v,
728
    NatSet.In v fVars ->
729 730
    exists vR, E v = Some vR /\
          (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
731

732
Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
733 734 735
  forall v, NatSet.In v S ->
       exists m: mType, Gamma v = Some m.

736
Lemma contained_flover_map_none (e: expr Q) (expmap1: FloverMap.t (affine_form Q)) expmap2:
737 738 739 740 741 742 743 744 745 746 747
  contained_flover_map expmap1 expmap2 ->
  FloverMap.find e expmap2 = None ->
  FloverMap.find e expmap1 = None.
Proof.
  intros cont Hfound1.
  unfold contained_flover_map in cont.
  destruct (FloverMap.find (elt:=affine_form Q) e expmap1) eqn: Heq; auto.
  apply cont in Heq.
  congruence.
Qed.

748
Lemma validAffineBounds_validRanges e (A: analysisResult) E Gamma fBits:
749 750 751
  (exists map af vR aiv aerr,
      FloverMap.find e A = Some (aiv, aerr) /\
      isSupersetIntv (toIntv af) aiv = true /\
752
      eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
753 754 755
      af_evals (afQ2R af) vR map) ->
  exists iv err vR,
    FloverMap.find e A = Some (iv, err) /\
756
    eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775
    (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
  intros sound_affine.
  destruct sound_affine as [map [af [vR [aiv [aerr [Haiv [Hsup [Hee Heval]]]]]]]].
  exists aiv, aerr, vR.
  split; try split; try auto.
  apply AffineArith.to_interval_containment in Heval.
  unfold isSupersetIntv in Hsup.
  apply andb_prop in Hsup as [Hsupl Hsupr].
  apply Qle_bool_iff in Hsupl.
  apply Qle_bool_iff in Hsupr.
  apply Qle_Rle in Hsupl.
  apply Qle_Rle in Hsupr.
  rewrite <- to_interval_to_intv in Heval.
  simpl in Heval.
  destruct Heval as [Heval1 Heval2].
  split; eauto using Rle_trans.
Qed.

776
Definition checked_expressions (A: analysisResult) E Gamma fBits fVars dVars e iexpmap inoise map1 :=
777
  exists af vR aiv aerr,
778
    NatSet.Subset (usedVars e) (NatSet.union fVars dVars) /\
779 780 781 782 783
    FloverMap.find e A = Some (aiv, aerr) /\
    isSupersetIntv (toIntv af) aiv = true /\
    FloverMap.find e iexpmap = Some af /\
    fresh inoise af /\
    (forall n, (n >= inoise)%nat -> map1 n = None) /\
784 785
    eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
    validRanges e A E Gamma fBits /\
786 787
    af_evals (afQ2R af) vR map1.

788
Lemma checked_expressions_contained A E Gamma fBits fVars dVars e expmap1 expmap2 map1 map2 noise1 noise2:
789 790 791 792
  contained_map map1 map2 ->
  contained_flover_map expmap1 expmap2 ->
  (noise2 >= noise1)%nat ->
  (forall n : nat, (n >= noise2)%nat -> map2 n = None) ->
793 794
  checked_expressions A E Gamma fBits fVars dVars e expmap1 noise1 map1 ->
  checked_expressions A E Gamma fBits fVars dVars e expmap2 noise2 map2.
795 796 797 798 799 800 801 802
Proof.
  intros cont contf Hnoise Hvalidmap checked1.
  unfold checked_expressions in checked1 |-*.
  destruct checked1 as [af [vR [aiv [aerr checked1]]]].
  exists af, vR, aiv, aerr.
  intuition; eauto using fresh_monotonic, af_evals_map_extension.
Qed.

803
Lemma checked_expressions_flover_map_add_compat A E Gamma fBits fVars dVars e e' af expmap noise map:
804
  Q_orderedExps.exprCompare e e' <> Eq ->
805 806
  checked_expressions A E Gamma fBits fVars dVars e' expmap noise map ->
  checked_expressions A E Gamma fBits fVars dVars e' (FloverMap.add e af expmap) noise map.
807 808 809 810 811 812 813 814
Proof.
  intros Hneq checked1.
  unfold checked_expressions in checked1 |-*.
  destruct checked1 as [af' [vR [aiv [aerr checked1]]]].
  exists af', vR, aiv, aerr.
  intuition.
  rewrite FloverMapFacts.P.F.add_neq_o; auto.
Qed.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
815

816
Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
817
      fVars dVars (E: env) Gamma fBits exprAfs noise iexpmap inoise map1:
818
  (forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
819
        checked_expressions A E Gamma fBits fVars dVars e iexpmap inoise map1) ->
820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835
  (inoise > 0)%nat ->
  (forall n, (n >= inoise)%nat -> map1 n = None) ->
  validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
  affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
  NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
  affine_fVars_P_sound fVars E P ->
  affine_vars_typed (NatSet.union fVars dVars) Gamma ->
  exists map2 af vR aiv aerr,
    contained_map map1 map2 /\
    contained_flover_map iexpmap exprAfs /\
    FloverMap.find e A = Some (aiv, aerr) /\
    isSupersetIntv (toIntv af) aiv = true /\
    FloverMap.find e exprAfs = Some af /\
    fresh noise af /\
    (forall n, (n >= noise)%nat -> map2 n = None) /\
    (noise >= inoise)%nat /\
836 837
    eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
    validRanges e A E Gamma fBits /\
838 839 840
    af_evals (afQ2R af) vR map2 /\
    (forall e, FloverMap.find e iexpmap = None ->
          (exists af, FloverMap.find e exprAfs = Some af) ->
841
          checked_expressions A E Gamma fBits fVars dVars e exprAfs noise map2).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
842
Proof.
843
  revert noise exprAfs inoise iexpmap map1.
844
  induction e;
845
    intros * visitedExpr inoisegtz validmap1 validBounds dVarsValid varsDisjoint fVarsSound varsTyped;
846
    simpl in validBounds.
847
  - specialize (dVarsValid n).
848
    specialize (fVarsSound n).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
849
    specialize (varsTyped n).
850
    pose proof visitedExpr as visitedExpr'.
851 852 853
    destruct (FloverMap.find (elt:=affine_form Q) (Var Q n) iexpmap) eqn: Hvisited.
    {
      inversion validBounds; subst; clear validBounds.
854
      specialize (visitedExpr (Var Q n)).
855 856 857 858 859 860 861 862 863 864 865 866
      assert (NatSet.Subset (usedVars (Var Q n)) (fVars  dVars)).
      {
        set_tac. set_tac. subst.
        hnf in varsDisjoint.
        specialize (varsDisjoint a0).
        destruct (NatSet.mem a0 dVars) eqn:?.
        + right. now apply NatSet.mem_spec.
        + left. apply varsDisjoint. set_tac.
      }
      destruct visitedExpr as [af [vR [aiv [aerr visitedExpr]]]]; eauto.
      exists map1, af, vR, aiv, aerr.
      intuition.
867
    }
868
    destruct (FloverMap.find (elt:=intv * error) (Var Q n) A) as [p |] eqn: Hares; simpl in validBounds; try congruence.
869
    destruct p as [aiv aerr].
Nikita Zyuzin's avatar
Nikita Zyuzin committed
870
    destruct (n mem dVars) eqn: Hmem.
871
    + rewrite NatSet.mem_spec in Hmem.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
872
      specialize (dVarsValid Hmem).
873 874
      assert (n  fVars  dVars) as H by intuition.
      specialize (varsTyped H) as [m varsTyped].
Nikita Zyuzin's avatar
Nikita Zyuzin committed
875
      destruct dVarsValid as [af [vR [iv [err dVarsValid]]]]; try reflexivity.
876
      inversion validBounds; subst; clear validBounds.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
877
      exists map1, af, vR, iv, err.
878
      intuition; try congruence.
879
    + destruct (isSupersetIntv (toIntv (fromIntv (P n) inoise)) aiv) eqn: Hsup; try congruence.
880
      inversion validBounds; subst; clear validBounds.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
881 882 883 884
      apply not_in_not_mem in Hmem.
      assert (n  fVars  dVars) as H by intuition.
      specialize (varsTyped H) as [m varsTyped].
      assert (n  fVars) as H' by intuition.
885
      specialize (fVarsSound H') as [vR [eMap interval_containment]].
886
      assert (FloverMap.find (Var Q n) (FloverMap.add (Var Q n) (fromIntv (P n) inoise) iexpmap) = Some (fromIntv (P n) inoise)) as Hfind
887
        by (rewrite FloverMapFacts.P.F.add_eq_o; try auto; apply Q_orderedExps.exprCompare_refl).
888
      assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Var Q n))) vR REAL) as Heeval
889
          by (constructor; auto; simpl; rewrite varsTyped; reflexivity).
890
      destruct (Qeq_bool (ivlo (P n)) (ivhi (P n))) eqn: Heq.
891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912
      * assert (af_evals (afQ2R (fromIntv (P n) inoise)) vR map1) as Hevals.
        {
          assert (fromIntv (P n) inoise = (AffineForm.Const (ivhi (P n) / (2 # 1) + ivlo (P n) / (2 # 1))%Q)) as HfromIntv
              by (unfold fromIntv; now rewrite Heq).
          pose proof Heq as Heq'.
          apply Qeq_bool_iff in Heq'.
          simpl in Heq'.
          apply Qeq_eqR in Heq'.
          rewrite Heq' in interval_containment.
          assert (vR = Q2R (snd (P n))) as HvR by lra.
          rewrite HfromIntv.
          unfold af_evals.
          simpl.
          rewrite Q2R_plus.
          repeat rewrite Q2R_div by lra.
          rewrite Heq'.
          rewrite HvR.
          lra.
        }
        assert (fresh (inoise + 1) (fromIntv (P n) inoise)) as Hfresh
            by (unfold fresh, fromIntv, get_max_index; rewrite Heq; simpl; lia).
        exists map1, (fromIntv (P n) inoise), vR, aiv, aerr.
913 914
        repeat split; auto.
        -- reflexivity.
915
        -- apply contained_flover_map_extension; assumption.
916 917 918 919
        -- intros n' Hn'.
           apply validmap1.
           lia.
        -- lia.
920 921 922
        -- apply validAffineBounds_validRanges.
           exists map1, (fromIntv (P n) inoise), vR, aiv, aerr.
           repeat split; auto.
923 924 925 926
        -- intros e Hnone Hsome.
           destruct Hsome as [afS Hsome].
           {
             destruct (FloverMapFacts.O.MO.eq_dec (Var Q n) e).
927 928
             - assert (Q_orderedExps.exprCompare e (Var Q n) = Eq)
                 by (now rewrite Q_orderedExps.exprCompare_eq_sym).
929
               rewrite FloverMapFacts.P.F.add_eq_o in Hsome; auto.
930 931 932 933
               inversion Hsome; subst; clear Hsome.
               unfold checked_expressions.
               exists (fromIntv (P n) inoise), vR, aiv, aerr.
               intuition.
934 935 936
               + rewrite usedVars_eq_compat; eauto.
                 set_tac.
                 left; set_tac; split; auto; subst; set_tac.
937 938
               + erewrite FloverMapFacts.P.F.find_o; eauto.
               + rewrite FloverMapFacts.P.F.add_eq_o; auto.
939
               + erewrite expr_compare_eq_eval_compat; eauto.
940 941 942 943 944
               + eapply validRanges_eq_compat; eauto.
                 simpl; split; auto.
                 apply validAffineBounds_validRanges.
                 exists map1, (fromIntv (P n) inoise), vR, aiv, aerr.
                 repeat split; auto.
945 946 947
             - rewrite FloverMapFacts.P.F.add_neq_o in Hsome; auto.
               congruence.
           }
948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 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 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039
      * assert (exists q, af_evals (afQ2R (fromIntv (P n) inoise)) vR (updMap map1 inoise q))
          as [q Hevals].
        {
          unfold af_evals, fromIntv.
          rewrite Heq.
          apply Qeq_bool_neq in Heq.
          simpl in Heq.
          simpl.
          setoid_rewrite upd_sound.
          simpl.
          apply Q.max_case_strong.
          - intros x y Hxy.
            apply Qeq_eqR in Hxy.
            rewrite Hxy.
            auto.
          - intros Hmax.
            apply Qle_Rle in Hmax.
            repeat rewrite Q2R_minus.
            repeat rewrite Q2R_plus.
            repeat rewrite Q2R_div; try lra.
            replace (Q2R (2#1)) with 2%R by lra.
            repeat rewrite Q2R_minus in Hmax.
            repeat rewrite Q2R_plus in Hmax.
            rewrite Q2R_div in Hmax; try lra.
            rewrite Q2R_div in Hmax; try lra.
            replace (Q2R (2#1)) with 2%R in Hmax by lra.
            pose (l := (Q2R (fst (P n)))).
            pose (h := (Q2R (snd (P n)))).
            fold l h in Hmax, interval_containment |-*.
            pose (noise_expression := ((vR - h / 2 - l / 2) / (h / 2 + l / 2 - l))%R).
            assert (-(1) <= noise_expression <= 1)%R as Hnoise.
            {
              unfold noise_expression.
              apply Rabs_Rle_condition.
              destruct (Rle_lt_dec (h / 2 + l / 2 - l) 0)%R as [Hle0 | Hle0].
              - apply Rle_lt_or_eq_dec in Hle0; destruct Hle0 as [Hlt | Hlt];
                  try (field_simplify in Hlt; assert (h = l) as Hz by lra; apply eqR_Qeq in Hz; lra).
              - rewrite Rdiv_abs_le_bounds; try lra.
                assert (0 < h - l)%R as H1 by lra.
                Rrewrite (vR - h / 2 - l /2 = vR - (h + l) / 2)%R.
                Rrewrite (1 * (h / 2 + l / 2 - l) = (h - l) / 2)%R.
                apply Rabs_Rle_condition; lra.
            }
            pose (noise := exist (fun x => -(1) <= x <= 1)%R noise_expression Hnoise).
            exists noise.
            unfold noise, noise_expression.
            simpl.
            field.
            intros Hnotz.
            field_simplify in Hnotz.
            assert (h = l) as Hz by lra.
            apply eqR_Qeq in Hz.
            lra.
          - intros Hmax.
            apply Qle_Rle in Hmax.
            repeat rewrite Q2R_minus.
            repeat rewrite Q2R_plus.
            repeat rewrite Q2R_div; try lra.
            replace (Q2R (2#1)) with 2%R by lra.
            repeat rewrite Q2R_minus in Hmax.
            repeat rewrite Q2R_plus in Hmax.
            rewrite Q2R_div in Hmax; try lra.
            rewrite Q2R_div in Hmax; try lra.
            replace (Q2R (2#1)) with 2%R in Hmax by lra.
            pose (l := (Q2R (fst (P n)))).
            pose (h := (Q2R (snd (P n)))).
            fold l h in Hmax, interval_containment |-*.
            pose (noise_expression := ((vR - h / 2 - l / 2) / (h / 2 + l / 2 - l))%R).
            assert (-(1) <= noise_expression <= 1)%R as Hnoise.
            {
              unfold noise_expression.
              apply Rabs_Rle_condition.
              destruct (Rle_lt_dec (h / 2 + l / 2 - l) 0)%R as [Hle0 | Hle0].
              - apply Rle_lt_or_eq_dec in Hle0; destruct Hle0 as [Hlt | Hlt];
                  try (field_simplify in Hlt; assert (h = l) as Hz by lra; apply eqR_Qeq in Hz; lra).
              - rewrite Rdiv_abs_le_bounds; try lra.
                assert (0 < h - l)%R as H1 by lra.
                Rrewrite (vR - h / 2 - l /2 = vR - (h + l) / 2)%R.
                Rrewrite (1 * (h / 2 + l / 2 - l) = (h - l) / 2)%R.
                apply Rabs_Rle_condition; lra.
            }
            pose (noise := exist (fun x => -(1) <= x <= 1)%R noise_expression Hnoise).
            exists noise.
            unfold noise, noise_expression.
            simpl.
            field.
            intros Hnotz.
            field_simplify in Hnotz.
            assert (h = l) as Hz by lra.
            apply eqR_Qeq in Hz.
            lra.
        }
1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051
        assert (forall n0 : nat, (n0 >= inoise + 1)%nat -> updMap map1 inoise q n0 = None).
        {
          intros n' Hn'.
          unfold updMap.
          destruct (n' =? inoise) eqn: Hneq.
          - apply beq_nat_true in Hneq.
            lia.
          - apply validmap1.
            lia.
        }
        assert (fresh (inoise + 1) (fromIntv (P n) inoise)) as Hfresh
            by (unfold fresh, fromIntv, get_max_index; rewrite Heq; simpl; lia).
1052 1053 1054 1055
        exists (updMap map1 inoise q), (fromIntv (P n) inoise), vR, aiv, aerr.
        repeat split; auto.
        -- apply contained_map_extension.
           apply validmap1; lia.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1056
        -- apply contained_flover_map_extension.
1057
           assumption.
1058
        -- lia.
1059 1060 1061
        -- apply validAffineBounds_validRanges.
           exists (updMap map1 inoise q), (fromIntv (P n) inoise), vR, aiv, aerr.
           repeat split; auto.
1062 1063 1064 1065
        -- intros e Hnone Hsome.
           destruct Hsome as [afS Hsome].
           {
             destruct (FloverMapFacts.O.MO.eq_dec (Var Q n) e).
1066 1067
             - assert (Q_orderedExps.exprCompare e (Var Q n) = Eq)
                 by (now rewrite Q_orderedExps.exprCompare_eq_sym).
1068
               rewrite FloverMapFacts.P.F.add_eq_o in Hsome; auto.
1069 1070 1071 1072
               inversion Hsome; subst; clear Hsome.
               unfold checked_expressions.
               exists (fromIntv (P n) inoise), vR, aiv, aerr.
               intuition.
1073 1074 1075
               + rewrite usedVars_eq_compat; eauto.
                 set_tac.
                 left; set_tac; split; auto; subst; set_tac.
1076 1077
               + erewrite FloverMapFacts.P.F.find_o; eauto.
               + rewrite FloverMapFacts.P.F.add_eq_o; auto.
1078
               + erewrite expr_compare_eq_eval_compat; eauto.
1079 1080 1081 1082 1083
               + eapply validRanges_eq_compat; eauto.
                 simpl; split; auto.
                 apply validAffineBounds_validRanges.
                 exists (updMap map1 inoise q), (fromIntv (P n) inoise), vR, aiv, aerr.
                 repeat split; auto.
1084 1085 1086
             - rewrite FloverMapFacts.P.F.add_neq_o in Hsome; auto.
               congruence.
           }
1087
  - pose proof visitedExpr as visitedExpr'.
1088
    unfold checked_expressions in visitedExpr.
1089 1090 1091
    destruct (FloverMap.find (elt:=affine_form Q) (Const m v) iexpmap) eqn: Hvisited.
    {
      inversion validBounds; subst; clear validBounds.
1092
      specialize (visitedExpr (Const m v)).
1093
      destruct visitedExpr as [af [vR [aiv [aerr visitedExpr]]]].
1094
      - eexists; eauto.
1095
      - exists map1, af, vR, aiv, aerr.
1096
        intuition.
1097
    }
1098 1099 1100
    destruct (FloverMap.find (elt:=intv * error) (Const m v) A) eqn: Hares;
      simpl in validBounds; try congruence.
    destruct p as [i e].
1101 1102 1103
    destruct (isSupersetIntv (v, v) i) eqn: Hsup; try congruence.
    assert (isSupersetIntv (v, v) i = true) as Hsup' by assumption.
    apply andb_prop in Hsup' as [L R].
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1104 1105 1106
    rewrite Qle_bool_iff in L, R.
    simpl ivlo in L, R.
    simpl ivhi in L, R.
1107 1108
    assert (fst i <= v) as L' by assumption.
    assert (v <= snd i) as R' by assumption.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1109 1110 1111
    apply Qle_Rle in L.
    apply Qle_Rle in R.
    inversion validBounds; subst; clear validBounds.
1112 1113 1114
    assert (isSupersetIntv (toIntv (fromIntv (v, v) noise)) i = true).
    {
      unfold fromIntv, toIntv.
1115 1116 1117 1118 1119 1120
      simpl.
      rewrite Qeq_bool_refl.
      apply andb_true_intro.
      split; rewrite Qle_bool_iff; simpl; field_simplify; Qrewrite ((2#1) * v * / (2#1) == v).
      * now Qrewrite (fst i / 1 == fst i).
      * now Qrewrite (snd i / 1 == snd i).
1121 1122 1123 1124
    }
    assert (fresh noise (fromIntv (v, v) noise))
      by (unfold fromIntv; simpl ivlo; simpl ivhi; rewrite Qeq_bool_refl;
          unfold fresh, get_max_index; rewrite get_max_index_aux_equation; lia).
1125
    assert (af_evals (afQ2R (fromIntv (v, v) noise)) (perturb (Q2R v) REAL 0) map1).
1126 1127
    {
      unfold perturb.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1128 1129 1130 1131 1132
      unfold fromIntv.
      simpl.
      rewrite Qeq_bool_refl.
      simpl.
      rewrite Q2R_plus.
1133 1134 1135
      rewrite Q2R_div; try lra.
      unfold af_evals, Ropt_eq