fractional.v 7.71 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Import gmap gmultiset.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
2
From iris.base_logic Require Export derived.
3
From iris.base_logic Require Import big_op.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
4
From iris.proofmode Require Import classes class_instances.
5
Set Default Proof Using "Type".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
6 7 8

Class Fractional {M} (Φ : Qp  uPred M) :=
  fractional p q : Φ (p + q)%Qp  Φ p  Φ q.
9 10 11 12
Class AsFractional {M} (P : uPred M) (Φ : Qp  uPred M) (q : Qp) := {
  as_fractional : P  Φ q;
  as_fractional_fractional :> Fractional Φ
}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
13 14 15 16 17 18 19 20 21 22

Arguments fractional {_ _ _} _ _.

Hint Mode AsFractional - + - - : typeclass_instances.
Hint Mode AsFractional - - + + : typeclass_instances.

Section fractional.
  Context {M : ucmraT}.
  Implicit Types P Q : uPred M.
  Implicit Types Φ : Qp  uPred M.
23
  Implicit Types q : Qp.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
24

25 26 27
  Lemma fractional_split P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    P  P1  P2.
28 29 30 31 32 33 34 35 36 37
  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.
  Proof. intros. by rewrite -fractional_split. Qed.
  Lemma fractional_split_2 P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    P1 - P2 - P.
  Proof. intros. apply uPred.wand_intro_r. by rewrite -fractional_split. Qed.

38 39 40
  Lemma fractional_half P P12 Φ q :
    AsFractional P Φ q  AsFractional P12 Φ (q/2) 
    P  P12  P12.
41 42 43 44 45 46 47 48 49
  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.
  Proof. intros. by rewrite -fractional_half. Qed.
  Lemma fractional_half_2 P P12 Φ q :
    AsFractional P Φ q  AsFractional P12 Φ (q/2) 
    P12 - P12 - P.
  Proof. intros. apply uPred.wand_intro_r. by rewrite -fractional_half. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
50

51 52 53
  (** Fractional and logical connectives *)
  Global Instance persistent_fractional P :
    PersistentP P  Fractional (λ _, P).
54
  Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
55 56 57 58 59

  Global Instance fractional_sep Φ Ψ :
    Fractional Φ  Fractional Ψ  Fractional (λ q, Φ q  Ψ q)%I.
  Proof.
    intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
60
    rewrite !assoc. f_equiv. by rewrite comm.
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
  Qed.

  Global Instance fractional_big_sepL {A} l Ψ :
    ( k (x : A), Fractional (Ψ k x)) 
    Fractional (M:=M) (λ q, [ list] kx  l, Ψ k x q)%I.
  Proof.
    intros ? q q'. rewrite -big_sepL_sepL. by setoid_rewrite fractional.
  Qed.

  Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
    ( k (x : A), Fractional (Ψ k x)) 
    Fractional (M:=M) (λ q, [ map] kx  m, Ψ k x q)%I.
  Proof.
    intros ? q q'. rewrite -big_sepM_sepM. by setoid_rewrite fractional.
  Qed.

  Global Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ :
    ( x, Fractional (Ψ x)) 
    Fractional (M:=M) (λ q, [ set] x  X, Ψ x q)%I.
  Proof.
    intros ? q q'. rewrite -big_sepS_sepS. by setoid_rewrite fractional.
  Qed.

  Global Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ :
    ( x, Fractional (Ψ x)) 
    Fractional (M:=M) (λ q, [ mset] x  X, Ψ x q)%I.
  Proof.
    intros ? q q'. rewrite -big_sepMS_sepMS. by setoid_rewrite fractional.
  Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
91 92 93
  (** Mult instances *)

  Global Instance mult_fractional_l Φ Ψ p :
