pviewshifts.v 8.99 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
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance to_wand_pvs E1 E2 R P Q :
29
  ToWand R P Q  ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31 32 33 34
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
Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2  Δ  Q  Δ  |={E1,E2}=> Q.
Proof. intros -> ->. apply pvs_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
47

48 49 50 51
Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P' E1' E2' P Q :
  envs_lookup i Δ = Some (p, P')  P' = (|={E1',E2'}=> P)%I 
  (E1' = E1  E2' = E2  E2  E1  E3
   E2 = E2'  E1  E1'  E2'  E1  E1'  E1'  E1  E2'  E1'  E3) 
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
  Δ'  (|={E2,E3}=> Q)  Δ  |={E1,E3}=> Q.
Proof.
55 56 57 58
  intros ? -> HE ? HQ. rewrite envs_replace_sound //; simpl.
  rewrite always_if_elim right_id pvs_frame_r wand_elim_r HQ.
  destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
  etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60
Qed.

61 62 63
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
64 65 66
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
  Δ'  fsa E Φ  Δ  Q.
Proof.
67
  intros ? -> ??. rewrite -(fsa_split Q) -fsa_pvs_fsa.
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69 70 71 72 73 74 75 76
  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.
77 78
  rewrite always_if_later (pvs_timeless E1 (?_ P)%I) pvs_frame_r.
  by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
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.

103
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
Robbert Krebbers's avatar
Robbert Krebbers committed
104 105 106 107

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

Tactic Notation "iPvs" open_constr(H) :=
128
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
130
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
131 132
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
    constr(pat) :=
133
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) "}" constr(pat) :=
136
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
139
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141 142
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
143
  iDestructHelp H as (fun H =>
144
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146 147
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) "}" constr(pat) :=
148
  iDestructHelp H as (fun H =>
149
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
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) "}" constr(pat) :=
153
  iDestructHelp H as (fun H =>
154
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
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) "}"
    constr(pat) :=
159
  iDestructHelp H as (fun H =>
160
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163 164
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) :=
165
  iDestructHelp H as (fun H =>
166
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188

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.

189
Tactic Notation "iPvsAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191 192
  let H := iFresh in
  let Hs := spec_pat.parse_one Hs in
  lazymatch Hs with
193
  | SGoal ?lr ?Hs =>
Robbert Krebbers's avatar
Robbert Krebbers committed
194 195 196 197 198
     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|
199
       |simpl; iDestruct H as pat]
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201 202
  | ?pat => fail "iPvsAssert: invalid pattern" pat
  end.
Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
203
  iPvsAssert Q with "[]" as pat.