Add the `iUnlock` tactic

_CoqProject

@@ -5,6 +5,7 @@ theories/lib/mset.v
 theories/lib/flock.v
 theories/lib/locking_heap.v
 theories/lib/U.v
+theories/lib/unlock_classes.v
 theories/c_translation/monad.v
 theories/c_translation/lifting.v
 theories/c_translation/proofmode.v

theories/c_translation/proofmode.v

@@ -3,6 +3,7 @@ From iris.heap_lang Require Import spin_lock assert par.
 From iris.algebra Require Import frac auth.
 From iris.base_logic.lib Require Import fractional.
 From iris_c.lib Require Import locking_heap mset flock.
+From iris_c.lib Require Export unlock_classes.
 From iris_c.c_translation Require Export monad lifting.
 From iris.proofmode Require Import coq_tactics.
 

theories/lib/unlock_classes.v

+From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Export tactics.
+From iris_c.lib Require Export locking_heap U.
+Import uPred.
+
+Section classes.
+  Context `{heapG Σ, locking_heapG Σ}.
+  Class IntoUnlock (P Q : iProp Σ) :=
+    into_unlock : P ⊢ U Q.
+  Class FromUnlock (P Q : iProp Σ) :=
+    from_unlock : U Q ⊢ P.
+  Global Instance into_unlock_intro P : IntoUnlock (U P) P.
+  Proof. rewrite /IntoUnlock. reflexivity. Qed.
+  Global Instance into_unlock_id P : IntoUnlock P P | 10.
+  Proof. apply U_intro. Qed.
+  Global Instance into_unlock_unlock l v : IntoUnlock (l ↦L v)%I (l ↦U v)%I | 0.
+  Proof. apply U_unlock. Qed.
+  Global Instance from_unlock_unlock P : FromUnlock (U P) P.
+  Proof. rewrite /FromUnlock. reflexivity. Qed.
+
+  Class IntoUnlockEnv (Γ1 Γ2 : env (iProp Σ)) :=
+    into_unlock_env : env_Forall2 IntoUnlock Γ1 Γ2.
+
+  Class IntoUnlockEnvs (Δ1 Δ2 : envs (iResUR Σ)) := {
+    into_unlock_persistent: [∗] (env_persistent Δ1) ⊢ [∗] (env_persistent Δ2);
+    into_unlocks_wf : envs_wf Δ1 → envs_wf Δ2;
+    into_unlock_spatial: IntoUnlockEnv (env_spatial Δ1) (env_spatial Δ2)
+  }.
+
+  Global Instance into_unlock_env_nil : IntoUnlockEnv Enil Enil.
+  Proof. constructor. Qed.
+  Global Instance into_unlock_env_snoc Γ1 Γ2 i P Q :
+    IntoUnlockEnv Γ1 Γ2 → IntoUnlock P Q →
+    IntoUnlockEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
+  Proof. by constructor. Qed.
+
+  Global Instance into_unlock_envs Γp Γs1 Γs2 :
+    IntoUnlockEnv Γs1 Γs2 →
+    IntoUnlockEnvs (Envs Γp Γs1) (Envs Γp Γs2).
+  Proof.
+    split; try done.
+    destruct 1; constructor; try naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
+  Qed.
+
+  Lemma into_unlock_env_sound Δ1 Δ2 :
+    IntoUnlockEnv Δ1 Δ2 → [∗] Δ1 ⊢ U ([∗] Δ2).
+  Proof.
+    intros Hs; simpl.
+    induction Hs; simpl.
+    - apply U_intro.
+    - rewrite -U_multiplicative. by apply uPred.sep_mono.
+  Qed.
+  Lemma into_unlock_envs_sound Δ1 Δ2 :
+    IntoUnlockEnvs Δ1 Δ2 → of_envs Δ1 ⊢ U (of_envs Δ2).
+  Proof.
+    intros [Hp Hs]; rewrite /of_envs /= -!U_multiplicative.
+    repeat apply uPred.sep_mono; try apply uPred.persistently_mono.
+    - rewrite -U_intro. apply uPred.pure_mono. apply Hs.
+    - rewrite -U_intro. by rewrite Hp.
+    - by apply into_unlock_env_sound.
+  Qed.
+
+  Lemma tac_unlock Δ Δ' Q Q' :
+    FromUnlock Q Q' →
+    IntoUnlockEnvs Δ Δ' →
+    envs_entails Δ' Q' → envs_entails Δ Q.
+  Proof.
+    rewrite /envs_entails=> Hf ? HQ.
+    rewrite into_unlock_envs_sound.
+    rewrite /FromUnlock in Hf. rewrite -Hf.
+    by apply U_mono.
+  Qed.
+End classes.
+
+Tactic Notation "iUnlock" :=
+  iStartProof;
+  let P := match goal with |- envs_entails _ ?P => P end in
+  eapply tac_unlock;
+    [apply _ || fail "iUnlock:" P "does not contain U"
+    |apply _
+    |lazy beta (* remove beta redexes caused by removing laters under binders*)].

theories/tests/test1.v

@@ -15,23 +15,23 @@ Section test.
     iIntros "Hl".
     iApply awp_bind.
     iApply a_seq_spec.
-    rewrite U_unlock. iRevert "Hl". rewrite -(U_mono (l ↦U #1) (awp _ _ _))%I. eauto.
-    iIntros "Hl". awp_pure _.
+    iUnlock.
+    awp_lam.
     iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
   Qed.
 
-  Lemma test2 (l : loc) R `{Timeless _ R}:
-    l ↦U #3 -∗
+  Lemma test2 (l r : loc) R `{Timeless _ R}:
+    l ↦U #3 -∗ r ↦L #0 -∗
     awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l))%E R (fun v => ⌜v = #1⌝).
   Proof.
-    iIntros "Hl".
+    iIntros "Hl Hr".
     iApply awp_bind.
     iApply (a_store_spec with "Hl"). iIntros "Hl".
     awp_lam.
     iApply awp_bind.
     iApply a_seq_spec.
-    rewrite U_unlock. iRevert "Hl". rewrite -(U_mono (l ↦U #1) (awp _ _ _))%I. eauto.
-    iIntros "Hl". awp_pure _.
+    iUnlock.
+    awp_lam.
     iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
   Qed.