Forked from
Iris / Iris
2413 commits behind the upstream repository.
-
Robbert Krebbers authored
Used the following script: sed ' s/\bCofeMor/OfeMor/g; s/\-c>/\-d>/g; s/\bcFunctor/oFunctor/g; s/\bCFunctor/OFunctor/g; s/\b\%CF/\%OF/g; s/\bconstCF/constOF/g; s/\bidCF/idOF/g s/\bdiscreteC/discreteO/g; s/\bleibnizC/leibnizO/g; s/\bunitC/unitO/g; s/\bprodC/prodO/g; s/\bsumC/sumO/g; s/\bboolC/boolO/g; s/\bnatC/natO/g; s/\bpositiveC/positiveO/g; s/\bNC/NO/g; s/\bZC/ZO/g; s/\boptionC/optionO/g; s/\blaterC/laterO/g; s/\bofe\_fun/discrete\_fun/g; s/\bdiscrete\_funC/discrete\_funO/g; s/\bofe\_morC/ofe\_morO/g; s/\bsigC/sigO/g; s/\buPredC/uPredO/g; s/\bcsumC/csumO/g; s/\bagreeC/agreeO/g; s/\bauthC/authO/g; s/\bnamespace_mapC/namespace\_mapO/g; s/\bcmra\_ofeC/cmra\_ofeO/g; s/\bucmra\_ofeC/ucmra\_ofeO/g; s/\bexclC/exclO/g; s/\bgmapC/gmapO/g; s/\blistC/listO/g; s/\bvecC/vecO/g; s/\bgsetC/gsetO/g; s/\bgset\_disjC/gset\_disjO/g; s/\bcoPsetC/coPsetO/g; s/\bgmultisetC/gmultisetO/g; s/\bufracC/ufracO/g s/\bfracC/fracO/g; s/\bvalidityC/validityO/g; s/\bbi\_ofeC/bi\_ofeO/g; s/\bsbi\_ofeC/sbi\_ofeO/g; s/\bmonPredC/monPredO/g; s/\bstateC/stateO/g; s/\bvalC/valO/g; s/\bexprC/exprO/g; s/\blocC/locO/g; ' -i $(find theories -name "*.v")
Robbert Krebbers authoredUsed the following script: sed ' s/\bCofeMor/OfeMor/g; s/\-c>/\-d>/g; s/\bcFunctor/oFunctor/g; s/\bCFunctor/OFunctor/g; s/\b\%CF/\%OF/g; s/\bconstCF/constOF/g; s/\bidCF/idOF/g s/\bdiscreteC/discreteO/g; s/\bleibnizC/leibnizO/g; s/\bunitC/unitO/g; s/\bprodC/prodO/g; s/\bsumC/sumO/g; s/\bboolC/boolO/g; s/\bnatC/natO/g; s/\bpositiveC/positiveO/g; s/\bNC/NO/g; s/\bZC/ZO/g; s/\boptionC/optionO/g; s/\blaterC/laterO/g; s/\bofe\_fun/discrete\_fun/g; s/\bdiscrete\_funC/discrete\_funO/g; s/\bofe\_morC/ofe\_morO/g; s/\bsigC/sigO/g; s/\buPredC/uPredO/g; s/\bcsumC/csumO/g; s/\bagreeC/agreeO/g; s/\bauthC/authO/g; s/\bnamespace_mapC/namespace\_mapO/g; s/\bcmra\_ofeC/cmra\_ofeO/g; s/\bucmra\_ofeC/ucmra\_ofeO/g; s/\bexclC/exclO/g; s/\bgmapC/gmapO/g; s/\blistC/listO/g; s/\bvecC/vecO/g; s/\bgsetC/gsetO/g; s/\bgset\_disjC/gset\_disjO/g; s/\bcoPsetC/coPsetO/g; s/\bgmultisetC/gmultisetO/g; s/\bufracC/ufracO/g s/\bfracC/fracO/g; s/\bvalidityC/validityO/g; s/\bbi\_ofeC/bi\_ofeO/g; s/\bsbi\_ofeC/sbi\_ofeO/g; s/\bmonPredC/monPredO/g; s/\bstateC/stateO/g; s/\bvalC/valO/g; s/\bexprC/exprO/g; s/\blocC/locO/g; ' -i $(find theories -name "*.v")
ufrac.v 1.74 KiB
(** 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 ufracO := leibnizO 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.