IntervalValidation.v 19.9 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
(**
Heiko Becker's avatar
Heiko Becker committed
2 3 4 5 6
    Interval arithmetic checker and its soundness proof.
    The function validIntervalbounds checks wether the given analysis result is
    a valid range arithmetic for each sub term of the given expression e.
    The computation is done using our formalized interval arithmetic.
    The function is used in CertificateChecker.v to build the full checker.
Heiko Becker's avatar
Heiko Becker committed
7
**)
8
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
9
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Heiko Becker's avatar
Heiko Becker committed
10
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps.
11

Heiko Becker's avatar
Heiko Becker committed
12 13
Import Lists.List.ListNotations.

Heiko Becker's avatar
Heiko Becker committed
14 15
Fixpoint freeVars (V:Type) (f:exp V) : list nat:=
  match f with
Heiko Becker's avatar
Heiko Becker committed
16
  |Const n => []
17 18
  |Var _ v => []
  |Param _ v => [v]
Heiko Becker's avatar
Heiko Becker committed
19 20
  |Unop o f1 => freeVars V f1
  |Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2)
Heiko Becker's avatar
Heiko Becker committed
21 22
  end.

23 24 25
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
  let (intv, _) := absenv e in
    match e with
26 27
    | Var _ v => false
    | Param _ v =>
28
      isSupersetIntv (P v) intv
29
    | Const n =>
30
      isSupersetIntv (n,n) intv
31
    | Unop o f1 =>
Heiko Becker's avatar
Heiko Becker committed
32 33
    let rec := validIntervalbounds f1 absenv P in
    let (iv1, _) := absenv f1 in
34
    let opres :=
Heiko Becker's avatar
Heiko Becker committed
35
        match o with
36 37 38 39 40 41 42 43 44
        | Neg =>
          let new_iv := negateIntv iv1 in
          isSupersetIntv new_iv intv
        | Inv =>
          let nodiv0 := orb
                          (andb (Qleb (ivhi iv1) 0) (negb (Qeq_bool (ivhi iv1) 0)))
                          (andb (Qleb 0 (ivlo iv1)) (negb (Qeq_bool (ivlo iv1) 0))) in
          let new_iv := invertIntv iv1 in
          andb (isSupersetIntv new_iv intv) nodiv0
Heiko Becker's avatar
Heiko Becker committed
45 46
        end
    in
47
    andb rec opres
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
    | Binop b e1 e2 =>
      let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
      let (iv1,_) := absenv e1 in
      let (iv2,_) := absenv e2 in
      let opres :=
          match b with
          | Plus =>
            let new_iv := addIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Sub =>
            let new_iv := subtractIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Mult =>
            let new_iv := multIntv iv1 iv2 in
            isSupersetIntv new_iv intv
Heiko Becker's avatar
Heiko Becker committed
63
          | Div =>
64 65 66
            let nodiv0 := orb
                            (andb (Qleb (ivhi iv2) 0) (negb (Qeq_bool (ivhi iv2) 0)))
                            (andb (Qleb 0 (ivlo iv2)) (negb (Qeq_bool (ivlo iv2) 0))) in
Heiko Becker's avatar
Heiko Becker committed
67
            let new_iv := divideIntv iv1 iv2 in
68
            andb (isSupersetIntv new_iv intv) nodiv0
69 70 71 72 73
          end
      in
      andb rec opres
    end.

Heiko Becker's avatar
Heiko Becker committed
74 75 76
Theorem ivbounds_approximatesPrecond_sound f absenv P:
  validIntervalbounds f absenv P = true ->
  forall v, In v (freeVars Q f) ->
77 78
       Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof.
Heiko Becker's avatar
Heiko Becker committed
79
  induction f; unfold validIntervalbounds.
80 81 82 83 84 85 86 87 88
  - intros approx_true v v_in_fV; simpl in *; contradiction.
  - intros approx_true v v_in_fV; simpl in *.
    unfold isSupersetIntv.
    destruct v_in_fV; try contradiction.
    subst.
    destruct (P v); destruct (absenv (Param Q v)); simpl in *.
    destruct i; simpl in *.
    apply Is_true_eq_left in approx_true; auto.
  - intros approx_true v0 v_in_fV; simpl in *; contradiction.
