viewshifts.v 4.42 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
5
(* TODO: State lemmas in terms of inv and own. *)

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

25
Lemma vs_alt E1 E2 P Q : (P  pvs E1 E2 Q)  P >{E1,E2}> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
Proof.
  intros; rewrite -{1}always_const; apply always_intro, impl_intro_l.
  by rewrite always_const (right_id _ _).
Qed.
30

Robbert Krebbers's avatar
Robbert Krebbers committed
31
Global Instance vs_ne E1 E2 n :
32
  Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
34

35
Global Instance vs_proper E1 E2 : Proper (() ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
36
Proof. apply ne_proper_2, _. Qed.
37

Robbert Krebbers's avatar
Robbert Krebbers committed
38
39
40
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.
41

42
43
Global Instance vs_mono' E1 E2 :
  Proper (flip () ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
47
48
49
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.
50

Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
53
54
55
56
57
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.
58

Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
62
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.
63

Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
68
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.
69

Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
73
74
75
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.
76

Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
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.
79

Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
83
84
85
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.
86

Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
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.
89
Lemma vs_open i P : ownI i P >{{[i]},}>  P.
Ralf Jung's avatar
Ralf Jung committed
90
Proof. intros; apply vs_alt, pvs_openI. Qed.
91

92
Lemma vs_open' E i P : i  E  ownI i P >{{[i]}  E,E}>  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
Proof.
  intros; rewrite -{2}(left_id_L  () E) -vs_mask_frame; last solve_elem_of.
  apply vs_open.
Qed.
97

98
Lemma vs_close i P : (ownI i P   P) >{,{[i]}}> True.
Ralf Jung's avatar
Ralf Jung committed
99
Proof. intros; apply vs_alt, pvs_closeI. Qed.
100

101
Lemma vs_close' E i P : i  E  (ownI i P   P) >{E,{[i]}  E}> True.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
104
105
Proof.
  intros; rewrite -{1}(left_id_L  () E) -vs_mask_frame; last solve_elem_of.
  apply vs_close.
Qed.
106
107

Lemma vs_ownG_updateP E m (P : iGst Λ Σ  Prop) :
108
  m ~~>: P  ownG m >{E}> ( m',  P m'  ownG m').
109
110
111
Proof. by intros; apply vs_alt, pvs_ownG_updateP. Qed.

Lemma vs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
Robbert Krebbers's avatar
Robbert Krebbers committed
112
113
    E (P : iGst Λ Σ  Prop) :
   ~~>: P  True >{E}> ( m',  P m'  ownG m').
114
115
Proof. by intros; apply vs_alt, pvs_ownG_updateP_empty. Qed.

116
Lemma vs_update E m m' : m ~~> m'  ownG m >{E}> ownG m'.
117
Proof. by intros; apply vs_alt, pvs_ownG_update. Qed.
118
Lemma vs_alloc E P : ¬set_finite E   P >{E}> ( i,  (i  E)  ownI i P).
Ralf Jung's avatar
Ralf Jung committed
119
Proof. by intros; apply vs_alt, pvs_allocI. Qed.
120

Robbert Krebbers's avatar
Robbert Krebbers committed
121
End vs.