frac.v 1.24 KB
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 14 15 16 17 18 19 20 21 22 23
Lemma frac_included (x y : frac) : x  y  (x < y)%Qc.
Proof.
  split.
  - intros [z ->%leibniz_equiv]; simpl.
    rewrite -{1}(Qcplus_0_r x). apply Qcplus_lt_mono_l, Qp_prf.
  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl.
    by rewrite (Qcplus_comm y) Qcplus_assoc Qcplus_opp_r Qcplus_0_l.
Qed.
Corollary frac_included_weak (x y : frac) : x  y  (x  y)%Qc.
Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.

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

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