From 4b0595559bfb0b13f5289eec3f5b352bc36f98d5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 20 Dec 2018 22:03:57 +0100
Subject: [PATCH] The unbounded fractional camera.

---
 _CoqProject              |  1 +
 theories/algebra/frac.v  |  8 +++++++
 theories/algebra/ufrac.v | 47 ++++++++++++++++++++++++++++++++++++++++
 3 files changed, 56 insertions(+)
 create mode 100644 theories/algebra/ufrac.v

diff --git a/_CoqProject b/_CoqProject
index 497e83782..13cda0b2a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -26,6 +26,7 @@ theories/algebra/gmultiset.v
 theories/algebra/coPset.v
 theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
+theories/algebra/ufrac.v
 theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index d76652cc9..f5f84eb01 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -1,8 +1,16 @@
+(** This file provides a version of the fractional camera whose elements are
+in the internal (0,1] of the rational numbers.
+
+Notice that this camera could in principle be obtained by restricting the
+validity of the unbounded fractional camera [ufrac]. *)
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
+(** Since the standard (0,1] fractional camera is used more often, we define
+[frac] through a [Notation] instead of a [Definition]. That way, Coq infers the
+[frac] camera by default when using the [Qp] type. *)
 Notation frac := Qp (only parsing).
 
 Section frac.
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
new file mode 100644
index 000000000..1b378db33
--- /dev/null
+++ b/theories/algebra/ufrac.v
@@ -0,0 +1,47 @@
+(** This file provides a "bounded" version of the fractional camera whose
+elements are in the interval (0,..) instead of (0,1]. *)
+From Coq.QArith Require Import Qcanon.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import proofmode_classes.
+Set Default Proof Using "Type".
+
+(** Since the standard (0,1] fractional camera [frac] is used more often, we
+define [ufrac] through a [Definition] instead of a [Notation]. That way, Coq
+infers the [frac] camera by default when using the [Qp] type. *)
+Definition ufrac := Qp.
+
+Section ufrac.
+Canonical Structure ufracC := leibnizC ufrac.
+
+Instance ufrac_valid : Valid ufrac := λ x, True.
+Instance ufrac_pcore : PCore ufrac := λ _, None.
+Instance ufrac_op : Op ufrac := λ x y, (x + y)%Qp.
+
+Lemma ufrac_included (x y : ufrac) : x ≼ y ↔ (x < y)%Qc.
+Proof. by rewrite Qp_lt_sum. Qed.
+
+Corollary ufrac_included_weak (x y : ufrac) : x ≼ y → (x ≤ y)%Qc.
+Proof. intros ?%ufrac_included. auto using Qclt_le_weak. Qed.
+
+Definition ufrac_ra_mixin : RAMixin ufrac.
+Proof. split; try apply _; try done. Qed.
+Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
+
+Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
+Proof. apply discrete_cmra_discrete. Qed.
+End ufrac.
+
+Global Instance ufrac_cancelable (q : ufrac) : Cancelable q.
+Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
+
+Global Instance ufrac_id_free (q : ufrac) : IdFree q.
+Proof.
+  intros [q0 Hq0] ? EQ%Qp_eq. rewrite -{1}(Qcplus_0_r q) in EQ.
+  eapply Qclt_not_eq; first done. by apply (inj (Qcplus q)).
+Qed.
+
+Lemma ufrac_op' (q p : ufrac) : (p â‹… q) = (p + q)%Qp.
+Proof. done. Qed.
+
+Global Instance is_op_ufrac (q : ufrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
+Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp_div_2. Qed.
-- 
GitLab