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.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7
Section frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
Canonical Structure fracC := leibnizC frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

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

15
Definition frac_ra_mixin : RAMixin frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
Proof.
17 18 19
  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
20
Qed.
21
Canonical Structure fracR := discreteR frac frac_ra_mixin.
22

23
End frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25

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

33
(** Exclusive *)
34
Global Instance frac_full_exclusive : Exclusive 1%Qp.
35
Proof.
36
  move => ? /Qcle_not_lt[]; simpl in *.
37 38
  by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
Qed.