From e68b27300a7087f21134f649ada7015e4d247821 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Wed, 17 Jun 2020 09:17:22 +0200
Subject: [PATCH] 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     | 19 +---------------
 theories/algebra/numbers.v           | 34 +++++++++++++++++++++++++---
 theories/algebra/proofmode_classes.v |  6 +----
 theories/heap_lang/lib/counter.v     |  2 +-
 4 files changed, 34 insertions(+), 27 deletions(-)

diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 015e46f5c..a775a716c 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -1,4 +1,4 @@
-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.
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index 70223478d..d1f65b46a 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -1,6 +1,6 @@
-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.
diff --git a/theories/algebra/proofmode_classes.v b/theories/algebra/proofmode_classes.v
index ebe66f815..2e42bebf5 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -1,4 +1,4 @@
-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.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 586f40b44..2e41a5905 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -1,5 +1,5 @@
 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.
-- 
GitLab