ssaPrgs.v 17.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.
Heiko Becker's avatar
Heiko Becker committed
10
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
11 12
Require Export Daisy.Commands.

13 14 15
Lemma validVars_add V (e:exp V) Vs n:
  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
Qed.

Lemma validVars_non_stuck (e:exp Q) inVars E:
41 42
 NatSet.Subset (usedVars e) inVars ->
  (forall v, NatSet.In v (usedVars e) ->
43 44
        exists r, (toREvalEnv E) v = Some (r, M0))%R ->
  exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0.
45
Proof.
46
    revert inVars E; induction e;
47 48 49 50 51
    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].
52
    exists vR; econstructor; eauto.
53
  - exists (perturb (Q2R v) 0); constructor.
54 55
    simpl (meps M0); rewrite Rabs_R0; rewrite Q2R0_is_0; lra.
  - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0)
56 57 58 59 60
      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.
61
      simpl (meps M0); rewrite Q2R0_is_0; rewrite Rabs_R0; lra.
62
  - repeat rewrite NatSet.subset_spec in *; simpl in *.
63
    assert (exists vR1, eval_exp (toREvalEnv E) (toREval (toRExp e1)) vR1 M0) as eval_e1_def.
64
    + eapply IHe1; eauto.
65 66 67 68
      * hnf; intros.
        apply vars_valid.
        rewrite NatSet.union_spec; auto.
      * intros.
69
        destruct (fVars_live v) as [vR E_def]; try eauto.
70
        apply NatSet.union_spec; auto.
71
    + assert (exists vR2, eval_exp (toREvalEnv E) (toREval (toRExp e2)) vR2 M0) as eval_e2_def.
72 73 74 75 76 77 78
      * 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. }
79 80
      * destruct eval_e1_def as [vR1 eval_e1_def];
          destruct eval_e2_def as [vR2 eval_e2_def].
81
        exists (perturb (evalBinop b vR1 vR2) 0); econstructor; eauto.
82
        auto.
83
        simpl. rewrite Q2R0_is_0. rewrite Rabs_R0; lra.
84
  - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e))  vR M0) as eval_r_def by (eapply IHe; eauto).
85
    destruct eval_r_def as [vr eval_r_def].
86
    exists vr.
87 88
    simpl toREval.
    auto.
89 90
Qed.

91
Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
92
 ssaLet m x e s inVars Vterm:
93
   NatSet.Subset (usedVars e) inVars->
94 95
   NatSet.mem x inVars = false ->
   ssaPrg s (NatSet.add x inVars) Vterm ->
96
   ssaPrg (Let m x e s) inVars Vterm
97
|ssaRet e inVars Vterm:
98 99
   NatSet.Subset (usedVars e) inVars ->
   NatSet.Equal inVars Vterm ->
100 101 102 103 104 105 106 107
   ssaPrg (Ret e) inVars Vterm.


Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
  ssaPrg f inVars outVars ->
  NatSet.Subset (Commands.freeVars f) inVars.
Proof.
  intros ssa_f; induction ssa_f.
108
  - simpl in *. hnf; intros a in_fVars.
109 110 111 112 113 114 115 116 117 118 119 120
    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.

121

122 123 124 125 126 127 128 129 130
Lemma ssa_equal_set V (f:cmd V) inVars inVars' outVars:
  NatSet.Equal inVars' inVars ->
  ssaPrg f inVars outVars ->
  ssaPrg f inVars' outVars.
Proof.
  intros set_eq ssa_f.
  revert set_eq; revert inVars'.
  induction ssa_f.
  - constructor.
131
    + rewrite set_eq; auto.
132 133 134 135 136 137 138 139
    + 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.
140 141
    + rewrite set_eq; auto.
    + rewrite set_eq; auto.
142 143
Qed.

144

145 146
Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) :=
  match f with
147
  |Let m x e g =>
148 149
    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