Heiko Becker's avatar
Heiko Becker committed
89 90 91 92 93 94 95 96
  - intros approx_unary_true v v_in_fV.
    unfold freeVars in v_in_fV.
    apply Is_true_eq_left in approx_unary_true.
    destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
    apply andb_prop_elim in approx_unary_true.
    destruct approx_unary_true.
    apply IHf; try auto.
    apply Is_true_eq_true; auto.
97 98 99 100
  - intros approx_bin_true v v_in_fV.
    unfold freeVars in v_in_fV.
    apply in_app_or in v_in_fV.
    apply Is_true_eq_left in approx_bin_true.
Heiko Becker's avatar
Heiko Becker committed
101
    destruct (absenv (Binop b f1 f2)); destruct (absenv f1); destruct (absenv f2); simpl in *.
102 103 104 105
    apply andb_prop_elim in approx_bin_true.
    destruct approx_bin_true.
    apply andb_prop_elim in H.
    destruct H.
Heiko Becker's avatar
Heiko Becker committed
106 107
    destruct v_in_fV as [v_in_fV_f1 | v_in_fV_f2].
    + apply IHf1; auto.
108
      apply Is_true_eq_true; auto.
Heiko Becker's avatar
Heiko Becker committed
109
    + apply IHf2; auto.
110 111 112
      apply Is_true_eq_true; auto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
Corollary Q2R_max4 a b c d:
  Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
  unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto.
Qed.

Corollary Q2R_min4 a b c d:
  Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
  unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
Qed.

Ltac env_assert absenv e name :=
  assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).

128 129 130 131 132 133 134 135 136 137 138 139 140 141
Lemma validBoundsDiv_uneq_zero e1 e2 absenv P ivlo_e2 ivhi_e2 err:
  absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
  validIntervalbounds (Binop Div e1 e2) absenv P = true ->
  (ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
  intros absenv_eq validBounds.
  unfold validIntervalbounds in validBounds.
  env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]].
  env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]].
  rewrite abs_div, abs_e1, absenv_eq in validBounds.
  apply Is_true_eq_left in validBounds.
  apply andb_prop_elim in validBounds.
  destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds.
  destruct validBounds as [_ nodiv0].
142 143
  apply Is_true_eq_true in nodiv0.
  apply le_neq_bool_to_lt_prop; auto.
144 145
Qed.

Heiko Becker's avatar
Heiko Becker committed
146 147 148 149 150 151
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) cenv:
  forall vR,
  precondValidForExec P cenv ->
  validIntervalbounds f absenv P = true ->
  eval_exp 0%R cenv (toRExp f) vR ->
  (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
152
Proof.
Heiko Becker's avatar
Heiko Becker committed
153 154
  induction f.
  - intros vR precond_valid valid_bounds eval_f.
155
    pose proof (ivbounds_approximatesPrecond_sound (Var Q n) absenv P valid_bounds) as env_approx_p.
156
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
157
    destruct (absenv (Var Q n)); inversion valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
158
  - intros vR precond_valid valid_bounds eval_f.
159
    pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P valid_bounds) as env_approx_p.
160
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
161 162
    case_eq (absenv (Param Q n)).
    intros intv err absenv_n.
Heiko Becker's avatar
Heiko Becker committed
163 164 165
    rewrite absenv_n in valid_bounds.
    unfold precondValidForExec in precond_valid.
    specialize (env_approx_p n).
Heiko Becker's avatar
Heiko Becker committed
166
    case_eq (P n); intros ivlo ivhi p_n.
167
    unfold isSupersetIntv, freeVars in env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
168 169
    assert (In n (n::nil)) as n_in_n by (unfold In; auto).
    specialize (env_approx_p n_in_n).
Heiko Becker's avatar
Heiko Becker committed
170 171
    rewrite p_n, absenv_n in env_approx_p.
    specialize (precond_valid n); rewrite p_n in precond_valid.
Heiko Becker's avatar
Heiko Becker committed
172
    inversion eval_f; subst.
Heiko Becker's avatar
Heiko Becker committed
173 174
    rewrite perturb_0_val; auto.
    destruct intv as [abslo abshi]; simpl in *.
175
    apply andb_prop_elim in env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
176 177
    destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi].
    destruct precond_valid as [ivlo_le_env env_le_ivhi].
178 179 180
    apply Is_true_eq_true in abslo_le_ivlo; apply Is_true_eq_true in ivhi_le_abshi.
    unfold Qleb in abslo_le_ivlo, ivhi_le_abshi.
    apply Qle_bool_iff in abslo_le_ivlo; apply Qle_bool_iff in ivhi_le_abshi.
