IntervalValidation.v 20 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
(**
Heiko Becker's avatar
Heiko Becker committed
2 3
    Interval arithmetic checker and its soundness proof.
    The function validIntervalbounds checks wether the given analysis result is
4
    a valid range arithmetic for each sub term of the given exprression e.
Heiko Becker's avatar
Heiko Becker committed
5 6
    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 9 10
From Coq
     Require Import QArith.QArith QArith.Qreals QArith.Qminmax Lists.List
     micromega.Psatz.
11

12 13 14 15 16 17 18 19 20
From Flover
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
     Infra.Ltacs Infra.RealSimps TypeValidator.

From Flover
     Require Export IntervalArithQ IntervalArith ssaPrgs RealRangeArith.

Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P:precond)
         (validVars:NatSet.t) :bool:=
21
  match FloverMap.find e A with
Heiko Becker's avatar
Heiko Becker committed
22 23 24 25 26 27 28 29 30 31 32
  | None => false
  | Some (intv, _) =>
       match e with
       | Var _ v =>
         if NatSet.mem v validVars
         then true
         else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
       | Const _ n => isSupersetIntv (n,n) intv
       | Unop o f =>
         if validIntervalbounds f A P validVars
         then
33
           match FloverMap.find f A with
Heiko Becker's avatar
Heiko Becker committed
34 35 36 37 38
           | None => false
           | Some (iv, _) =>
          match o with
          | Neg =>
            let new_iv := negateIntv iv in
39
            isSupersetIntv new_iv intv
Heiko Becker's avatar
Heiko Becker committed
40 41 42 43 44 45 46 47
          | Inv =>
            if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
                ((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))))
            then
              let new_iv := invertIntv iv in
              isSupersetIntv new_iv intv
            else false
          end
Heiko Becker's avatar
Heiko Becker committed
48
        end
49
      else false
Heiko Becker's avatar
Heiko Becker committed
50
    | Binop op f1 f2 =>
Heiko Becker's avatar
Heiko Becker committed
51 52
      if ((validIntervalbounds f1 A P validVars) &&
          (validIntervalbounds f2 A P validVars))
53
      then
54
        match FloverMap.find f1 A, FloverMap.find f2 A with
Heiko Becker's avatar
Heiko Becker committed
55
        | Some (iv1, _), Some (iv2, _) =>
Heiko Becker's avatar
Heiko Becker committed
56
          match op with
57 58 59 60 61 62 63 64 65
          | 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
66
          | Div =>
67 68 69 70 71 72
            if (((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
                ((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))))
            then
              let new_iv := divideIntv iv1 iv2 in
              isSupersetIntv new_iv intv
            else false
73
          end
Heiko Becker's avatar
Heiko Becker committed
74 75
        | _, _ => false
        end
76
      else false
77
    | Fma f1 f2 f3 =>
78 79 80
      if ((validIntervalbounds f1 A P validVars) &&
          (validIntervalbounds f2 A P validVars) &&
          (validIntervalbounds f3 A P validVars))
81
      then
82
        match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
83 84 85 86 87
        | Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
          let new_iv := addIntv iv1 (multIntv iv2 iv3) in
          isSupersetIntv new_iv intv
        | _, _, _ => false
        end
88
      else false
89
    | Downcast _ f1 =>
Heiko Becker's avatar
Heiko Becker committed
90
      if (validIntervalbounds f1 A P validVars)
91
      then
92
        match FloverMap.find f1 A with
Heiko Becker's avatar
Heiko Becker committed
93 94
        | None => false
        | Some (iv1, _) =>
95
        (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv)
Heiko Becker's avatar
Heiko Becker committed
96
        end
97 98
      else
        false
Heiko Becker's avatar
Heiko Becker committed
99 100
       end
  end.
101

102 103
Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond)
         (validVars:NatSet.t) :bool:=
104
  match f with
105
  | Let m x e g =>
106
    match FloverMap.find e A, FloverMap.find (Var Q x) A with
