frac.v 1.97 KB
Newer Older
1
From Coq.QArith Require Import Qcanon.
2
From iris.algebra Require Export cmra.
3
Set Default Proof Using "Type".
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
15
(* TODO: Find better place for this lemma. *)
Lemma Qp_le_sum (x y : Qp) : (x < y)%Qc  ( z, y = x + z)%Qp.
16
17
18
19
Proof.
  split.
  - 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.
20
21
  - intros [z ->%leibniz_equiv]; simpl.
    rewrite -{1}(Qcplus_0_r x). apply Qcplus_lt_mono_l, Qp_prf.
22
Qed.
23
24
25
26

Lemma frac_included (x y : frac) : x  y  (x < y)%Qc.
Proof. symmetry. exact: Qp_le_sum. Qed.

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

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

Global Instance frac_cmra_discrete : CMRADiscrete fracR.
Proof. apply discrete_cmra_discrete. Qed.
40
End frac.
Robbert Krebbers's avatar
Robbert Krebbers committed
41

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

47
48
49
50
51
52
53
54
55
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
56
57
58
59
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
60
Proof. done. Qed.