working sim_apply

theories/opt/ex1.v

@@ -37,9 +37,8 @@ Proof.
   apply sim_body_init_call. simpl.
 
   (* Alloc *)
-  sim_bind (Alloc _) (Alloc _). simpl.
-  apply sim_body_alloc_shared. simpl. intros -> ->.
+  sim_apply sim_body_alloc_local. simpl.
 
   (* Let *)
-  sim_bind (Let _ _ _) (Let _ _ _).
+  sim_apply sim_body_let_place. simpl.
 Abort.

theories/sim/refl_step.v

@@ -1220,6 +1220,11 @@ Lemma sim_body_let_val fs ft r n x (vs1 vt1: value) es2 et2 σs σt Φ :
   r ⊨{n,fs,ft} (let: x := vs1 in es2, σs) ≥ ((let: x := vt1 in et2), σt) : Φ.
 Proof. apply sim_body_let; eauto. Qed.
 
+Lemma sim_body_let_place fs ft r n x ls lt ts tt tys tyt es2 et2 σs σt Φ :
+  r ⊨{n,fs,ft} (subst x (Place ls ts tys) es2, σs) ≥ (subst x (Place lt tt tyt) et2, σt) : Φ →
+  r ⊨{n,fs,ft} (let: x := Place ls ts tys in es2, σs) ≥ ((let: x := Place lt tt tyt in et2), σt) : Φ.
+Proof. apply sim_body_let; eauto. Qed.
+
 (** Ref *)
 Lemma sim_body_ref fs ft r n l tgs tgt Ts Tt σs σt Φ :
   r ⊨{n,fs,ft} (#[ScPtr l tgs], σs) ≥ (#[ScPtr l tgt], σt) : Φ →

theories/sim/tactics.v

@@ -32,3 +32,14 @@ Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
       )
     )
   end.
+
+Tactic Notation "sim_apply" open_constr(lem) :=
+  match goal with
+  | |- _ ⊨{_,_,_} (?es, _) ≥ (?et, _) : _ =>
+    reshape_expr es ltac:(fun Ks es =>
+      reshape_expr et ltac:(fun Kt et =>
+        eapply (sim_body_bind _ _ _ _ Ks Kt es et);
+        eapply lem
+      )
+    )
+  end.