viewshifts.v 4.33 KB
Newer Older
1
Require Export program_logic.pviewshifts.
Ralf Jung's avatar
Ralf Jung committed
2
Require Import program_logic.ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
3

4
Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
5
  ( (P  pvs E1 E2 Q))%I.
6
7
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
12
13
14
15
16
17
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.
18
19
20
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
Import uPred.

23
Lemma vs_alt E1 E2 P Q : (P  pvs E1 E2 Q)  P >{E1,E2}> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
26
27
28
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 :
29
  Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
31
Global Instance vs_proper E1 E2 : Proper (() ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
34
35
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.
36
37
Global Instance vs_mono' E1 E2 :
  Proper (flip () ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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.
76
Lemma vs_open i P : ownI i P >{{[i]},}>  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Proof. intros; apply vs_alt, pvs_open. Qed.
78
Lemma vs_open' E i P : i  E  ownI i P >{{[i]}  E,E}>  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
81
82
Proof.
  intros; rewrite -{2}(left_id_L  () E) -vs_mask_frame; last solve_elem_of.
  apply vs_open.
Qed.
83
Lemma vs_close i P : (ownI i P   P) >{,{[i]}}> True.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Proof. intros; apply vs_alt, pvs_close. Qed.
85
Lemma vs_close' E i P : i  E  (ownI i P   P) >{E,{[i]}  E}> True.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
88
89
Proof.
  intros; rewrite -{1}(left_id_L  () E) -vs_mask_frame; last solve_elem_of.
  apply vs_close.
Qed.
90
Lemma vs_updateP E m (P : iGst Λ Σ  Prop) :
91
  m ~~>: P  ownG m >{E}> ( m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof. by intros; apply vs_alt, pvs_updateP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
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.
97
Lemma vs_update E m m' : m ~~> m'  ownG m >{E}> ownG m'.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Proof. by intros; apply vs_alt, pvs_update. Qed.
99
Lemma vs_alloc E P : ¬set_finite E   P >{E}> ( i,  (i  E)  ownI i P).
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
Proof. by intros; apply vs_alt, pvs_alloc. Qed.
End vs.