A bit of cleanup

theories/examples/lock.v

@@ -142,18 +142,6 @@ Section lock_rules_r.
   Variable (E1 E2 : coPset).
   Variable (Δ : list (prodC valC valC -n> iProp Σ)).
 
-  Lemma steps_newlock ρ j K
-    (Hcl : nclose specN ⊆ E1) :
-    spec_ctx ρ -∗ j ⤇ fill K (newlock #())
-    ={E1}=∗ ∃ l : loc, j ⤇ fill K (of_val #l) ∗ l ↦ₛ #false.
-  Proof.
-    iIntros "#Hspec Hj".
-    unfold newlock. unlock.
-    tp_rec j. simpl.
-    tp_alloc j as l "Hl". tp_normalise j.
-    by iExists _; iFrame.
-  Qed.
-
   Lemma bin_log_related_newlock_r Γ K t τ 
     (Hcl : nclose specN ⊆ E1) :
     (∀ l : loc, l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #l : τ) -∗
@@ -180,19 +168,7 @@ Section lock_rules_r.
   Global Opaque newlock.
   
   Transparent acquire. 
-  Lemma steps_acquire ρ j K l
-    (Hcl : nclose specN ⊆ E1) :
-    spec_ctx ρ -∗ l ↦ₛ #false -∗ j ⤇ fill K (acquire #l)
-    ={E1}=∗ j ⤇ fill K Unit ∗ l ↦ₛ #true.
-  Proof.
-    iIntros "#Hspec Hl Hj". 
-    unfold acquire. unlock.
-    tp_rec j.
-    tp_cas_suc j. simpl.
-    tp_if_true j.
-    by iFrame.
-  Qed.
-  
+ 
   Lemma bin_log_related_acquire_r Γ K l t τ
     (Hcl : nclose specN ⊆ E1) :
     l ↦ₛ #false -∗
@@ -245,17 +221,6 @@ Section lock_rules_r.
   Global Opaque acquire.
 
   Transparent release.
-  Lemma steps_release ρ j K l (b : bool)
-    (Hcl : nclose specN ⊆ E1) :
-    spec_ctx ρ -∗ l ↦ₛ #b -∗ j ⤇ fill K (release #l)
-    ={E1}=∗ j ⤇ fill K #() ∗ l ↦ₛ #false.
-  Proof.
-    iIntros "#Hspec Hl Hj". unfold release. unlock.
-    tp_rec j.
-    tp_store j.
-    by iFrame.
-  Qed.
-
   Lemma bin_log_related_release_r Γ K l t τ (b : bool)
     (Hcl : nclose specN ⊆ E1) :
     l ↦ₛ #b -∗
@@ -270,34 +235,6 @@ Section lock_rules_r.
   Qed.
 
   Global Opaque release.
-
-  Lemma steps_with_lock ρ j K e ev l P Q v w:
-    to_val e = Some ev →
-    (∀ K', spec_ctx ρ -∗ P -∗ j ⤇ fill K' (App e (of_val w))
-            ={E1}=∗ j ⤇ fill K' (of_val v) ∗ Q) →
-    (nclose specN ⊆ E1) →
-    spec_ctx ρ -∗ P -∗ l ↦ₛ #false -∗
-    j ⤇ fill K (with_lock e #l w)
-    ={E1}=∗ j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ #false.
-  Proof.
-    iIntros (Hev Hpf ?) "#Hspec HP Hl Hj".
-    unfold with_lock. unlock.
-    tp_rec j.
-    tp_rec j.
-    tp_rec j.
-    tp_bind j (App acquire (# l)).
-    tp_apply j steps_acquire with "Hl" as "Hl".
-    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.
-    tp_bind j (App release _).    
-    tp_apply j steps_release with "Hl" as "Hl".
-    tp_normalise j.
-    tp_rec j.
-    by iFrame.
-  Qed.
   
   Lemma bin_log_related_with_lock_r Γ K Q e ev ew cl v w l t τ :
     (to_val e = Some cl) →

theories/logrel/proofmode/tactics_rel.v

@@ -395,10 +395,10 @@ Tactic Notation "rel_store_l" :=
     |simpl; reflexivity  (* eres = fill K () *)
     |simpl (* new goal *)].
 
-Lemma tac_rel_store_r `{logrelG Σ} ℶ1 ℶ2 E1 E2 Δ Γ K i1 (l : loc) t' v' e t tres τ v :
+Lemma tac_rel_store_r `{logrelG Σ} ℶ1 ℶ2 E1 E2 Δ Γ K i1 (l : loc) v' e e' t tres τ v :
   nclose specN ⊆ E1 →
-  t = fill K (Store (# l) t') →
-  to_val t' = Some v' →
+  t = fill K (Store (# l) e') →
+  to_val e' = Some v' →
   envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
   envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) ℶ1 = Some ℶ2 →
   tres = fill K Unit →

theories/logrel/rules.v

@@ -289,12 +289,12 @@ Section properties.
     done.
   Qed.
 
-  Lemma bin_log_related_store_r Δ Γ E1 E2 K l e v v' t τ
+  Lemma bin_log_related_store_r Δ Γ E1 E2 K l e e' v v' τ
     (Hmasked : nclose specN ⊆ E1) :
-    to_val e = Some v' →
+    to_val e' = Some v' →
     l ↦ₛ v -∗
-    (l ↦ₛ v' -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#()) : τ)
-    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#l <- e) : τ.
+    (l ↦ₛ v' -∗ {E1,E2;Δ;Γ} ⊨ e ≤log≤ fill K (#()) : τ) -∗
+    {E1,E2;Δ;Γ} ⊨ e ≤log≤ fill K (#l <- e') : τ.
   Proof.
     iIntros (?) "Hl Hlog".
     pose (Φ := (fun w => ⌜w = #()⌝ ∗ l ↦ₛ v')%I).