viewshifts.v 4.01 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
Require Export iris.pviewshifts.

Definition vs {Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
  ( (P  pvs E1 E2 Q))%I.
Arguments vs {_} _ _ _%I _%I.
Instance: Params (@vs) 3.
Notation "P >{ E1 , E2 }> Q" := (vs E1 E2 P%I Q%I)
  (at level 69, E1 at level 1, format "P  >{ E1 , E2 }>  Q") : uPred_scope.
Notation "P >{ E1 , E2 }> Q" := (True  vs E1 E2 P%I Q%I)
  (at level 69, E1 at level 1, format "P  >{ E1 , E2 }>  Q") : C_scope.
Notation "P >{ E }> Q" := (vs E E P%I Q%I)
  (at level 69, E at level 1, format "P  >{ E }>  Q") : uPred_scope.
Notation "P >{ E }> Q" := (True  vs E E P%I Q%I)
  (at level 69, E at level 1, format "P  >{ E }>  Q") : C_scope.

Section vs.
Context {Σ : iParam}.
Implicit Types P Q : iProp Σ.
19
Implicit Types m : iGst Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21
Import uPred.

22
Lemma vs_alt E1 E2 P Q : (P  pvs E1 E2 Q)  P >{E1,E2}> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25 26 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
Proof.
  intros; rewrite -{1}always_const; apply always_intro, impl_intro_l.
  by rewrite always_const (right_id _ _).
Qed.
Global Instance vs_ne E1 E2 n :
  Proper (dist n ==> dist n ==> dist n) (@vs Σ E1 E2).
Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
Global Instance vs_proper E1 E2 : Proper (() ==> () ==> ()) (@vs Σ E1 E2).
Proof. apply ne_proper_2, _. Qed.
Lemma vs_mono E1 E2 P P' Q Q' :
  P  P'  Q'  Q  P' >{E1,E2}> Q'  P >{E1,E2}> Q.
Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
Global Instance vs_mono' E1 E2: Proper (flip () ==> () ==> ()) (@vs Σ E1 E2).
Proof. by intros until 2; apply vs_mono. Qed.

Lemma vs_false_elim E1 E2 P : False >{E1,E2}> P.
Proof. apply vs_alt, False_elim. Qed.
Lemma vs_timeless E P : TimelessP P   P >{E}> P.
Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
  E2  E1  E3  (P >{E1,E2}> Q  Q >{E2,E3}> R)  P >{E1,E3}> R.
Proof.
  intros; rewrite -always_and; apply always_intro, impl_intro_l.
  rewrite always_and (associative _) (always_elim (P  _)) impl_elim_r.
  by rewrite pvs_impl_r; apply pvs_trans.
Qed.
Lemma vs_transitive' E P Q R : (P >{E}> Q  Q >{E}> R)  P >{E}> R.
Proof. apply vs_transitive; solve_elem_of. Qed.
Lemma vs_reflexive E P : P >{E}> P.
Proof. apply vs_alt, pvs_intro. Qed.
Lemma vs_impl E P Q :  (P  Q)  P >{E}> Q.
Proof.
  apply always_intro, impl_intro_l.
  by rewrite always_elim impl_elim_r -pvs_intro.
Qed.
Lemma vs_frame_l E1 E2 P Q R : P >{E1,E2}> Q  (R  P) >{E1,E2}> (R  Q).
Proof.
  apply always_intro, impl_intro_l.
  rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -(associative _).
  by rewrite always_elim wand_elim_r.
Qed.
Lemma vs_frame_r E1 E2 P Q R : P >{E1,E2}> Q  (P  R) >{E1,E2}> (Q  R).
Proof. rewrite !(commutative _ _ R); apply vs_frame_l. Qed.
Lemma vs_mask_frame E1 E2 Ef P Q :
  Ef  (E1  E2) =   P >{E1,E2}> Q  P >{E1  Ef,E2  Ef}> Q.
Proof.
  intros ?; apply always_intro, impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//.
  by rewrite always_elim impl_elim_r.
Qed.
Lemma vs_mask_frame' E Ef P Q : Ef  E =   P >{E}> Q  P >{E  Ef}> Q.
Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
Lemma vs_open i P : inv i P >{{[i]},}>  P.
Proof. intros; apply vs_alt, pvs_open. Qed.
Lemma vs_open' E i P : i  E  inv i P >{{[i]}  E,E}>  P.
Proof.
  intros; rewrite -{2}(left_id_L  () E) -vs_mask_frame; last solve_elem_of.
  apply vs_open.
Qed.
Lemma vs_close i P : (inv i P   P) >{,{[i]}}> True.
Proof. intros; apply vs_alt, pvs_close. Qed.
Lemma vs_close' E i P : i  E  (inv i P   P) >{E,{[i]}  E}> True.
Proof.
  intros; rewrite -{1}(left_id_L  () E) -vs_mask_frame; last solve_elem_of.
  apply vs_close.
Qed.
88
Lemma vs_updateP E m (P : iGst Σ  Prop) :
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90 91 92 93 94 95
  m : P  ownG m >{E}> ( m',  P m'  ownG m').
Proof. by intros; apply vs_alt, pvs_updateP. Qed.
Lemma vs_update E m m' : m  m'  ownG m >{E}> ownG m'.
Proof. by intros; apply vs_alt, pvs_update. Qed.
Lemma vs_alloc E P : ¬set_finite E   P >{E}> ( i,  (i  E)  inv i P).
Proof. by intros; apply vs_alt, pvs_alloc. Qed.
End vs.