150 151 152 153 154 155 156 157 158 159 160 161 162 163
  end.

Lemma validSSA_sound f inVars:
  validSSA f inVars = true ->
  exists outVars, ssaPrg f inVars outVars.
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.
164 165
    + rewrite <- NatSet.subset_spec; auto.
    + rewrite negb_true_iff in L0. auto.
166 167
  - intros inVars validSSA_ret.
    simpl in *.
168
    exists inVars.
169
    constructor; auto.
170 171
    + rewrite <- NatSet.subset_spec; auto.
    + hnf; intros; split; auto.
172 173
Qed.

174
Lemma ssa_shadowing_free m x y v v' e f inVars outVars E:
175
  ssaPrg (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars ->
176
  NatSet.In y inVars ->
177
  eval_exp E (toREval (toRExp e)) v M0 ->
178
  forall E n, updEnv x m v (updEnv y m v' E) n = updEnv y m v' (updEnv x m v E) n.
179 180 181 182 183 184 185 186 187 188 189 190 191
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.
192
    rewrite y_free in H6. inversion H6.
193 194 195 196
  - intros n_neq_x.
    case_eq (n =? y); auto.
Qed.

197

198
Lemma shadowing_free_rewriting_exp e v E1 E2:
199 200 201
(*  (forall n, exists v m,
        E1 n = Some (v,m) ->
        exists m', (E2 n = Some (v,m') /\ (meps m) == (meps m'))) ->*)
202
  (forall n, E1 n = E2 n)->
203 204
  eval_exp E1 (toREval e) v M0 <->
  eval_exp E2 (toREval e) v M0.
205
Proof.
206 207
  revert v E1 E2.
  induction e; intros v' E1 E2 agree_on_vars.
208 209
  - split; intros eval_Var.
    + inversion eval_Var; subst.
210 211 212
      (*assert (m1 = M0) by (apply ifisMorePreciseM0; auto); subst.*)
      rewrite agree_on_vars in H2.
      apply Var_load; auto.
213
    + inversion eval_Var; subst.
214 215
      rewrite <- agree_on_vars in H2.
      apply Var_load; auto.
216 217 218 219 220 221
  - 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.
222 223 224 225 226
  - split; intros eval_Binop; inversion eval_Binop; subst; econstructor; eauto;
      assert (M0 = M0) as M00 by auto;
      pose proof (ifM0isJoin_l M0 m1 m2 M00 H2);
      pose proof (ifM0isJoin_r M0 m1 m2 M00 H2);
      subst;
227
      try (erewrite IHe1; eauto);
228 229
      try (erewrite IHe2; eauto); auto.
  - split; intros eval_Downcast; inversion eval_Downcast; subst; try auto; erewrite IHe; eauto.
230 231
Qed.

232
Lemma shadowing_free_rewriting_cmd f E1 E2 vR:
233
  (forall n, E1 n = E2 n) ->
234 235
  bstep (toREvalCmd f) E1 vR M0 <->
  bstep (toREvalCmd f) E2 vR M0.
236
Proof.
237
revert E1 E2 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_exp in H5; auto.
241 242
      econstructor; eauto.
      rewrite <- IHf.
243
      apply H6.
244 245
      intros n'; unfold updEnv.
      case_eq (n' =? n); auto.
246
    + erewrite <- shadowing_free_rewriting_exp in H5; auto.
247 248
      econstructor; eauto.
      rewrite IHf.
249
      apply H6.
250 251 252 253 254 255 256
      intros n'; unfold updEnv.
      case_eq (n' =? n); auto.
  - split; intros bstep_Ret; inversion bstep_Ret; subst.
    + erewrite shadowing_free_rewriting_exp in H0; auto.
      constructor; auto.
    + erewrite <- shadowing_free_rewriting_exp in H0; auto.
      constructor; auto.
257
Qed.
258

259
Lemma dummy_bind_ok e v x v' inVars E:
260
  NatSet.Subset (usedVars e) inVars ->
261
  NatSet.mem x inVars = false ->
262 263
  eval_exp E (toREval (toRExp e)) v M0 ->
  eval_exp (updEnv x M0 v' E) (toREval (toRExp e)) v M0.
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 M0 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.
282
      auto.
283
      rewrite H; auto. 
284
  - inversion eval_e; subst; constructor; auto.
285
  - inversion eval_e; subst; econstructor; eauto.
286
  - simpl in valid_vars.
287 288
    inversion eval_e; subst; econstructor; eauto;
      assert (M0 = M0) as M00 by auto;
289 290
      pose proof (ifM0isJoin_l M0 m1 m2 M00 H2);
      pose proof (ifM0isJoin_r M0 m1 m2 M00 H2);
291
      subst.
292
    + eapply IHe1; eauto.
293 294 295
      hnf; intros a in_e1.
      apply valid_vars;
        rewrite NatSet.union_spec; auto.
296
    + eapply IHe2; eauto.
297 298
      hnf; intros a in_e2.
      apply valid_vars;
299 300
        rewrite NatSet.union_spec; auto.
  - apply (IHe v1 x v2 inVars E); auto.
301 302 303 304
Qed.

Fixpoint exp_subst (e:exp Q) x e_new :=
  match e with
305
  |Var _ m v => if v =? x then e_new else Var Q m v
306 307
  |Unop op e1 => Unop op (exp_subst e1 x e_new)
  |Binop op e1 e2 => Binop op (exp_subst e1 x e_new) (exp_subst e2 x e_new)
308
  |Downcast m e1 => Downcast m (exp_subst e1 x e_new)
309 310 311
  | e => e
  end.

312
Lemma exp_subst_correct e e_sub E x v v_res:
313 314 315
  eval_exp E (toREval (toRExp e_sub)) v M0 ->
  eval_exp (updEnv x M0 v E) (toREval (toRExp e)) v_res M0 <->
  eval_exp E (toREval (toRExp (exp_subst e x e_sub))) v_res M0.
316 317 318 319
Proof.
  intros eval_e.
  revert v_res.
  induction e.
320
  - intros v_res; split; [intros eval_upd | intros eval_subst].
321 322 323
    + unfold updEnv in eval_upd. simpl in *.
      inversion eval_upd; subst.
      case_eq (n =? x); intros; try auto.
324 325 326 327
      * rewrite H in H2.
        inversion H2; subst; auto.
      * rewrite H in H2. 
        apply Var_load; auto.
328 329 330 331
    + simpl in eval_subst.
      case_eq (n =? x); intros n_eq_case;
        rewrite n_eq_case in eval_subst.
      * simpl.
332
        assert (updEnv x M0 v E n = Some (v_res, M0)).
333
        { unfold updEnv; rewrite n_eq_case.
334
          f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. }
335
        { econstructor; eauto. } 
336
      * simpl. inversion eval_subst; subst.
337
        assert (E n = updEnv x M0 v E n).
338
        { unfold updEnv; rewrite n_eq_case; reflexivity. }
339
        { rewrite H in H2. apply Var_load; auto. } (*unfold updEnv in *. rewrite n_eq_case in *. unfold toREvalEnv. apply H4. }*)
340 341 342 343
  - 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].
344
    + inversion eval_upd; econstructor; auto;
345
        rewrite <- IHe; auto.
346
    + inversion eval_subst; constructor; try auto;
347
        rewrite IHe; auto.
348
  - intros v_res; split; [intros eval_upd | intros eval_subst].
349
    + inversion eval_upd; econstructor; auto;
350 351 352
        assert (M0 = M0) as M00 by auto; pose proof (ifM0isJoin_l M0 m1 m2 M00 H2);
          pose proof (ifM0isJoin_r M0 m1 m2 M00 H2); subst.
      * apply H2.
353 354
      * rewrite <- IHe1; auto.
      * rewrite <- IHe2; auto.
355 356 357 358
    + inversion eval_subst; econstructor; auto;
        assert (M0 = M0) as M00 by auto; pose proof (ifM0isJoin_l M0 m1 m2 M00 H2);
          pose proof (ifM0isJoin_r M0 m1 m2 M00 H2); subst.
      * apply H2.
359 360
      * rewrite IHe1; auto.
      * rewrite IHe2; auto.
361
  - split; [intros eval_upd | intros eval_subst].
362 363
    + rewrite <- IHe; auto.
    + rewrite IHe; auto.
364 365 366 367
Qed.

Fixpoint map_subst (f:cmd Q) x e :=
  match f with
368
  |Let m y e_y g => Let m y (exp_subst e_y x e) (map_subst g x e)
369 370 371
  |Ret e_r => Ret (exp_subst e_r x e)
  end.

372
(*
373 374 375 376 377 378 379 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
Lemma updEnv_comp_toREval (n:nat) (v:R):
  forall E var, updEnv n M0 v (toREvalEnv E) var = toREvalEnv (updEnv n M0 v E) var.
Proof.
  intros.
  unfold updEnv; unfold toREvalEnv.
  case_eq (var =? n); intros; auto.
Qed.

Lemma bli (e:exp Q) (n:nat) (v vR:R) (E:env):
  eval_exp (toREvalEnv (updEnv n M0 v E)) (toREval (toRExp e)) vR M0 <->
  eval_exp (updEnv n M0 v (toREvalEnv E)) (toREval (toRExp e)) vR M0.
Proof.
  revert e n v vR E.
  induction e; split; intros.
  - inversion H; subst; econstructor; eauto.
    rewrite updEnv_comp_toREval; auto.
  - inversion H; subst; econstructor; eauto.
    rewrite <- updEnv_comp_toREval; auto.
  - inversion H; subst; econstructor; eauto.
  - inversion H; subst; econstructor; eauto.
  - inversion H; subst; econstructor; eauto; apply IHe; auto.
  - inversion H; subst; econstructor; eauto; apply IHe; auto.
  - inversion H; subst; econstructor; eauto;
      assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
      assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst.
    apply IHe1; auto.
    apply IHe2; auto.
  - inversion H; subst; econstructor; eauto;
      assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
      assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst.
    apply IHe1; auto.
    apply IHe2; auto.
  - apply IHe; auto.
  - apply IHe; auto.
Qed.
408

409 410 411 412 413 414 415 416 417 418 419
Lemma bla (c: cmd Q) (n:nat) (v vR:R) (E:env):
  bstep (toREvalCmd (toRCmd c)) (updEnv n M0 v (toREvalEnv E)) vR M0 <->
  bstep (toREvalCmd (toRCmd c)) (toREvalEnv (updEnv n M0 v E)) vR M0.
Proof.
  revert c n v vR E.
  induction c; split; intros.
  - inversion H; subst.
    econstructor; eauto.
    apply bli; eauto.
    apply IHc; auto.
Admitted.
Raphaël Monat's avatar
Raphaël Monat committed
420
(*     remember (updEnv n0 M0 v (toREvalEnv E)) as E'. *)
421

Raphaël Monat's avatar
Raphaël Monat committed
422 423 424 425 426 427
(*     replace E' with (toREvalEnv E') in H9. *)
(*     + apply IHc in H9. *)
(*       rewrite HeqE' in H9. *)
(*       replace E with (toREvalEnv E) by admit. *)
(*       apply H9. *)
(* Admitted. *)
428
*)
429

430
Lemma stepwise_substitution x e v f E vR inVars outVars:
431
  ssaPrg (toREvalCmd (toRCmd f)) inVars outVars ->
432
  NatSet.In x inVars ->
433
  NatSet.Subset (usedVars e) inVars ->
434 435 436
  eval_exp E (toREval (toRExp e)) v M0 ->
  bstep (toREvalCmd (toRCmd f)) (updEnv x M0 v E) vR M0 <->
  bstep (toREvalCmd (toRCmd (map_subst f x e))) E vR M0.
437
Proof.
438 439
  revert E e x vR inVars outVars.
  induction f; intros E e0 x vR inVars outVars ssa_f x_free valid_vars_e eval_e.
440 441 442
  - split; [ intros bstep_let | intros bstep_subst].
    + inversion bstep_let; subst.
      inversion ssa_f; subst.
443 444 445 446
      assert (forall E var, updEnv n M0 v0 (updEnv x M0 v E) var = updEnv x M0 v (updEnv n M0 v0 E) var).
      * eapply ssa_shadowing_free.
        apply ssa_f.
        apply x_free.
447 448
        apply H5.
      * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H6; try eauto.
449 450 451 452 453 454 455
        simpl in *.
        econstructor; eauto.
        { rewrite <- exp_subst_correct; eauto. }
        { rewrite <- IHf; eauto.
          rewrite NatSet.add_spec; right; auto.
          apply validVars_add; auto.
          eapply dummy_bind_ok; eauto. }
456 457 458
    + inversion bstep_subst; subst.
      simpl in *.
      inversion ssa_f; subst.
459 460
      econstructor; try auto.
      rewrite exp_subst_correct; eauto.
461 462
      rewrite <- IHf in H6; eauto.
      * rewrite <- shadowing_free_rewriting_cmd in H6; eauto.
463
        eapply ssa_shadowing_free; eauto.
464
        rewrite <- exp_subst_correct in H5; eauto.
465
      * rewrite NatSet.add_spec; auto.
Raphaël Monat's avatar
Raphaël Monat committed
466
      * apply validVars_add; auto.
467
      * eapply dummy_bind_ok; eauto.
468 469 470
  - split; [intros bstep_let | intros bstep_subst].
    + inversion bstep_let; subst.
      simpl in *.
471
      rewrite exp_subst_correct in H0; eauto.
472 473 474 475
      constructor. assumption.
    + inversion bstep_subst; subst.
      simpl in *.
      rewrite <- exp_subst_correct in H0; eauto.
476
      econstructor; eauto.
477
Qed.
478 479 480

Fixpoint let_subst (f:cmd Q) :=
  match f with
481
  | Let m x e1 g =>
482 483 484 485 486 487 488
    match (let_subst g) with
    |Some e' =>  Some (exp_subst e' x e1)
    |None => None
    end
  | Ret e1 =>  Some e1
  end.

489
Theorem let_free_form f E vR inVars outVars e:
490
  ssaPrg f inVars outVars ->
491
  bstep (toREvalCmd (toRCmd f)) E vR M0 ->
492
  let_subst f = Some e ->
493
  bstep (toREvalCmd (toRCmd (Ret e))) E vR M0.
494
Proof.
495
    revert E vR inVars outVars e;
496
    induction f;
497
    intros E vR inVars outVars e_subst ssa_f bstep_f subst_step.
498 499 500 501 502 503
  - simpl.
    inversion bstep_f; subst.
    inversion ssa_f; subst.
    simpl in subst_step.
    case_eq (let_subst f).
    + intros f_subst subst_f_eq.
504
      specialize (IHf (updEnv n M0 v E) vR (NatSet.add n inVars) outVars f_subst H9 H6 subst_f_eq).
505 506 507 508 509 510 511 512 513 514 515 516
      rewrite subst_f_eq in subst_step.
      inversion IHf; subst.
      constructor.
      inversion subst_step.
      subst.
      rewrite <- exp_subst_correct; eauto.
    + intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step.
  - inversion bstep_f; subst.
    constructor.
    simpl in *.
    inversion subst_step; subst.
    assumption.
517
Qed.