From 4516513e7676468a4a28085bff2044f55ac926ef Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Tue, 16 Jun 2020 15:15:51 +0200
Subject: [PATCH] Separate module for number RAs, box max_nat, absorb for
 min_nat

---
 _CoqProject                          |   1 +
 theories/algebra/cmra.v              | 131 -------------------------
 theories/algebra/local_updates.v     |  12 ++-
 theories/algebra/numbers.v           | 140 +++++++++++++++++++++++++++
 theories/algebra/proofmode_classes.v |   2 +-
 theories/heap_lang/lib/counter.v     |  20 ++--
 6 files changed, 159 insertions(+), 147 deletions(-)
 create mode 100644 theories/algebra/numbers.v

diff --git a/_CoqProject b/_CoqProject
index 036d7ec24..824d3c1f4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -14,6 +14,7 @@ theories/algebra/cmra.v
 theories/algebra/big_op.v
 theories/algebra/cmra_big_op.v
 theories/algebra/sts.v
+theories/algebra/numbers.v
 theories/algebra/auth.v
 theories/algebra/gmap.v
 theories/algebra/ofe.v
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 2ad7df55b..5755ff3a2 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1054,137 +1054,6 @@ Section empty.
   Proof. by constructor. Qed.
 End empty.
 
-(** ** Natural numbers *)
-Section nat.
-  Instance nat_valid : Valid nat := λ x, True.
-  Instance nat_validN : ValidN nat := λ n x, True.
-  Instance nat_pcore : PCore nat := λ x, Some 0.
-  Instance nat_op : Op nat := plus.
-  Definition nat_op_plus x y : x â‹… y = x + y := eq_refl.
-  Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
-  Proof. by rewrite nat_le_sum. Qed.
-  Lemma nat_ra_mixin : RAMixin nat.
-  Proof.
-    apply ra_total_mixin; try by eauto.
-    - solve_proper.
-    - intros x y z. apply Nat.add_assoc.
-    - intros x y. apply Nat.add_comm.
-    - by exists 0.
-  Qed.
-  Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
-
-  Global Instance nat_cmra_discrete : CmraDiscrete natR.
-  Proof. apply discrete_cmra_discrete. Qed.
-
-  Instance nat_unit : Unit nat := 0.
-  Lemma nat_ucmra_mixin : UcmraMixin nat.
-  Proof. split; apply _ || done. Qed.
-  Canonical Structure natUR : ucmraT := UcmraT nat nat_ucmra_mixin.
-
-  Global Instance nat_cancelable (x : nat) : Cancelable x.
-  Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
-End nat.
-
-(** ** Natural numbers with [max] as the operation. *)
-Definition mnat := nat.
-
-Section mnat.
-  Instance mnat_unit : Unit mnat := 0.
-  Instance mnat_valid : Valid mnat := λ x, True.
-  Instance mnat_validN : ValidN mnat := λ n x, True.
-  Instance mnat_pcore : PCore mnat := Some.
-  Instance mnat_op : Op mnat := Nat.max.
-  Definition mnat_op_max x y : x â‹… y = x `max` y := eq_refl.
-  Lemma mnat_included (x y : mnat) : x ≼ y ↔ x ≤ y.
-  Proof.
-    split.
-    - intros [z ->]; unfold op, mnat_op; lia.
-    - exists y. by symmetry; apply Nat.max_r.
-  Qed.
-  Lemma mnat_ra_mixin : RAMixin mnat.
-  Proof.
-    apply ra_total_mixin; apply _ || eauto.
-    - intros x y z. apply Nat.max_assoc.
-    - intros x y. apply Nat.max_comm.
-    - intros x. apply Max.max_idempotent.
-  Qed.
-  Canonical Structure mnatR : cmraT := discreteR mnat mnat_ra_mixin.
-
-  Global Instance mnat_cmra_discrete : CmraDiscrete mnatR.
-  Proof. apply discrete_cmra_discrete. Qed.
-
-  Lemma mnat_ucmra_mixin : UcmraMixin mnat.
-  Proof. split; apply _ || done. Qed.
-  Canonical Structure mnatUR : ucmraT := UcmraT mnat mnat_ucmra_mixin.
-
-  Global Instance mnat_core_id (x : mnat) : CoreId x.
-  Proof. by constructor. Qed.
-End mnat.
-
-(** ** Natural numbers with [min] as the operation. *)
-Record min_nat := MinNat { min_nat_car :> nat }.
-
-Canonical Structure min_natO := leibnizO min_nat.
-
-Section min_nat.
-  Instance min_nat_valid : Valid min_nat := λ x, True.
-  Instance min_nat_validN : ValidN min_nat := λ n x, True.
-  Instance min_nat_pcore : PCore min_nat := Some.
-  Instance min_nat_op : Op min_nat := λ n m, MinNat (n `min` m).
-  Definition min_nat_op_min x y : MinNat x â‹… MinNat y = MinNat (x `min` y) := eq_refl.
-
-  Lemma min_nat_included (x y : min_nat) : x ≼ y ↔ (min_nat_car x) ≥ (min_nat_car y).
-  Proof.
-    split.
-    - intros [z ->]. simpl. lia.
-    - exists y. rewrite /op /min_nat_op. rewrite Nat.min_r; last lia. by destruct y.
-  Qed.
-  Lemma min_nat_ra_mixin : RAMixin min_nat.
-  Proof.
-    apply ra_total_mixin; apply _ || eauto.
-    - intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
-    - intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
-    - intros [x]. by rewrite min_nat_op_min Min.min_idempotent.
-  Qed.
-  Canonical Structure min_natR : cmraT := discreteR min_nat min_nat_ra_mixin.
-
-  Global Instance min_nat_cmra_discrete : CmraDiscrete min_natR.
-  Proof. apply discrete_cmra_discrete. Qed.
-
-  Global Instance min_nat_core_id (x : min_nat) : CoreId x.
-  Proof. by constructor. Qed.
-End min_nat.
-
-(** ** Positive integers. *)
-Section positive.
-  Instance pos_valid : Valid positive := λ x, True.
-  Instance pos_validN : ValidN positive := λ n x, True.
-  Instance pos_pcore : PCore positive := λ x, None.
-  Instance pos_op : Op positive := Pos.add.
-  Definition pos_op_plus x y : x â‹… y = (x + y)%positive := eq_refl.
-  Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
-  Proof. by rewrite Plt_sum. Qed.
-  Lemma pos_ra_mixin : RAMixin positive.
-  Proof.
-    split; try by eauto.
-    - by intros ??? ->.
-    - intros ???. apply Pos.add_assoc.
-    - intros ??. apply Pos.add_comm.
-  Qed.
-  Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
-
-  Global Instance pos_cmra_discrete : CmraDiscrete positiveR.
-  Proof. apply discrete_cmra_discrete. Qed.
-
-  Global Instance pos_cancelable (x : positive) : Cancelable x.
-  Proof. intros n y z ??. by eapply Pos.add_reg_l, leibniz_equiv. Qed.
-  Global Instance pos_id_free (x : positive) : IdFree x.
-  Proof.
-    intros y ??. apply (Pos.add_no_neutral x y). rewrite Pos.add_comm.
-    by apply leibniz_equiv.
-  Qed.
-End positive.
-
 (** ** Product *)
 Section prod.
   Context {A B : cmraT}.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 93f185ff3..015e46f5c 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra numbers.
 Set Default Proof Using "Type".
 
 (** * Local updates *)
