frac.v 1.24 KB
Newer Older
 1 ``````From Coq.QArith Require Import Qcanon. `````` Robbert Krebbers committed Mar 10, 2016 2 ``````From iris.algebra Require Export cmra. `````` Robbert Krebbers committed Feb 26, 2016 3 `````` `````` Robbert Krebbers committed Jun 01, 2016 4 ``````Notation frac := Qp (only parsing). `````` Robbert Krebbers committed Feb 26, 2016 5 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 6 7 ``````Section frac. Canonical Structure fracC := leibnizC frac. `````` Robbert Krebbers committed Feb 26, 2016 8 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 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 committed May 28, 2016 12 `````` `````` Robbert Krebbers committed Oct 02, 2016 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. `````` Jacques-Henri Jourdan committed Jun 01, 2016 24 ``````Definition frac_ra_mixin : RAMixin frac. `````` Robbert Krebbers committed Feb 26, 2016 25 ``````Proof. `````` Jacques-Henri Jourdan committed Jun 01, 2016 26 `````` split; try apply _; try done. `````` Robbert Krebbers committed Jun 01, 2016 27 `````` unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done. `````` Jacques-Henri Jourdan committed Jun 01, 2016 28 `````` rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak. `````` Robbert Krebbers committed Feb 26, 2016 29 ``````Qed. `````` Jacques-Henri Jourdan committed Jun 01, 2016 30 31 ``````Canonical Structure fracR := discreteR frac frac_ra_mixin. End frac. `````` Robbert Krebbers committed Feb 26, 2016 32 `````` `````` Jacques-Henri Jourdan committed May 31, 2016 33 ``````(** Exclusive *) `````` Jacques-Henri Jourdan committed Jun 01, 2016 34 ``````Global Instance frac_full_exclusive : Exclusive 1%Qp. `````` Jacques-Henri Jourdan committed May 31, 2016 35 ``````Proof. `````` Robbert Krebbers committed Jun 01, 2016 36 `````` move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. `````` Jacques-Henri Jourdan committed May 31, 2016 37 ``Qed.``