pviewshifts.v 8.76 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
From iris.proofmode Require Import coq_tactics spec_patterns.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export pviewshifts.
Import uPred.

Section pvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.

10
11
12
Global Instance to_assumption_pvs E p P Q :
  ToAssumption p P Q  ToAssumption p P (|={E}=> Q)%I.
Proof. rewrite /ToAssumption=>->. apply pvs_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
17
18
19
20
21
22
23
Global Instance sep_split_pvs E P Q1 Q2 :
  SepSplit P Q1 Q2  SepSplit (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /SepSplit=><-. apply pvs_sep. Qed.
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
  OrSplit P Q1 Q2  OrSplit (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /OrSplit=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
Global Instance exists_split_pvs {A} E1 E2 P (Φ : A  iProp Λ Σ) :
  ExistSplit P Φ  ExistSplit (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof.
  rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
24
Global Instance frame_pvs E1 E2 R P mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  Frame R P mQ 
26
  Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> if mQ is Some Q then Q else True))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
28
29
30
31
32
33
34
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance to_wand_pvs E1 E2 R P Q :
  ToWand R P Q  ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.

Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
    (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A  iProp Λ Σ) := {
  fsa_split : fsa E Φ  P;
35
  fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38
39
40
}.
Global Arguments fsa_split {_} _ _ _ _ _ {_}.
Global Instance fsa_split_pvs E P :
  FSASplit (|={E}=> P)%I E pvs_fsa True (λ _, P).
Proof. split. done. apply _. Qed.
41
42
43
Global Instance fsa_split_fsa {A} (fsa : FSA Λ Σ A) E Φ :
  FrameShiftAssertion fsaV fsa  FSASplit (fsa E Φ) E fsa fsaV Φ.
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
47

Lemma tac_pvs_intro Δ E Q : Δ  Q  Δ  |={E}=> Q.
Proof. intros ->. apply pvs_intro. Qed.

48
49
Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P' P Q :
  envs_lookup i Δ = Some (p, P')  P' = (|={E1,E2}=> P)%I 
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
52
53
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
  E2  E1  E3 
  Δ'  (|={E2,E3}=> Q)  Δ  |={E1,E3}=> Q.
Proof.
54
  intros ? -> ?? HQ. rewrite envs_replace_sound //; simpl. destruct p.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
57
58
  - by rewrite always_elim right_id pvs_frame_r wand_elim_r HQ pvs_trans.
  - by rewrite right_id pvs_frame_r wand_elim_r HQ pvs_trans.
Qed.

59
60
61
Lemma tac_pvs_elim_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P' P Q Φ :
  envs_lookup i Δ = Some (p, P')  P' = (|={E}=> P)%I 
  FSASplit Q E fsa fsaV Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
  Δ'  fsa E Φ  Δ  Q.
Proof.
65
  intros ? -> ??. rewrite -(fsa_split Q) -fsa_pvs_fsa.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
67
68
69
70
71
72
73
74
75
76
77
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
  eapply tac_pvs_elim; set_solver.
Qed.

Lemma tac_pvs_timeless Δ Δ' E1 E2 i p P Q :
  envs_lookup i Δ = Some (p,  P)%I  TimelessP P 
  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' 
  Δ'  (|={E1,E2}=> Q)  Δ  (|={E1,E2}=> Q).
Proof.
  intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
  destruct p.
  - rewrite always_later (pvs_timeless E1 ( P)%I) pvs_frame_r.
    by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
  - rewrite (pvs_timeless E1 P) pvs_frame_r right_id wand_elim_r HQ.
    by rewrite pvs_trans; last set_solver.
Qed.

Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
  FSASplit Q E fsa fsaV Φ 
  envs_lookup i Δ = Some (p,  P)%I  TimelessP P 
  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' 
  Δ'  fsa E Φ  Δ  Q.
Proof.
  intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
  eauto using tac_pvs_timeless.
Qed.

Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
  FSASplit Q E fsa fsaV Φ 
  envs_split lr js Δ = Some (Δ1,Δ2) 
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
  Δ1  (|={E}=> P)  Δ2'  fsa E Φ  Δ  Q.
Proof.
  intros ??? HP HQ. rewrite -(fsa_split Q) -fsa_pvs_fsa -HQ envs_split_sound //.
  rewrite HP envs_app_sound //; simpl.
  by rewrite right_id pvs_frame_r wand_elim_r.
Qed.
End pvs.

Tactic Notation "iPvsIntro" := apply tac_pvs_intro.

Tactic Notation "iPvsCore" constr(H) :=
  match goal with
  | |- _  |={_,_}=> _ =>
109
    eapply tac_pvs_elim with _ _ H _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
110
      [env_cbv; reflexivity || fail "iPvs:" H "not found"
111
112
      |let P := match goal with |- ?P = _ => P end in
       reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
Robbert Krebbers's avatar
Robbert Krebbers committed
113
114
115
      |env_cbv; reflexivity
      |try (rewrite (idemp_L ()); reflexivity)|]
  | |- _ =>
116
    eapply tac_pvs_elim_fsa with _ _ _ _ H _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
117
      [env_cbv; reflexivity || fail "iPvs:" H "not found"
118
119
      |let P := match goal with |- ?P = _ => P end in
       reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
Robbert Krebbers's avatar
Robbert Krebbers committed
120
      |let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
121
       apply _ || fail "iPvs:" P "not a pvs"
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
124
125
      |env_cbv; reflexivity|simpl]
  end.

Tactic Notation "iPvs" open_constr(H) :=
126
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
128
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
    constr(pat) :=
131
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) "}" constr(pat) :=
134
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
137
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
140
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
141
  iDestructHelp H as (fun H =>
142
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
145
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) "}" constr(pat) :=
146
  iDestructHelp H as (fun H =>
147
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
150
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
151
  iDestructHelp H as (fun H =>
152
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
156
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
    constr(pat) :=
157
  iDestructHelp H as (fun H =>
158
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
161
162
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
    simple_intropattern(x8) "}" constr(pat) :=
163
  iDestructHelp H as (fun H =>
164
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
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

Tactic Notation "iTimeless" constr(H) :=
  match goal with
  | |- _  |={_,_}=> _ =>
     eapply tac_pvs_timeless with _ H _ _;
       [env_cbv; reflexivity || fail "iTimeless:" H "not found"
       |let P := match goal with |- TimelessP ?P => P end in
        apply _ || fail "iTimeless: " P "not timeless"
       |env_cbv; reflexivity|simpl]
  | |- _ =>
     eapply tac_pvs_timeless_fsa with _ _ _ _ H _ _ _;
       [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
        apply _ || fail "iTimeless: " P "not a pvs"
       |env_cbv; reflexivity || fail "iTimeless:" H "not found"
       |let P := match goal with |- TimelessP ?P => P end in
        apply _ || fail "iTimeless: " P "not timeless"
       |env_cbv; reflexivity|simpl]
  end.

Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
  iTimeless H; iDestruct H as Hs.

Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
  let H := iFresh in
  let Hs := spec_pat.parse_one Hs in
  lazymatch Hs with
191
  | SAssert ?lr ?Hs =>
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
195
196
     eapply tac_pvs_assert with _ _ _ _ _ _ lr Hs H Q _;
       [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
        apply _ || fail "iPvsAssert: " P "not a pvs"
       |env_cbv; reflexivity || fail "iPvsAssert:" Hs "not found"
       |env_cbv; reflexivity|
197
       |simpl; iDestruct H as pat]
Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
201
  | ?pat => fail "iPvsAssert: invalid pattern" pat
  end.
Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
  iPvsAssert Q as pat with "[]".