diff --git a/_CoqProject b/_CoqProject index 497e83782ce1c89c178983a0191e87b2cb2924c6..13cda0b2ad25d99e816b2b893c4521454fba7d31 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 d76652cc9f5877b92821a4f23c94fde1b079b667..f5f84eb01cf3f4fb43fcde9ef143018548e7da74 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 0000000000000000000000000000000000000000..1b378db332bf62a98772e3e548dd6322c7e64d77 --- /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.