RealRangeArith.v 12.3 KB
Newer Older
1
From Coq
2
     Require Import QArith.QArith QArith.Qreals QArith.Qminmax micromega.Psatz Recdef.
3 4 5

From Flover
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Heiko Becker's avatar
Heiko Becker committed
6 7
     Infra.Ltacs Infra.RealSimps TypeValidator ssaPrgs IntervalArithQ
     IntervalArith Commands.
8 9 10 11 12 13 14 15 16 17 18 19 20 21

Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
  forall v, NatSet.In v dVars ->
       exists vR iv err,
         E v =  Some vR /\
         FloverMap.find (Var Q v) A = Some (iv, err) /\
         (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.

Ltac kill_trivial_exists :=
  match goal with
  | [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
  | [ |- exists iv err, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
  end.

22
Fixpoint validRanges e (A:analysisResult) E Gamma :Prop :=
23 24 25
  match e with
  | Var _ x => True
  | Const m v => True
26
  | Unop u e1 => validRanges e1 A E Gamma
27 28 29 30 31 32
  | Binop b e1 e2 =>
    (b = Div ->
     (forall iv2 err,
         FloverMap.find e2 A = Some (iv2, err) ->
         ((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
         ((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))) = true)) /\
33
    validRanges e1 A E Gamma /\ validRanges e2 A E Gamma
34
  | Fma e1 e2 e3 =>
35 36 37
    validRanges e1 A E Gamma /\ validRanges e2 A E Gamma /\
    validRanges e3 A E Gamma
  | Downcast m e1 => validRanges e1 A E Gamma
38 39 40
  end /\
  exists iv err vR,
    FloverMap.find e A = Some (iv, err) /\
41
    eval_expr E Gamma (toREval (toRExp e)) vR REAL /\
42 43
    (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.

44 45
Corollary validRanges_single e A E Gamma:
  validRanges e A E Gamma ->
46 47
  exists iv err vR,
    FloverMap.find e A = Some (iv, err) /\
48
    eval_expr E Gamma (toREval (toRExp e)) vR REAL /\
49 50 51 52 53
    (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
  destruct e; intros [_ valid_e]; simpl in *; try auto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
54 55
Lemma validRanges_swap Gamma1 Gamma2:
  forall e A E,
56
    (forall n, Gamma1 n =  Gamma2 n) ->
Heiko Becker's avatar
Heiko Becker committed
57 58 59 60 61 62 63
    validRanges e A E Gamma1 ->
    validRanges e A E Gamma2.
Proof.
  induction e; intros * Gamma_swap valid1; simpl in *; try (split; auto);
    try (
        destruct valid1 as [_ [? [? [? [? [? ?]]]]]];
        repeat eexists; eauto;
64
        [eapply swap_Gamma_eval_expr with (Gamma1 := Gamma1); eauto |
Heiko Becker's avatar
Heiko Becker committed
65 66 67 68 69 70 71
         lra |
         lra]).
  - destruct valid1; auto.
  - destruct valid1 as [[? [? ?]] ?]; auto.
  - destruct valid1 as [[? [? ?]] ?]; auto.
  - destruct valid1; auto.
Qed.
72

73
Fixpoint validRangesCmd (f:cmd Q) A E Gamma {struct f} : Prop :=
74 75
  match f with
  | Let m x e g =>
76
    validRanges e A E Gamma /\
77 78
    (forall vR, eval_expr E Gamma (toREval (toRExp e)) vR REAL ->
             validRangesCmd g A (updEnv x vR E) Gamma)
79
  | Ret e => validRanges e A E Gamma
80 81 82
  end /\
  exists iv_e err_e vR,
    FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
83
    bstep (toREvalCmd (toRCmd f)) E Gamma vR REAL /\
84 85
    (Q2R (fst iv_e) <=  vR <= Q2R (snd iv_e))%R.

86 87
Corollary validRangesCmd_single f A E Gamma:
  validRangesCmd f A E Gamma ->
88 89
  exists iv_e err_e vR,
    FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
90
    bstep (toREvalCmd (toRCmd f)) E Gamma vR REAL /\
91 92 93 94
    (Q2R (fst iv_e) <=  vR <= Q2R (snd iv_e))%R.
Proof.
  destruct f; simpl in *; intros [ _ valid_f]; auto.
Qed.
95 96

Lemma validRangesCmd_swap:
Heiko Becker's avatar
Heiko Becker committed
97
  forall f A E Gamma1 Gamma2,
98
    (forall n, Gamma1 n =  Gamma2 n) ->
Heiko Becker's avatar
Heiko Becker committed
99 100
    validRangesCmd f A E Gamma1 ->
    validRangesCmd f A E Gamma2.
101 102 103 104 105
Proof.
  induction f; intros * Gamma_swap valid1; simpl in *; try (split; auto);
    try (
        destruct valid1 as [_ [? [? [? [? [? ?]]]]]];
        repeat eexists; eauto;
106
        [eapply swap_Gamma_bstep with (Gamma1 := Gamma1); eauto |
107 108 109 110
         lra |
         lra]).
  - destruct valid1 as [[? valid_all_exec] ?]; split.
    + eapply validRanges_swap; eauto.
111 112
    + intros. eapply IHf; [ auto | eapply valid_all_exec].
      eapply swap_Gamma_eval_expr with (Gamma1 := Gamma2); eauto.
113 114
  - destruct valid1.
    eapply validRanges_swap; eauto.
115 116
Qed.

117
Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma:
118
  Q_orderedExps.eq e1 e2 ->
119 120
  validRanges e1 A E Gamma ->
  validRanges e2 A E Gamma.
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 232 233 234 235 236 237 238 239 240 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
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.
    + apply N.compare_eq in Heq; subst.
      rewrite N.eqb_refl in H; congruence.
  - 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.
    + apply N.compare_eq in Heq; subst.
      rewrite N.eqb_refl in *; congruence.
Qed.

281
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma vR' m n c fVars dVars outVars:
282 283 284
  ssa (Let m n e' c) (fVars  dVars) outVars ->
  NatSet.Subset (usedVars e) (fVars  dVars) ->
  ~ (n  fVars  dVars) ->
285
  validRanges e A E Gamma ->
286
  validRanges e A (updEnv n vR' E) Gamma.
287
  (*(updDefVars (Var R n) REAL Gamma). *)
288 289 290 291 292 293
Proof.
  intros Hssa Hsub Hnotin Hranges.
  induction e.
  - split; auto.
    destruct Hranges as [_ [iv [err [vR Hranges]]]].
    exists iv, err, vR; intuition.
294 295 296 297
    eapply eval_expr_ssa_extension; eassumption.
    (*eapply swap_Gamma_eval_expr.
    + intros *. symmetry. eapply Rmap_updVars_comm.
    eapply eval_expr_ssa_extension; try eassumption. *)
298 299 300
  - split; auto.
    destruct Hranges as [_ [iv [err [vR Hranges]]]].
    exists iv, err, vR; intuition.
301 302
    eapply eval_expr_ssa_extension; eassumption.
    (* eapply swap_Gamma_eval_expr.
303
    eapply Rmap_updVars_comm.
304
    eapply eval_expr_ssa_extension; try eassumption. *)
305 306 307 308 309 310
  - simpl in Hsub.
    destruct Hranges as [Hunopranges Hranges].
    specialize (IHe Hsub Hunopranges).
    split; auto.
    destruct Hranges as [iv [err [vR Hranges]]].
    exists iv, err, vR; intuition.
311 312
    eapply eval_expr_ssa_extension; eauto.
    (* eapply swap_Gamma_eval_expr.
313
    eapply Rmap_updVars_comm.
314
    eapply eval_expr_ssa_extension; try eassumption. *)
315 316 317 318 319 320 321 322 323 324 325
    rewrite usedVars_toREval_toRExp_compat; auto.
  - simpl in Hsub.
    assert (NatSet.Subset (usedVars e1) (fVars  dVars)) as Hsub1 by set_tac.
    assert (NatSet.Subset (usedVars e2) (fVars  dVars)) as Hsub2 by (clear Hsub1; set_tac).
    destruct Hranges as [[Hdiv [Hranges1 Hranges2]] Hranges].
    specialize (IHe1 Hsub1 Hranges1).
    specialize (IHe2 Hsub2 Hranges2).
    simpl.
    repeat split; auto.
    destruct Hranges as [iv [err [vR Hranges]]].
    exists iv, err, vR; intuition.
326 327
    eapply eval_expr_ssa_extension; eauto.
    (* eapply swap_Gamma_eval_expr.
328
    eapply Rmap_updVars_comm.
329
    eapply eval_expr_ssa_extension; try eassumption. *)
330 331 332 333 334 335 336 337 338 339 340 341 342 343
    simpl.
    repeat rewrite usedVars_toREval_toRExp_compat; auto.
  - simpl in Hsub.
    assert (NatSet.Subset (usedVars e1) (fVars  dVars)) as Hsub1 by set_tac.
    assert (NatSet.Subset (usedVars e2) (fVars  dVars)) as Hsub2 by (clear Hsub1; set_tac).
    assert (NatSet.Subset (usedVars e3) (fVars  dVars)) as Hsub3 by (clear Hsub1 Hsub2; set_tac).
    destruct Hranges as [[Hranges1 [Hranges2 Hranges3]] Hranges].
    specialize (IHe1 Hsub1 Hranges1).
    specialize (IHe2 Hsub2 Hranges2).
    specialize (IHe3 Hsub3 Hranges3).
    simpl.
    repeat split; auto.
    destruct Hranges as [iv [err [vR Hranges]]].
    exists iv, err, vR; intuition.
344 345
    eapply eval_expr_ssa_extension; eauto.
    (* eapply swap_Gamma_eval_expr.
346
    eapply Rmap_updVars_comm.
347
    eapply eval_expr_ssa_extension; try eassumption. *)
348 349 350 351 352 353 354 355
    simpl.
    repeat rewrite usedVars_toREval_toRExp_compat; auto.
  - simpl in Hsub.
    destruct Hranges as [Hranges' Hranges].
    specialize (IHe Hsub Hranges').
    split; auto.
    destruct Hranges as [iv [err [vR Hranges]]].
    exists iv, err, vR; intuition.
356 357
    eapply eval_expr_ssa_extension; eauto.
    (* eapply swap_Gamma_eval_expr.
358
    eapply Rmap_updVars_comm.
359
    eapply eval_expr_ssa_extension; try eassumption. *)
360
    rewrite usedVars_toREval_toRExp_compat; auto.
Heiko Becker's avatar
Heiko Becker committed
361
Qed.