fractional.v 7.04 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
23
24

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

41
42
43
  (** Fractional and logical connectives *)
  Global Instance persistent_fractional P :
    PersistentP P  Fractional (λ _, P).
44
  Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
45
46
47
48
49

  Global Instance fractional_sep Φ Ψ :
    Fractional Φ  Fractional Ψ  Fractional (λ q, Φ q  Ψ q)%I.
  Proof.
    intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
50
    rewrite !assoc. f_equiv. by rewrite comm.
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
80
  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
81
82
83
  (** Mult instances *)

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
131
  Global Instance into_and_fractional b P P1 P2 Φ q1 q2 :
132
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
Ralf Jung's avatar
Ralf Jung committed
133
134
135
136
137
138
139
140
141
142
    IntoAnd b P P1 P2.
  Proof.
    (* TODO: We need a better way to handle this boolean here.
       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. *)
    intros H1 H2 H3. apply mk_into_and_sep. revert H1 H2 H3.
    by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _].
  Qed.
  Global Instance into_and_fractional_half b P Q Φ q :
143
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
Ralf Jung's avatar
Ralf Jung committed
144
145
146
147
148
    IntoAnd b P Q Q | 100.
  Proof.
    intros H1 H2. apply mk_into_and_sep. revert H1 H2.
    by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _].
  Qed.
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169

  (* 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
170
  Proof.
171
172
173
174
175
176
    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
177
178
  Qed.
End fractional.