@@ -198,9 +198,11 @@ Proof.
   compute -[minus plus]; lia.
 Qed.
 
-Lemma mnat_local_update (x y x' : mnatUR) :
-  x ≤ x' → (x,y) ~l~> (x',x').
+Lemma max_nat_local_update (x y x' : max_natUR) :
+  max_nat_car x ≤ max_nat_car x' → (x,y) ~l~> (x',x').
 Proof.
-  intros ??; apply local_update_unital_discrete=> z _.
-  compute -[max]; lia.
+  move: x y x' => [x] [y] [y'] /= ??.
+  apply local_update_unital_discrete=> [[z]] _.
+  rewrite 2!max_nat_op_max. inversion 1.
+  split; first done. apply f_equal. lia.
 Qed.
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
new file mode 100644
index 000000000..70223478d
--- /dev/null
+++ b/theories/algebra/numbers.v
@@ -0,0 +1,140 @@
+From iris.algebra Require Export cmra.
+
+(** ** Natural numbers *)
+Section nat.
+  Instance nat_valid : Valid nat := λ x, True.
+  Instance nat_validN : ValidN nat := λ n x, True.
+  Instance nat_pcore : PCore nat := λ x, Some 0.
+  Instance nat_op : Op nat := plus.
+  Definition nat_op_plus x y : x â‹… y = x + y := eq_refl.
+  Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
+  Proof. by rewrite nat_le_sum. Qed.
+  Lemma nat_ra_mixin : RAMixin nat.
+  Proof.
+    apply ra_total_mixin; try by eauto.
+    - solve_proper.
+    - intros x y z. apply Nat.add_assoc.
+    - intros x y. apply Nat.add_comm.
+    - by exists 0.
+  Qed.
+  Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
+
+  Global Instance nat_cmra_discrete : CmraDiscrete natR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
+  Instance nat_unit : Unit nat := 0.
+  Lemma nat_ucmra_mixin : UcmraMixin nat.
+  Proof. split; apply _ || done. Qed.
+  Canonical Structure natUR : ucmraT := UcmraT nat nat_ucmra_mixin.
+
+  Global Instance nat_cancelable (x : nat) : Cancelable x.
+  Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
+End nat.
+
+(** ** Natural numbers with [max] as the operation. *)
+Record max_nat := MaxNat { max_nat_car : nat }.
+
+Canonical Structure max_natO := leibnizO max_nat.
+
+Section max_nat.
+  Instance max_nat_unit : Unit max_nat := MaxNat 0.
+  Instance max_nat_valid : Valid max_nat := λ x, True.
+  Instance max_nat_validN : ValidN max_nat := λ n x, True.
+  Instance max_nat_pcore : PCore max_nat := Some.
+  Instance max_nat_op : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
+  Definition max_nat_op_max x y : MaxNat x â‹… MaxNat y = MaxNat (x `max` y) := eq_refl.
+  Lemma max_nat_included x y : x ≼ y ↔ max_nat_car x ≤ max_nat_car y.
+  Proof.
+    split.
+    - intros [z ->]. simpl. lia.
+    - exists y. rewrite /op /max_nat_op. rewrite Nat.max_r; last lia. by destruct y.
+  Qed.
+  Lemma max_nat_ra_mixin : RAMixin max_nat.
+  Proof.
+    apply ra_total_mixin; apply _ || eauto.
+    - intros [x] [y] [z]. repeat rewrite max_nat_op_max. by rewrite Nat.max_assoc.
+    - intros [x] [y]. by rewrite max_nat_op_max Nat.max_comm.
+    - intros [x]. by rewrite max_nat_op_max Max.max_idempotent.
+  Qed.
+  Canonical Structure max_natR : cmraT := discreteR max_nat max_nat_ra_mixin.
+
+  Global Instance max_nat_cmra_discrete : CmraDiscrete max_natR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
+  Lemma max_nat_ucmra_mixin : UcmraMixin max_nat.
+  Proof. split; try apply _ || done. intros [x]. done. Qed.
+  Canonical Structure max_natUR : ucmraT := UcmraT max_nat max_nat_ucmra_mixin.
+
+  Global Instance max_nat_core_id (x : max_nat) : CoreId x.
+  Proof. by constructor. Qed.
+End max_nat.
+
+(** ** Natural numbers with [min] as the operation. *)
+Record min_nat := MinNat { min_nat_car : nat }.
+
+Canonical Structure min_natO := leibnizO min_nat.
+
+Section min_nat.
+  Instance min_nat_valid : Valid min_nat := λ x, True.
+  Instance min_nat_validN : ValidN min_nat := λ n x, True.
+  Instance min_nat_pcore : PCore min_nat := Some.
+  Instance min_nat_op : Op min_nat := λ n m, MinNat (min_nat_car n `min` min_nat_car m).
+  Definition min_nat_op_min x y : MinNat x â‹… MinNat y = MinNat (x `min` y) := eq_refl.
+
+  Lemma min_nat_included (x y : min_nat) : x ≼ y ↔ min_nat_car y ≤ min_nat_car x.
+  Proof.
+    split.
+    - intros [z ->]. simpl. lia.
+    - exists y. rewrite /op /min_nat_op. rewrite Nat.min_r; last lia. by destruct y.
+  Qed.
+  Lemma min_nat_ra_mixin : RAMixin min_nat.
+  Proof.
+    apply ra_total_mixin; apply _ || eauto.
+    - intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
+    - intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
+    - intros [x]. by rewrite min_nat_op_min Min.min_idempotent.
+  Qed.
+  Canonical Structure min_natR : cmraT := discreteR min_nat min_nat_ra_mixin.
+
+  Global Instance min_nat_cmra_discrete : CmraDiscrete min_natR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
+  Global Instance min_nat_core_id (x : min_nat) : CoreId x.
+  Proof. by constructor. Qed.
+
+  Global Instance : LeftAbsorb (=) (MinNat 0) (â‹…).
+  Proof. done. Qed.
+
+  Global Instance : RightAbsorb (=) (MinNat 0) (â‹…).
+  Proof. intros [x]. by rewrite min_nat_op_min Min.min_0_r. Qed.
+End min_nat.
+
+(** ** Positive integers. *)
+Section positive.
+  Instance pos_valid : Valid positive := λ x, True.
+  Instance pos_validN : ValidN positive := λ n x, True.
+  Instance pos_pcore : PCore positive := λ x, None.
+  Instance pos_op : Op positive := Pos.add.
+  Definition pos_op_plus x y : x â‹… y = (x + y)%positive := eq_refl.
+  Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
+  Proof. by rewrite Plt_sum. Qed.
+  Lemma pos_ra_mixin : RAMixin positive.
+  Proof.
+    split; try by eauto.
+    - by intros ??? ->.
+    - intros ???. apply Pos.add_assoc.
+    - intros ??. apply Pos.add_comm.
+  Qed.
+  Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
+
+  Global Instance pos_cmra_discrete : CmraDiscrete positiveR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
+  Global Instance pos_cancelable (x : positive) : Cancelable x.
+  Proof. intros n y z ??. by eapply Pos.add_reg_l, leibniz_equiv. Qed.
+  Global Instance pos_id_free (x : positive) : IdFree x.
+  Proof.
+    intros y ??. apply (Pos.add_no_neutral x y). rewrite Pos.add_comm.
+    by apply leibniz_equiv.
+  Qed.
+End positive.
diff --git a/theories/algebra/proofmode_classes.v b/theories/algebra/proofmode_classes.v
index c87bc6fa2..ebe66f815 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra numbers.
 From iris.proofmode Require Export classes.
 
 (* There are various versions of [IsOp] with different modes:
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 52fc59ab7..586f40b44 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -13,8 +13,8 @@ Definition incr : val := rec: "incr" "l" :=
 Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
-Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
-Definition mcounterΣ : gFunctors := #[GFunctor (authR mnatUR)].
+Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR max_natUR) }.
+Definition mcounterΣ : gFunctors := #[GFunctor (authR max_natUR)].
 
 Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
 Proof. solve_inG. Qed.
