pviewshifts.v 10.9 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26
Instance frame_pvs E1 E2 R P mQ :
  Frame R P mQ 
  Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> from_option True mQ))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 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 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
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;
  fsa_split_fsa :> FrameShiftAssertion fsaV fsa;
}.
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.

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

Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P Q :
  envs_lookup i Δ = Some (p, |={E1,E2}=> P)%I 
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
  E2  E1  E3 
  Δ'  (|={E2,E3}=> Q)  Δ  |={E1,E3}=> Q.
Proof.
  intros ??? HQ. rewrite envs_replace_sound //; simpl. destruct p.
  - 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.

Lemma tac_pvs_elim_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
  envs_lookup i Δ = Some (p, |={E}=> P)%I  FSASplit Q E fsa fsaV Φ 
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
  Δ'  fsa E Φ  Δ  Q.
Proof.
  intros ???. rewrite -(fsa_split Q) -fsa_pvs_fsa.
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
100 101 102
Hint Extern 10 (Frame _ (|={_,_}=> _) _) =>
  class_apply frame_pvs : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
103 104 105 106 107 108 109 110 111 112 113 114 115
Tactic Notation "iPvsIntro" := apply tac_pvs_intro.

Tactic Notation "iPvsCore" constr(H) :=
  match goal with
  | |- _  |={_,_}=> _ =>
    eapply tac_pvs_elim with _ _ H _ _;
      [env_cbv; reflexivity || fail "iPvs:" H "not found"
      |env_cbv; reflexivity
      |try (rewrite (idemp_L ()); reflexivity)|]
  | |- _ =>
    eapply tac_pvs_elim_fsa with _ _ _ _ H _ _ _;
      [env_cbv; reflexivity || fail "iPvs:" H "not found"
      |let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
116
       apply _ || fail "iPvs:" P "not a pvs"
Robbert Krebbers's avatar
Robbert Krebbers committed
117 118 119 120
      |env_cbv; reflexivity|simpl]
  end.

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

Tactic Notation "iPvs" open_constr(lem) constr(Hs) :=
162
  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as "?").
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" constr(pat) :=
164
  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
165 166
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
    simple_intropattern(x1) "}" constr(pat) :=
167
  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
    simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
  iPoseProof lem Hs as (fun H =>
171
    iPvsCore H; last iDestruct H as { x1 x2 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173 174 175
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
    constr(pat) :=
  iPoseProof lem Hs as (fun H =>
176
    iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179 180
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
    simple_intropattern(x4) "}" constr(pat) :=
  iPoseProof lem Hs as (fun H =>
181
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
182 183 184 185
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
    simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
  iPoseProof lem Hs as (fun H =>
186
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188 189 190 191
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
    constr(pat) :=
  iPoseProof lem Hs as (fun H =>
192
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
193 194 195 196 197
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
    simple_intropattern(x7) "}" constr(pat) :=
  iPoseProof lem Hs as (fun H =>
198
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200 201 202 203
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "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) :=
  iPoseProof lem Hs as (fun H =>
204
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236

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
  | SSplit ?lr ?Hs =>
     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|
237
       |simpl; iDestruct H as pat]
Robbert Krebbers's avatar
Robbert Krebbers committed
238 239 240 241
  | ?pat => fail "iPvsAssert: invalid pattern" pat
  end.
Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
  iPvsAssert Q as pat with "[]".