Merge branch 'ralf/seal' into 'master'

Seal ghost_var and mnat_own

See merge request iris/iris!571

theories/base_logic/lib/ghost_var.v

@@ -15,22 +15,24 @@ Definition ghost_varΣ (A : Type) : gFunctors := #[ GFunctor (frac_agreeR $ leib
 Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
 Proof. solve_inG. Qed.
 
-Section definitions.
-  Context `{!ghost_varG Σ A} (γ : gname).
+Definition ghost_var_def `{!ghost_varG Σ A} (γ : gname) (q : Qp) (a : A) : iProp Σ :=
+  own γ (to_frac_agree (A:=leibnizO A) q a).
+Definition ghost_var_aux : seal (@ghost_var_def). Proof. by eexists. Qed.
+Definition ghost_var := ghost_var_aux.(unseal).
+Definition ghost_var_eq : @ghost_var = @ghost_var_def := ghost_var_aux.(seal_eq).
+Arguments ghost_var {Σ A _} γ q a.
 
-  Definition ghost_var (q : Qp) (a : A) : iProp Σ :=
-    own γ (to_frac_agree (A:=leibnizO A) q a).
-End definitions.
+Local Ltac unseal := rewrite ?ghost_var_eq /ghost_var_def.
 
 Section lemmas.
   Context `{!ghost_varG Σ A}.
   Implicit Types (a : A) (q : Qp).
 
   Global Instance ghost_var_timeless γ q a : Timeless (ghost_var γ q a).
-  Proof. apply _. Qed.
+  Proof. unseal. apply _. Qed.
 
   Global Instance ghost_var_fractional γ a : Fractional (λ q, ghost_var γ q a).
-  Proof. intros q1 q2. rewrite /ghost_var -own_op -frac_agree_op //. Qed.
+  Proof. intros q1 q2. unseal. rewrite -own_op -frac_agree_op //. Qed.
   Global Instance ghost_var_as_fractional γ a q :
     AsFractional (ghost_var γ q a) (λ q, ghost_var γ q a) q.
   Proof. split; [done|]. apply _. Qed.
@@ -38,15 +40,15 @@ Section lemmas.
   Lemma ghost_var_alloc_strong a (P : gname → Prop) :
     pred_infinite P →
     ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_var γ 1 a.
-  Proof. intros. iApply own_alloc_strong; done. Qed.
+  Proof. unseal. intros. iApply own_alloc_strong; done. Qed.
   Lemma ghost_var_alloc a :
     ⊢ |==> ∃ γ, ghost_var γ 1 a.
-  Proof. iApply own_alloc. done. Qed.
+  Proof. unseal. iApply own_alloc. done. Qed.
 
   Lemma ghost_var_valid_2 γ a1 q1 a2 q2 :
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ a1 = a2⌝.
   Proof.
-    iIntros "Hvar1 Hvar2".
+    unseal. iIntros "Hvar1 Hvar2".
     iDestruct (own_valid_2 with "Hvar1 Hvar2") as %[Hq Ha]%frac_agree_op_valid.
     done.
   Qed.
@@ -67,7 +69,7 @@ Section lemmas.
   Lemma ghost_var_update b γ a :
     ghost_var γ 1 a ==∗ ghost_var γ 1 b.
   Proof.
-    iApply own_update. apply cmra_update_exclusive. done.
+    unseal. iApply own_update. apply cmra_update_exclusive. done.
   Qed.
   Lemma ghost_var_update_2 b γ a1 q1 a2 q2 :
     (q1 + q2 = 1)%Qp →
@@ -86,5 +88,3 @@ Section lemmas.
   Proof. iApply ghost_var_update_2. apply Qp_half_half. Qed.
 
 End lemmas.
-
-Typeclasses Opaque ghost_var.

theories/base_logic/lib/mnat.v

@@ -20,24 +20,37 @@ Definition mnatΣ : gFunctors := #[ GFunctor mnat_authR ].
 Instance subG_mnatΣ Σ : subG mnatΣ Σ → mnatG Σ.
 Proof. solve_inG. Qed.
 
-Definition mnat_own_auth `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
+Definition mnat_own_auth_def `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
   own γ (mnat_auth_auth q n).
-Definition mnat_own_lb `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
+Definition mnat_own_auth_aux : seal (@mnat_own_auth_def). Proof. by eexists. Qed.
+Definition mnat_own_auth := mnat_own_auth_aux.(unseal).
+Definition mnat_own_auth_eq : @mnat_own_auth = @mnat_own_auth_def := mnat_own_auth_aux.(seal_eq).
+Arguments mnat_own_auth {Σ _} γ q n.
+
+Definition mnat_own_lb_def `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
   own γ (mnat_auth_frag n).
+Definition mnat_own_lb_aux : seal (@mnat_own_lb_def). Proof. by eexists. Qed.
+Definition mnat_own_lb := mnat_own_lb_aux.(unseal).
+Definition mnat_own_lb_eq : @mnat_own_lb = @mnat_own_lb_def := mnat_own_lb_aux.(seal_eq).
+Arguments mnat_own_lb {Σ _} γ n.
+
+Local Ltac unseal := rewrite
+  ?mnat_own_auth_eq /mnat_own_auth_def
+  ?mnat_own_lb_eq /mnat_own_lb_def.
 
 Section mnat.
   Context `{!mnatG Σ}.
   Implicit Types (n m : nat).
 
   Global Instance mnat_own_auth_timeless γ q n : Timeless (mnat_own_auth γ q n).
