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

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

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

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

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

(** Internalized properties *)
24
Lemma frac_equivI {M} (x y : frac) : x  y  (x = y : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
25
Proof. by uPred.unseal. Qed.
26
Lemma frac_validI {M} (x : frac) :  x  ( (x  1)%Qc : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Proof. by uPred.unseal. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
28

29
(** Exclusive *)
30
Global Instance frac_full_exclusive : Exclusive 1%Qp.
31
Proof.
32
  move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
33
Qed.