Get rid of some unnecessary closedness conditions

F_mu_ref_conc/examples/counter.v

@@ -282,7 +282,6 @@ Section CG_Counter.
 
     iApply (bin_log_related_pair _ with "[]").
     - rel_rec_l.
-      { unfold FG_increment. unlock. simpl_subst/=. solve_closed. }
       unfold CG_increment. unlock.
       rel_rec_r.
       rel_rec_r.
@@ -291,9 +290,7 @@ Section CG_Counter.
       { unfold CG_increment. unlock; simpl_subst/=. reflexivity. }
       iApply (FG_CG_increment_refinement with "Hinv").
     - rel_rec_l.
-      { unfold counter_read. unlock. simpl_subst/=. solve_closed. }
       rel_rec_r.
-      { unfold counter_read. unlock. simpl_subst/=. solve_closed. }
       iApply (counter_read_refinement with "Hinv").
   Qed.
 End CG_Counter.

F_mu_ref_conc/proofmode/classes.v

@@ -5,6 +5,25 @@ Class PureExec (P : Prop) (e1 e2 : expr) := {
   pure_exec_puredet : P -> ∀ σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs;
 }.
 
+(* DF: Some tactics will loop pretty badly and consume lots of memory if you make this an instance *)
+Lemma PureExec_Closed P e1 e2 `{Hcl : Closed X e1} `{HP: PureExec P e1 e2} : P -> Closed X e2.
+Proof.
+destruct HP as [Hpure Hstep].
+intros p. specialize (Hpure p). specialize (Hstep p).
+specialize (Hpure inhabitant).
+unfold head_reducible in *.
+destruct Hpure as (e' & σ' & efs & Hst).
+destruct (Hstep inhabitant e' σ' efs Hst) as (? & ? & ?); subst.
+destruct e1; inv_head_step;
+  unfold Closed in *; simpl in Hcl; simpl;
+  destruct_and?; split_and?; eauto.
+- apply Closed_mono with ∅; [ | set_solver ].
+  destruct f, x; simpl in *; eauto;
+    repeat apply is_closed_subst_preserve; eauto;
+    try apply of_val_closed.
+- apply of_val_closed'.
+Qed.
+
 Instance pure_binop op e1 v1 e2 v2 v `(to_val e1 = Some v1) `(to_val e2 = Some v2):
   PureExec (binop_eval op v1 v2 = Some v)
            (BinOp op e1 e2)

F_mu_ref_conc/proofmode/rel_tactics.v

@@ -99,12 +99,13 @@ Lemma tac_rel_pure_l `{logrelG Σ} K e1 Δ' E1 E2 Δ Γ e e2 ϕ t τ (b : bool)
   PureExec ϕ e1 e2 →
   ϕ →
   Closed ∅ e1 →
-  Closed ∅ e2 →
   ((b = true ∧ E1 = E2) ∨ b = false) →
   (Δ' ⊢ ▷?b bin_log_related E1 E2 Δ Γ (fill K e2) t τ) →
   (Δ' ⊢ bin_log_related E1 E2 Δ Γ e t τ).
 Proof.
-  intros Hfill Hpure Hϕ ?? Hb Hp. subst.
+  intros Hfill Hpure Hϕ ? Hb Hp. subst.
+  assert (Closed ∅ e2).
+  { eapply PureExec_Closed; eauto. }
   destruct b.
   - destruct Hb as [[_ ?] | Hb']; last by inversion Hb'. subst.    
     rewrite -(bin_log_pure_l Δ Γ E2 K e1 e2 t τ).
@@ -126,7 +127,6 @@ Tactic Notation "rel_pure_l" open_constr(ef) :=
       |apply _                     (* PureExec ϕ e1 e2 *)
       |try (exact I || reflexivity || tac_rel_done)
       |try (simpl; solve_closed)           (* Closed ∅ e1 *)
-      |try (simpl_subst/=; solve_closed)   (* Closed ∅ e2 *) (* we might get subst' here *)
       |first [left; split; reflexivity | right; reflexivity] (* E1 = E2? *)
       |try iNext; simpl_subst/= (* new goal *)])
   || fail "rel_pure_l: cannot find the reduct".
@@ -152,12 +152,13 @@ Lemma tac_rel_pure_r `{logrelG Σ} K e1 Δ' E1 E2 Δ Γ e e2 ϕ t τ :
   PureExec ϕ e1 e2 →
   ϕ →
   Closed ∅ e1 →
-  Closed ∅ e2 →
   nclose specN ⊆ E1 →
   (Δ' ⊢ bin_log_related E1 E2 Δ Γ t (fill K e2) τ) →
   (Δ' ⊢ bin_log_related E1 E2 Δ Γ t e τ).
 Proof.
-  intros Hfill Hpure Hϕ ??? Hp. subst.
+  intros Hfill Hpure Hϕ ?? Hp. subst.
+  assert (Closed ∅ e2).
+  { eapply PureExec_Closed; eauto. }
   rewrite -(bin_log_pure_r Δ Γ E1 E2 K e1 e2 t τ).
   { exact Hp. }
   { assumption. } 
@@ -177,7 +178,6 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
       |apply _                     (* PureExec ϕ e1 e2 *)
       |try (exact I || reflexivity || tac_rel_done)
       |try (simpl; solve_closed)           (* Closed ∅ e1 *)
-      |try (simpl_subst/=; solve_closed)   (* Closed ∅ e2 *) (* we might get subst' here *)
       |solve_ndisj                 (* ↑specN ⊆ E1 *)
       |try iNext; simpl_subst/=    (* new goal *)])
   || fail "rel_pure_r: cannot find the reduct".