Define substitution on reified syntax

- This allows us to get rid of `rewrite !Closed_subst_id.`

F_mu_ref_conc/examples/counter.v

@@ -49,8 +49,7 @@ Section CG_Counter.
     {E1,E2;Γ} ⊨ t ≤log≤ fill K ((CG_increment $/ LocV x $/ LocV l) Unit)%E : τ)%I.
   Proof.
     iIntros (?) "Hx Hl Hlog".
-    unfold CG_increment. unlock. simpl.
-    rewrite !Closed_subst_id.
+    unfold CG_increment. unlock. simpl_subst/=.
     rel_rec_r.
     rel_bind_r (acquire #l).
     iApply (bin_log_related_acquire_r with "Hl"); eauto. iIntros "Hl". simpl.
@@ -222,11 +221,10 @@ Section CG_Counter.
   Proof.
     iIntros "#Hinv".
     iApply bin_log_related_arrow.
-    { unfold FG_increment. unlock; simpl. reflexivity. }
-    { unfold CG_increment. unlock; simpl. reflexivity. }
-    { unfold FG_increment. unlock; simpl. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
-    { unfold CG_increment. unlock; simpl.
-      rewrite !Closed_subst_id. solve_closed. }
+    { unfold FG_increment. unlock; simpl_subst. reflexivity. }
+    { unfold CG_increment. unlock; simpl_subst. reflexivity. }
+    { unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
+    { unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
 
     iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
     iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
@@ -300,13 +298,12 @@ Section CG_Counter.
     iApply (bin_log_related_pair _ with "[]").
     - rel_rec_l.
       rel_rec_r.
-      unfold CG_increment. unlock; simpl. rewrite !Closed_subst_id.
+      unfold CG_increment. unlock; simpl_subst/=.
       rel_rec_r.
       replace (λ: <>, acquire #l ;; #cnt' <- BinOp Add (Nat 1) (! #cnt');; release #l)%E
-        with (CG_increment $/ LocV cnt' $/ LocV l)%E.
+        with (CG_increment $/ LocV cnt' $/ LocV l)%E; last first.
+      { unfold CG_increment. unlock; simpl_subst/=. reflexivity. }
       iApply (FG_CG_increment_refinement with "Hinv").
-      { unfold CG_increment. unlock; simpl.
-        rewrite !Closed_subst_id. reflexivity. }
     - rel_rec_l.
       rel_rec_r.
       iApply (counter_read_refinement with "Hinv").

F_mu_ref_conc/examples/lock.v

@@ -87,9 +87,9 @@ Section proof.
   Proof.
     iIntros "#Hspec Hl Hj". 
     unfold acquire.
-    tp_rec j. 
+    tp_rec j.
     tp_cas_suc j. 
-    tp_if_true j. tp_normalise j.    
+    tp_if_true j.
     by iFrame.
   Qed.
   
@@ -100,7 +100,6 @@ Section proof.
     -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
-    unfold acquire.
     rel_rec_r.
     rel_cas_suc_r. simpl.
     rel_if_r.
@@ -147,24 +146,20 @@ Section proof.
   Proof.
     iIntros (Hev Hpf ?) "#Hspec HP Hl Hj".
     unfold with_lock. unlock. (* TODO :( *)
-    tp_rec j; eauto; simpl.
-    rewrite !Closed_subst_id. (* simplify subst automatically? *)
-    tp_rec j; eauto; simpl.
-    rewrite !Closed_subst_id.    
-    tp_rec j; eauto using to_of_val; simpl.
-    rewrite !Closed_subst_id.    
+    tp_rec j.
+    tp_rec j.
+    tp_rec j; eauto using to_of_val.
     tp_bind j (App acquire (Loc l)).
     tp_apply j steps_acquire with "Hl" as "Hl".
-    tp_rec j. simpl.
+    tp_rec j.
     tp_bind j (App e _).
     iMod (Hpf with "Hspec HP Hj") as "[Hj HQ]". 
     tp_normalise j.
-    tp_rec j; eauto using to_of_val; simpl.
-    rewrite !Closed_subst_id.
+    tp_rec j; eauto using to_of_val.
     tp_bind j (App release _).    
     tp_apply j steps_release with "Hl" as "Hl".
     tp_normalise j.
-    tp_rec j; simpl.
+    tp_rec j.
     by iFrame.
   Qed.
   
@@ -182,23 +177,22 @@ Section proof.
     iIntros (????) "HA Hl Hlog".
     rel_bind_r (with_lock e).
     unfold with_lock. unlock. (*TODO: unlock here needed *)
-    iApply (bin_log_related_rec_r); eauto. simpl. rewrite !Closed_subst_id.
+    iApply (bin_log_related_rec_r); eauto. simpl_subst.
     rel_bind_r (App _ (#l)%E).
-    iApply (bin_log_related_rec_r); eauto. simpl. rewrite !Closed_subst_id.
-    iApply (bin_log_related_rec_r); eauto. simpl. rewrite !Closed_subst_id.
+    iApply (bin_log_related_rec_r); eauto. simpl_subst.
+    iApply (bin_log_related_rec_r); eauto. simpl_subst.
     rel_bind_r (App acquire (Loc l)).
     iApply (bin_log_related_acquire_r Γ (_ :: K) l with "Hl"); auto.
     iIntros "Hl". simpl.
-    iApply (bin_log_related_rec_r); eauto. simpl.
+    iApply (bin_log_related_rec_r); eauto. simpl_subst/=.
     rel_bind_r (App e ew).
     iApply "HA". iIntros "HQ". simpl.
-    iApply (bin_log_related_rec_r); eauto. simpl. rewrite !Closed_subst_id.
+    iApply (bin_log_related_rec_r); eauto. simpl_subst.
     rel_bind_r (App release _).
     iApply (bin_log_related_release_r with "Hl"); eauto.
     iIntros "Hl". simpl.
-    iApply (bin_log_related_rec_r); eauto. simpl.
+    iApply (bin_log_related_rec_r); eauto. simpl_subst.
     iApply ("Hlog" with "HQ Hl").
   Qed.
 
-  Global Opaque with_lock.
 End proof.

F_mu_ref_conc/lang.v

@@ -8,7 +8,6 @@ Module lang.
 
   Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
 
-
   (** ** Expressions *)
   Inductive binop := Add | Sub | Eq | Le | Lt.
 
@@ -428,3 +427,7 @@ Ltac solve_atomic :=
 
 Hint Extern 0 (language.atomic _) => solve_atomic.
 Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
+
+(* This lemma is helpful for tactics on locked values and for reifying locked values. *)
+Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
+Proof. by unlock. Qed.

F_mu_ref_conc/reflection.v

@@ -3,7 +3,7 @@ From stdpp Require Import strings gmap mapset stringmap.
 Import lang.
 
 Module R.
-  Inductive expr :=
+Inductive expr :=
   | Val (v : lang.val)
   | ClosedExpr (e : lang.expr) `{Closed ∅ e}  
   | Var (x : string)
@@ -144,6 +144,51 @@ Proof.
   - intros. eapply is_closed_weaken; eauto. set_solver.
 Qed.
 
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | Val _ => e
+  | ClosedExpr _ _ => e
+  | Var y => if decide (x = y) then es else Var y
+  | Rec f y e =>
+    Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
+  | TLam e => TLam (subst x es e)
+  | TApp e => TApp (subst x es e)
+  | Lit l => Lit l
+  | Loc l => Loc l
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
+  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
+  | Fst e => Fst (subst x es e)
+  | Snd e => Snd (subst x es e)
+  | Fold e => Fold (subst x es e)
+  | Unfold e => Unfold (subst x es e)
+  | Pack e => Pack (subst x es e)
+  | Unpack e0 e =>
+    Unpack (subst x es e0) (subst x es e)
+  | InjL e => InjL (subst x es e)
+  | InjR e => InjR (subst x es e)
+  | Case e0 e1 e2 =>
+    Case (subst x es e0)
+         (subst x es e1)
+         (subst x es e2)
+  | Fork e => Fork (subst x es e)
+  | Alloc e => Alloc (subst x es e)
+  | Load e => Load (subst x es e)
+  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
+  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
+  end.
+
+Lemma subst_correct x es e :
+  lang.subst x (to_expr es) (to_expr e) = to_expr (subst x es e).
+Proof.
+  induction e; cbn; try (congruence || naive_solver).
+  - by rewrite (@Closed_subst_id _ _ _ (of_val_closed v)).
+  - by rewrite (@Closed_subst_id _ _ _ H).
+  - case_match; eauto.
+  - case_match; eauto. congruence.
+Qed.
+
 End R.
 
 Ltac solve_closed :=
@@ -156,4 +201,18 @@ Ltac solve_closed :=
      eapply R.is_closed_correct; vm_compute; exact I
   end.
 Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
+
+Ltac simpl_subst :=
+  cbn[subst'];
+  repeat match goal with
+  | |- context [subst ?x ?er ?e] =>
+      let er' := R.of_expr er in let e' := R.of_expr e in
+      change (subst x er e) with (subst x (R.to_expr er') (R.to_expr e'));
+      rewrite (R.subst_correct x); simpl
+  end;
+  unfold R.to_expr.
+Tactic Notation "simpl_subst/=" := simpl; simpl_subst.
+
+(* TODO: the following breaks a lot of shit *)
+(* Arguments subst : simpl never. *)
 Arguments R.to_expr : simpl never.

F_mu_ref_conc/rel_tactics.v

@@ -6,9 +6,6 @@ From iris_logrel.F_mu_ref_conc Require Export lang tactics logrel_binary relatio
 Set Default Proof Using "Type".
 Import lang.
 
-Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
-Proof. by unlock. Qed.
-
 (* Applied to goals that are equalities of expressions. Will try to unlock the
    LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
 Ltac solve_of_val_unlock := try apply of_val_unlock; fast_done.
@@ -106,7 +103,7 @@ Tactic Notation "rel_rec_l" :=
         |try solve_closed
         |fast_done (* to_val e' = Some v *)
         |try fast_done (* eres = subst ... *)
-        |simpl; rewrite ?Closed_subst_id; iNext (* new goal *)]
+        |try simpl_subst/=; iNext (* new goal *)]
       end)
   || fail "rel_rec_l: cannot find '(λx.e) ..'".
 
@@ -612,7 +609,7 @@ Tactic Notation "rel_rec_r" :=
         |try solve_closed
         |fast_done (* to_val e' = Some v *)
         |try fast_done (* eres = subst ... *)
-        |simpl; rewrite ?Closed_subst_id (* new goal *)]
+        |try simpl_subst/= (* new goal *)]
       end)
   || fail "rel_rec_r: cannot find '(λx.e) ..'".
 

F_mu_ref_conc/tactics.v

@@ -128,10 +128,10 @@ Tactic Notation "tp_normalise" constr(j) :=
     | lazymatch goal with
       | |- fill ?K ?e = _ =>
           by rewrite /= ?fill_app /=
-      (* | |- ?e = _ => rewrite /= ?fill_nil /= *)
+      | |- ?e = _ => try fast_done
       end
     |env_cbv; reflexivity
-    |(* new goal *)].
+    |try simpl_subst (* new goal *)].
 
 Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
   iStartProof;
@@ -279,7 +279,7 @@ Tactic Notation "tp_rec" constr(j) :=
     |try fast_done
     |try solve_closed
     |env_cbv; reflexivity || fail "tp_rec: this should not happen"
-    |(* new goal *)]. 
+    |simpl_subst (* new goal *)].
 
 
 Lemma tac_tp_nat_binop `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e op a b Q :
@@ -1006,7 +1006,7 @@ Proof.
   tp_normalise j.
   tp_cas_suc k; tp_normalise k.
   tp_if_true k; tp_normalise k. 
-  tp_rec k; tp_normalise k.
+  tp_rec k. tp_normalise k.
   tp_fst k; tp_normalise k.
   iExists k.
   done.