Merge branch 'robbert/mnat' into 'master'

Include fragment in `mnat_auth_auth`

See merge request iris/iris!569

theories/algebra/lib/mnat_auth.v

@@ -9,26 +9,27 @@ Definition mnat_auth   := auth max_natUR.
 Definition mnat_authR  := authR max_natUR.
 Definition mnat_authUR := authUR max_natUR.
 
+(** [mnat_auth_auth] is the authoritative element. The definition includes the
+fragment at the same value so that lemma [mnat_auth_included], which states that
+[mnat_auth_frag n ≼ mnat_auth_auth q n], does not require a frame-preserving
+update. *)
+Definition mnat_auth_auth (q : Qp) (n : nat) : mnat_auth :=
+  ●{q} MaxNat n ⋅ ◯ MaxNat n.
+Definition mnat_auth_frag (n : nat) : mnat_auth := ◯ MaxNat n.
+
 Section mnat_auth.
   Implicit Types (n : nat).
 
-  Definition mnat_auth_auth (q : Qp) (n : nat) : mnat_auth := ●{q} MaxNat n.
-  Definition mnat_auth_frag          (n : nat) : mnat_auth := ◯ MaxNat n.
-
   Global Instance mnat_auth_frag_core_id n : CoreId (mnat_auth_frag n).
   Proof. apply _. Qed.
 
   Lemma mnat_auth_auth_frac_op q1 q2 n :
     mnat_auth_auth q1 n ⋅ mnat_auth_auth q2 n ≡ mnat_auth_auth (q1 + q2) n.