Heiko Becker's avatar
Heiko Becker committed
181 182 183 184 185 186 187 188
    apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi.
    split.
    + eapply Rle_trans.
      apply abslo_le_ivlo.
      apply ivlo_le_env.
    + eapply Rle_trans.
      apply env_le_ivhi.
      apply ivhi_le_abshi.
Heiko Becker's avatar
Heiko Becker committed
189
  - intros vR valid_precond valid_bounds eval_f.
190
    pose proof (ivbounds_approximatesPrecond_sound (Const v) absenv P valid_bounds) as env_approx_p.
191
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
192
    destruct (absenv (Const v)) as [intv err]; simpl.
193 194
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
195
    destruct valid_bounds as [valid_lo valid_hi].
Heiko Becker's avatar
Heiko Becker committed
196
    inversion eval_f; subst.
Heiko Becker's avatar
Heiko Becker committed
197
    rewrite perturb_0_val; auto.
198 199
    unfold contained; simpl.
    split.
Heiko Becker's avatar
Heiko Becker committed
200
    + apply Is_true_eq_true in valid_lo.
201
      unfold Qleb in *.
Heiko Becker's avatar
Heiko Becker committed
202 203 204 205 206 207
      apply Qle_bool_iff in valid_lo.
      apply Qle_Rle in valid_lo; auto.
    + apply Is_true_eq_true in valid_hi.
      unfold Qleb in *.
      apply Qle_bool_iff in valid_hi.
      apply Qle_Rle in valid_hi; auto.
Heiko Becker's avatar
Heiko Becker committed
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
  - intros vR valid_precond valid_bounds eval_f;
      pose proof (ivbounds_approximatesPrecond_sound (Unop u f) absenv P valid_bounds) as env_approx_p.
    case_eq (absenv (Unop u f)); intros intv err absenv_unop.
    destruct intv as [unop_lo unop_hi]; simpl.
    unfold validIntervalbounds in valid_bounds.
    rewrite absenv_unop in valid_bounds.
    case_eq (absenv f); intros intv_f err_f absenv_f.
    rewrite absenv_f in valid_bounds.
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
    destruct valid_bounds as [valid_rec valid_unop].
    apply Is_true_eq_true in valid_rec.
    inversion eval_f; subst.
    + specialize (IHf v1 valid_precond valid_rec H2).
      rewrite absenv_f in IHf; simpl in IHf.
223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238
      (* TODO: Make lemma *)
      unfold isSupersetIntv in valid_unop.
      apply andb_prop_elim in valid_unop.
      destruct valid_unop as [valid_lo valid_hi].
      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
      pose proof (interval_negation_valid (Q2R (fst intv_f),(Q2R (snd intv_f))) v1) as negation_valid.
      unfold contained, negateInterval in negation_valid; simpl in *.
      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
      destruct IHf.
      unfold eval_unop; split.
      * eapply Rle_trans. apply valid_lo.
        rewrite Q2R_opp; lra.
      * eapply Rle_trans.
        Focus 2. apply valid_hi.
        rewrite Q2R_opp; lra.
