ssaPrgs.v 21.7 KB
Newer Older
1 2 3 4 5 6 7
(**
  We define a pseudo SSA predicate.
  The formalization is similar to the renamedApart property in the LVC framework by Schneider, Smolka and Hack
  http://dblp.org/rec/conf/itp/SchneiderSH15
  Our predicate is not as fully fledged as theirs, but we especially borrow the idea of annotating
  the program with the predicate with the set of free and defined variables
**)
8 9
Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals.
Require Import Coq.micromega.Psatz.
10 11
Require Import Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
Require Export Flover.Commands.
12

13
Lemma validVars_add V (e:expr V) Vs n:
14 15
  NatSet.Subset (usedVars e) Vs ->
  NatSet.Subset (usedVars e) (NatSet.add n Vs).
Heiko Becker's avatar
Heiko Becker committed
16
Proof.
17 18 19 20
  induction e; try auto.
  - intros valid_subset.
    hnf. intros a in_singleton.
    specialize (valid_subset a in_singleton).
Heiko Becker's avatar
Heiko Becker committed
21 22 23
    rewrite NatSet.add_spec; right; auto.
  - intros vars_binop.
    simpl in *.
24 25 26 27 28 29 30 31 32 33 34 35 36 37
    intros a in_empty.
    inversion in_empty.
  - simpl; intros in_vars.
    intros a in_union.
    rewrite NatSet.union_spec in in_union.
    destruct in_union.
    + apply IHe1; try auto.
      hnf; intros.
      apply in_vars.
      rewrite NatSet.union_spec; auto.
    + apply IHe2; try auto.
      hnf; intros.
      apply in_vars.
      rewrite NatSet.union_spec; auto.
38 39 40 41
  - intros vars_fma.
    simpl in *.
    intros a used_vars.
    firstorder.
42 43
Qed.

44
(*
45
Lemma validVars_non_stuck (e:expr Q) inVars E:
46 47
 NatSet.Subset (usedVars e) inVars ->
  (forall v, NatSet.In v (usedVars e) ->
48 49
        exists r, (toREvalEnv E) v = Some (r, REAL))%R ->
  exists vR, eval_expr (toREvalEnv E) (toREval (toRExp e)) vR REAL.
50
Proof.
51
    revert inVars E; induction e;
52 53 54 55 56
    intros inVars E vars_valid fVars_live.
  - simpl in *.
    assert (NatSet.In n (NatSet.singleton n)) as in_n by (rewrite NatSet.singleton_spec; auto).
    specialize (fVars_live n in_n).
    destruct fVars_live as [vR E_def].
57
    exists vR; econstructor; eauto.
58
  - exists (perturb (Q2R v) 0); constructor.
59 60
    simpl (meps REAL); rewrite Rabs_R0; rewrite Q2R0_is_0; lra.
  - assert (exists vR, eval_expr (toREvalEnv E) (toREval (toRExp e)) vR REAL)
61 62 63 64 65
      as eval_e_def by (eapply IHe; eauto).
    destruct eval_e_def as [ve eval_e_def].
    case_eq u; intros; subst.
    + exists (evalUnop Neg ve); constructor; auto.
    + exists (perturb (evalUnop Inv ve) 0); constructor; auto.
66
      simpl (meps REAL); rewrite Q2R0_is_0; rewrite Rabs_R0; lra.
67
  - repeat rewrite NatSet.subset_spec in *; simpl in *.
68
    assert (exists vR1, eval_expr (toREvalEnv E) (toREval (toRExp e1)) vR1 REAL) as eval_e1_def.
69
    + eapply IHe1; eauto.
70 71 72 73
      * hnf; intros.
        apply vars_valid.
        rewrite NatSet.union_spec; auto.
      * intros.
74
        destruct (fVars_live v) as [vR E_def]; try eauto.
75
        apply NatSet.union_spec; auto.
76
    + assert (exists vR2, eval_expr (toREvalEnv E) (toREval (toRExp e2)) vR2 REAL) as eval_e2_def.
77 78 79 80 81 82 83
      * eapply IHe2; eauto.
        { hnf; intros.
        apply vars_valid.
        rewrite NatSet.union_spec; auto. }
        { intros.
          destruct (fVars_live v) as [vR E_def]; try eauto.
          apply NatSet.union_spec; auto. }
84 85
      * destruct eval_e1_def as [vR1 eval_e1_def];
          destruct eval_e2_def as [vR2 eval_e2_def].
86
        exists (perturb (evalBinop b vR1 vR2) 0).
87
        replace REAL with (computeJoin REAL REAL) by auto.
88 89
        constructor; auto.
        simpl meps; rewrite Q2R0_is_0. rewrite Rabs_R0; lra.
90
  - assert (exists vR, eval_expr (toREvalEnv E) (toREval (toRExp e))  vR REAL) as eval_r_def by (eapply IHe; eauto).
91
    destruct eval_r_def as [vr eval_r_def].
92
    exists vr.
93 94
    simpl toREval.
    auto.
95
Qed. *)
96 97


