viewshifts.v 4.41 KB
Newer Older
1 2
From iris.program_logic Require Import ownership.
From iris.program_logic Require Export pviewshifts invariants ghost_ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.proofmode Require Import pviewshifts.
4
Import uPred.
5

6
Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
7
  ( (P  |={E1,E2}=> Q))%I.
8 9
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
10
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
11
  (at level 99, E1,E2 at level 50, Q at level 200,
12
   format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
13 14
Notation "P ={ E1 , E2 }=> Q" := (True  (P ={E1,E2}=> Q)%I)
  (at level 99, E1, E2 at level 50, Q at level 200,
15
   format "P  ={ E1 , E2 }=>  Q") : C_scope.
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=>  Q") : uPred_scope.
Notation "P ={ E }=> Q" := (True  (P ={E}=> Q)%I)
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=>  Q") : C_scope.

Notation "P <={ E1 , E2 }=> Q" := ((P ={E1,E2}=> Q)  (Q ={E2,E1}=> P))%I
  (at level 99, E1,E2 at level 50, Q at level 200,
   format "P  <={ E1 , E2 }=>  Q") : uPred_scope.
Notation "P <={ E1 , E2 }=> Q" := (True  (P <={E1,E2}=> Q)%I)
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "P  <={ E1 , E2 }=>  Q") : C_scope.
Notation "P <={ E }=> Q" := (P <={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "P  <={ E }=>  Q") : uPred_scope.
Notation "P <={ E }=> Q" := (True  (P <={E}=> Q)%I)
  (at level 99, E at level 50, Q at level 200,
   format "P  <={ E }=>  Q") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36

Section vs.
37
Context {Λ : language} {Σ : iFunctor}.
38
Implicit Types P Q R : iProp Λ Σ.
39
Implicit Types N : namespace.
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41
Lemma vs_alt E1 E2 P Q : P  (|={E1,E2}=> Q)  P ={E1,E2}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Proof. iIntros {Hvs} "! ?". by iApply Hvs. Qed.
43

Robbert Krebbers's avatar
Robbert Krebbers committed
44
Global Instance vs_ne E1 E2 n :
45
  Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
Ralf Jung's avatar
Ralf Jung committed
46
Proof. solve_proper. Qed.
47

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

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

55
Global Instance vs_mono' E1 E2 :
56
  Proper (flip () ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58

59
Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Proof. iIntros "! []". Qed.
61
Lemma vs_timeless E P : TimelessP P   P ={E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Proof. iIntros {?} "! HP". by iApply pvs_timeless. Qed.
63

Robbert Krebbers's avatar
Robbert Krebbers committed
64
Lemma vs_transitive E1 E2 E3 P Q R :
65
  E2  E1  E3  ((P ={E1,E2}=> Q)  (Q ={E2,E3}=> R))  (P ={E1,E3}=> R).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  iIntros {?} "#[HvsP HvsQ] ! HP".
68
  iPvs ("HvsP" with "! HP") as "HQ"; first done. by iApply ("HvsQ" with "!").
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Qed.
70

71
Lemma vs_transitive' E P Q R : ((P ={E}=> Q)  (Q ={E}=> R))  (P ={E}=> R).
72
Proof. apply vs_transitive; set_solver. Qed.
73
Lemma vs_reflexive E P : P ={E}=> P.
74
Proof. by iIntros "! HP". Qed.
75

76
Lemma vs_impl E P Q :  (P  Q)  (P ={E}=> Q).
77
Proof. iIntros "#HPQ ! HP". by iApply "HPQ". Qed.
78

79
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
80
Proof. iIntros "#Hvs ! [$ HP]". by iApply "Hvs". Qed.
81

82
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
83
Proof. iIntros "#Hvs ! [HP $]". by iApply "Hvs". Qed.
84

Robbert Krebbers's avatar
Robbert Krebbers committed
85
Lemma vs_mask_frame E1 E2 Ef P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
86
  Ef  E1  E2  (P ={E1,E2}=> Q)  (P ={E1  Ef,E2  Ef}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
87
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
  iIntros {?} "#Hvs ! HP". iApply pvs_mask_frame; auto. by iApply "Hvs".
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Qed.
90

Robbert Krebbers's avatar
Robbert Krebbers committed
91
Lemma vs_mask_frame' E Ef P Q : Ef  E  (P ={E}=> Q)  (P ={E  Ef}=> Q).
92
Proof. intros; apply vs_mask_frame; set_solver. Qed.
93

94
Lemma vs_inv N E P Q R :
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  nclose N  E  (inv N R  ( R  P ={E  nclose N}=>  R  Q))  (P ={E}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  iIntros {?} "#[? Hvs] ! HP". eapply pvs_inv; eauto.
98
  iIntros "HR". iApply ("Hvs" with "!"). by iSplitL "HR".
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Qed.
100

101
Lemma vs_alloc N P :  P ={N}=> inv N P.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Proof. iIntros "! HP". by iApply inv_alloc. Qed.
103
End vs.
104

105
Section vs_ghost.
106
Context `{inG Λ Σ A}.
107
Implicit Types a : A.
108
Implicit Types P Q R : iPropG Λ Σ.
109

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
117
Lemma vs_own_empty `{Empty A, !CMRAUnit A} E γ : True ={E}=> own γ .
118
Proof. by intros; eapply vs_alt, own_empty. Qed.
119
End vs_ghost.