Library iris.algebra.frac

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 iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes.
From iris.prelude Require Import options.

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.
  Canonical Structure fracO := leibnizO frac.

  Local Instance frac_valid_instance : Valid frac := λ x, (x 1)%Qp.
  Local Instance frac_pcore_instance : PCore frac := λ _, None.
  Local Instance frac_op_instance : Op frac := λ x y, (x + y)%Qp.

  Lemma frac_valid p : p (p 1)%Qp.
  Proof. done. Qed.
  Lemma frac_op p q : p q = (p + q)%Qp.
  Proof. done. Qed.
  Lemma frac_included p q : p q (p < q)%Qp.
  Proof. by rewrite Qp_lt_sum. Qed.

  Corollary frac_included_weak p q : p q (p q)%Qp.
  Proof. rewrite frac_included. apply Qp_lt_le_incl. Qed.

  Definition frac_ra_mixin : RAMixin frac.
  Proof.
    split; try apply _; try done.
    intros p q. rewrite !frac_valid frac_op⇒ ?.
    trans (p + q)%Qp; last done. apply Qp_le_add_l.
  Qed.
  Canonical Structure fracR := discreteR frac frac_ra_mixin.

  Global Instance frac_cmra_discrete : CmraDiscrete fracR.
  Proof. apply discrete_cmra_discrete. Qed.
  Global Instance frac_full_exclusive : Exclusive 1%Qp.
  Proof. intros p. apply Qp_not_add_le_l. Qed.
  Global Instance frac_cancelable (q : frac) : Cancelable q.
  Proof. intros n p1 p2 _. apply (inj (Qp_add q)). Qed.
  Global Instance frac_id_free (q : frac) : IdFree q.
  Proof. intros p _. apply Qp_add_id_free. Qed.

  Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
  Proof. done. Qed.
  Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
  Proof. by rewrite /IsOp' /IsOp frac_op Qp_div_2. Qed.
End frac.