pviewshifts.v 7.62 KB
Newer Older
1 2 3
From iris.program_logic Require Export iris.
From iris.program_logic Require Import ownership.
From iris.algebra Require Import upred_big_op gmap.
4
From iris.proofmode Require Import tactics classes.
5
Import uPred.
Ralf Jung's avatar
Ralf Jung committed
6

7 8 9
Program Definition pvs_def `{irisG Λ Σ}
    (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
  (wsat  ownE E1 =r=  (wsat  ownE E2  P))%I.
Ralf Jung's avatar
Ralf Jung committed
10 11 12
Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
Definition pvs := proj1_sig pvs_aux.
Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
13 14
Arguments pvs {_ _ _} _ _ _%I.
Instance: Params (@pvs) 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
15

16
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q)
17
  (at level 99, E1, E2 at level 50, Q at level 200,
18
   format "|={ E1 , E2 }=>  Q") : uPred_scope.
19 20 21
Notation "P ={ E1 , E2 }=★ Q" := (P - |={E1,E2}=> Q)%I
  (at level 99, E1,E2 at level 50, Q at level 200,
   format "P  ={ E1 , E2 }=★  Q") : uPred_scope.
22 23 24
Notation "P ={ E1 , E2 }=> Q" := (P  |={E1,E2}=> Q)
  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.

25
Notation "|={ E }=> Q" := (pvs E E Q)
26 27 28
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }=>  Q") : uPred_scope.
Notation "P ={ E }=★ Q" := (P - |={E}=> Q)%I
29 30
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=★  Q") : uPred_scope.
31 32
Notation "P ={ E }=> Q" := (P  |={E}=> Q)
  (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
33

34
Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2}=> ( |={E2,E1}=> Q))%I
35 36
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }▷=>  Q") : uPred_scope.
37 38 39
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }▷=>  Q") : uPred_scope.
40

Robbert Krebbers's avatar
Robbert Krebbers committed
41
Section pvs.
42 43
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
44

45 46 47
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ _ E1 E2).
Proof. rewrite pvs_eq. solve_proper. Qed.
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ _ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49
Proof. apply ne_proper, _. Qed.

50
Lemma pvs_intro' E1 E2 P : E2  E1  ((|={E2,E1}=> True) - P) ={E1,E2}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Proof.
52
  intros (E1''&->&?)%subseteq_disjoint_union_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
  rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE) !==>".
54 55
  iApply except_last_intro. iApply "H".
  iIntros "[$ $] !==>". by iApply except_last_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Qed.
57
Lemma except_last_pvs E1 E2 P :  (|={E1,E2}=> P) ={E1,E2}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
Proof.
59
  rewrite pvs_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Qed.
61
Lemma rvs_pvs E P : (|=r=> P) ={E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Proof.
63
  rewrite pvs_eq /pvs_def. iIntros "H [$ $]"; iVs "H".
64
  iVsIntro. by iApply except_last_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Qed.
66
Lemma pvs_mono E1 E2 P Q : (P  Q)  (|={E1,E2}=> P) ={E1,E2}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Proof.
68 69
  rewrite pvs_eq /pvs_def. iIntros (HPQ) "HP HwE".
  rewrite -HPQ. by iApply "HP".
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Qed.
71
Lemma pvs_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
73
  rewrite pvs_eq /pvs_def. iIntros "HP HwE".
74
  iVs ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Qed.
76 77
Lemma pvs_mask_frame_r' E1 E2 Ef P :
  E1  Ef  (|={E1,E2}=> E2  Ef  P) ={E1  Ef,E2  Ef}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Proof.
79
  intros. rewrite pvs_eq /pvs_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
80 81
  iVs ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
  iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
82
  iVsIntro; iApply except_last_intro. by iApply "HP".
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Qed.
84 85
Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P)  Q ={E1,E2}=> P  Q.
Proof. rewrite pvs_eq /pvs_def. by iIntros "[HwP $]". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86

87
(** * Derived rules *)
88
Global Instance pvs_mono' E1 E2 : Proper (() ==> ()) (@pvs Λ Σ _ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Proof. intros P Q; apply pvs_mono. Qed.
90
Global Instance pvs_flip_mono' E1 E2 :
91
  Proper (flip () ==> flip ()) (@pvs Λ Σ _ E1 E2).
92
Proof. intros P Q; apply pvs_mono. Qed.
93 94 95

Lemma pvs_intro E P : P ={E}=> P.
Proof. iIntros "HP". by iApply rvs_pvs. Qed.
96 97
Lemma pvs_except_last E1 E2 P : (|={E1,E2}=>  P) ={E1,E2}=> P.
Proof. by rewrite {1}(pvs_intro E2 P) except_last_pvs pvs_trans. Qed.
98

99
Lemma pvs_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q) ={E1,E2}=> P  Q.
100
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
101
Lemma pvs_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}=> Q.
102
Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
103
Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}=> Q.
104
Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123

Lemma pvs_trans_frame E1 E2 E3 P Q :
  ((Q ={E2,E3}= True)  |={E1,E2}=> (Q  P)) ={E1,E3}=> P.
Proof.
  rewrite pvs_frame_l assoc -(comm _ Q) wand_elim_r.
  by rewrite pvs_frame_r left_id pvs_trans.
Qed.

Lemma pvs_mask_frame_r E1 E2 Ef P :
  E1  Ef  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}=> P.
Proof.
  iIntros (?) "H". iApply pvs_mask_frame_r'; auto.
  iApply pvs_wand_r; iFrame "H"; eauto.
Qed.
Lemma pvs_mask_mono E1 E2 P : E1  E2  (|={E1}=> P) ={E2}=> P.
Proof.
  intros (Ef&->&?)%subseteq_disjoint_union_L. by apply pvs_mask_frame_r.
Qed.

124
Lemma pvs_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}=> P  Q.
125 126
Proof. by rewrite pvs_frame_r pvs_frame_l pvs_trans. Qed.
Lemma pvs_big_sepM `{Countable K} {A} E (Φ : K  A  iProp Σ) (m : gmap K A) :
127
  ([ map] kx  m, |={E}=> Φ k x) ={E}=> [ map] kx  m, Φ k x.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Proof.
