frac.v 1.05 KB
 1 ``````From Coq.QArith Require Import Qcanon. `````` Robbert Krebbers committed Mar 10, 2016 2 3 ``````From iris.algebra Require Export cmra. From iris.algebra Require Import upred. `````` Robbert Krebbers committed Feb 26, 2016 4 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 5 ``````Notation frac := Qp. `````` Robbert Krebbers committed Feb 26, 2016 6 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 7 ``````Section frac. `````` Robbert Krebbers committed Feb 26, 2016 8 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 9 ``````Canonical Structure fracC := leibnizC frac. `````` Robbert Krebbers committed Feb 26, 2016 10 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 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 committed May 28, 2016 14 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 15 ``````Definition frac_ra_mixin : RAMixin frac. `````` Robbert Krebbers committed Feb 26, 2016 16 ``````Proof. `````` Jacques-Henri Jourdan committed Jun 01, 2016 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 committed Feb 26, 2016 20 ``````Qed. `````` Jacques-Henri Jourdan committed Jun 01, 2016 21 ``````Canonical Structure fracR := discreteR frac frac_ra_mixin. `````` Robbert Krebbers committed May 27, 2016 22 `````` `````` Jacques-Henri Jourdan committed Jun 01, 2016 23 ``````End frac. `````` Robbert Krebbers committed Feb 26, 2016 24 25 `````` (** Internalized properties *) `````` Jacques-Henri Jourdan committed Jun 01, 2016 26 27 ``````Lemma frac_equivI {M} (x y : frac) : x ≡ y ⊣⊢ (x = y : uPred M). `````` Robbert Krebbers committed May 28, 2016 28 ``````Proof. by uPred.unseal. Qed. `````` Jacques-Henri Jourdan committed Jun 01, 2016 29 30 ``````Lemma frac_validI {M} (x : frac) : ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M). `````` Robbert Krebbers committed May 28, 2016 31 ``````Proof. by uPred.unseal. Qed. `````` 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. `````` Jacques-Henri Jourdan committed Jun 01, 2016 36 `````` move => ? /Qcle_not_lt[]; simpl in *. `````` Jacques-Henri Jourdan committed May 31, 2016 37 38 `````` by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. Qed.``````