@@ -23,10 +23,10 @@ Section mono_proof.
   Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
 
   Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
-    ∃ n, own γ (● (n : mnat)) ∗ l ↦ #n.
+    ∃ n, own γ (● (MaxNat n)) ∗ l ↦ #n.
 
   Definition mcounter (l : loc) (n : nat) : iProp Σ :=
-    ∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)).
+    ∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (MaxNat n)).
 
   (** The main proofs. *)
   Global Instance mcounter_persistent l n : Persistent (mcounter l n).
@@ -36,7 +36,7 @@ Section mono_proof.
     {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
+    iMod (own_alloc (● (MaxNat O) ⋅ ◯ (MaxNat O))) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0. by iFrame. }
@@ -54,15 +54,15 @@ Section mono_proof.
     iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iDestruct (own_valid_2 with "Hγ Hγf")
-        as %[?%mnat_included _]%auth_both_valid.
+        as %[?%max_nat_included _]%auth_both_valid.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-      { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
+      { apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. }
       wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_pures. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
       iApply (own_mono with "Hγf").
       (* FIXME: FIXME(Coq #6294): needs new unification *)
-      apply: auth_frag_mono. by apply mnat_included, le_n_S.
+      apply: auth_frag_mono. by apply max_nat_included, le_n_S.
     - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
       wp_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
@@ -76,9 +76,9 @@ Section mono_proof.
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
     wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
-      as %[?%mnat_included _]%auth_both_valid.
+      as %[?%max_nat_included _]%auth_both_valid.
     iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-    { apply auth_update, (mnat_local_update _ _ c); auto. }
+    { apply auth_update, (max_nat_local_update _ _ (MaxNat c)); auto. }
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
   Qed.
-- 
GitLab