Heiko Becker's avatar
Heiko Becker committed
239 240
    + specialize (IHf v1 valid_precond valid_rec H3).
      rewrite absenv_f in IHf; simpl in IHf.
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306
      apply andb_prop_elim in valid_unop.
      destruct valid_unop as [valid_unop nodiv0].
      (* TODO: Make lemma *)
      unfold isSupersetIntv in valid_unop.
      apply andb_prop_elim in valid_unop.
      destruct valid_unop as [valid_lo valid_hi].
      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
      assert ((Q2R (ivhi intv_f) < 0)%R \/ (0 < Q2R (ivlo intv_f))%R) as nodiv0_prop.
       * apply Is_true_eq_true in nodiv0.
         apply le_neq_bool_to_lt_prop in nodiv0.
         destruct nodiv0.
         { left; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. }
         { right; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. }
       * pose proof (interval_inversion_valid (Q2R (fst intv_f),(Q2R (snd intv_f))) v1) as inv_valid.
         unfold contained, invertInterval in inv_valid; simpl in *.
         apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
         destruct IHf.
         rewrite perturb_0_val; auto.
         unfold eval_unop, perturb; split.
         { eapply Rle_trans. apply valid_lo.
           destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
           (* TODO: Extract lemma maybe *)
           - assert (0 < - (Q2R (snd intv_f)))%R as negation_pos by lra.
             assert (- (Q2R (snd intv_f)) <= - v1)%R as negation_flipped_hi by lra.
             apply Rinv_le_contravar in negation_flipped_hi; try auto.
             rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra.
             rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra.
             apply Ropp_le_contravar in negation_flipped_hi.
             repeat rewrite Ropp_involutive in negation_flipped_hi;
               rewrite Q2R_inv; auto.
             hnf; intros is_0.
             rewrite <- Q2R0_is_0 in nodiv0_neg.
             apply Rlt_Qlt in nodiv0_neg; lra.
           - rewrite Q2R_inv.
             apply Rinv_le_contravar; try lra.
             hnf; intros is_0.
             assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
             rewrite <- Q2R0_is_0 in nodiv0_pos.
             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
         }
         { eapply Rle_trans.
           Focus 2. apply valid_hi.
           destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
           - assert (Q2R (fst intv_f) < 0)%R as fst_lt_0 by lra.
             assert (0 < - (Q2R (fst intv_f)))%R as negation_pos by lra.
             assert (- v1 <= - (Q2R (fst intv_f)))%R as negation_flipped_lo by lra.
             apply Rinv_le_contravar in negation_flipped_lo; try auto.
             rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra.
             rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra.
             apply Ropp_le_contravar in negation_flipped_lo.
             repeat rewrite Ropp_involutive in negation_flipped_lo;
               rewrite Q2R_inv; auto.
             hnf; intros is_0.
             rewrite <- Q2R0_is_0 in negation_pos.
             rewrite <- Q2R_opp in negation_pos.
             apply Rlt_Qlt in negation_pos; lra.
             assert (0 < - (Q2R (snd intv_f)))%R by lra.
             lra.
           - rewrite Q2R_inv.
             apply Rinv_le_contravar; try lra.
             hnf; intros is_0.
             assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
             rewrite <- Q2R0_is_0 in nodiv0_pos.
             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
         }
Heiko Becker's avatar
Heiko Becker committed
307 308 309
  - intros vR valid_precond valid_bounds eval_f; inversion eval_f; subst.
    pose proof (ivbounds_approximatesPrecond_sound (Binop b f1 f2) absenv P valid_bounds) as env_approx_p.
    rewrite perturb_0_val in eval_f; auto.
Heiko Becker's avatar
Heiko Becker committed
310 311
    rewrite perturb_0_val; auto.
    simpl in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
312 313 314 315
    case_eq (absenv (Binop b f1 f2)); intros iv err absenv_bin.
    case_eq (absenv f1); intros iv1 err1 absenv_f1.
    case_eq (absenv f2); intros iv2 err2 absenv_f2.
    rewrite absenv_bin, absenv_f1, absenv_f2 in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
316 317 318 319 320 321
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
    destruct valid_bounds as [valid_rec valid_bin].
    apply andb_prop_elim in valid_rec.
    destruct valid_rec as [valid_e1 valid_e2].
    apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in  valid_e2.
Heiko Becker's avatar
Heiko Becker committed
322 323 324 325
    specialize (IHf1 v1 valid_precond valid_e1 H4);
      specialize (IHf2 v2 valid_precond valid_e2 H5).
    rewrite absenv_f1 in IHf1.
    rewrite absenv_f2 in IHf2.
326 327 328
    destruct b; simpl in *.
    + pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
      unfold validIntervalAdd in valid_add.
Heiko Becker's avatar
Heiko Becker committed
329
      specialize (valid_add v1 v2 IHf1 IHf2).
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351
      unfold contained in valid_add.
      unfold isSupersetIntv in valid_bin.
      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
      destruct valid_add as [valid_add_lo valid_add_hi].
      split.
      { eapply Rle_trans. apply valid_lo.
        unfold ivlo. unfold addIntv.
        simpl in valid_add_lo.
        repeat rewrite <- Q2R_plus in valid_add_lo.
        rewrite <- Q2R_min4 in valid_add_lo.
        unfold absIvUpd; auto. }
      { eapply Rle_trans.
        Focus 2.
        apply valid_hi.
        unfold ivlo, addIntv.
        simpl in valid_add_hi.
        repeat rewrite <- Q2R_plus in valid_add_hi.
        rewrite <- Q2R_max4 in valid_add_hi.
        unfold absIvUpd; auto. }
Heiko Becker's avatar
Heiko Becker committed
352
    + pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
