viewshifts.v 4.57 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
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18

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

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
Proof.
  intros; rewrite -{1}always_const; apply always_intro, impl_intro_l.
  by rewrite always_const (right_id _ _).
Qed.
27

Robbert Krebbers's avatar
Robbert Krebbers committed
28
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

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

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

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

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

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

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

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

67
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
68
69
70
71
72
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.
73

74
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
75
Proof. rewrite !(commutative _ _ R); apply vs_frame_l. Qed.
76

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

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

87
88
89
90
91
(* FIXME I really should not need parenthesis around the pre- and postcondition
   of a view shift. *)
Lemma vs_open_close N E P Q R :
  nclose N  E 
  (inv N R  (R  P) ={E  nclose N}=> (R  Q))  P ={E}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof.
93
94
95
96
97
98
99
  intros HN. apply always_intro'; first by apply _. apply impl_intro_l.
  rewrite associative (commutative _ P) -associative.
  rewrite -pvs_open_close; first (apply and_mono; first done); last done.
  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
103
Lemma vs_alloc (N : namespace) P :  P ={N}=> inv N P.
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
114
Lemma vs_own_updateP E γ a (P : A  Prop) :
  a ~~>: P  own i γ a ={E}=> ( a',  P a'  own i γ a').
Proof. by intros; apply vs_alt, own_updateP. Qed.
115

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

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

End vs_ghost.