From 5ffa64f9637c5e02822841ee4cb1f967a02767ac Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 22 Jan 2017 16:42:45 +0100
Subject: [PATCH] (CM)RA structure for positive.

---
 theories/algebra/cmra.v | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 8fe2f1ddf..cd15455b1 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -933,6 +933,32 @@ Section mnat.
   Proof. by constructor. Qed.
 End mnat.
 
+(** ** 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.
+    split.
+    - intros [z ->]; unfold op, pos_op. lia.
+    - exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
+  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 posR : cmraT := discreteR positive pos_ra_mixin.
+
+  Global Instance pos_cmra_discrete : CMRADiscrete posR.
+  Proof. constructor; apply _ || done. Qed.
+End positive.
+
 (** ** Product *)
 Section prod.
   Context {A B : cmraT}.
-- 
GitLab