pviewshifts.v 8.09 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
25
Global Instance frame_pvs E1 E2 R P Q :
  Frame R P Q  Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance to_wand_pvs E1 E2 R P Q :
28
  ToWand R P Q  ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
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 Λ Σ) := {
33
  fsa_split : fsa E Φ  P;
34
  fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
37
38
39
}.
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.
40
41
42
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
43

44
45
46
47
48
49
50
Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
  FSASplit Q E fsa fsaV Φ  ToAssert P Q (|={E}=> P).
Proof.
  intros.
  by rewrite /ToAssert pvs_frame_r wand_elim_r -(fsa_split Q) fsa_pvs_fsa.
Qed.

51
Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2  (Δ  Q)  Δ  |={E1,E2}=> Q.
52
Proof. intros -> ->. apply pvs_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
53

54
55
56
57
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
58
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
59
  (Δ' ={E2,E3}=> Q)  Δ ={E1,E3}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Proof.
61
62
63
64
  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
65
66
Qed.

67
68
69
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
70
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
71
  (Δ'  fsa E Φ)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
73
  intros ? -> ??. rewrite -(fsa_split Q) -fsa_pvs_fsa.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76
77
78
79
  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 Δ' 
80
  (Δ' ={E1,E2}=> Q)  Δ ={E1,E2}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
Proof.
  intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
83
84
  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
85
86
87
88
89
90
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 Δ' 
91
  (Δ'  fsa E Φ)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
95
96
97
Proof.
  intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
  eauto using tac_pvs_timeless.
Qed.
End pvs.

98
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102

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

Tactic Notation "iPvs" open_constr(H) :=
123
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
125
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
    constr(pat) :=
128
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) "}" constr(pat) :=
131
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
134
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
138
  iDestructHelp H as (fun H =>
139
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } 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)
    simple_intropattern(x5) "}" constr(pat) :=
143
  iDestructHelp H as (fun H =>
144
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } 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) simple_intropattern(x6) "}" constr(pat) :=
148
  iDestructHelp H as (fun H =>
149
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
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) :=
154
  iDestructHelp H as (fun H =>
155
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
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) :=
160
  iDestructHelp H as (fun H =>
161
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182

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.