Add IdemP instances, consolidate numbers lemmas

Add IdempP instances for min_nat and max_nat.

Move additional numbers related lemmas and instances into the numbers file.

theories/algebra/local_updates.v

-From iris.algebra Require Export cmra numbers.
+From iris.algebra Require Export cmra.
 Set Default Proof Using "Type".
 
 (** * Local updates *)
@@ -189,20 +189,3 @@ Proof.
   move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
   eapply cmra_validN_le. eapply Hy. lia.
 Qed.
-
-(** * Natural numbers  *)
-Lemma nat_local_update (x y x' y' : nat) :
-  x + y' = x' + y → (x,y) ~l~> (x',y').
-Proof.
-  intros ??; apply local_update_unital_discrete=> z _.
-  compute -[minus plus]; lia.
-Qed.
-
-Lemma max_nat_local_update (x y x' : max_natUR) :
-  max_nat_car x ≤ max_nat_car x' → (x,y) ~l~> (x',x').
-Proof.
-  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.

theories/algebra/numbers.v

-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra local_updates proofmode_classes.
 
-(** ** Natural numbers *)
+(** ** Natural numbers with [add] as the operation. *)
 Section nat.
   Instance nat_valid : Valid nat := λ x, True.
   Instance nat_validN : ValidN nat := λ n x, True.
@@ -29,6 +29,13 @@ Section nat.
 
   Global Instance nat_cancelable (x : nat) : Cancelable x.
   Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
+
+  Lemma nat_local_update (x y x' y' : nat) :
+    x + y' = x' + y → (x,y) ~l~> (x',y').
+  Proof.
+    intros ??; apply local_update_unital_discrete=> z _.
+    compute -[minus plus]; lia.
+  Qed.
 End nat.
 
 (** ** Natural numbers with [max] as the operation. *)
@@ -43,6 +50,7 @@ Section max_nat.
   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.
@@ -67,6 +75,18 @@ Section max_nat.
 
   Global Instance max_nat_core_id (x : max_nat) : CoreId x.
   Proof. by constructor. Qed.
+
+  Lemma max_nat_local_update (x y x' : max_natUR) :
+    max_nat_car x ≤ max_nat_car x' → (x,y) ~l~> (x',x').
+  Proof.
+    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.
+
+  Global Instance : @IdemP max_nat (=) (⋅).
+  Proof. intros [x]. rewrite max_nat_op_max. apply f_equal. lia. Qed.
 End max_nat.
 
 (** ** Natural numbers with [min] as the operation. *)
@@ -107,9 +127,17 @@ Section min_nat.
 
   Global Instance : RightAbsorb (=) (MinNat 0) (⋅).
   Proof. intros [x]. by rewrite min_nat_op_min Min.min_0_r. Qed.
+
+  Global Instance : @IdemP min_nat (=) (⋅).
+  Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed.
+
+  (* This one has a higher precendence than [is_op_op] so we get a [+] instead
+     of an [⋅]. *)
+  Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
+  Proof. done. Qed.
 End min_nat.
 
-(** ** Positive integers. *)
+(** ** Positive integers with [Pos.add] as the operation. *)
 Section positive.
   Instance pos_valid : Valid positive := λ x, True.
   Instance pos_validN : ValidN positive := λ n x, True.

theories/algebra/proofmode_classes.v

-From iris.algebra Require Export cmra numbers.
+From iris.algebra Require Export cmra.
 From iris.proofmode Require Export classes.
 
 (* There are various versions of [IsOp] with different modes:
@@ -48,7 +48,3 @@ Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
 Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
   IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
 Proof. by constructor. Qed.
-(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
-an [⋅]. *)
-Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
-Proof. done. Qed.

theories/heap_lang/lib/counter.v

 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import lib.frac_auth auth.
+From iris.algebra Require Import lib.frac_auth numbers auth.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.