fractional.v 5.95 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 8 9 10 11 12 13 14 15 16 17 18 19 20 21
From iris.proofmode Require Import classes class_instances.

Class Fractional {M} (Φ : Qp  uPred M) :=
  fractional p q : Φ (p + q)%Qp  Φ p  Φ q.
Class AsFractional {M} (P : uPred M) (Φ : Qp  uPred M) (q : Qp) :=
  as_fractional : P  Φ q.

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

38 39 40 41 42 43 44 45 46
  (** 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.
47
    rewrite !assoc. f_equiv. by rewrite comm.
48 49 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
  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
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
  (** Mult instances *)

  Global Instance mult_fractional_l Φ Ψ p :
    ( q, AsFractional (Φ q) Ψ (q * p))  Fractional Ψ  Fractional Φ.
  Proof. intros AF F q q'. by rewrite !AF Qp_mult_plus_distr_l F. Qed.
  Global Instance mult_fractional_r Φ Ψ p :
    ( q, AsFractional (Φ q) Ψ (p * q))  Fractional Ψ  Fractional Φ.
  Proof. intros AF F q q'. by rewrite !AF Qp_mult_plus_distr_r F. Qed.

  (* 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.
  Proof. done. Qed.
  Instance mult_as_fractional_r P Φ p q :
    AsFractional P Φ (p * q)  AsFractional P (λ q, Φ (p * q)%Qp) q.
  Proof. done. Qed.

  (** Proof mode instances *)
  Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2)  Fractional Φ 
    AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    FromSep P P1 P2.
  Proof. by rewrite /FromSep=> -> -> -> ->. Qed.
  Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
    AsFractional P1 Φ q1  AsFractional P2 Φ q2  Fractional Φ 
    AsFractional P Φ (q1 + q2) 
    FromSep P P1 P2 | 10.
  Proof. by rewrite /FromSep=> -> -> <- ->. Qed.

  Global Instance from_sep_fractional_half_fwd P Q Φ q :
    AsFractional P Φ q  Fractional Φ 
    AsFractional Q Φ (q/2) 
    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 :
    AsFractional P Φ (q/2)  Fractional Φ 
    AsFractional Q Φ q 
    FromSep Q P P.
  Proof. rewrite /FromSep=> -> <- ->. by rewrite Qp_div_2. Qed.

  Global Instance into_and_fractional P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2)  Fractional Φ 
    AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    IntoAnd false P P1 P2.
  Proof. by rewrite /AsFractional /IntoAnd=>->->->->. Qed.
  Global Instance into_and_fractional_half P Q Φ q :
    AsFractional P Φ q  Fractional Φ 
    AsFractional Q Φ (q/2) 
    IntoAnd false P Q Q | 100.
  Proof. by rewrite /AsFractional /IntoAnd -{1}(Qp_div_2 q)=>->->->. Qed.

  Global Instance frame_fractional_l R Q PP' QP' Φ r p p' :
    AsFractional R Φ r  AsFractional PP' Φ (p + p')  Fractional Φ 
    Frame R (Φ p) Q  MakeSep Q (Φ p') QP'  Frame R PP' QP'.
  Proof. rewrite /Frame=>->->-><-<-. by rewrite assoc. Qed.
  Global Instance frame_fractional_r R Q PP' PQ Φ r p p' :
    AsFractional R Φ r  AsFractional PP' Φ (p + p')  Fractional Φ 
    Frame R (Φ p') Q  MakeSep (Φ p) Q PQ  Frame R PP' PQ.
  Proof.
141
    rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
142 143 144 145 146 147 148
  Qed.
  Global Instance frame_fractional_half P Q R Φ p:
    AsFractional R Φ (p/2)  AsFractional P Φ p  Fractional Φ 
    AsFractional Q Φ (p/2)%Qp 
    Frame R P Q.
  Proof. by rewrite /Frame -{2}(Qp_div_2 p)=>->->->->. Qed.
End fractional.