From aec7c174aa81a5a2e9e8504723fc170169e3f9d3 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Mon, 12 Dec 2016 21:49:37 +0100 Subject: [PATCH] Some tweaks. --- theories/base_logic/lib/fractional.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v index e4545fde..98c4a03d 100644 --- a/theories/base_logic/lib/fractional.v +++ b/theories/base_logic/lib/fractional.v @@ -19,24 +19,23 @@ Section fractional. Implicit Types Φ : Qp → uPred M. Implicit Types p q : Qp. - Lemma fractional_split `{Fractional _ Φ} p q : + Lemma fractional_split `{!Fractional Φ} p q : Φ (p + q)%Qp ⊢ Φ p ∗ Φ q. Proof. by rewrite fractional. Qed. - Lemma fractional_combine `{Fractional _ Φ} p q : + Lemma fractional_combine `{!Fractional Φ} p q : Φ p ∗ Φ q ⊢ Φ (p + q)%Qp. Proof. by rewrite fractional. Qed. - Lemma fractional_half_equiv `{Fractional _ Φ} p : + Lemma fractional_half_equiv `{!Fractional Φ} p : Φ p ⊣⊢ Φ (p/2)%Qp ∗ Φ (p/2)%Qp. Proof. by rewrite -(fractional (p/2) (p/2)) Qp_div_2. Qed. - Lemma fractional_half `{Fractional _ Φ} p : + Lemma fractional_half `{!Fractional Φ} p : Φ p ⊢ Φ (p/2)%Qp ∗ Φ (p/2)%Qp. Proof. by rewrite fractional_half_equiv. Qed. - Lemma half_fractional `{Fractional _ Φ} p q : + Lemma half_fractional `{!Fractional Φ} p q : Φ (p/2)%Qp ∗ Φ (p/2)%Qp ⊢ Φ p. Proof. by rewrite -fractional_half_equiv. Qed. (** Fractional and logical connectives *) - Global Instance persistent_fractional P : PersistentP P → Fractional (λ _, P). Proof. intros HP q q'. by apply uPred_derived.always_sep_dup. Qed. -- GitLab