viewshifts.v 4.29 KB
Newer Older
1
Require Export program_logic.pviewshifts.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

3
Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
4
  ( (P  pvs E1 E2 Q))%I.
5
6
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
12
13
14
15
16
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.
17
18
19
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
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
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 :
28
  Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
30
Global Instance vs_proper E1 E2 : Proper (() ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
34
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.
35
36
Global Instance vs_mono' E1 E2 :
  Proper (flip () ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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.
75
Lemma vs_open i P : ownI i P >{{[i]},}>  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof. intros; apply vs_alt, pvs_open. Qed.
77
Lemma vs_open' E i P : i  E  ownI i P >{{[i]}  E,E}>  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
79
80
81
Proof.
  intros; rewrite -{2}(left_id_L  () E) -vs_mask_frame; last solve_elem_of.
  apply vs_open.
Qed.
82
Lemma vs_close i P : (ownI i P   P) >{,{[i]}}> True.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Proof. intros; apply vs_alt, pvs_close. Qed.
84
Lemma vs_close' E i P : i  E  (ownI i P   P) >{E,{[i]}  E}> True.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
87
88
Proof.
  intros; rewrite -{1}(left_id_L  () E) -vs_mask_frame; last solve_elem_of.
  apply vs_close.
Qed.
89
Lemma vs_updateP E m (P : iGst Λ Σ  Prop) :
90
  m ~~>: P  ownG m >{E}> ( m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Proof. by intros; apply vs_alt, pvs_updateP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
95
Lemma vs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
    E (P : iGst Λ Σ  Prop) :
   ~~>: P  True >{E}> ( m',  P m'  ownG m').
Proof. by intros; apply vs_alt, pvs_updateP_empty. Qed.
96
Lemma vs_update E m m' : m ~~> m'  ownG m >{E}> ownG m'.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Proof. by intros; apply vs_alt, pvs_update. Qed.
98
Lemma vs_alloc E P : ¬set_finite E   P >{E}> ( i,  (i  E)  ownI i P).
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
Proof. by intros; apply vs_alt, pvs_alloc. Qed.
End vs.