fractional.v 7.93 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.bi Require Export bi.
2
From iris.proofmode Require Import classes class_instances.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.prelude Require Import options.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
4

Robbert Krebbers's avatar
Robbert Krebbers committed
5
Class Fractional {PROP : bi} (Φ : Qp  PROP) :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
6
  fractional p q : Φ (p + q)%Qp  Φ p  Φ q.
Ralf Jung's avatar
Ralf Jung committed
7
Global Arguments Fractional {_} _%I : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9

Class AsFractional {PROP : bi} (P : PROP) (Φ : Qp  PROP) (q : Qp) := {
10
11
12
  as_fractional : P  Φ q;
  as_fractional_fractional :> Fractional Φ
}.
Ralf Jung's avatar
Ralf Jung committed
13
Global Arguments AsFractional {_} _%I _%I _%Qp.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
14

Ralf Jung's avatar
Ralf Jung committed
15
Global Arguments fractional {_ _ _} _ _.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
16

17
Global Hint Mode AsFractional - + - - : typeclass_instances.
18
19
(* To make [as_fractional_fractional] a useful instance, we have to
allow [q] to be an evar. *)
20
Global Hint Mode AsFractional - - + - : typeclass_instances.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
21
22

Section fractional.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
25
  Context {PROP : bi}.
  Implicit Types P Q : PROP.
  Implicit Types Φ : Qp  PROP.
26
  Implicit Types q : Qp.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
27

28
29
30
31
32
33
34
35
  Global Instance Fractional_proper :
    Proper (pointwise_relation _ () ==> iff) (@Fractional PROP).
  Proof.
    rewrite /Fractional.
    intros Φ1 Φ2 Hequiv.
    by setoid_rewrite Hequiv.
  Qed.

36
37
38
  Lemma fractional_split P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    P  P1  P2.
39
40
41
42
  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.
43
  Proof. intros. by rewrite -(fractional_split P). Qed.
44
45
46
  Lemma fractional_split_2 P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    P1 - P2 - P.
47
  Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
48

49
50
51
52
53
  Lemma fractional_merge P1 P2 Φ q1 q2 `{!Fractional Φ} :
    AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    P1 - P2 - Φ (q1 + q2)%Qp.
  Proof. move=>-[-> _] [-> _]. rewrite fractional. apply bi.wand_intro_r. done. Qed.

54
55
56
  Lemma fractional_half P P12 Φ q :
    AsFractional P Φ q  AsFractional P12 Φ (q/2) 
    P  P12  P12.
57
58
59
60
  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.
61
  Proof. intros. by rewrite -(fractional_half P). Qed.
62
63
64
  Lemma fractional_half_2 P P12 Φ q :
    AsFractional P Φ q  AsFractional P12 Φ (q/2) 
    P12 - P12 - P.
65
  Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
66

67
  (** Fractional and logical connectives *)
68
69
  Global Instance persistent_fractional (P : PROP) :
    Persistent P  TCOr (Affine P) (Absorbing P)  Fractional (λ _, P).
70
  Proof. intros ?? q q'. apply: bi.persistent_sep_dup. Qed.
71
72
73
74
75

  Global Instance fractional_sep Φ Ψ :
    Fractional Φ  Fractional Ψ  Fractional (λ q, Φ q  Ψ q)%I.
  Proof.
    intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
76
    rewrite !assoc. f_equiv. by rewrite comm.
77
78
79
80
  Qed.

  Global Instance fractional_big_sepL {A} l Ψ :
    ( k (x : A), Fractional (Ψ k x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    Fractional (PROP:=PROP) (λ q, [ list] kx  l, Ψ k x q)%I.
82
  Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed.
83
84
85

  Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
    ( k (x : A), Fractional (Ψ k x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
86
    Fractional (PROP:=PROP) (λ q, [ map] kx  m, Ψ k x q)%I.
87
  Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.
88
89
90

  Global Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ :
    ( x, Fractional (Ψ x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    Fractional (PROP:=PROP) (λ q, [ set] x  X, Ψ x q)%I.
92
  Proof. intros ? q q'. rewrite -big_sepS_sep. by setoid_rewrite fractional. Qed.
93
94
95

  Global Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ :
    ( x, Fractional (Ψ x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
96
    Fractional (PROP:=PROP) (λ q, [ mset] x  X, Ψ x q)%I.
97
  Proof. intros ? q q'. rewrite -big_sepMS_sep. by setoid_rewrite fractional. Qed.
98

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
99
100
  (** Mult instances *)

Robbert Krebbers's avatar
Robbert Krebbers committed
101
  Global Instance mul_fractional_l Φ Ψ p :
102
103
    ( q, AsFractional (Φ q) Ψ (q * p))  Fractional Φ.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
    intros H q q'. rewrite ->!as_fractional, Qp_mul_add_distr_r. by apply H.
105
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
  Global Instance mul_fractional_r Φ Ψ p :
107
108
    ( q, AsFractional (Φ q) Ψ (p * q))  Fractional Φ.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
    intros H q q'. rewrite ->!as_fractional, Qp_mul_add_distr_l. by apply H.
110
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
111
112
113
114
115
116

  (* 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. *)
117
  Local Instance mul_as_fractional_l P Φ p q :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
118
    AsFractional P Φ (q * p)  AsFractional P (λ q, Φ (q * p)%Qp) q.
119
  Proof.
120
121
    intros H. split; first apply H. eapply (mul_fractional_l _ Φ p).
    split; first done. apply H.
122
  Qed.
123
  Local Instance mul_as_fractional_r P Φ p q :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
124
    AsFractional P Φ (p * q)  AsFractional P (λ q, Φ (p * q)%Qp) q.
125
  Proof.
126
127
    intros H. split; first apply H. eapply (mul_fractional_r _ Φ p).
    split; first done. apply H.
128
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
129
130

  (** Proof mode instances *)
131
  Global Instance from_and_fractional_fwd P P1 P2 Φ q1 q2 :
132
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
    FromSep P P1 P2.
  Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
135
  Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
136
    AsFractional P1 Φ q1  AsFractional P2 Φ q2  AsFractional P Φ (q1 + q2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
    FromSep P P1 P2 | 10.
  Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
139

Robbert Krebbers's avatar
Robbert Krebbers committed
140
  Global Instance from_sep_fractional_half_fwd P Q Φ q :
141
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
    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 :
145
    AsFractional P Φ (q/2)  AsFractional Q Φ q 
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
    FromSep Q P P.
  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
148

149
  Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
150
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
151
    IntoSep P P1 P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
153
  Proof. intros. rewrite /IntoSep [P]fractional_split //. Qed.

154
  Global Instance into_sep_fractional_half P Q Φ q :
155
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
156
    IntoSep P Q Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
158
159

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

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