pviewshifts.v 7.78 KB
Newer Older
1
From iris.program_logic Require Export iris.
2
From iris.program_logic Require Import wsat.
3
From iris.algebra Require Import upred_big_op gmap.
4
From iris.proofmode Require Import tactics classes.
5
Import uPred.
Ralf Jung's avatar
Ralf Jung committed
6

7
8
9
Program Definition pvs_def `{irisG Λ Σ}
    (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
  (wsat  ownE E1 =r=  (wsat  ownE E2  P))%I.
Ralf Jung's avatar
Ralf Jung committed
10
11
12
Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
Definition pvs := proj1_sig pvs_aux.
Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
13
14
Arguments pvs {_ _ _} _ _ _%I.
Instance: Params (@pvs) 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
15

16
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q)
17
  (at level 99, E1, E2 at level 50, Q at level 200,
18
   format "|={ E1 , E2 }=>  Q") : uPred_scope.
19
20
21
Notation "P ={ E1 , E2 }=★ Q" := (P - |={E1,E2}=> Q)%I
  (at level 99, E1,E2 at level 50, Q at level 200,
   format "P  ={ E1 , E2 }=★  Q") : uPred_scope.
22
23
24
Notation "P ={ E1 , E2 }=> Q" := (P  |={E1,E2}=> Q)
  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.

25
Notation "|={ E }=> Q" := (pvs E E Q)
26
27
28
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }=>  Q") : uPred_scope.
Notation "P ={ E }=★ Q" := (P - |={E}=> Q)%I
29
30
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=★  Q") : uPred_scope.
31
32
Notation "P ={ E }=> Q" := (P  |={E}=> Q)
  (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
33

34
Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2}=> ( |={E2,E1}=> Q))%I
35
36
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }▷=>  Q") : uPred_scope.
37
38
39
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }▷=>  Q") : uPred_scope.
40

Robbert Krebbers's avatar
Robbert Krebbers committed
41
Section pvs.
42
43
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
44

45
46
47
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ _ E1 E2).
Proof. rewrite pvs_eq. solve_proper. Qed.
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ _ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
Proof. apply ne_proper, _. Qed.

50
Lemma pvs_intro_mask E1 E2 P : E2  E1  P  |={E1,E2}=> |={E2,E1}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Proof.
52
  intros (E1''&->&?)%subseteq_disjoint_union_L.
53
54
55
  rewrite pvs_eq /pvs_def ownE_op //. iIntros "H ($ & $ & HE) !==>".
  iApply except_last_intro. iIntros "[$ $] !==>" . iApply except_last_intro.
  by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Qed.
57

58
Lemma except_last_pvs E1 E2 P :  (|={E1,E2}=> P) ={E1,E2}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Proof.
60
  rewrite pvs_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
Qed.
62

63
Lemma rvs_pvs E P : (|=r=> P) ={E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Proof.
65
  rewrite pvs_eq /pvs_def. iIntros "H [$ $]"; iVs "H".
66
  iVsIntro. by iApply except_last_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Qed.
68

69
Lemma pvs_mono E1 E2 P Q : (P  Q)  (|={E1,E2}=> P) ={E1,E2}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof.
71
72
  rewrite pvs_eq /pvs_def. iIntros (HPQ) "HP HwE".
  rewrite -HPQ. by iApply "HP".
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Qed.
74

75
Lemma pvs_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
77
  rewrite pvs_eq /pvs_def. iIntros "HP HwE".
78
  iVs ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
80

81
82
Lemma pvs_mask_frame_r' E1 E2 Ef P :
  E1  Ef  (|={E1,E2}=> E2  Ef  P) ={E1  Ef,E2  Ef}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Proof.
84
  intros. rewrite pvs_eq /pvs_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
85
86
  iVs ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
  iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
87
  iVsIntro; iApply except_last_intro. by iApply "HP".
Robbert Krebbers's avatar
Robbert Krebbers committed
88
Qed.
89

90
91
Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P)  Q ={E1,E2}=> P  Q.
Proof. rewrite pvs_eq /pvs_def. by iIntros "[HwP $]". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92

93
(** * Derived rules *)
94
Global Instance pvs_mono' E1 E2 : Proper (() ==> ()) (@pvs Λ Σ _ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Proof. intros P Q; apply pvs_mono. Qed.
96
Global Instance pvs_flip_mono' E1 E2 :
97
  Proper (flip () ==> flip ()) (@pvs Λ Σ _ E1 E2).
98
Proof. intros P Q; apply pvs_mono. Qed.
99
100
101

Lemma pvs_intro E P : P ={E}=> P.
Proof. iIntros "HP". by iApply rvs_pvs. Qed.
102
103
Lemma pvs_except_last E1 E2 P : (|={E1,E2}=>  P) ={E1,E2}=> P.
Proof. by rewrite {1}(pvs_intro E2 P) except_last_pvs pvs_trans. Qed.
104

105
Lemma pvs_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q) ={E1,E2}=> P  Q.
106
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
107
Lemma pvs_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}=> Q.
108
Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
109
Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}=> Q.
110
Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
111

112
113
114
115
116
Lemma pvs_intro' E1 E2 P : E2  E1  ((|={E2,E1}=> True) - P) ={E1,E2}=> P.
Proof.
  iIntros (?) "Hw". iApply pvs_wand_l. iFrame. by iApply pvs_intro_mask.
Qed.

117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
Lemma pvs_trans_frame E1 E2 E3 P Q :
  ((Q ={E2,E3}= True)  |={E1,E2}=> (Q  P)) ={E1,E3}=> P.
Proof.
  rewrite pvs_frame_l assoc -(comm _ Q) wand_elim_r.
  by rewrite pvs_frame_r left_id pvs_trans.
Qed.

Lemma pvs_mask_frame_r E1 E2 Ef P :
  E1  Ef  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}=> P.
Proof.
  iIntros (?) "H". iApply pvs_mask_frame_r'; auto.
  iApply pvs_wand_r; iFrame "H"; eauto.
Qed.
Lemma pvs_mask_mono E1 E2 P : E1  E2  (|={E1}=> P) ={E2}=> P.
Proof.
  intros (Ef&->&?)%subseteq_disjoint_union_L. by apply pvs_mask_frame_r.
Qed.

135
Lemma pvs_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}=> P  Q.
136
137
Proof. by rewrite pvs_frame_r pvs_frame_l pvs_trans. Qed.
Lemma pvs_big_sepM `{Countable K} {A} E (Φ : K  A  iProp Σ) (m : gmap K A) :
138
  ([ map] kx  m, |={E}=> Φ k x) ={E}=> [ map] kx  m, Φ k x.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Proof.