Heiko Becker's avatar
Heiko Becker committed
98
Inductive ssa (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
99
 ssaLet m x e s inVars Vterm:
100
   NatSet.Subset (usedVars e) inVars->
101
   NatSet.mem x inVars = false ->
Heiko Becker's avatar
Heiko Becker committed
102
   ssa s (NatSet.add x inVars) Vterm ->
103
   ssa (Let m x e s) inVars Vterm
104
|ssaRet e inVars Vterm:
105 106
   NatSet.Subset (usedVars e) inVars ->
   NatSet.Equal inVars Vterm ->
Heiko Becker's avatar
Heiko Becker committed
107
   ssa (Ret e) inVars Vterm.
108 109 110


Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
Heiko Becker's avatar
Heiko Becker committed
111
  ssa f inVars outVars ->
112
  NatSet.Subset (freeVars f) inVars.
113 114
Proof.
  intros ssa_f; induction ssa_f.
115
  - simpl in *. hnf; intros a in_fVars.
116 117 118 119 120 121 122 123 124 125 126 127
    rewrite NatSet.remove_spec, NatSet.union_spec in in_fVars.
    destruct in_fVars as [in_union not_eq].
    destruct in_union; try auto.
    specialize (IHssa_f a H1).
    rewrite NatSet.add_spec in IHssa_f.
    destruct IHssa_f; subst; try auto.
    exfalso; apply not_eq; auto.
  - hnf; intros.
    simpl in H1.
    apply H; auto.
Qed.

128

129 130
Lemma ssa_equal_set V (f:cmd V) inVars inVars' outVars:
  NatSet.Equal inVars' inVars ->
Heiko Becker's avatar
Heiko Becker committed
131 132
  ssa f inVars outVars ->
  ssa f inVars' outVars.
133 134 135 136 137
Proof.
  intros set_eq ssa_f.
  revert set_eq; revert inVars'.
  induction ssa_f.
  - constructor.
138
    + rewrite set_eq; auto.
139 140 141 142 143 144 145 146
    + case_eq (NatSet.mem x inVars'); intros case_mem; try auto.
      rewrite NatSet.mem_spec in case_mem.
      rewrite set_eq in case_mem.
      rewrite <- NatSet.mem_spec in case_mem.
      rewrite case_mem in *; congruence.
    + apply IHssa_f; auto.
      apply NatSetProps.Dec.F.add_m; auto.
  - constructor.
147 148
    + rewrite set_eq; auto.
    + rewrite set_eq; auto.
149 150
Qed.

151

152 153
Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) :=
  match f with
154
  |Let m x e g =>
155 156
    andb (andb (negb (NatSet.mem x inVars)) (NatSet.subset (usedVars e) inVars)) (validSSA g (NatSet.add x inVars))
  |Ret e => NatSet.subset (usedVars e) inVars
157 158 159 160
  end.

Lemma validSSA_sound f inVars:
  validSSA f inVars = true ->
Heiko Becker's avatar
Heiko Becker committed
161
  exists outVars, ssa f inVars outVars.
162 163 164 165 166 167 168 169 170
Proof.
  revert inVars; induction f.
  - intros inVars validSSA_let.
    simpl in *.
    andb_to_prop validSSA_let.
    specialize (IHf (NatSet.add n inVars) R).
    destruct IHf as [outVars IHf].
    exists outVars.
    constructor; eauto.
171 172
    + rewrite <- NatSet.subset_spec; auto.
    + rewrite negb_true_iff in L0. auto.
173 174
  - intros inVars validSSA_ret.
    simpl in *.
175
    exists inVars.
176
    constructor; auto.
177 178
    + rewrite <- NatSet.subset_spec; auto.
    + hnf; intros; split; auto.
179 180
Qed.

181
Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars:
182
  ssa (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars ->
183
  NatSet.In y inVars ->
184
  eval_expr E defVars (toREval (toRExp e)) v REAL ->
185
  forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n.
186 187 188 189 190 191 192 193 194 195 196 197 198
Proof.
  intros ssa_let y_free eval_e.
  inversion ssa_let; subst.
  intros E' n; unfold updEnv.
  case_eq (n =? x).
  - intros n_eq_x.
    rewrite Nat.eqb_eq in n_eq_x.
    case_eq (n =? y); try auto.
    intros n_eq_y.
    rewrite Nat.eqb_eq in n_eq_y.
    rewrite n_eq_x in n_eq_y.
    rewrite <- n_eq_y in y_free.
    rewrite <- NatSet.mem_spec in y_free.
199
    rewrite y_free in H6. inversion H6.
200 201 202 203
  - intros n_neq_x.
    case_eq (n =? y); auto.
Qed.

204
(*
205
Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
206
  (forall n, E1 n = E2 n)->
207 208
  eval_expr E1 defVars (toREval e) v REAL <->
  eval_expr E2 defVars (toREval e) v REAL.
209
Proof.
210 211
  revert v E1 E2.
  induction e; intros v' E1 E2 agree_on_vars.
212 213
  - split; intros eval_Var.
    + inversion eval_Var; subst.
214 215
      rewrite agree_on_vars in H1.
      constructor; auto.
216
    + inversion eval_Var; subst.
217
      rewrite <- agree_on_vars in H1.
218
      eapply Var_load; eauto.
219 220 221 222 223 224
  - split; intros eval_Const; inversion eval_Const; subst; econstructor; auto.
  - split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto.
    + erewrite IHe; eauto.
    + erewrite IHe; eauto.
    + erewrite <- IHe; eauto.
    + erewrite <- IHe; eauto.
225 226
  - split; intros eval_Binop; inversion eval_Binop; subst; econstructor; eauto.
    destruct m1; destruct m2; inversion H2.
227
      try (erewrite IHe1; eauto);
228
      try (erewrite IHe2; eauto); auto.
229
  - split; intros eval_Downcast; simpl; simpl in eval_Downcast; erewrite IHe; eauto.
230 231
Qed.

232
Lemma shadowing_free_rewriting_cmd f E1 E2 vR defVars:
233
  (forall n, E1 n = E2 n) ->
234 235
  bstep (toREvalCmd f) E1 defVars vR REAL <->
  bstep (toREvalCmd f) E2 defVars vR REAL.
236
Proof.
237
revert E1 E2 defVars vR.
238
  induction f; intros E1 E2 vR agree_on_vars.
239
  - split; intros bstep_Let; inversion bstep_Let; subst.
240
    + erewrite shadowing_free_rewriting_expr in H8; auto.
241 242
      econstructor; eauto.
      rewrite <- IHf.
243
      apply H10.
244 245
      intros n'; unfold updEnv.
      case_eq (n' =? n); auto.
246
    + erewrite <- shadowing_free_rewriting_expr in H8; auto.
247 248
      econstructor; eauto.
      rewrite IHf.
249
      apply H10.
250 251 252
      intros n'; unfold updEnv.
      case_eq (n' =? n); auto.
  - split; intros bstep_Ret; inversion bstep_Ret; subst.
253
    + erewrite shadowing_free_rewriting_expr in H1; auto.
254
      constructor; auto.
255
    + erewrite <- shadowing_free_rewriting_expr in H1; auto.
256 257 258
      constructor; auto.
Qed.

259
Lemma dummy_bind_ok e v x v' inVars E defVars:
260
  NatSet.Subset (usedVars e) inVars ->
261
  NatSet.mem x inVars = false ->
262 263
  eval_expr E defVars (toREval (toRExp e)) v REAL ->
  eval_expr (updEnv x v' E) defVars (toREval (toRExp e)) v REAL.
264
Proof.
265 266
  revert v x v' inVars E.
  induction e; intros v1 x v2 inVars E valid_vars x_not_free eval_e.
267
  - inversion eval_e; subst.
268
    assert ((updEnv x v2 E) n = E n).
269 270 271 272 273
    + unfold updEnv.
      case_eq (n =? x); try auto.
      intros n_eq_x.
      rewrite Nat.eqb_eq in n_eq_x.
      subst; simpl in *.
274 275 276 277 278 279 280
      hnf in valid_vars.
      assert (NatSet.mem x (NatSet.singleton x) = true)
        as in_singleton by (rewrite NatSet.mem_spec, NatSet.singleton_spec; auto).
      rewrite NatSet.mem_spec in *.
      specialize (valid_vars x in_singleton).
      rewrite <- NatSet.mem_spec in valid_vars.
      rewrite valid_vars in *; congruence.
281
    + econstructor; eauto.
282
      rewrite H; auto.
283
  - inversion eval_e; subst; constructor; auto.
284
  - inversion eval_e; subst; econstructor; eauto.
285
  - simpl in valid_vars.
286
    inversion eval_e; subst; econstructor; eauto;
287
    destruct m1; destruct m2; inversion H2;
288
      subst.
289
    + eapply IHe1; eauto.
290 291 292
      hnf; intros a in_e1.
      apply valid_vars;
        rewrite NatSet.union_spec; auto.
293
    + eapply IHe2; eauto.
294 295 296
      hnf; intros a in_e2.
      apply valid_vars;
        rewrite NatSet.union_spec; auto.
297
  - apply (IHe v1 x v2 inVars E); auto.
298 299
Qed.

300
Fixpoint expr_subst (e:expr Q) x e_new :=
301
  match e with
302
  |Var _ v => if v =? x then e_new else Var Q v
303 304 305
  |Unop op e1 => Unop op (expr_subst e1 x e_new)
  |Binop op e1 e2 => Binop op (expr_subst e1 x e_new) (expr_subst e2 x e_new)
  |Downcast m e1 => Downcast m (expr_subst e1 x e_new)
306 307
  | e => e
  end.
308
*)
309
(* Lemma expr_subst_correct e e_sub E x v v_res defVars: *)
310 311 312
(*   eval_expr E defVars (toREval (toRExp e_sub)) v REAL -> *)
(*   eval_expr (updEnv x v E) defVars (toREval (toRExp e)) v_res REAL <-> *)
(*   eval_expr E defVars (toREval (toRExp (expr_subst e x e_sub))) v_res REAL. *)
313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332
(* Proof. *)
(*   intros eval_e. *)
(*   revert v_res. *)
(*   induction e. *)
(*   - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(*     + unfold updEnv in eval_upd. simpl in *. *)
(*       inversion eval_upd; subst. *)
(*       case_eq (n =? x); intros; try auto. *)
(*       * rewrite H in H1. *)
(*         inversion H1; subst; auto. *)
(*       * rewrite H in H1.  *)
(*         eapply Var_load; eauto. *)
(*     + simpl in eval_subst. *)
(*       case_eq (n =? x); intros n_eq_case; *)
(*         rewrite n_eq_case in eval_subst. *)
(*       * simpl. *)
(*         assert (updEnv x v E n = Some v_res). *)
(*         { unfold updEnv; rewrite n_eq_case. *)
(*           f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. } *)
(*         { econstructor; eauto. *)
333

334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359
(*           rewrite n_eq_case; auto. }  *)
(*       * simpl. inversion eval_subst; subst. *)
(*         assert (E n = updEnv x v E n). *)
(*         { unfold updEnv; rewrite n_eq_case; reflexivity. } *)
(*         { rewrite H in H1. eapply Var_load; eauto. rewrite n_eq_case. auto. } *)
(*   - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(*     + inversion eval_upd; constructor; auto. *)
(*     + inversion eval_subst; constructor; auto. *)
(*   - split; [intros eval_upd | intros eval_subst]. *)
(*     + inversion eval_upd; econstructor; auto; *)
(*         rewrite <- IHe; auto. *)
(*     + inversion eval_subst; constructor; try auto; *)
(*         rewrite IHe; auto. *)
(*   - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(*     + inversion eval_upd; econstructor; auto; *)
(*       destruct m1; destruct m2; inversion H2. *)
(*       * rewrite <- IHe1; auto. *)
(*       * rewrite <- IHe2; auto. *)
(*     + inversion eval_subst; econstructor; auto; *)
(*         destruct m1; destruct m2; inversion H2. *)
(*       * rewrite IHe1; auto. *)
(*       * rewrite IHe2; auto. *)
(*   - split; [intros eval_upd | intros eval_subst]. *)
(*     + rewrite <- IHe; auto. *)
(*     + rewrite IHe; auto. *)
(* Qed. *)
360

361 362
(* Fixpoint map_subst (f:cmd Q) x e := *)
(*   match f with *)
363 364
(*   |Let m y e_y g => Let m y (expr_subst e_y x e) (map_subst g x e) *)
(*   |Ret e_r => Ret (expr_subst e_r x e) *)
365
(*   end. *)
366

367 368 369 370
(* Lemma stepwise_substitution x e v f E vR inVars outVars defVars: *)
(*   ssa (toREvalCmd (toRCmd f)) inVars outVars -> *)
(*   NatSet.In x inVars -> *)
(*   NatSet.Subset (usedVars e) inVars -> *)
371 372 373
(*   eval_expr E defVars (toREval (toRExp e)) v REAL -> *)
(*   bstep (toREvalCmd (toRCmd f)) (updEnv x v E) (fun n => if (n =? x) then Some REAL else defVars n) vR REAL <-> *)
(*   bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR REAL. *)
374 375 376 377 378 379 380 381 382 383 384 385 386 387
(* Proof. *)
(*   revert E e x vR inVars outVars defVars. *)
(*   induction f; intros E e0 x vR inVars outVars defVars ssa_f x_free valid_vars_e eval_e. *)
(*   - split; [ intros bstep_let | intros bstep_subst]. *)
(*     + inversion bstep_let; subst. *)
(*       inversion ssa_f; subst. *)
(*       assert (forall E var, updEnv n v0 (updEnv x v E) var = updEnv x v (updEnv n v0 E) var). *)
(*       * eapply ssa_shadowing_free. *)
(*         apply ssa_f. *)
(*         apply x_free. *)
(*         eauto. *)
(*       * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H8; try eauto. *)
(*         simpl in *. *)
(*         econstructor; eauto. *)
388
(*         { rewrite <- expr_subst_correct; eauto. } *)
389 390 391 392 393 394 395 396 397
(*         { rewrite <- IHf; eauto. *)
(*           admit. *)
(*           rewrite NatSet.add_spec; right; auto. *)
(*           apply validVars_add; auto. *)
(*           eapply dummy_bind_ok; eauto. } *)
(*     + inversion bstep_subst; subst. *)
(*       simpl in *. *)
(*       inversion ssa_f; subst. *)
(*       econstructor; try auto. *)
398
(*       rewrite expr_subst_correct; eauto. *)
399 400 401 402
(*       rewrite <- IHf in H8; eauto. *)
(*       * rewrite <- shadowing_free_rewriting_cmd in H8; eauto. *)
(*         admit. *)
(*         (* eapply ssa_shadowing_free; eauto. *) *)
403
(*         (* rewrite <- expr_subst_correct in H7; eauto. *) *)
404 405 406 407 408 409
(*       * rewrite NatSet.add_spec; auto. *)
(*       * apply validVars_add; auto. *)
(*       * eapply dummy_bind_ok; eauto. *)
(*   - split; [intros bstep_let | intros bstep_subst]. *)
(*     + inversion bstep_let; subst. *)
(*       simpl in *. *)
410
(*       rewrite expr_subst_correct in H0; eauto. *)
411 412 413
(*       constructor. assumption. *)
(*     + inversion bstep_subst; subst. *)
(*       simpl in *. *)
414
(*       rewrite <- expr_subst_correct in H0; eauto. *)
415 416
(*       econstructor; eauto. *)
(* Admitted. *)
417

418 419 420
(* Fixpoint let_subst (f:cmd Q) := *)
(*   match f with *)
(*   | Let m x e1 g => *)
421
(*     expr_subst (let_subst g) x e1 *)
422 423
(*   | Ret e1 => e1 *)
(*   end. *)
424

425
(* Lemma eval_subst_subexpr E e' n e vR defVars: *)
426
(*   NatSet.In n (usedVars e) -> *)
427 428
(*   eval_expr E defVars (toREval (toRExp (expr_subst e n e'))) vR REAL -> *)
(*   exists v, eval_expr E defVars (toREval (toRExp e')) v REAL. *)
429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446
(* Proof. *)
(*   revert E e' n vR. *)
(*   induction e; *)
(*   intros E e' n' vR n_fVar eval_subst; simpl in *; try eauto. *)
(*   - case_eq (n =? n'); intros case_n; rewrite case_n in *; eauto. *)
(*     rewrite NatSet.singleton_spec in n_fVar. *)
(*     exfalso. *)
(*     rewrite Nat.eqb_neq in case_n. *)
(*     apply case_n; auto. *)
(*   - inversion n_fVar. *)
(*   - inversion eval_subst; subst; *)
(*       eapply IHe; eauto. *)
(*   - inversion eval_subst; subst. *)
(*     rewrite NatSet.union_spec in n_fVar. *)
(*     destruct m1; destruct m2; inversion H2. *)
(*     destruct n_fVar as [n_fVar_e1 | n_fVare2]; *)
(*       [eapply IHe1; eauto | eapply IHe2; eauto]. *)
(* Qed. *)
447

448
(* Lemma bstep_subst_subexpr_any E e x f vR defVars: *)
449
(*   NatSet.In x (liveVars f) -> *)
450 451
(*   bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR REAL -> *)
(*   exists E' v, eval_expr E' defVars (toREval (toRExp e)) v REAL. *)
452 453 454 455 456 457 458 459
(* Proof. *)
(*   revert E e x vR defVars; *)
(*     induction f; *)
(*     intros E e' x vR defVars x_live eval_f. *)
(*   - inversion eval_f; subst. *)
(*     simpl in x_live. *)
(*     rewrite NatSet.union_spec in x_live. *)
(*     destruct x_live as [x_used | x_live]. *)
460
(*     + exists E. eapply eval_subst_subexpr; eauto. *)
461 462 463 464
(*     + eapply IHf; eauto. *)
(* Admitted. *)
(*   - simpl in *. *)
(*     inversion eval_f; subst. *)
465
(*     exists E. eapply eval_subst_subexpr; eauto. *)
466
(* Qed. *)
467

468
(* Lemma bstep_subst_subexpr_ret E e x e' vR defVars: *)
469
(*   NatSet.In x (liveVars (Ret e')) -> *)
470 471
(*   bstep (toREvalCmd (toRCmd (map_subst (Ret e') x e))) E defVars vR REAL -> *)
(*   exists v, eval_expr E defVars (toREval (toRExp e)) v REAL. *)
472 473 474
(* Proof. *)
(*   simpl; intros x_live bstep_ret. *)
(*   inversion bstep_ret; subst. *)
475
(*   eapply eval_subst_subexpr; eauto. *)
476
(* Qed. *)
477

478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493
(* Lemma no_forward_refs V (f:cmd V) inVars outVars: *)
(*   ssa f inVars outVars -> *)
(*   forall v, NatSet.In v (definedVars f) -> *)
(*        NatSet.mem v inVars = false. *)
(* Proof. *)
(*   intros ssa_f; induction ssa_f; simpl. *)
(*   - intros v v_defVar. *)
(*     rewrite NatSet.add_spec in v_defVar. *)
(*     destruct v_defVar as [v_x | v_defVar]. *)
(*     + subst; auto. *)
(*     + specialize (IHssa_f v v_defVar). *)
(*       case_eq (NatSet.mem v inVars); intros mem_inVars; try auto. *)
(*       assert (NatSet.mem v (NatSet.add x inVars) = true) by (rewrite NatSet.mem_spec, NatSet.add_spec, <- NatSet.mem_spec; auto). *)
(*       congruence. *)
(*   - intros v v_in_empty; inversion v_in_empty. *)
(* Qed. *)
494

495
(* Lemma bstep_subst_subexpr_let E e x y e' g vR m defVars: *)
496 497 498
(*   NatSet.In x (liveVars (Let m y e' g)) -> *)
(*   (forall x, NatSet.In x (usedVars e) -> *)
(*         exists v, E x = v) -> *)
499 500
(*   bstep (toREvalCmd (toRCmd (map_subst (Let m y e' g) x e))) E defVars vR REAL -> *)
(*   exists v, eval_expr E defVars (toREval (toRExp e)) v REAL. *)
501 502 503 504 505 506 507 508 509
(* Proof. *)
(*   revert E e x y e' vR; *)
(*     induction g; *)
(*     intros E e0 x y e' vR x_live uedVars_def bstep_f. *)
(*   - simpl in *. *)
(*     inversion bstep_f; subst. *)
(*     specialize (IHg (updEnv y m v E) e0 x n e). *)
(*     rewrite NatSet.union_spec in x_live. *)
(*     destruct x_live as [x_used | x_live]. *)
510
(*     + eapply eval_subst_subexpr; eauto. *)
511 512
(*     + edestruct IHg as [v0 eval_v0]; eauto. *)
(* Admitted. *)
513

514 515 516 517 518
(* Theorem let_free_agree f E vR inVars outVars e defVars: *)
(*   ssa f inVars outVars -> *)
(*   (forall v, NatSet.In v (definedVars f) -> *)
(*         NatSet.In v (liveVars f)) -> *)
(*   let_subst f = e -> *)
519 520
(*   bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR REAL -> *)
(*   bstep (toREvalCmd (toRCmd f)) E defVars vR REAL. *)
521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543
(* Proof. *)
(*   intros ssa_f. *)
(*   revert E vR e; *)
(*     induction ssa_f; *)
(*     intros E vR e_subst dVars_live subst_step bstep_e; *)
(*     simpl in *. *)
(*   (* Let Case, prove that the value of the let binding must be used somewhere *) *)
(*   - case_eq (let_subst s). *)
(*     + intros e0 subst_s; rewrite subst_s in *. *)
(* Admitted. *)
(*       (*inversion subst_step; subst. *)
(*       clear subst_s subst_step. *)
(*       inversion bstep_e; subst. *)
(*       specialize (dVars_live x). *)
(*       rewrite NatSet.add_spec in dVars_live. *)
(*       assert (NatSet.In x (NatSet.union (usedVars e) (liveVars s))) *)
(*         as x_used_or_live *)
(*           by (apply dVars_live; auto). *)
(*       rewrite NatSet.union_spec in x_used_or_live. *)
(*       destruct x_used_or_live as [x_used | x_live]. *)
(*       * specialize (H x x_used). *)
(*         rewrite <- NatSet.mem_spec in H; congruence. *)
(*       * *)
544

545 546 547
(*     eapply let_b. *)
(*     Focus 2. *)
(*     eapply IHssa_f; try auto. *) *)
548

549 550
(* Theorem let_free_form f E vR inVars outVars e defVars: *)
(*   ssa f inVars outVars -> *)
551
(*   bstep (toREvalCmd (toRCmd f)) E defVars vR REAL -> *)
552
(*   let_subst f = e -> *)
553
(*   bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR REAL. *)
554 555 556 557 558 559 560 561 562 563
(* Proof. *)
(*     revert E vR inVars outVars e; *)
(*     induction f; *)
(*     intros E vR inVars outVars e_subst ssa_f bstep_f subst_step. *)
(*   - simpl. *)
(*     inversion bstep_f; subst. *)
(*     inversion ssa_f; subst. *)
(* Admitted. *)
(* (* case_eq (let_subst f). *)
(*     + intros f_subst subst_f_eq. *)
564
(*       specialize (IHf (updEnv n REAL v E) vR (NatSet.add n inVars) outVars f_subst H9 H7 subst_f_eq). *)
565 566 567 568 569
(*       rewrite subst_f_eq in subst_step. *)
(*       inversion IHf; subst. *)
(*       constructor. *)
(*       inversion subst_step. *)
(*       subst. *)
570
(*       rewrite <- expr_subst_correct; eauto. *)
571 572 573 574 575 576 577 578
(*     + intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step. *)
(*   - inversion bstep_f; subst. *)
(*     constructor. *)
(*     simpl in *. *)
(*     inversion subst_step; subst. *)
(*     assumption. *)
(* Qed. *)
(*  *) *)
579

580 581 582 583 584 585 586 587 588 589 590 591 592 593 594
(* (* *)
(* Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env) *)
(*       (ParamEnv:param_env) (P:precond) (eps:R): *)
(*   ssa Q f inVars outVars -> *)
(*   (forall v, NatSet.In v (freeVars e) -> *)
(*         (Q2R (ivlo (P v)) <= ParamEnv v <= Q2R (ivhi (P v))))%R -> *)
(*   (forall v, NatSet.In v inVars -> *)
(*         exists r, VarEnv v = Some r) -> *)
(*   exists vR, *)
(*     bstep (toRCmd f) VarEnv ParamEnv P eps (Nop R) vR. *)
(* Proof. *)
(*   intros ssa_f; revert VarEnv ParamEnv P eps. *)
(*   induction ssa_f; *)
(*     intros VarEnv ParamEnv P eps fVars_live. *)
(*   - *)
595
(*  *) *)