fractional.v 7.41 KB
 Robbert Krebbers committed Oct 30, 2017 1 ``````From iris.bi Require Export bi. `````` Ralf Jung committed Mar 21, 2018 2 ``````From iris.proofmode Require Import classes class_instances_bi. `````` Ralf Jung committed Jan 05, 2017 3 ``````Set Default Proof Using "Type". `````` Jacques-Henri Jourdan committed Nov 23, 2016 4 `````` `````` Robbert Krebbers committed Oct 30, 2017 5 ``````Class Fractional {PROP : bi} (Φ : Qp → PROP) := `````` Jacques-Henri Jourdan committed Nov 23, 2016 6 `````` fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q. `````` Robbert Krebbers committed Oct 30, 2017 7 8 9 ``````Arguments Fractional {_} _%I : simpl never. Class AsFractional {PROP : bi} (P : PROP) (Φ : Qp → PROP) (q : Qp) := { `````` Jacques-Henri Jourdan committed Dec 13, 2016 10 11 12 `````` as_fractional : P ⊣⊢ Φ q; as_fractional_fractional :> Fractional Φ }. `````` Robbert Krebbers committed Oct 30, 2017 13 ``````Arguments AsFractional {_} _%I _%I _%Qp. `````` Jacques-Henri Jourdan committed Nov 23, 2016 14 15 16 17 `````` Arguments fractional {_ _ _} _ _. Hint Mode AsFractional - + - - : typeclass_instances. `````` Ralf Jung committed May 13, 2019 18 19 20 ``````(* To make [as_fractional_fractional] a useful instance, we have to allow [q] to be an evar. *) Hint Mode AsFractional - - + - : typeclass_instances. `````` Jacques-Henri Jourdan committed Nov 23, 2016 21 22 `````` Section fractional. `````` Robbert Krebbers committed Oct 30, 2017 23 24 25 `````` Context {PROP : bi}. Implicit Types P Q : PROP. Implicit Types Φ : Qp → PROP. `````` Robbert Krebbers committed Mar 15, 2017 26 `````` Implicit Types q : Qp. `````` Jacques-Henri Jourdan committed Nov 23, 2016 27 `````` `````` Ralf Jung committed Mar 15, 2017 28 29 30 `````` Lemma fractional_split P P1 P2 Φ q1 q2 : AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → P ⊣⊢ P1 ∗ P2. `````` Robbert Krebbers committed Mar 21, 2017 31 32 33 34 `````` Proof. by move=>-[-> ->] [-> _] [-> _]. Qed. Lemma fractional_split_1 P P1 P2 Φ q1 q2 : AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → P -∗ P1 ∗ P2. `````` Robbert Krebbers committed Apr 25, 2019 35 `````` Proof. intros. by rewrite -(fractional_split P). Qed. `````` Robbert Krebbers committed Mar 21, 2017 36 37 38 `````` Lemma fractional_split_2 P P1 P2 Φ q1 q2 : AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → P1 -∗ P2 -∗ P. `````` Robbert Krebbers committed Apr 25, 2019 39 `````` Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed. `````` Robbert Krebbers committed Mar 21, 2017 40 `````` `````` Ralf Jung committed Mar 15, 2017 41 42 43 `````` Lemma fractional_half P P12 Φ q : AsFractional P Φ q → AsFractional P12 Φ (q/2) → P ⊣⊢ P12 ∗ P12. `````` Robbert Krebbers committed Mar 21, 2017 44 45 46 47 `````` Proof. by rewrite -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed. Lemma fractional_half_1 P P12 Φ q : AsFractional P Φ q → AsFractional P12 Φ (q/2) → P -∗ P12 ∗ P12. `````` Robbert Krebbers committed Apr 25, 2019 48 `````` Proof. intros. by rewrite -(fractional_half P). Qed. `````` Robbert Krebbers committed Mar 21, 2017 49 50 51 `````` Lemma fractional_half_2 P P12 Φ q : AsFractional P Φ q → AsFractional P12 Φ (q/2) → P12 -∗ P12 -∗ P. `````` Robbert Krebbers committed Apr 25, 2019 52 `````` Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed. `````` Jacques-Henri Jourdan committed Nov 23, 2016 53 `````` `````` Jacques-Henri Jourdan committed Dec 06, 2016 54 55 `````` (** Fractional and logical connectives *) Global Instance persistent_fractional P : `````` Robbert Krebbers committed Oct 30, 2017 56 57 `````` Persistent P → Absorbing P → Fractional (λ _, P). Proof. intros ?? q q'. by apply bi.persistent_sep_dup. Qed. `````` Jacques-Henri Jourdan committed Dec 06, 2016 58 59 60 61 62 `````` Global Instance fractional_sep Φ Ψ : Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I. Proof. intros ?? q q'. rewrite !fractional -!assoc. f_equiv. `````` Jacques-Henri Jourdan committed Dec 06, 2016 63 `````` rewrite !assoc. f_equiv. by rewrite comm. `````` Jacques-Henri Jourdan committed Dec 06, 2016 64 65 66 67 `````` Qed. Global Instance fractional_big_sepL {A} l Ψ : (∀ k (x : A), Fractional (Ψ k x)) → `````` Robbert Krebbers committed Oct 30, 2017 68 `````` Fractional (PROP:=PROP) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I. `````` Robbert Krebbers committed May 01, 2019 69 `````` Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed. `````` Jacques-Henri Jourdan committed Dec 06, 2016 70 71 72 `````` Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ : (∀ k (x : A), Fractional (Ψ k x)) → `````` Robbert Krebbers committed Oct 30, 2017 73 `````` Fractional (PROP:=PROP) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I. `````` Robbert Krebbers committed May 01, 2019 74 `````` Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed. `````` Jacques-Henri Jourdan committed Dec 06, 2016 75 76 77 `````` Global Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ : (∀ x, Fractional (Ψ x)) → `````` Robbert Krebbers committed Oct 30, 2017 78 `````` Fractional (PROP:=PROP) (λ q, [∗ set] x ∈ X, Ψ x q)%I. `````` Robbert Krebbers committed May 01, 2019 79 `````` Proof. intros ? q q'. rewrite -big_sepS_sep. by setoid_rewrite fractional. Qed. `````` Jacques-Henri Jourdan committed Dec 06, 2016 80 81 82 `````` Global Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ : (∀ x, Fractional (Ψ x)) → `````` Robbert Krebbers committed Oct 30, 2017 83 `````` Fractional (PROP:=PROP) (λ q, [∗ mset] x ∈ X, Ψ x q)%I. `````` Robbert Krebbers committed May 01, 2019 84 `````` Proof. intros ? q q'. rewrite -big_sepMS_sep. by setoid_rewrite fractional. Qed. `````` Jacques-Henri Jourdan committed Dec 06, 2016 85 `````` `````` Jacques-Henri Jourdan committed Nov 23, 2016 86 87 88 `````` (** Mult instances *) Global Instance mult_fractional_l Φ Ψ p : `````` Jacques-Henri Jourdan committed Dec 13, 2016 89 90 91 92 `````` (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Φ. Proof. intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_l. by apply H. Qed. `````` Jacques-Henri Jourdan committed Nov 23, 2016 93 `````` Global Instance mult_fractional_r Φ Ψ p : `````` Jacques-Henri Jourdan committed Dec 13, 2016 94 95 96 97 `````` (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Φ. Proof. intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_r. by apply H. Qed. `````` Jacques-Henri Jourdan committed Nov 23, 2016 98 99 100 101 102 103 104 105 `````` (* REMARK: These two instances do not work in either direction of the search: - In the forward direction, they make the search not terminate - In the backward direction, the higher order unification of Φ with the goal does not work. *) Instance mult_as_fractional_l P Φ p q : AsFractional P Φ (q * p) → AsFractional P (λ q, Φ (q * p)%Qp) q. `````` Jacques-Henri Jourdan committed Dec 13, 2016 106 107 108 109 `````` Proof. intros H. split. apply H. eapply (mult_fractional_l _ Φ p). split. done. apply H. Qed. `````` Jacques-Henri Jourdan committed Nov 23, 2016 110 111 `````` Instance mult_as_fractional_r P Φ p q : AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) q. `````` Jacques-Henri Jourdan committed Dec 13, 2016 112 113 114 115 `````` Proof. intros H. split. apply H. eapply (mult_fractional_r _ Φ p). split. done. apply H. Qed. `````` Jacques-Henri Jourdan committed Nov 23, 2016 116 117 `````` (** Proof mode instances *) `````` Robbert Krebbers committed Mar 22, 2017 118 `````` Global Instance from_and_fractional_fwd P P1 P2 Φ q1 q2 : `````` Jacques-Henri Jourdan committed Dec 13, 2016 119 `````` AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → `````` Robbert Krebbers committed Oct 30, 2017 120 121 `````` FromSep P P1 P2. Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed. `````` Jacques-Henri Jourdan committed Nov 23, 2016 122 `````` Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 : `````` Jacques-Henri Jourdan committed Dec 13, 2016 123 `````` AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P Φ (q1 + q2) → `````` Robbert Krebbers committed Oct 30, 2017 124 125 `````` FromSep P P1 P2 | 10. Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed. `````` Jacques-Henri Jourdan committed Nov 23, 2016 126 `````` `````` Robbert Krebbers committed Oct 30, 2017 127 `````` Global Instance from_sep_fractional_half_fwd P Q Φ q : `````` Jacques-Henri Jourdan committed Dec 13, 2016 128 `````` AsFractional P Φ q → AsFractional Q Φ (q/2) → `````` Robbert Krebbers committed Oct 30, 2017 129 130 131 `````` FromSep P Q Q | 10. Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed. Global Instance from_sep_fractional_half_bwd P Q Φ q : `````` Jacques-Henri Jourdan committed Dec 13, 2016 132 `````` AsFractional P Φ (q/2) → AsFractional Q Φ q → `````` Robbert Krebbers committed Oct 30, 2017 133 134 `````` FromSep Q P P. Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed. `````` Jacques-Henri Jourdan committed Nov 23, 2016 135 `````` `````` Robbert Krebbers committed Oct 30, 2017 136 `````` Global Instance into_sep_fractional P P1 P2 Φ q1 q2 : `````` Jacques-Henri Jourdan committed Dec 13, 2016 137 `````` AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → `````` Robbert Krebbers committed Oct 30, 2017 138 `````` IntoSep P P1 P2. `````` Robbert Krebbers committed Oct 30, 2017 139 140 `````` Proof. intros. rewrite /IntoSep [P]fractional_split //. Qed. `````` Robbert Krebbers committed Oct 30, 2017 141 `````` Global Instance into_sep_fractional_half P Q Φ q : `````` Jacques-Henri Jourdan committed Dec 13, 2016 142 `````` AsFractional P Φ q → AsFractional Q Φ (q/2) → `````` Robbert Krebbers committed Oct 30, 2017 143 `````` IntoSep P Q Q | 100. `````` Robbert Krebbers committed Oct 30, 2017 144 `````` Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed. `````` Jacques-Henri Jourdan committed Dec 13, 2016 145 146 `````` (* The instance [frame_fractional] can be tried at all the nodes of `````` Jacques-Henri Jourdan committed Nov 03, 2017 147 `````` the proof search. The proof search then fails almost always on `````` Jacques-Henri Jourdan committed Dec 13, 2016 148 `````` [AsFractional R Φ r], but the slowdown is still noticeable. For `````` Ralf Jung committed Mar 15, 2017 149 `````` that reason, we factorize the three instances that could have been `````` Jacques-Henri Jourdan committed Dec 13, 2016 150 `````` defined for that purpose into one. *) `````` Robbert Krebbers committed Mar 15, 2017 151 `````` Inductive FrameFractionalHyps `````` Robbert Krebbers committed Oct 30, 2017 152 `````` (p : bool) (R : PROP) (Φ : Qp → PROP) (RES : PROP) : Qp → Qp → Prop := `````` Robbert Krebbers committed Mar 15, 2017 153 `````` | frame_fractional_hyps_l Q q q' r: `````` Robbert Krebbers committed Mar 22, 2017 154 155 `````` Frame p R (Φ q) Q → MakeSep Q (Φ q') RES → `````` Robbert Krebbers committed Mar 15, 2017 156 157 `````` FrameFractionalHyps p R Φ RES r (q + q') | frame_fractional_hyps_r Q q q' r: `````` Robbert Krebbers committed Mar 22, 2017 158 159 `````` Frame p R (Φ q') Q → MakeSep Q (Φ q) RES → `````` Robbert Krebbers committed Mar 15, 2017 160 161 162 163 `````` FrameFractionalHyps p R Φ RES r (q + q') | frame_fractional_hyps_half q : AsFractional RES Φ (q/2) → FrameFractionalHyps p R Φ RES (q/2) q. `````` Jacques-Henri Jourdan committed Dec 13, 2016 164 165 `````` Existing Class FrameFractionalHyps. Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r `````` Robbert Krebbers committed Mar 15, 2017 166 `````` frame_fractional_hyps_half. `````` Robbert Krebbers committed Mar 22, 2017 167 `````` `````` Robbert Krebbers committed Mar 15, 2017 168 169 170 171 `````` Global Instance frame_fractional p R r Φ P q RES: AsFractional R Φ r → AsFractional P Φ q → FrameFractionalHyps p R Φ RES r q → Frame p R P RES. `````` Jacques-Henri Jourdan committed Nov 23, 2016 172 `````` Proof. `````` Jacques-Henri Jourdan committed Dec 13, 2016 173 `````` rewrite /Frame=>-[HR _][->?]H. `````` Robbert Krebbers committed Mar 15, 2017 174 `````` revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0]. `````` Robbert Krebbers committed Oct 30, 2017 175 176 `````` - rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc. - rewrite fractional /Frame /MakeSep=><-<-=>_. `````` Robbert Krebbers committed Mar 15, 2017 177 `````` by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)). `````` 178 `````` - move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp_div_2. `````` Jacques-Henri Jourdan committed Nov 23, 2016 179 180 `````` Qed. End fractional.``````