Commit d6389a35 by Robbert Krebbers

### Not all [Qp]s are [frac]s, so make the notation only parsing.

parent fce8b28c
 ... @@ -2,10 +2,9 @@ From Coq.QArith Require Import Qcanon. ... @@ -2,10 +2,9 @@ From Coq.QArith Require Import Qcanon. From iris.algebra Require Export cmra. From iris.algebra Require Export cmra. From iris.algebra Require Import upred. From iris.algebra Require Import upred. Notation frac := Qp. Notation frac := Qp (only parsing). Section frac. Section frac. Canonical Structure fracC := leibnizC frac. Canonical Structure fracC := leibnizC frac. Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc. Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc. ... @@ -19,20 +18,16 @@ Proof. ... @@ -19,20 +18,16 @@ Proof. rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak. rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak. Qed. Qed. Canonical Structure fracR := discreteR frac frac_ra_mixin. Canonical Structure fracR := discreteR frac frac_ra_mixin. End frac. End frac. (** Internalized properties *) (** Internalized properties *) Lemma frac_equivI {M} (x y : frac) : Lemma frac_equivI {M} (x y : frac) : x ≡ y ⊣⊢ (x = y : uPred M). x ≡ y ⊣⊢ (x = y : uPred M). Proof. by uPred.unseal. Qed. Proof. by uPred.unseal. Qed. Lemma frac_validI {M} (x : frac) : Lemma frac_validI {M} (x : frac) : ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M). ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M). Proof. by uPred.unseal. Qed. Proof. by uPred.unseal. Qed. (** Exclusive *) (** Exclusive *) Global Instance frac_full_exclusive : Exclusive 1%Qp. Global Instance frac_full_exclusive : Exclusive 1%Qp. Proof. Proof. move => ? /Qcle_not_lt[]; simpl in *. move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. Qed. Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!