fractional.v 7.41 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_bi.
3
Set Default Proof Using "Type".
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
Arguments Fractional {_} _%I : simpl never.

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

Arguments fractional {_ _ _} _ _.

Hint Mode AsFractional - + - - : typeclass_instances.
18
19
20
(* To make [as_fractional_fractional] a useful instance, we have to
allow [q] to be an evar. *)
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
  Lemma fractional_split P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    P  P1  P2.
31
32
33
34
  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.
35
  Proof. intros. by rewrite -(fractional_split P). Qed.
36
37
38
  Lemma fractional_split_2 P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
    P1 - P2 - P.
39
  Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
40

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

54
55
  (** Fractional and logical connectives *)
  Global Instance persistent_fractional P :
56
57
    Persistent P  Absorbing P  Fractional (λ _, P).
  Proof. intros ?? q q'. by apply bi.persistent_sep_dup. Qed.
58
59
60
61
62

  Global Instance fractional_sep Φ Ψ :
    Fractional Φ  Fractional Ψ  Fractional (λ q, Φ q  Ψ q)%I.
  Proof.
    intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
63
    rewrite !assoc. f_equiv. by rewrite comm.
64
65
66
67
  Qed.

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

  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
73
    Fractional (PROP:=PROP) (λ q, [ map] kx  m, Ψ k x q)%I.
74
  Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.
75
76
77

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

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
86
87
88
  (** Mult instances *)

  Global Instance mult_fractional_l Φ Ψ p :
89
90
91
92
    ( 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
93
  Global Instance mult_fractional_r Φ Ψ p :
94
95
96
97
    ( 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
98
99
100
101
102
103
104
105

  (* 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.
106
107
108
109
  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
110
111
  Instance mult_as_fractional_r P Φ p q :
    AsFractional P Φ (p * q)  AsFractional P (λ q, Φ (p * q)%Qp) q.
112
113
114
115
  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
116
117

  (** Proof mode instances *)
118
  Global Instance from_and_fractional_fwd P P1 P2 Φ q1 q2 :
119
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
    FromSep P P1 P2.
  Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
122
  Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
123
    AsFractional P1 Φ q1  AsFractional P2 Φ q2  AsFractional P Φ (q1 + q2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
    FromSep P P1 P2 | 10.
  Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
126

Robbert Krebbers's avatar
Robbert Krebbers committed
127
  Global Instance from_sep_fractional_half_fwd P Q Φ q :
128
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
131
    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 :
132
    AsFractional P Φ (q/2)  AsFractional Q Φ q 
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
    FromSep Q P P.
  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
135

136
  Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
137
    AsFractional P Φ (q1 + q2)  AsFractional P1 Φ q1  AsFractional P2 Φ q2 
138
    IntoSep P P1 P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
  Proof. intros. rewrite /IntoSep [P]fractional_split //. Qed.

141
  Global Instance into_sep_fractional_half P Q Φ q :
142
    AsFractional P Φ q  AsFractional Q Φ (q/2) 
143
    IntoSep P Q Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
145
146

  (* The instance [frame_fractional] can be tried at all the nodes of
147
     the proof search. The proof search then fails almost always on
148
     [AsFractional R Φ r], but the slowdown is still noticeable.  For
149
     that reason, we factorize the three instances that could have been
150
     defined for that purpose into one. *)
151
  Inductive FrameFractionalHyps
Robbert Krebbers's avatar
Robbert Krebbers committed
152
      (p : bool) (R : PROP) (Φ : Qp  PROP) (RES : PROP) : Qp  Qp  Prop :=
153
    | frame_fractional_hyps_l Q q q' r:
154
155
       Frame p R (Φ q) Q 
       MakeSep Q (Φ q') RES 
156
157
       FrameFractionalHyps p R Φ RES r (q + q')
    | frame_fractional_hyps_r Q q q' r:
158
159
       Frame p R (Φ q') Q 
       MakeSep Q (Φ q) RES 
160
161
162
163
       FrameFractionalHyps p R Φ RES r (q + q')
    | frame_fractional_hyps_half q :
       AsFractional RES Φ (q/2) 
       FrameFractionalHyps p R Φ RES (q/2) q.
164
165
  Existing Class FrameFractionalHyps.
  Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
166
    frame_fractional_hyps_half.
167

168
169
170
171
  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
172
  Proof.
173
    rewrite /Frame=>-[HR _][->?]H.
174
    revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
    - rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
    - rewrite fractional /Frame /MakeSep=><-<-=>_.
177
      by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
178
    - move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp_div_2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
179
180
  Qed.
End fractional.