viewshifts.v 4.32 KB
Newer Older
1
2
From program_logic Require Import ownership.
From program_logic Require Export pviewshifts invariants ghost_ownership.
3
Import uPred.
4

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

25
Lemma vs_alt E1 E2 P Q : P  (|={E1,E2}=> Q)  P ={E1,E2}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Proof.
27
  intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
28
  by rewrite always_const right_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
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).
Ralf Jung's avatar
Ralf Jung committed
33
Proof. solve_proper. 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
Lemma vs_mono E1 E2 P P' Q Q' :
39
  P  P'  Q'  Q  (P' ={E1,E2}=> Q')  (P ={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
40
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
Proof. by intros until 2; apply vs_mono. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
51
Lemma vs_transitive E1 E2 E3 P Q R :
52
  E2  E1  E3  ((P ={E1,E2}=> Q)  (Q ={E2,E3}=> R))  (P ={E1,E3}=> R).
Robbert Krebbers's avatar
Robbert Krebbers committed
53
Proof.
54
  intros; rewrite -always_and; apply: always_intro. apply impl_intro_l.
55
  rewrite always_and assoc (always_elim (P  _)) impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57
  by rewrite pvs_impl_r; apply pvs_trans.
Qed.
58

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

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

70
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
71
Proof.
72
  apply always_intro', impl_intro_l.
73
  rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
  by rewrite always_elim wand_elim_r.
Qed.
76

77
Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q)  (P  R ={E1,E2}=> Q  R).
78
Proof. rewrite !(comm _ _ R); apply vs_frame_l. Qed.
79

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

87
Lemma vs_mask_frame' E Ef P Q : Ef  E =   (P ={E}=> Q)  (P ={E  Ef}=> Q).
88
Proof. intros; apply vs_mask_frame; set_solver. Qed.
89

90
91
Lemma vs_open_close N E P Q R :
  nclose N  E 
Ralf Jung's avatar
Ralf Jung committed
92
  (inv N R  ( R  P ={E  nclose N}=>  R  Q))  (P ={E}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Proof.
94
  intros; apply: always_intro. apply impl_intro_l.
95
  rewrite always_and_sep_r assoc [(P  _)%I]comm -assoc.
Ralf Jung's avatar
Ralf Jung committed
96
  eapply pvs_open_close; [by eauto with I..|].
97
  rewrite sep_elim_r. apply wand_intro_l.
98
  (* Oh wow, this is annyoing... *)
99
  rewrite assoc -always_and_sep_r'.
100
  by rewrite /vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Qed.
102

103
Lemma vs_alloc N P :  P ={N}=> inv N P.
104
Proof. by intros; apply vs_alt, inv_alloc. Qed.
105

106
End vs.
107

108
Section vs_ghost.
109
Context `{inG Λ Σ A}.
110
Implicit Types a : A.
111
Implicit Types P Q R : iPropG Λ Σ.
112

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

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

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