context of breaking example in data_races.v

theories/simulang/na_inv/examples/data_races.v

@@ -97,6 +97,53 @@ Section data_race.
   Lemma int_is_unboxed (z : Z) : val_is_unboxed #z.
   Proof. done. Qed.
 
+
+Ltac simpl_subst :=
+  repeat match goal with
+    | |- context C [apply_func ?fn ?v] =>
+      (* Unfold [apply_func] if the function's components are available *)
+      let arg := open_constr:(_ : string) in
+      let body := open_constr:(_ : expr) in
+      unify fn (arg, body);
+      change (apply_func fn v) with (subst arg v body)
+    end;
+  repeat match goal with
+    | |- context C [subst ?x ?v ?e] =>
+      lazymatch e with
+      | subst _ _ _ => fail
+      | _ => idtac
+      end;
+      pattern (subst x v e);
+      let e' := W.of_expr e in
+      simple refine (W.tac_to_expr_subst _ _ _ _ e' _ _ _ _); [ shelve
+      | simpl; rewrite ?list_to_map_to_list; reflexivity
+      | (* shelve here instead of [compute_done] *)shelve
+      |];
+      simple refine (W.tac_to_expr_combine_subst_map _ _ _ _ _); [ shelve |
+      (* shelve here instead of [compute_done] *) shelve | ];
+      simpl
+    end.
+From iris.proofmode Require Import coq_tactics reduction.
+From iris.proofmode Require Export tactics.
+
+Tactic Notation "source_pure" open_constr(efoc) :=
+  iStartProof;
+  to_source;
+  lazymatch goal with
+  | |- envs_entails _ (source_red ?e_s _ _) =>
+    let e_s := eval simpl in e_s in
+    reshape_expr e_s ltac:(fun K_s e_s' =>
+      unify e_s' efoc;
+      eapply (tac_source_red_pure _ _ _ e_s' _ K_s _ _);
+      [ iSolveTC                       (* PureExec *)
+      | try solve_vals_compare_safe    (* The pure condition for PureExec --
+         handles trivial goals, including [vals_compare_safe] *)
+      | (* new goal *)
+      ])
+    || fail "source_red_pure: cannot find" efoc "in" e_s "or" efoc "is not a redex"
+  | _ => fail "source_red_pure: not a 'sim'"
+  end.
+
   Lemma hoist_load_sim:
     ⊢ log_rel hoist_load_t hoist_load_s.
   Proof.
@@ -152,7 +199,17 @@ Section data_race.
       rewrite bool_decide_eq_true_2; last done.
       sim_pures. iApply sim_expr_base. iLeft. iApply lift_post_val.
 
-      sim_pures. source_load. target_load. to_sim. sim_pures.
+      sim_pures. source_load. target_load. to_sim. 
+      source_pure _. 
+      source_red_expr_eval simpl. 
+
+      unshelve simpl_subst. 
+      2: { timeout 4 vm_compute. 
+        Eval vm_compute in (W.subst "res" #z_r
+    (W.Let <> (W.FreeN (W.Val #1) (W.Val #lr_s))
+       (W.Let <> (W.FreeN (W.Val #1) (W.Val #li_s)) (W.Var "res")))).
+
+        sim_pures.
       (* cleanup *)
       source_free. source_free. target_free. target_free. sim_pures.
       iApply (sim_bij_release (NaRead q) with "Hbij Hc Hl_t Hl_s [//]").