129 130
  apply (big_opM_forall (λ P Q, P ={E}=> Q)); auto using pvs_intro.
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
Qed.
132
Lemma pvs_big_sepS `{Countable A} E (Φ : A  iProp Σ) X :
133
  ([ set] x  X, |={E}=> Φ x) ={E}=> [ set] x  X, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Proof.
135 136
  apply (big_opS_forall (λ P Q, P ={E}=> Q)); auto using pvs_intro.
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
End pvs.
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 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

(** Proofmode class instances *)
Section proofmode_classes.
  Context `{irisG Λ Σ}.
  Implicit Types P Q : iProp Σ.

  Global Instance from_pure_pvs E P φ : FromPure P φ  FromPure (|={E}=> P) φ.
  Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.

  Global Instance from_assumption_pvs E p P Q :
    FromAssumption p P (|=r=> Q)  FromAssumption p P (|={E}=> Q)%I.
  Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.

  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.

  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.

  Global Instance or_split_pvs E1 E2 P Q1 Q2 :
    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.

  Global Instance exists_split_pvs {A} E1 E2 P (Φ : A  iProp Σ) :
    FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
  Proof.
    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
  Qed.

  Global Instance frame_pvs E1 E2 R P Q :
    Frame R P Q  Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
  Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.

  Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
  Proof. by rewrite /IsExceptLast except_last_pvs. Qed.

  Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
  Proof. by rewrite /FromVs -rvs_pvs. Qed.

  Global Instance elim_vs_rvs_pvs E1 E2 P Q :
    ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
  Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
  Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
    ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
  Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
End proofmode_classes.

Hint Extern 2 (coq_tactics.of_envs _  _) =>
  match goal with |- _  |={_}=> _ => iVsIntro end.