upd

theories/axiomatic/logrel/ghost_state.v

@@ -49,9 +49,8 @@ Section derived.
 End derived.
 
 (** ** The mono nat ghost theory *)
-Notation mono_nat_lb := mono_nat_lb_own.
-Check mono_nat_auth.
-Check mono_nat_lb.
+Check mono.
+Check lb.
 
 Check mono_nat_make_bound.
 Check mono_nat_use_bound.
@@ -59,10 +58,10 @@ Check mono_nat_increase_val.
 Check mono_nat_new.
 
 (* The lb resource is persistent *)
-Check mono_nat_lb_own_persistent.
+Check mono_nat_lb_persistent.
 (* Both resources are also timeless *)
-Check mono_nat_lb_own_timeless.
-Check mono_nat_auth_own_timeless.
+Check mono_nat_lb_timeless.
+Check mono_nat_mono_timeless.
 
 Section mono_derived.
 (** In addition to the known [heapGS] assumption, we now also need to assume that the ghost state for the theory of mono_nat has been registered with Iris, expressed through the [mono_natG] assumption.
@@ -72,15 +71,15 @@ Section mono_derived.
 
   Lemma mono_nat_increase γ n m :
     n ≤ m →
-    mono_nat_auth γ n -∗ |==> mono_nat_auth γ m.
+    mono γ n -∗ |==> mono γ m.
   Proof.
-    (* FIXME exercise *)
+    (* FIXME: exercise *)
   Admitted.
 
   Lemma mono_nat_increase_wp γ n m e Φ :
     n ≤ m →
-    (mono_nat_auth γ m -∗ WP e {{ Φ }}) -∗
-    (mono_nat_auth γ n -∗ WP e {{ Φ }}).
+    (mono γ m -∗ WP e {{ Φ }}) -∗
+    (mono γ n -∗ WP e {{ Φ }}).
   Proof.
     iIntros (Hle) "He Hauth".
     iApply upd_wp. iApply (upd_wand with "[Hauth]"); last iApply "He".
@@ -88,9 +87,9 @@ Section mono_derived.
   Qed.
 
   Lemma mono_nat_new_wp e Φ n :
-    (∀ γ, mono_nat_auth γ n -∗ WP e {{ Φ }}) -∗ WP e {{ Φ }}.
+    (∀ γ, mono γ n -∗ WP e {{ Φ }}) -∗ WP e {{ Φ }}.
   Proof.
-    (* FIXME: exercise *)
+    (* FIXME exercise *)
   Admitted.
 End mono_derived.
 
@@ -100,8 +99,8 @@ Section ipm.
   Implicit Types (P Q : iProp Σ).
 
   Lemma update_ipm_1 γ n :
-    mono_nat_auth γ 0 -∗
-    |==> mono_nat_auth γ n.
+    mono γ 0 -∗
+    |==> mono γ n.
   Proof.
     iIntros "Hauth".
     (* [iMod] will eliminate an update modality in front of the hypothesis (using [upd_bind]) *)
@@ -114,8 +113,8 @@ Section ipm.
   Abort.
 
   Lemma update_ipm_2 γ n e Φ  :
-    mono_nat_auth γ 0 -∗
-    (mono_nat_auth γ n -∗ WP e {{ Φ }}) -∗
+    mono γ 0 -∗
+    (mono γ n -∗ WP e {{ Φ }}) -∗
     WP e {{ Φ }}.
   Proof.
     iIntros "Hauth He".
@@ -125,7 +124,7 @@ Section ipm.
   Abort.
 
   Lemma update_ipm_3 n γ :
-    (|==> mono_nat_auth γ n) -∗ |==> mono_nat_auth γ (S n).
+    (|==> mono γ n) -∗ |==> mono γ (S n).
   Proof.
     (* the [>] intro pattern will eliminate an update when introducing an assumption *)
     iIntros ">Hauth". by iApply mono_nat_increase_val.
@@ -148,9 +147,9 @@ Section logrel_symbol.
   Definition symbolN := nroot .@ "symbol".
 
   Definition mono_nat_inv γ l : iProp Σ :=
-    ∃ n : nat, l ↦ #n ∗ mono_nat_auth γ n.
+    ∃ n : nat, l ↦ #n ∗ mono γ n.
   Definition mono_natT γ : semtypeO :=
-    mk_semtype (λ v, ∃ (n : nat), ⌜v = #n⌝ ∗ mono_nat_lb_own γ n)%I.
+    mk_semtype (λ v, ∃ (n : nat), ⌜v = #n⌝ ∗ lb γ n)%I.
 
   Lemma mk_symbol_semtyped :
     TY 0; ∅ ⊨ mk_symbol : symbolT.
@@ -161,13 +160,13 @@ Section logrel_symbol.
     subst γ. rewrite subst_map_empty. unfold mk_symbol. simpl.
     wp_alloc l as "Hl". wp_pures.
     (* We allocate the ghost state + invariant *)
-    iMod (mono_nat_own_alloc 0) as "(%γ & Hauth & _)".
+    iMod (mono_nat_new 0) as "(%γ & Hauth)".
     iApply (inv_alloc symbolN (mono_nat_inv γ l) with "[Hauth Hl]").
     { unfold mono_nat_inv. eauto with iFrame. }
     iIntros "#HInv".
     iApply wp_value.
-    iExists _. iSplit; first done.
-    iExists (mono_natT γ), _, _. iSplit; first done. iSplit.
+    iExists _. iSplitR; first done.
+    iExists (mono_natT γ), _, _. iSplitR; first done. iSplit.
     - (* mkSym *)
       iIntros (w) "!> ->".
       wp_pures. iApply (inv_open with "HInv"); first set_solver.
@@ -190,7 +189,6 @@ Section logrel_symbol.
   Qed.
 End logrel_symbol.
 
-
 (** Exercise: Oneshot *)
 Section logrel_oneshot.
   Import logrel.notation syntactic logrel.

theories/axiomatic/logrel/ghost_state_lib.v

@@ -40,35 +40,54 @@ End updates.
 Section mononat.
   Context `{heapGS Σ} `{mono_natG Σ}.
 
-  Definition mono_nat_auth γ n := mono_nat_auth_own γ 1%Qp n.
-  Notation mono_nat_lb := mono_nat_lb_own.
+  Definition mono_def γ n := mono_nat_auth_own γ 1%Qp n.
+  Definition mono_aux : seal (@mono_def). Proof. by eexists. Qed.
+  Definition mono := mono_aux.(unseal).
+  Definition mono_eq : @mono = @mono_def := mono_aux.(seal_eq).
+
+  Definition lb_def := mono_nat_lb_own.
+  Definition lb_aux : seal (@lb_def). Proof. by eexists. Qed.
+  Definition lb := lb_aux.(unseal).
+  Definition lb_eq : @lb = @lb_def := lb_aux.(seal_eq).
 
   Lemma mono_nat_make_bound γ n :
-    mono_nat_auth γ n -∗ mono_nat_lb γ n.
+    mono γ n -∗ lb γ n.
   Proof.
+    rewrite mono_eq lb_eq.
     iApply mono_nat_lb_own_get.
   Qed.
 
   Lemma mono_nat_use_bound γ n m :
-    mono_nat_auth γ n -∗ mono_nat_lb γ m -∗ ⌜n ≥ m⌝.
+    mono γ n -∗ lb γ m -∗ ⌜n ≥ m⌝.
   Proof.
+    rewrite mono_eq lb_eq.
     iIntros "Hauth Hlb". iPoseProof (mono_nat_lb_own_valid with "Hauth Hlb") as "(_ & $)".
   Qed.
 
   Lemma mono_nat_increase_val γ n :
-    mono_nat_auth γ n -∗ |==> mono_nat_auth γ (S n).
+    mono γ n -∗ |==> mono γ (S n).
   Proof.
+    rewrite mono_eq.
     iIntros "Hauth".
     iMod (mono_nat_own_update with "Hauth") as "($ & _)"; eauto.
   Qed.
 
   Lemma mono_nat_new n :
-    ⊢ |==> ∃ γ, mono_nat_auth γ n.
+    ⊢ |==> ∃ γ, mono γ n.
   Proof.
+    rewrite mono_eq.
     iMod (mono_nat_own_alloc n) as "(%γ & ? & _)"; eauto with iFrame.
   Qed.
+
+  Global Instance mono_nat_lb_persistent γ n : Persistent (lb γ n).
+  Proof. rewrite lb_eq. apply _. Qed.
+  Global Instance mono_nat_lb_timeless γ n : Timeless (lb γ n).
+  Proof. rewrite lb_eq. apply _. Qed.
+  Global Instance mono_nat_mono_timeless γ n : Timeless (mono γ n).
+  Proof. rewrite mono_eq. apply _. Qed.
 End mononat.
 
+
 (** Half algebra: provides two halves *)
 Class halvesG Σ (A : Type) := HalvesG { halvesG_ghost_varG :> ghost_varG Σ A; }.
 Definition halvesΣ A : gFunctors := ghost_varΣ A.