make tactics work for simple sim

theories/opt/ex1.v

@@ -31,11 +31,12 @@ Proof.
   apply (sim_fun_simple1 10)=>// rf es css et cs vs vt FREL ??. simplify_eq/=.
 
   (* InitCall *)
-  apply sim_simple_init_call=>c /= {css}.
-(*
+  apply sim_simple_init_call=> c /= {css}.
+
   (* Alloc *)
-  sim_apply sim_body_alloc_local. simpl.
+  sim_apply sim_simple_alloc_local=> l t /=.
 
+(*
   (* Let *)
   sim_apply sim_body_let_place. simpl.
 *)

theories/sim/simple.v

@@ -7,10 +7,7 @@ To go the other direction, [apply sim_simplify NEW_POST]. Then you will likely
 want to clean some stuff from your context.
 *)
 
-From stbor.sim Require Export instance refl_step.
-
-Section simple.
-Implicit Types Φ: resUR → nat → result → call_id_stack → result → call_id_stack → Prop.
+From stbor.sim Require Import body instance refl_step.
 
 Definition fun_post_simple initial_call_id_stack (r: resUR) (n: nat) vs css vt cst :=
   (∃ c, cst = c::initial_call_id_stack) ∧
@@ -23,11 +20,14 @@ Definition sim_simple fs ft r n es css et cst
     r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) :
     (λ r n vs' σs' vt' σt', Φ r n vs' σs'.(scs) vt' σt'.(scs)).
 
-Notation "r ⊨ˢ{ n , fs , ft } ( es , css ) '≥' ( et , cst ) : Φ" :=
+Notation "r ⊨ˢ{ n , fs , ft } ( es , css ) ≥ ( et , cst ) : Φ" :=
   (sim_simple fs ft r n%nat es%E css et%E cst Φ)
   (at level 70, es, et at next level,
    format "'[hv' r  '/' ⊨ˢ{ n , fs , ft }  '/  ' '[ ' ( es ,  css ) ']'  '/' ≥  '/  ' '[ ' ( et ,  cst ) ']'  '/' :  Φ ']'").
 
+Section simple.
+Implicit Types Φ: resUR → nat → result → call_id_stack → result → call_id_stack → Prop.
+
 (* FIXME: does this [apply]? *)
 Lemma sim_simplify
   (Φnew: resUR → nat → result → call_id_stack → result → call_id_stack → Prop)
@@ -37,7 +37,7 @@ Lemma sim_simplify
   r ⊨ˢ{ n , fs , ft } (es, σs.(scs)) ≥ (et, σt.(scs)) : Φnew →
   r ⊨{ n , fs , ft } (es, σs) ≥ (et, σt) : Φ.
 Proof.
-  intros HΦ HH. eapply sim_local_body_post_mono; last by apply HH.
+  intros HΦ HH. eapply sim_local_body_post_mono; last exact: HH.
   apply HΦ.
 Qed.
 
@@ -66,6 +66,20 @@ Proof.
   admit.
 Admitted.
 
+Lemma sim_simple_bind fs ft
+  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
+  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft)))
+  es et r n css cst Φ :
+  r ⊨ˢ{n,fs,ft} (es, css) ≥ (et, cst)
+    : (λ r' n' es' css' et' cst',
+        r' ⊨ˢ{n',fs,ft} (fill Ks es', css') ≥ (fill Kt et', cst') : Φ) →
+  r ⊨ˢ{n,fs,ft} (fill Ks es, css) ≥ (fill Kt et, cst) : Φ.
+Proof.
+  intros HH σs σt <-<-. apply sim_body_bind.
+  eapply sim_local_body_post_mono; last exact: HH.
+  clear. simpl. intros r n vs σs vt σt HH. exact: HH.
+Qed.
+
 Lemma sim_simple_init_call fs ft r n es css et cst Φ :
   (∀ c: call_id,
     let r' := res_callState c (csOwned ∅) in

theories/sim/tactics.v

 From stbor.lang Require Export lang.
+From stbor.sim Require Export simple.
 From stbor.sim Require Import body.
 
 Ltac reshape_expr e tac :=
@@ -31,6 +32,14 @@ Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
         eapply (sim_body_bind _ _ _ _ Ks Kt es et)
       )
     )
+  | |- _ ⊨ˢ{_,_,_} (?es, _) ≥ (?et, _) : _ =>
+    reshape_expr es ltac:(fun Ks es =>
+      unify es efocs;
+      reshape_expr et ltac:(fun Kt et =>
+        unify et efoct;
+        eapply (sim_simple_bind _ _ Ks Kt es et)
+      )
+    )
   end.
 
 Tactic Notation "sim_apply" open_constr(lem) :=
@@ -42,4 +51,11 @@ Tactic Notation "sim_apply" open_constr(lem) :=
         eapply lem
       )
     )
+  | |- _ ⊨ˢ{_,_,_} (?es, _) ≥ (?et, _) : _ =>
+    reshape_expr es ltac:(fun Ks es =>
+      reshape_expr et ltac:(fun Kt et =>
+        eapply (sim_simple_bind _ _ Ks Kt es et);
+        eapply lem
+      )
+    )
   end.