pviewshifts.v 8.19 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
Global Instance from_pure_pvs E P φ : FromPure P φ  FromPure (|={E}=> P) φ.
Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
12
13
14
15
16
17
Global Instance from_assumption_pvs E p P Q :
  FromAssumption p P Q  FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply pvs_intro. 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
19
20
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Global Instance exists_split_pvs {A} E1 E2 P (Φ : A  iProp Λ Σ) :
22
  FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Proof.
24
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Robbert Krebbers's avatar
Robbert Krebbers committed
25
Qed.
26
27
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
28
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
29
30
31
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
32

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

46
Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
47
  IsFSA Q E fsa fsaV Φ  IntoAssert P Q (|={E}=> P).
48
Proof.
49
  intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
50
51
Qed.

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

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

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 
70
  IsFSA Q E fsa fsaV Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
72
  (Δ'  fsa E Φ)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Proof.
74
  intros ? -> ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
77
78
79
80
  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 Δ' 
81
  (Δ' ={E1,E2}=> Q)  Δ ={E1,E2}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
Proof.
  intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
84
85
  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
86
87
88
Qed.

Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
89
  IsFSA Q E fsa fsaV Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
  envs_lookup i Δ = Some (p,  P)%I  TimelessP P 
  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' 
92
  (Δ'  fsa E Φ)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Proof.
94
  intros ????. rewrite (is_fsa Q) -fsa_pvs_fsa.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
97
98
  eauto using tac_pvs_timeless.
Qed.
End pvs.

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

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

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

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 _ _ _;
174
       [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
177
178
179
180
181
182
183
        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.