Heiko Becker's avatar
Heiko Becker committed
107 108 109 110 111 112 113 114
    | Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) =>
      if (validIntervalbounds e A P validVars &&
                              Qeq_bool (e_lo) (x_lo) &&
                              Qeq_bool (e_hi) (x_hi))
      then validIntervalboundsCmd g A P (NatSet.add x validVars)
      else false
    | _, _ => false
    end
115
  |Ret e =>
Heiko Becker's avatar
Heiko Becker committed
116
   validIntervalbounds e A P validVars
117 118
  end.

Heiko Becker's avatar
Heiko Becker committed
119 120 121 122 123 124 125 126 127 128 129 130
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.

Heiko Becker's avatar
Heiko Becker committed
131
Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
132
  FloverMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) ->
Heiko Becker's avatar
Heiko Becker committed
133
  validIntervalbounds (Binop Div e1 e2) A P V = true ->
134 135
  (ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
136
  intros A_eq validBounds; cbn in *.
137
  Flover_compute; try congruence.
138
  apply le_neq_bool_to_lt_prop; auto.
139
Qed.
140

141
Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P:precond)
142
        fVars dVars (E:env) Gamma:
143 144 145 146
  validIntervalbounds f A P dVars = true ->
  dVars_range_valid dVars E A ->
  NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
  fVars_P_sound fVars E P ->
147
  validTypes f Gamma DeltaMapR ->
148
  validRanges f A E (toRTMap (toRExpMap Gamma)).
149
Proof.
150 151
  induction f;
    intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
152
    cbn in *.
153
  - Flover_compute.
154
    split; try auto.
155 156
    destruct (NatSet.mem n dVars) eqn:?; simpl in *.
    + destruct (valid_definedVars n)
157
        as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
158 159 160
        try set_tac.
      rewrite map_n in *.
      inversion Heqo; subst.
161 162
      kill_trivial_exists.
      eexists; split; [auto| split; try eauto ].
163
      eapply Var_load; simpl; try auto.
164 165
      destruct (types_defined) as [m [find_m _]].
      eapply toRExpMap_some in  find_m; simpl; eauto.
166
      match_simpl; auto.
167 168
    + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]];
        set_tac; try auto.
169
      assert (NatSet.In n fVars) by set_tac.
170 171
      andb_to_prop valid_bounds.
      canonize_hyps; simpl in *.
172 173
      kill_trivial_exists.
      eexists; split; [auto | split].
174
      * econstructor; try eauto.
175 176
        destruct (types_defined) as [m [find_m _]].
        eapply toRExpMap_some in find_m; simpl; eauto.
177
        match_simpl; auto.
178
      * lra.
179 180
  - split; [auto |].
    Flover_compute; canonize_hyps; simpl in *.
181
    kill_trivial_exists.
182
    exists (perturb (Q2R v) REAL 0).
183
    split; [eauto| split].
184 185
    + econstructor; try eauto.
      cbn. rewrite Rabs_R0; lra.
186
    + unfold perturb; simpl; lra.
187
  - Flover_compute; simpl in *; try congruence.
188 189 190
    assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_e.
    { apply IHf; try auto.
      destruct types_defined as [? [? [[? ?] ?]]]; auto. }
191 192 193 194
    split; try auto.
    apply validRanges_single in valid_e.
    destruct valid_e as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]].
    rewrite Heqo0 in iveq_f; inversion iveq_f; subst.
195 196 197 198
    inversion iveq_f; subst.
    destruct u; try andb_to_prop R; simpl in *.
    + kill_trivial_exists.
      exists (evalUnop Neg vF); split;
199
        [auto | split ; [econstructor; eauto | ]].
200 201 202 203
      * cbn; auto.
      *  canonize_hyps.
         rewrite Q2R_opp in *.
         simpl; lra.
204
    + rename L0 into nodiv0.
205
      apply le_neq_bool_to_lt_prop in nodiv0.
206
      kill_trivial_exists.
207
      exists (perturb (evalUnop Inv vF) REAL 0); split;
208
        [destruct i; auto | split].
209
      * econstructor; eauto.
210
        { auto. }
211
        { simpl. rewrite Rabs_R0; lra. }
212
        (* Absence of division by zero *)
