frac.v 801 Bytes
Newer Older
1
From Coq.QArith Require Import Qcanon.
2
From iris.algebra Require Export cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
3

4
Notation frac := Qp (only parsing).
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6 7
Section frac.
Canonical Structure fracC := leibnizC frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9 10 11
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
12

13
Definition frac_ra_mixin : RAMixin frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
Proof.
15
  split; try apply _; try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
  unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
17
  rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Qed.
19 20
Canonical Structure fracR := discreteR frac frac_ra_mixin.
End frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
21

22
(** Exclusive *)
23
Global Instance frac_full_exclusive : Exclusive 1%Qp.
24
Proof.
25
  move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
26
Qed.