-  Proof. apply _. Qed.
+  Proof. unseal. apply _. Qed.
   Global Instance mnat_own_lb_timeless γ n : Timeless (mnat_own_lb γ n).
-  Proof. apply _. Qed.
+  Proof. unseal. apply _. Qed.
   Global Instance mnat_own_lb_persistent γ n : Persistent (mnat_own_lb γ n).
-  Proof. apply _. Qed.
+  Proof. unseal. apply _. Qed.
 
   Global Instance mnat_own_auth_fractional γ n : Fractional (λ q, mnat_own_auth γ q n).
-  Proof. intros p q. rewrite -own_op mnat_auth_auth_frac_op //. Qed.
+  Proof. unseal. intros p q. rewrite -own_op mnat_auth_auth_frac_op //. Qed.
 
   Global Instance mnat_own_auth_as_fractional γ q n :
     AsFractional (mnat_own_auth γ q n) (λ q, mnat_own_auth γ q n) q.
@@ -46,21 +59,21 @@ Section mnat.
   Lemma mnat_own_auth_agree γ q1 q2 n1 n2 :
     mnat_own_auth γ q1 n1 -∗ mnat_own_auth γ q2 n2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
   Proof.
-    iIntros "H1 H2".
+    unseal. iIntros "H1 H2".
     iDestruct (own_valid_2 with "H1 H2") as %?%mnat_auth_frac_op_valid; done.
   Qed.
 
   Lemma mnat_own_auth_exclusive γ n1 n2 :
     mnat_own_auth γ 1 n1 -∗ mnat_own_auth γ 1 n2 -∗ False.
   Proof.
-    iIntros "H1 H2".
+    unseal. iIntros "H1 H2".
     iDestruct (own_valid_2 with "H1 H2") as %[]%mnat_auth_auth_op_valid.
   Qed.
 
   Lemma mnat_own_lb_valid γ q n m :
     mnat_own_auth γ q n -∗ mnat_own_lb γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
   Proof.
-    iIntros "Hauth Hlb".
+    unseal. iIntros "Hauth Hlb".
     iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mnat_auth_both_frac_valid.
     auto.
   Qed.
@@ -71,16 +84,17 @@ Section mnat.
   "Hauth") as "#Hfrag"]. *)
   Lemma mnat_get_lb γ q n :
     mnat_own_auth γ q n -∗ mnat_own_lb γ n.
-  Proof. apply own_mono, mnat_auth_included. Qed.
+  Proof. unseal. apply own_mono, mnat_auth_included. Qed.
 
   Lemma mnat_own_lb_le γ n n' :
     n' ≤ n →
     mnat_own_lb γ n -∗ mnat_own_lb γ n'.
-  Proof. intros. by apply own_mono, mnat_auth_frag_mono. Qed.
+  Proof. unseal. intros. by apply own_mono, mnat_auth_frag_mono. Qed.
 
   Lemma mnat_alloc n :
     ⊢ |==> ∃ γ, mnat_own_auth γ 1 n ∗ mnat_own_lb γ n.
   Proof.
+    unseal.
     iMod (own_alloc (mnat_auth_auth 1 n ⋅ mnat_auth_frag n)) as (γ) "[??]".
     { apply mnat_auth_both_valid; auto. }
     auto with iFrame.
@@ -89,7 +103,7 @@ Section mnat.
   Lemma mnat_update n' γ n :
     n ≤ n' →
     mnat_own_auth γ 1 n ==∗ mnat_own_auth γ 1 n'.
-  Proof. intros. by apply own_update, mnat_auth_update. Qed.
+  Proof. unseal. intros. by apply own_update, mnat_auth_update. Qed.
 
   Lemma mnat_update_with_lb γ n n' :
     n ≤ n' →
@@ -100,5 +114,3 @@ Section mnat.
     iDestruct (mnat_get_lb with "Hauth") as "#Hlb"; auto.
   Qed.
 End mnat.
-
-Typeclasses Opaque mnat_own_auth mnat_own_lb.