213 214
        { hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
               rewrite Q2R0_is_0 in nodiv0; lra. }
215
      * canonize_hyps.
216 217 218
        pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f)))
                                             (a :=vF))
          as inv_valid.
219 220 221 222
         unfold invertInterval in inv_valid; simpl in *.
         destruct inv_valid; try auto.
         { destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
         { split; eapply Rle_trans.
223
           - apply L1.
224 225 226 227 228 229 230 231 232 233 234
           - rewrite Q2R_inv; try auto.
             destruct nodiv0; try lra.
             hnf; intros.
             assert (0 < Q2R (snd iv_f))%R.
             { eapply Rlt_le_trans.
               apply Qlt_Rlt in H1.
               rewrite <- Q2R0_is_0.
               apply H1. lra.
             }
             rewrite <- Q2R0_is_0 in H3.
             apply Rlt_Qlt in H3.
235
             lra.
236 237 238 239 240
           - apply H0.
           - rewrite <- Q2R_inv; try auto.
             hnf; intros.
             destruct nodiv0; try lra.
             assert (Q2R (fst iv_f) < 0)%R.
241 242 243 244
             { rewrite <- Q2R0_is_0.
               apply Qlt_Rlt in H2.
               eapply Rle_lt_trans; try eauto.
               lra. }
245 246
             rewrite <- Q2R0_is_0 in H3.
             apply Rlt_Qlt in H3. lra. }
247 248 249
  - destruct types_defined
      as [? [? [[? [? ?]]?]]].
    assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
250
        by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
251
    assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
252 253 254 255 256 257 258 259 260
        by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
    repeat split;
      [ intros; subst; Flover_compute; congruence |
                       auto | auto |].
    apply validRanges_single in valid_f1;
      apply validRanges_single in valid_f2.
    destruct valid_f1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]].
    destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
    Flover_compute; try congruence.
261
    kill_trivial_exists.
262
    exists (perturb (evalBinop b vF1 vF2) REAL 0);
263 264
      split; [destruct i; auto | ].
    inversion env1; inversion env2; subst.
265 266
      destruct b; simpl in *.
    * split;
267 268
        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
         try rewrite Rabs_R0; cbn; try auto; try lra|].
269 270 271
      pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                          (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_add.
272 273 274
      specialize (valid_add vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
275
      canonize_hyps; simpl in *.
276 277
      repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
278
      unfold perturb. lra.
279
    * split;
280 281
        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
         try rewrite Rabs_R0; cbn; try auto; lra|].
282 283
      pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                             (Q2R (fst iv_f2), Q2R (snd iv_f2)))
284
        as valid_sub.
285 286 287
      specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
288
      canonize_hyps; simpl in *.
289 290 291
      repeat rewrite <- Q2R_opp in *;
        repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
292
      unfold perturb; lra.
293
    * split;
294 295
        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
         try rewrite Rabs_R0; cbn; try auto; lra|].
296 297
      pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                                (Q2R (fst iv_f2), Q2R (snd iv_f2)))
298
        as valid_mul.
299 300 301
      specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
302
      canonize_hyps; simpl in *.
303 304
      repeat rewrite <- Q2R_mult in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
305
      unfold perturb; lra.
306 307 308 309
    * andb_to_prop R.
      canonize_hyps.
      apply le_neq_bool_to_lt_prop in L.
      split;
310 311
        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
         try rewrite Rabs_R0; cbn; try auto; try lra|].
312 313 314
      (* No division by zero proof *)
      { hnf; intros.
        destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. }
315
      { pose proof (interval_division_valid (a:=vF1) (b:=vF2)
316 317
                                            ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                            (Q2R (fst iv_f2), Q2R (snd iv_f2)))
318
        as valid_div.
319 320 321
        simpl in *.
        destruct valid_div; try auto.
        - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
322
        - assert (~ (snd iv_f2) == 0).
323
          { hnf; intros. destruct L; try lra.
324
            assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H9; lra).
325
            lra. }
326
          assert (~ (fst iv_f2) == 0).
