fractional.v 6.65 KB
Newer Older
1
From iris.prelude 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 5 6 7
From iris.proofmode Require Import classes class_instances.

Class Fractional {M} (Φ : Qp  uPred M) :=
  fractional p q : Φ (p + q)%Qp  Φ p  Φ q.
8 9 10 11
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
12 13 14 15 16 17 18 19 20 21 22 23

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.
  Implicit Types p q : Qp.

Robbert Krebbers's avatar
Robbert Krebbers committed
24
  Lemma fractional_split `{!Fractional Φ} p q :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
25 26
    Φ (p + q)%Qp  Φ p  Φ q.
  Proof. by rewrite fractional. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  Lemma fractional_combine `{!Fractional Φ} p q :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
28 29
    Φ p  Φ q  Φ (p + q)%Qp.
  Proof. by rewrite fractional. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  Lemma fractional_half_equiv `{!Fractional Φ} p :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
31 32
    Φ p  Φ (p/2)%Qp  Φ (p/2)%Qp.
  Proof. by rewrite -(fractional (p/2) (p/2)) Qp_div_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  Lemma fractional_half `{!Fractional Φ} p :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
34 35
    Φ p  Φ (p/2)%Qp  Φ (p/2)%Qp.
  Proof. by rewrite fractional_half_equiv. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
  Lemma half_fractional `{!Fractional Φ} p q :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
37 38 39
    Φ (p/2)%Qp  Φ (p/2)%Qp  Φ p.
  Proof. by rewrite -fractional_half_equiv. Qed.

40 41 42 43 44 45 46 47 48
  (** 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.

  Global Instance fractional_sep Φ Ψ :
    Fractional Φ  Fractional Ψ  Fractional (λ q, Φ q  Ψ q)%I.
  Proof.
    intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
49
    rewrite !assoc. f_equiv. by rewrite comm.
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
  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
80 81 82
  (** Mult instances *)

  Global Instance mult_fractional_l Φ Ψ p :
83 84 85 86
    ( 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
87
  Global Instance mult_fractional_r Φ Ψ p :
88 89 90 91
    ( 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
92 93 94 95 96 97 98 99

  (* 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.
100 101 102 103
  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
104 105
  Instance mult_as_fractional_r P Φ p q :
    AsFractional P Φ (p * q)  AsFractional P (λ q, Φ (p * q)%Qp) q.
106 107 108 109
  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
110 111 112

  (** Proof mode instances *)
  Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
113
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
114
    FromSep P P1 P2.
115
  Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
116
  Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
117
    AsFractional P1 Φ q1  AsFractional P2 Φ q2  AsFractional P Φ (q1 + q2) 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
118
    FromSep P P1 P2 | 10.
119
  Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
120 121

  Global Instance from_sep_fractional_half_fwd P Q Φ q :
122
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
123
    FromSep P Q Q | 10.
124
  Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
125
  Global Instance from_sep_fractional_half_bwd P Q Φ q :
126
    AsFractional P Φ (q/2)  AsFractional Q Φ q 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
127
    FromSep Q P P.
128
  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
129 130

  Global Instance into_and_fractional P P1 P2 Φ q1 q2 :
131
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
132
    IntoAnd false P P1 P2.
133
  Proof. by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
134
  Global Instance into_and_fractional_half P Q Φ q :
135
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
136
    IntoAnd false P Q Q | 100.
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
  Proof. by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed.

  (* 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
     that reason, we factorize the three instances that could ave been
     defined for that purpose into one. *)
  Inductive FrameFractionalHyps R Φ RES : Qp  Qp  Prop :=
  | frame_fractional_hyps_l Q p p' r:
      Frame R (Φ p) Q  MakeSep Q (Φ p') RES 
      FrameFractionalHyps R Φ RES r (p + p')
  | frame_fractional_hyps_r Q p p' r:
      Frame R (Φ p') Q  MakeSep Q (Φ p) RES 
      FrameFractionalHyps R Φ RES r (p + p')
  | frame_fractional_hyps_half p:
      AsFractional RES Φ (p/2)%Qp  FrameFractionalHyps R Φ RES (p/2)%Qp p.
  Existing Class FrameFractionalHyps.
  Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
         frame_fractional_hyps_half.
  Global Instance frame_fractional R r Φ P p RES:
    AsFractional R Φ r  AsFractional P Φ p  FrameFractionalHyps R Φ RES r p 
    Frame R P RES.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
159
  Proof.
160 161 162 163 164 165
    rewrite /Frame=>-[HR _][->?]H.
    revert H HR=>-[Q p0 p0' r0|Q p0 p0' r0|p0].
    - rewrite fractional=><-<-. by rewrite assoc.
    - rewrite fractional=><-<-=>_.
      rewrite (comm _ Q (Φ p0)) !assoc. f_equiv. by rewrite comm.
    - move=>-[-> _]->. by rewrite -fractional Qp_div_2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
166 167
  Qed.
End fractional.