diff --git a/algebra/frac.v b/algebra/frac.v index ad065890bf534d4a600121f3af29e8c1dd2fd8b2..9efcba2c2f85cb9f1969cd34d6a034da065ef8f0 100644 --- a/algebra/frac.v +++ b/algebra/frac.v @@ -2,10 +2,9 @@ From Coq.QArith Require Import Qcanon. From iris.algebra Require Export cmra. From iris.algebra Require Import upred. -Notation frac := Qp. +Notation frac := Qp (only parsing). Section frac. - Canonical Structure fracC := leibnizC frac. Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc. @@ -19,20 +18,16 @@ Proof. rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak. Qed. Canonical Structure fracR := discreteR frac frac_ra_mixin. - End frac. (** Internalized properties *) -Lemma frac_equivI {M} (x y : frac) : - x ≡ y ⊣⊢ (x = y : uPred M). +Lemma frac_equivI {M} (x y : frac) : x ≡ y ⊣⊢ (x = y : uPred M). Proof. by uPred.unseal. Qed. -Lemma frac_validI {M} (x : frac) : - ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M). +Lemma frac_validI {M} (x : frac) : ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M). Proof. by uPred.unseal. Qed. (** Exclusive *) Global Instance frac_full_exclusive : Exclusive 1%Qp. Proof. - move => ? /Qcle_not_lt[]; simpl in *. - by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. + move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. Qed.