Heiko Becker's avatar
Heiko Becker committed
353
      specialize (valid_sub v1 v2 IHf1 IHf2).
Heiko Becker's avatar
Heiko Becker committed
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
      unfold contained in valid_sub.
      unfold isSupersetIntv in valid_bin.
      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
      destruct valid_sub as [valid_sub_lo valid_sub_hi].
      split.
      * eapply Rle_trans. apply valid_lo.
        unfold ivlo. unfold subtractIntv.
        simpl in valid_sub_lo.
        repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo.
        repeat rewrite <- Q2R_minus in valid_sub_lo.
        rewrite <- Q2R_min4 in valid_sub_lo.
        unfold absIvUpd; auto.
      * eapply Rle_trans.
        Focus 2.
        apply valid_hi.
        unfold ivlo, addIntv.
        simpl in valid_sub_hi.
        repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi.
        repeat rewrite <- Q2R_minus in valid_sub_hi.
        rewrite <- Q2R_max4 in valid_sub_hi.
        unfold absIvUpd; auto.
    + pose proof (interval_multiplication_valid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_mul.
Heiko Becker's avatar
Heiko Becker committed
379
      specialize (valid_mul v1 v2 IHf1 IHf2).
Heiko Becker's avatar
Heiko Becker committed
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401
      unfold contained in valid_mul.
      unfold isSupersetIntv in valid_bin.
      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
      destruct valid_mul as [valid_mul_lo valid_mul_hi].
      split.
      * eapply Rle_trans. apply valid_lo.
        unfold ivlo. unfold multIntv.
        simpl in valid_mul_lo.
        repeat rewrite <- Q2R_mult in valid_mul_lo.
        rewrite <- Q2R_min4 in valid_mul_lo.
        unfold absIvUpd; auto.
      * eapply Rle_trans.
        Focus 2.
        apply valid_hi.
        unfold ivlo, addIntv.
        simpl in valid_mul_hi.
        repeat rewrite <- Q2R_mult in valid_mul_hi.
        rewrite <- Q2R_max4 in valid_mul_hi.
        unfold absIvUpd; auto.
402 403 404
    + pose proof (divisionIsValid v1 v2 (Q2R (fst iv1), Q2R (snd iv1)) (Q2R (fst iv2),Q2R (snd iv2))) as valid_div.
      unfold contained in valid_div.
      unfold isSupersetIntv in valid_bin.
405
      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_bin nodiv0].
406 407 408 409
      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452
      apply orb_prop_elim in nodiv0.
      assert (snd iv2 < 0 \/ 0 < fst iv2).
      * destruct nodiv0 as [lt_0 | lt_0];
          apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0];
            apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0;
              apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0;
                rewrite Qle_bool_iff in le_0;
                rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0];
                  [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto.
      * destruct valid_div as [valid_div_lo valid_div_hi]; simpl; try auto.
        { rewrite <- Q2R0_is_0.
          destruct H; [left | right]; apply Qlt_Rlt; auto. }
        { unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi.
          simpl in *.
          assert (Q2R (fst iv2) <= (Q2R (snd iv2)))%R by lra.
          assert (~ snd iv2 == 0).
          - destruct H; try lra.
            hnf; intros ivhi2_0.
            apply Rle_Qle in H0.
            rewrite ivhi2_0 in H0.
            lra.
          - assert (~ fst iv2 == 0).
            + destruct H; try lra.
              hnf; intros ivlo2_0.
              apply Rle_Qle in H0.
              rewrite ivlo2_0 in H0.
              lra.
              + split.
                * eapply Rle_trans. apply valid_lo.
                  unfold ivlo. unfold multIntv.
                  simpl in valid_div_lo.
                  rewrite <- Q2R_inv in valid_div_lo; [ | auto].
                  rewrite <- Q2R_inv in valid_div_lo; [ | auto].
                  repeat rewrite <- Q2R_mult in valid_div_lo.
                  rewrite <- Q2R_min4 in valid_div_lo; auto.
                * eapply Rle_trans.
                  Focus 2.
                  apply valid_hi.
                  simpl in valid_div_hi.
                  rewrite <- Q2R_inv in valid_div_hi; [ | auto].
                  rewrite <- Q2R_inv in valid_div_hi; [ | auto].
                  repeat rewrite <- Q2R_mult in valid_div_hi.
                  rewrite <- Q2R_max4 in valid_div_hi; auto. }
453
Qed.