frac.v 2.2 KB
 Robbert Krebbers committed Dec 21, 2018 1 2 3 4 5 ``````(** This file provides a version of the fractional camera whose elements are in the internal (0,1] of the rational numbers. Notice that this camera could in principle be obtained by restricting the validity of the unbounded fractional camera [ufrac]. *) `````` 6 ``````From Coq.QArith Require Import Qcanon. `````` Robbert Krebbers committed Mar 10, 2016 7 ``````From iris.algebra Require Export cmra. `````` Robbert Krebbers committed Oct 31, 2017 8 ``````From iris.algebra Require Import proofmode_classes. `````` Ralf Jung committed Jan 05, 2017 9 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Feb 26, 2016 10 `````` `````` Robbert Krebbers committed Dec 21, 2018 11 12 13 ``````(** Since the standard (0,1] fractional camera is used more often, we define [frac] through a [Notation] instead of a [Definition]. That way, Coq infers the [frac] camera by default when using the [Qp] type. *) `````` Robbert Krebbers committed Jun 01, 2016 14 ``````Notation frac := Qp (only parsing). `````` Robbert Krebbers committed Feb 26, 2016 15 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 16 17 ``````Section frac. Canonical Structure fracC := leibnizC frac. `````` Robbert Krebbers committed Feb 26, 2016 18 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 19 20 21 ``````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 committed May 28, 2016 22 `````` `````` Ralf Jung committed Mar 10, 2017 23 ``````Lemma frac_included (x y : frac) : x ≼ y ↔ (x < y)%Qc. `````` Robbert Krebbers committed Mar 11, 2017 24 ``````Proof. by rewrite Qp_lt_sum. Qed. `````` Ralf Jung committed Mar 10, 2017 25 `````` `````` Robbert Krebbers committed Oct 02, 2016 26 27 28 ``````Corollary frac_included_weak (x y : frac) : x ≼ y → (x ≤ y)%Qc. Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed. `````` Jacques-Henri Jourdan committed Jun 01, 2016 29 ``````Definition frac_ra_mixin : RAMixin frac. `````` Robbert Krebbers committed Feb 26, 2016 30 ``````Proof. `````` Jacques-Henri Jourdan committed Jun 01, 2016 31 `````` split; try apply _; try done. `````` Robbert Krebbers committed Jun 01, 2016 32 `````` unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done. `````` Jacques-Henri Jourdan committed Jun 01, 2016 33 `````` rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak. `````` Robbert Krebbers committed Feb 26, 2016 34 ``````Qed. `````` Jacques-Henri Jourdan committed Jun 01, 2016 35 ``````Canonical Structure fracR := discreteR frac frac_ra_mixin. `````` Robbert Krebbers committed Feb 09, 2017 36 `````` `````` Robbert Krebbers committed Oct 25, 2017 37 ``````Global Instance frac_cmra_discrete : CmraDiscrete fracR. `````` Robbert Krebbers committed Feb 09, 2017 38 ``````Proof. apply discrete_cmra_discrete. Qed. `````` Jacques-Henri Jourdan committed Jun 01, 2016 39 ``````End frac. `````` Robbert Krebbers committed Feb 26, 2016 40 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 41 ``````Global Instance frac_full_exclusive : Exclusive 1%Qp. `````` Jacques-Henri Jourdan committed May 31, 2016 42 ``````Proof. `````` Robbert Krebbers committed Jun 01, 2016 43 `````` move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. `````` Jacques-Henri Jourdan committed May 31, 2016 44 ``````Qed. `````` Zhen Zhang committed Oct 10, 2016 45 `````` `````` Jacques-Henri Jourdan committed Feb 01, 2017 46 47 48 49 50 51 52 53 54 ``````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 committed Mar 09, 2017 55 56 57 58 ``````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 committed Oct 10, 2016 59 ``````Proof. done. Qed. `````` Robbert Krebbers committed Jun 08, 2017 60 `````` `````` Robbert Krebbers committed Jun 08, 2017 61 62 ``````Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp. Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.``````