viewshifts.v 4.48 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import program_logic.ownership.
2
3
Require Export program_logic.pviewshifts program_logic.invariants program_logic.ghost_ownership.
Import uPred.
4

5
Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
6
  ( (P  pvs E1 E2 Q))%I.
7
8
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
9
10
11
12
13
14
15
16
17
18
Notation "P >{ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
  (at level 199, E1 at level 1, E2 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 199, E1 at level 1, E2 at level 1,
   format "P  >{ E1 , E2 }=>  Q") : C_scope.
Notation "P >{ E }=> Q" := (vs E E P%I Q%I)
  (at level 199, E at level 1, format "P  >{ E }=>  Q") : uPred_scope.
Notation "P >{ E }=> Q" := (True  vs E E P%I Q%I)
  (at level 199, E at level 1, format "P  >{ E }=>  Q") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20

Section vs.
21
Context {Λ : language} {Σ : iFunctor}.
22
Implicit Types P Q R : iProp Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
23

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
37
Lemma vs_mono E1 E2 P P' Q Q' :
38
  P  P'  Q'  Q  (P' >{E1,E2}=> Q')  (P >{E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
39
Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
40

41
42
Global Instance vs_mono' E1 E2 :
  Proper (flip () ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
Proof. by intros until 2; apply vs_mono. Qed.

45
Lemma vs_false_elim E1 E2 P : False >{E1,E2}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Proof. apply vs_alt, False_elim. Qed.
47
Lemma vs_timeless E P : TimelessP P   P >{E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
49

Robbert Krebbers's avatar
Robbert Krebbers committed
50
Lemma vs_transitive E1 E2 E3 P Q R :
51
  E2  E1  E3  ((P >{E1,E2}=> Q)  (Q >{E2,E3}=> R))  (P >{E1,E3}=> R).
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54
55
56
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.
57

58
Lemma vs_transitive' E P Q R : ((P >{E}=> Q)  (Q >{E}=> R))  (P >{E}=> R).
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Proof. apply vs_transitive; solve_elem_of. Qed.
60
Lemma vs_reflexive E P : P >{E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
Proof. apply vs_alt, pvs_intro. Qed.
62

63
Lemma vs_impl E P Q :  (P  Q)  (P >{E}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
Proof.
  apply always_intro, impl_intro_l.
  by rewrite always_elim impl_elim_r -pvs_intro.
Qed.
68

69
Lemma vs_frame_l E1 E2 P Q R : (P >{E1,E2}=> Q)  (R  P >{E1,E2}=> R  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
73
74
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.
75

76
Lemma vs_frame_r E1 E2 P Q R : (P >{E1,E2}=> Q)  (P  R >{E1,E2}=> Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Proof. rewrite !(commutative _ _ R); apply vs_frame_l. Qed.
78

Robbert Krebbers's avatar
Robbert Krebbers committed
79
Lemma vs_mask_frame E1 E2 Ef P Q :
80
  Ef  (E1  E2) =   (P >{E1,E2}=> Q)  (P >{E1  Ef,E2  Ef}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
83
84
Proof.
  intros ?; apply always_intro, impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//.
  by rewrite always_elim impl_elim_r.
Qed.
85

86
Lemma vs_mask_frame' E Ef P Q : Ef  E =   (P >{E}=> Q)  (P >{E  Ef}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
87
Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
88

89
90
Lemma vs_open_close N E P Q R :
  nclose N  E 
91
  (inv N R  ( R  P >{E  nclose N}=>  R  Q))  (P >{E}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof.
93
  intros; apply (always_intro' _ _), impl_intro_l.
94
  rewrite associative (commutative _ P) -associative.
95
  rewrite -(pvs_open_close E N) //; apply and_mono; first done.
96
97
98
99
  apply wand_intro_l.
  (* Oh wow, this is annyoing... *)
  rewrite always_and_sep_r' associative -always_and_sep_r'.
  by rewrite /vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Qed.
101

102
Lemma vs_alloc (N : namespace) P :  P >{N}=> inv N P.
103
Proof. by intros; apply vs_alt, pvs_alloc. Qed.
104

105
End vs.
106

107
108
109
110
Section vs_ghost.
Context {Λ : language} {Σ : gid  iFunctor} (i : gid) `{!InG Λ Σ i A}.
Implicit Types a : A.
Implicit Types P Q R : iProp Λ (globalC Σ).
111

112
113
Lemma vs_own_updateP E γ a φ :
  a ~~>: φ  own i γ a >{E}=>  a',  φ a'  own i γ a'.
114
Proof. by intros; apply vs_alt, own_updateP. Qed.
115

116
117
Lemma vs_own_updateP_empty `{Empty A, !CMRAIdentity A} E γ φ :
   ~~>: φ  True >{E}=>  a',  φ a'  own i γ a'.
118
Proof. by intros; eapply vs_alt, own_updateP_empty. Qed.
119

120
Lemma vs_update E γ a a' : a ~~> a'  own i γ a >{E}=> own i γ a'.
121
122
123
Proof. by intros; apply vs_alt, own_update. Qed.

End vs_ghost.