-  Proof. rewrite /mnat_auth_auth auth_auth_frac_op //. Qed.
-
-  Lemma mnat_auth_auth_op_valid n1 n2 :
-    ✓ (mnat_auth_auth 1 n1 ⋅ mnat_auth_auth 1 n2) ↔ False.
-  Proof. rewrite auth_auth_op_valid //. Qed.
-
-  Lemma mnat_auth_frac_op_valid q1 q2 n1 n2 :
-    ✓ (mnat_auth_auth q1 n1 ⋅ mnat_auth_auth q2 n2) ↔ ✓ (q1 + q2)%Qp ∧ n1 = n2.
-  Proof. rewrite auth_auth_frac_op_valid. naive_solver. Qed.
+  Proof.
+    rewrite /mnat_auth_auth auth_auth_frac_op.
+    rewrite (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    by rewrite -core_id_dup (comm _ (◯ _)).
+  Qed.
 
   Lemma mnat_auth_frag_op n1 n2 :
     mnat_auth_frag n1 ⋅ mnat_auth_frag n2 = mnat_auth_frag (n1 `max` n2).
@@ -39,38 +40,50 @@ Section mnat_auth.
   Lemma mnat_auth_frag_op_le_l n n' :
     n' ≤ n →
     mnat_auth_frag n = mnat_auth_frag n' ⋅ mnat_auth_frag n.
+  Proof. intros. rewrite mnat_auth_frag_op Nat.max_r //. Qed.
+
+  Lemma mnat_auth_frac_op_valid q1 q2 n1 n2 :
+    ✓ (mnat_auth_auth q1 n1 ⋅ mnat_auth_auth q2 n2) ↔ ✓ (q1 + q2)%Qp ∧ n1 = n2.
   Proof.
-    intros Hle.
-    rewrite mnat_auth_frag_op.
-    rewrite Nat.max_r //.
+    rewrite /mnat_auth_auth (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
+    - move=> /cmra_valid_op_l /auth_auth_frac_op_valid. naive_solver.
+    - intros [? ->]. rewrite -core_id_dup -auth_auth_frac_op.
+      by apply auth_both_frac_valid_discrete.
   Qed.
 
+  Lemma mnat_auth_auth_op_valid n1 n2 :
+    ✓ (mnat_auth_auth 1 n1 ⋅ mnat_auth_auth 1 n2) ↔ False.
+  Proof. rewrite mnat_auth_frac_op_valid. naive_solver. Qed.
+
   Lemma mnat_auth_both_frac_valid q n m :
     ✓ (mnat_auth_auth q n ⋅ mnat_auth_frag m) ↔ ✓ q ∧ m ≤ n.
   Proof.
-    rewrite auth_both_frac_valid_discrete.
-    rewrite max_nat_included /=.
-    naive_solver.
+    rewrite /mnat_auth_auth /mnat_auth_frag -assoc -auth_frag_op.
+    rewrite auth_both_frac_valid_discrete max_nat_included /=.
+    naive_solver lia.
   Qed.
 
   Lemma mnat_auth_both_valid n m :
     ✓ (mnat_auth_auth 1 n ⋅ mnat_auth_frag m) ↔ m ≤ n.
   Proof. rewrite mnat_auth_both_frac_valid frac_valid'. naive_solver. Qed.
 
+  Lemma mnat_auth_frag_mono n1 n2 : n1 ≤ n2 → mnat_auth_frag n1 ≼ mnat_auth_frag n2.
+  Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
+
   Lemma mnat_auth_auth_valid n : ✓ mnat_auth_auth 1 n.
-  Proof. apply auth_auth_valid; done. Qed.
+  Proof. by apply auth_both_valid. Qed.
+
+  Lemma mnat_auth_included q n : mnat_auth_frag n ≼ mnat_auth_auth q n.
+  Proof. apply cmra_included_r. Qed.
 
   Lemma mnat_auth_update n n' :
     n ≤ n' →
-    mnat_auth_auth 1 n ~~> mnat_auth_auth 1 n' ⋅ mnat_auth_frag n'.
+    mnat_auth_auth 1 n ~~> mnat_auth_auth 1 n'.
   Proof.
-    intros Hle.
-    apply auth_update_alloc, max_nat_local_update; done.
+    intros. rewrite /mnat_auth_auth /mnat_auth_frag.
+    by apply auth_update, max_nat_local_update.
   Qed.
-
-  Lemma mnat_auth_alloc_frag q n :
-    mnat_auth_auth q n ~~> mnat_auth_auth q n ⋅ mnat_auth_frag n.
-  Proof. by apply (auth_update_frac_alloc _ _ _). Qed.
 End mnat_auth.
 
 Typeclasses Opaque mnat_auth_auth mnat_auth_frag.

theories/algebra/numbers.v

@@ -46,6 +46,7 @@ End nat.
 
 (** ** Natural numbers with [max] as the operation. *)
 Record max_nat := MaxNat { max_nat_car : nat }.
+Add Printing Constructor max_nat.
 
 Canonical Structure max_natO := leibnizO max_nat.
 
@@ -101,6 +102,7 @@ End max_nat.
 
 (** ** Natural numbers with [min] as the operation. *)
 Record min_nat := MinNat { min_nat_car : nat }.
+Add Printing Constructor min_nat.
 
 Canonical Structure min_natO := leibnizO min_nat.
 

theories/base_logic/lib/mnat.v

@@ -20,11 +20,8 @@ Definition mnatΣ : gFunctors := #[ GFunctor mnat_authR ].
 Instance subG_mnatΣ Σ : subG mnatΣ Σ → mnatG Σ.
 Proof. solve_inG. Qed.
 
-(** [mnat_own_auth] is the authoritative nat. The definition includes the
-fragment at the same value so that [mnat_get_lb] does not require an
-update modality. *)
 Definition mnat_own_auth `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
-  own γ (mnat_auth_auth q n ⋅ mnat_auth_frag n).
+  own γ (mnat_auth_auth q n).
 Definition mnat_own_lb `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
   own γ (mnat_auth_frag n).
 
@@ -40,11 +37,7 @@ Section mnat.
   Proof. apply _. Qed.
 
   Global Instance mnat_own_auth_fractional γ n : Fractional (λ q, mnat_own_auth γ q n).
-  Proof.
-    rewrite /mnat_own_auth. setoid_rewrite own_op.
-    apply fractional_sep; [|apply _].
-    intros p q. rewrite -own_op mnat_auth_auth_frac_op //.
-  Qed.
+  Proof. 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.
@@ -53,61 +46,50 @@ Section mnat.
   Lemma mnat_own_auth_agree γ q1 q2 n1 n2 :
     mnat_own_auth γ q1 n1 -∗ mnat_own_auth γ q2 n2 -∗ ⌜✓ (q1 + q2)%Qp ∧ n1 = n2⌝.
   Proof.
-    iIntros "[H1 _] [H2 _]".
+    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 _]".
+    iIntros "H1 H2".
     iDestruct (own_valid_2 with "H1 H2") as %[]%mnat_auth_auth_op_valid.
   Qed.
 
-  (** The conclusion of this lemma is persistent; the proofmode will preserve the
-  [mnat_own_auth] in the premise as long as the conclusion is introduced to the
-  persistent context, for example with [iDestruct (mnat_get_lb with
-  "Hauth") as "#Hfrag"]. *)
-  Lemma mnat_get_lb γ q n :
-    mnat_own_auth γ q n -∗ mnat_own_lb γ n.
-  Proof. iIntros "[_ $]". Qed.
-
-  Lemma mnat_alloc n :
-    ⊢ |==> ∃ γ, mnat_own_auth γ 1 n ∗ mnat_own_lb γ n.
-  Proof.
-    iMod (own_alloc (mnat_auth_auth 1 n ⋅ mnat_auth_frag n)) as (γ) "Hauth".
-    { apply mnat_auth_both_valid; auto. }
-    iModIntro. iExists γ.
-    iDestruct (mnat_get_lb with "Hauth") as "#Hlb".
-    auto.
-  Qed.
-
   Lemma mnat_own_lb_valid γ q n m :
     mnat_own_auth γ q n -∗ mnat_own_lb γ m -∗ ⌜✓ q ∧ m ≤ n⌝.
   Proof.
-    iIntros "[Hauth _] Hlb".
+    iIntros "Hauth Hlb".
     iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mnat_auth_both_frac_valid.
     auto.
   Qed.
 
+  (** The conclusion of this lemma is persistent; the proofmode will preserve the
+  [mnat_own_auth] in the premise as long as the conclusion is introduced to the
+  persistent context, for example with [iDestruct (mnat_get_lb with
+  "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.
+
   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.
+
+  Lemma mnat_alloc n :
+    ⊢ |==> ∃ γ, mnat_own_auth γ 1 n ∗ mnat_own_lb γ n.
   Proof.
-    intros Hle.
-    rewrite /mnat_own_lb.
-    rewrite (mnat_auth_frag_op_le_l n n') //.
-    iIntros "[$ _]".
+    iMod (own_alloc (mnat_auth_auth 1 n ⋅ mnat_auth_frag n)) as (γ) "[??]".
+    { apply mnat_auth_both_valid; auto. }
+    auto with iFrame.
   Qed.
 
   Lemma mnat_update n' γ n :
     n ≤ n' →
     mnat_own_auth γ 1 n ==∗ mnat_own_auth γ 1 n'.
-  Proof.
-    iIntros (Hlb) "[Hauth _]".
-    iMod (own_update with "Hauth") as "$"; [|done].
-    apply mnat_auth_update; auto.
-  Qed.
+  Proof. intros. by apply own_update, mnat_auth_update. Qed.
 
   Lemma mnat_update_with_lb γ n n' :
     n ≤ n' →
@@ -115,8 +97,7 @@ Section mnat.
   Proof.
     iIntros (Hlb) "Hauth".
     iMod (mnat_update n' with "Hauth") as "Hauth"; auto.
-    iDestruct (mnat_get_lb with "Hauth") as "#Hlb".
-    auto.
+    iDestruct (mnat_get_lb with "Hauth") as "#Hlb"; auto.
   Qed.
 End mnat.