94 95 96 97
    ( 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's avatar
Jacques-Henri Jourdan committed
98
  Global Instance mult_fractional_r Φ Ψ p :
99 100 101 102
    ( 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's avatar
Jacques-Henri Jourdan committed
103 104 105 106 107 108 109 110

  (* 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.
111 112 113 114
  Proof.
    intros H. split. apply H. eapply (mult_fractional_l _ Φ p).
    split. done. apply H.
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
115 116
  Instance mult_as_fractional_r P Φ p q :
    AsFractional P Φ (p * q)  AsFractional P (λ q, Φ (p * q)%Qp) q.
117 118 119 120
  Proof.
    intros H. split. apply H. eapply (mult_fractional_r _ Φ p).
    split. done. apply H.
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
121 122

  (** Proof mode instances *)
123
  Global Instance from_and_fractional_fwd P P1 P2 Φ q1 q2 :
124
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
125 126
    FromAnd false P P1 P2.
  Proof. by rewrite /FromAnd=>-[-> ->] [-> _] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
127
  Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
128
    AsFractional P1 Φ q1  AsFractional P2 Φ q2  AsFractional P Φ (q1 + q2) 
129 130
    FromAnd false P P1 P2 | 10.
  Proof. by rewrite /FromAnd=>-[-> _] [-> <-] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
131

132
  Global Instance from_and_fractional_half_fwd P Q Φ q :
133
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
134 135 136
    FromAnd false P Q Q | 10.
  Proof. by rewrite /FromAnd -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed.
  Global Instance from_and_fractional_half_bwd P Q Φ q :
137
    AsFractional P Φ (q/2)  AsFractional Q Φ q 
138 139
    FromAnd false Q P P.
  Proof. rewrite /FromAnd=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
140

Ralf Jung's avatar
Ralf Jung committed
141
  Global Instance into_and_fractional b P P1 P2 Φ q1 q2 :
142
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
Ralf Jung's avatar
Ralf Jung committed
143 144
    IntoAnd b P P1 P2.
  Proof.
145 146 147
    (* TODO: We need a better way to handle this boolean here; always
       applying mk_into_and_sep (which only works after introducing all
       assumptions) is rather annoying.
Ralf Jung's avatar
Ralf Jung committed
148 149 150
       Ideally, it'd not even be possible to make the mistake that
       was originally made here, which is to give this instance for
       "false" only, thus breaking some intro patterns. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
151
    intros. apply mk_into_and_sep. rewrite [P]fractional_split //.
Ralf Jung's avatar
Ralf Jung committed
152 153
  Qed.
  Global Instance into_and_fractional_half b P Q Φ q :
154
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
Ralf Jung's avatar
Ralf Jung committed
155
    IntoAnd b P Q Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  Proof. intros. apply mk_into_and_sep. rewrite [P]fractional_half //. Qed.
157 158 159 160

  (* The instance [frame_fractional] can be tried at all the nodes of
     the proof search. The proof search then fails almost always on
     [AsFractional R Φ r], but the slowdown is still noticeable.  For
161
     that reason, we factorize the three instances that could have been
162
     defined for that purpose into one. *)
163 164 165
  Inductive FrameFractionalHyps
      (p : bool) (R : uPred M) (Φ : Qp  uPred M) (RES : uPred M) : Qp  Qp  Prop :=
    | frame_fractional_hyps_l Q q q' r:
166 167
       Frame p R (Φ q) Q 
       MakeSep Q (Φ q') RES 
168 169
       FrameFractionalHyps p R Φ RES r (q + q')
    | frame_fractional_hyps_r Q q q' r:
170 171
       Frame p R (Φ q') Q 
       MakeSep Q (Φ q) RES 
172 173 174 175
       FrameFractionalHyps p R Φ RES r (q + q')
    | frame_fractional_hyps_half q :
       AsFractional RES Φ (q/2) 
       FrameFractionalHyps p R Φ RES (q/2) q.
176 177
  Existing Class FrameFractionalHyps.
  Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
178
    frame_fractional_hyps_half.
179

180 181 182 183
  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's avatar
Jacques-Henri Jourdan committed
184
  Proof.
185
    rewrite /Frame=>-[HR _][->?]H.
186
    revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
187 188
    - rewrite fractional=><-<-. by rewrite assoc.
    - rewrite fractional=><-<-=>_.
189 190
      by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
    - move=>-[-> _]->. by rewrite uPred.always_if_elim -fractional Qp_div_2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
191 192
  Qed.
End fractional.