140
141
  apply (big_opM_forall (λ P Q, P ={E}=> Q)); auto using pvs_intro.
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Qed.
143
Lemma pvs_big_sepS `{Countable A} E (Φ : A  iProp Σ) X :
144
  ([ set] x  X, |={E}=> Φ x) ={E}=> [ set] x  X, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof.
146
147
  apply (big_opS_forall (λ P Q, P ={E}=> Q)); auto using pvs_intro.
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
End pvs.
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200

(** Proofmode class instances *)
Section proofmode_classes.
  Context `{irisG Λ Σ}.
  Implicit Types P Q : iProp Σ.

  Global Instance from_pure_pvs E P φ : FromPure P φ  FromPure (|={E}=> P) φ.
  Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.

  Global Instance from_assumption_pvs E p P Q :
    FromAssumption p P (|=r=> Q)  FromAssumption p P (|={E}=> Q)%I.
  Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.

  Global Instance into_wand_pvs E1 E2 R P Q :
    IntoWand R P Q  IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
  Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.

  Global Instance from_sep_pvs E P Q1 Q2 :
    FromSep P Q1 Q2  FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
  Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.

  Global Instance or_split_pvs E1 E2 P Q1 Q2 :
    FromOr P Q1 Q2  FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
  Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.

  Global Instance exists_split_pvs {A} E1 E2 P (Φ : A  iProp Σ) :
    FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
  Proof.
    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
  Qed.

  Global Instance frame_pvs E1 E2 R P Q :
    Frame R P Q  Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
  Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.

  Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
  Proof. by rewrite /IsExceptLast except_last_pvs. Qed.

  Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
  Proof. by rewrite /FromVs -rvs_pvs. Qed.

  Global Instance elim_vs_rvs_pvs E1 E2 P Q :
    ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
  Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
  Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
    ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
  Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
End proofmode_classes.

Hint Extern 2 (coq_tactics.of_envs _  _) =>
  match goal with |- _  |={_}=> _ => iVsIntro end.