CMRA on nat with max as op.

algebra/cmra.v

@@ -758,35 +758,70 @@ Section nat.
   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.
     split.
     - intros [z ->]; unfold op, nat_op; lia.
     - exists (y - x). by apply le_plus_minus.
   Qed.
-  Lemma nat_cmra_mixin : CMRAMixin nat.
+  Lemma nat_ra_mixin : RAMixin nat.
   Proof.
-    apply discrete_cmra_mixin, ra_total_mixin; try by eauto.
+    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 :=
-    CMRAT nat (@discrete_cofe_mixin _ equivL _) nat_cmra_mixin.
+  Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
 
   Instance nat_empty : Empty nat := 0.
   Lemma nat_ucmra_mixin : UCMRAMixin nat.
   Proof. split; apply _ || done. Qed.
   Canonical Structure natUR : ucmraT :=
-    UCMRAT nat (@discrete_cofe_mixin _ equivL _) nat_cmra_mixin nat_ucmra_mixin.
+    discreteUR nat nat_ra_mixin nat_ucmra_mixin.
 
   Global Instance nat_cmra_discrete : CMRADiscrete natR.
   Proof. constructor; apply _ || done. Qed.
-  Global Instance nat_persistent (x : ()) : Persistent x.
-  Proof. by constructor. Qed.
 End nat.
 
+Definition mnat := nat.
+
+Section mnat.
+  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 := max.
+  Definition mnat_op_max x y : x ⋅ y = max x 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; try by eauto.
+    - solve_proper.
+    - solve_proper.
+    - 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.
+
+  Instance mnat_empty : Empty mnat := 0.
+  Lemma mnat_ucmra_mixin : UCMRAMixin mnat.
+  Proof. split; apply _ || done. Qed.
+  Canonical Structure mnatUR : ucmraT :=
+    discreteUR mnat mnat_ra_mixin mnat_ucmra_mixin.
+
+  Global Instance mnat_cmra_discrete : CMRADiscrete mnatR.
+  Proof. constructor; apply _ || done. Qed.
+  Global Instance mnat_persistent (x : mnat) : Persistent x.
+  Proof. by constructor. Qed.
+End mnat.
+
 (** ** Product *)
 Section prod.
   Context {A B : cmraT}.

algebra/updates.v

@@ -241,11 +241,14 @@ Section option.
 End option.
 
 (** * Natural numbers  *)
-Lemma nat_local_update (x y : nat) mz :
-  x ~l~> y @ mz.
+Lemma nat_local_update (x y : nat) mz : x ~l~> y @ mz.
 Proof.
-  split. done.
-  unfold opM, op, dist, cofe_dist, cmra_cofeC, cmra_op, cmra_dist, natR, nat_op,
-         discrete_dist, equiv, equivL.
-  destruct mz as [z|]; intros n [z'|]; lia.
+  split; first done.
+  compute -[plus]; destruct mz as [z|]; intros n [z'|]; lia.
+Qed.
+
+Lemma mnat_local_update (x y : mnat) mz : x ≤ y → x ~l~> y @ mz.
+Proof.
+  split; first done.
+  compute -[max]; destruct mz as [z|]; intros n [z'|]; lia.
 Qed.