frac.v 2.2 KB
Newer Older
1 2 3 4 5
(** 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]. *)
6
From Coq.QArith Require Import Qcanon.
7
From iris.algebra Require Export cmra.
8
From iris.algebra Require Import proofmode_classes.
9
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11 12 13
(** 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. *)
14
Notation frac := Qp (only parsing).
Robbert Krebbers's avatar
Robbert Krebbers committed
15

16 17
Section frac.
Canonical Structure fracC := leibnizC frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
18

19 20 21
Instance frac_valid : Valid frac := λ x, (x  1)%Qc.
Instance frac_pcore : PCore frac := λ _, None.
Instance frac_op : Op frac := λ x y, (x + y)%Qp.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

23
Lemma frac_included (x y : frac) : x  y  (x < y)%Qc.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
Proof. by rewrite Qp_lt_sum. Qed.
25

26 27 28
Corollary frac_included_weak (x y : frac) : x  y  (x  y)%Qc.
Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.

29
Definition frac_ra_mixin : RAMixin frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Proof.
31
  split; try apply _; try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
33
  rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
Qed.
35
Canonical Structure fracR := discreteR frac frac_ra_mixin.
36

37
Global Instance frac_cmra_discrete : CmraDiscrete fracR.
38
Proof. apply discrete_cmra_discrete. Qed.
39
End frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41
Global Instance frac_full_exclusive : Exclusive 1%Qp.
42
Proof.
43
  move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
44
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
45

46 47 48 49 50 51 52 53 54
Global Instance frac_cancelable (q : frac) : Cancelable q.
Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.

Global Instance frac_id_free (q : frac) : 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.

Ralf Jung's avatar
Ralf Jung committed
55 56 57 58
Lemma frac_op' (q p : Qp) : (p  q) = (p + q)%Qp.
Proof. done. Qed.

Lemma frac_valid' (p : Qp) :  p  (p  1%Qp)%Qc.
Zhen Zhang's avatar
Zhen Zhang committed
59
Proof. done. Qed.
60

61 62
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.