327
          { hnf; intros; destruct L; try lra.
328
            assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H10; lra).
329 330 331 332 333 334 335
            lra. }
          repeat (rewrite <- Q2R_inv in *; try auto).
          repeat rewrite <- Q2R_mult in *.
          rewrite <- Q2R_min4, <- Q2R_max4 in *.
          unfold perturb.
          lra.
      }
336 337 338
  - destruct types_defined
      as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
        assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
339
        by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
340
    assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
341
        by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
342
    assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3
343 344 345 346 347 348 349 350 351
        by (Flover_compute; try congruence; apply IHf3; try auto; set_tac).
    repeat split; try auto.
    apply validRanges_single in valid_f1;
      apply validRanges_single in valid_f2;
      apply validRanges_single in valid_f3.
    destruct valid_f1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]].
    destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
    destruct valid_f3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]].
    Flover_compute; try congruence.
352
    kill_trivial_exists.
353
    exists (perturb (evalFma vF1 vF2 vF3) REAL 0); split; try auto.
354 355
    inversion env1; inversion env2; inversion env3; subst.
    split; [auto | ].
356 357
    * eapply Fma_dist' with (delta := 0%R); eauto; try congruence; cbn;
        try rewrite Rabs_R0; try auto; lra.
358 359
    * pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
      specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
360
      remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
361
      pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
362
      rewrite Heqiv_f23prod in valid_add, valid_mul.
363 364 365 366 367 368 369 370
      unfold multIntv in valid_add.
      canonize_hyps.
      simpl in *.
      repeat rewrite <- Q2R_mult in *;
        repeat rewrite <- Q2R_min4, <- Q2R_max4 in *;
        repeat rewrite <- Q2R_plus in *;
        repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
      specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
371
      unfold evalFma, evalBinop, perturb.
372
      lra.
373 374 375
  - destruct types_defined
      as [mG [find_mG [[validt_f _] _]]].
        assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_f1
376 377 378 379 380
        by (Flover_compute; try congruence; apply IHf; auto).
    split; try auto.
    apply validRanges_single in valid_f1.
    destruct valid_f1 as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]].
    Flover_compute.
381
    inversion env_f; subst.
382
    kill_trivial_exists.
383
    exists (perturb vF REAL 0).
384
    split; [destruct i; try auto |].
385 386
    split; [eapply Downcast_dist'; try eauto; cbn; try rewrite Rabs_R0 |];
      try lra; try auto.
387 388 389
    canonize_hyps.
    unfold perturb.
    simpl in *; lra.
390 391
Qed.

392
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
393
  forall Gamma E fVars dVars outVars P,
='s avatar
= committed
394
    ssa f (NatSet.union fVars dVars) outVars ->
395 396
    dVars_range_valid dVars E A ->
    fVars_P_sound fVars E P ->
='s avatar
= committed
397
    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
Heiko Becker's avatar
Heiko Becker committed
398
    validIntervalboundsCmd f A P dVars = true ->
399
    validTypesCmd f Gamma DeltaMapR ->
400
    validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
='s avatar
= committed
401 402
Proof.
  induction f;
403 404
    intros *  ssa_f dVars_sound fVars_valid usedVars_subset
                    valid_bounds_f valid_types_f;
405
    cbn in *.
406
  - Flover_compute.
='s avatar
= committed
407
    inversion ssa_f; subst.
408
    canonize_hyps.
409 410 411 412
    pose proof (validIntervalbounds_sound e Gamma (E:=E) (fVars:=fVars) L) as validIV_e.
    destruct valid_types_f
             as [[mG [find_mG [_ [_ [validt_e validt_f]]]]] _].
    assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e.
413 414
    { apply validIV_e; try auto.
      set_tac. repeat split; auto.
415 416 417
      hnf; intros; subst.
      set_tac. }
    assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
418 419
    { hnf. intros a; split; intros in_set; set_tac.
      - destruct in_set as [ ? | [? ?]]; try auto; set_tac.
420
        destruct H0; auto.
421 422
      - destruct in_set as [? | ?]; try auto; set_tac.
        destruct H as [? | [? ?]]; auto. }
423
    pose proof (validRanges_single _ _ _ _ valid_e) as valid_single_e.
424 425
    destruct valid_single_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]].
    rewrite find_v in *; inversion Heqo; subst.
426 427
    specialize (IHf Gamma (updEnv n v E) fVars (NatSet.add n dVars)) as IHf_spec.
    assert (validRangesCmd f A (updEnv n v E) (toRTMap (toRExpMap Gamma))).
428 429 430
    { eapply IHf_spec; eauto.
      - eapply ssa_equal_set. symmetry in H. apply H. apply H7.
      - intros v0 mem_v0.
431 432
        unfold updEnv.
        case_eq (v0 =? n); intros v0_eq.
433
        + rename R1 into eq_lo;
434 435
            rename R0 into eq_hi.
          rewrite Nat.eqb_eq in v0_eq; subst.
436 437
          exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra.
        + apply dVars_sound.
438 439
          set_tac.
          destruct mem_v0 as [? | [? ?]]; try auto.
440
          rewrite Nat.eqb_neq in v0_eq.
441 442
          congruence.
      - intros v0 mem_fVars.
443 444 445
        unfold updEnv.
        case_eq (v0 =? n); intros case_v0; auto.
        rewrite Nat.eqb_eq in case_v0; subst.
446 447
        assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac.
        exfalso; set_tac. apply H6; set_tac; auto.
448
      - intros x x_contained.
449
        set_tac.
450 451 452 453
        repeat split; try auto.
        + hnf; intros; subst. apply H1; set_tac.
        + hnf; intros. apply H1; set_tac. }
    (*
454
        destruct x_contained as [x_free | x_def].
455
        + destruct (types_valid x) as [m_x Gamma_x]; try set_tac.
456 457 458 459
          exists m_x.
          unfold updDefVars. case_eq (x =? n); intros eq_case; try auto.
          rewrite Nat.eqb_eq in eq_case.
          subst.
460 461
          exfalso; apply H6; set_tac.
        + set_tac.
462
          destruct x_def as [x_n | x_def]; subst.
463 464 465 466
          *  exists REAL; unfold updDefVars; rewrite Nat.eqb_refl; auto.
          * destruct x_def. destruct (types_valid x) as [m_x Gamma_x].
            { rewrite NatSet.union_spec; auto. }
            { exists m_x.
467 468 469
              unfold updDefVars; case_eq (x =? n); intros eq_case; try auto.
              rewrite Nat.eqb_eq in eq_case; subst.
              congruence. }
470
    { clear L R1 R0 R IHf.
471 472 473
        hnf. intros a a_freeVar.
        rewrite NatSet.diff_spec in a_freeVar.
        destruct a_freeVar as [a_freeVar a_no_dVar].
='s avatar
= committed
474
        apply usedVars_subset.
475
        simpl.
='s avatar
= committed
476 477
        rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
        repeat split; try auto.
478
        + hnf; intros; subst.
479
          apply a_no_dVar.
480 481
          rewrite NatSet.add_spec; auto.
        + hnf; intros a_dVar.
482
          apply a_no_dVar.
483 484 485 486 487 488
          rewrite NatSet.add_spec; auto. } *)
    { repeat split; try auto.
      - intros vR ?.
        assert (vR = v) by (eapply meps_0_deterministic; eauto); subst.
        auto.
      - apply validRangesCmd_single in H0.
489 490
        destruct H0 as [? [? [? [? [? ?]]]]].
        repeat eexists; eauto.
491 492 493
        econstructor; try eauto.
        + lra.
        + lra. }
='s avatar
= committed
494
  - unfold validIntervalboundsCmd in valid_bounds_f.
495 496 497
    pose proof (validIntervalbounds_sound e (E:=E) Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
    destruct valid_types_f as [? ?].
    assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e by (apply valid_iv_e; auto).
498 499 500
    split; try auto.
    apply validRanges_single in valid_e.
    destruct valid_e as [?[?[? [? [? ?]]]]]; try auto.
501
    simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
502
Qed.