viewshifts.v 2.83 KB
Newer Older
1 2
From iris.program_logic Require Import ownership.
From iris.program_logic Require Export pviewshifts invariants ghost_ownership.
3
From iris.proofmode Require Import pviewshifts invariants.
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 15
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17

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

Global Instance vs_ne E1 E2 n :
23
  Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
Ralf Jung's avatar
Ralf Jung committed
24
Proof. solve_proper. Qed.
25

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

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

33
Global Instance vs_mono' E1 E2 :
34
  Proper (flip () ==> () ==> ()) (@vs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
35
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
36

37
Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
38
Proof. iIntros "[]". Qed.
39
Lemma vs_timeless E P : TimelessP P   P ={E}=> P.
40
Proof. by apply pvs_timeless. Qed.
41

Robbert Krebbers's avatar
Robbert Krebbers committed
42
Lemma vs_transitive E1 E2 E3 P Q R :
43
  E2  E1  E3  (P ={E1,E2}=> Q)  (Q ={E2,E3}=> R)  P ={E1,E3}=> R.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  iIntros {?} "#[HvsP HvsQ] ! HP".
46
  iPvs ("HvsP" with "HP") as "HQ"; first done. by iApply "HvsQ".
Robbert Krebbers's avatar
Robbert Krebbers committed
47
Qed.
48

49
Lemma vs_transitive' E P Q R : (P ={E}=> Q)  (Q ={E}=> R)  (P ={E}=> R).
50
Proof. apply vs_transitive; set_solver. Qed.
51
Lemma vs_reflexive E P : P ={E}=> P.
52
Proof. by iIntros "HP". Qed.
53

54
Lemma vs_impl E P Q :  (P  Q)  P ={E}=> Q.
55
Proof. iIntros "#HPQ ! HP". by iApply "HPQ". Qed.
56

57
Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q)  R  P ={E1,E2}=> R  Q.
58
Proof. iIntros "#Hvs ! [$ HP]". by iApply "Hvs". Qed.
59

60
Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q)  P  R ={E1,E2}=> Q  R.
61
Proof. iIntros "#Hvs ! [HP $]". by iApply "Hvs". Qed.
62

Robbert Krebbers's avatar
Robbert Krebbers committed
63
Lemma vs_mask_frame E1 E2 Ef P Q :
64
  Ef  E1  E2  (P ={E1,E2}=> Q)  P ={E1  Ef,E2  Ef}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  iIntros {?} "#Hvs ! HP". iApply pvs_mask_frame; auto. by iApply "Hvs".
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Qed.
68

69
Lemma vs_mask_frame' E Ef P Q : Ef  E  (P ={E}=> Q)  P ={E  Ef}=> Q.
70
Proof. intros; apply vs_mask_frame; set_solver. Qed.
71

72
Lemma vs_inv N E P Q R :
73
  nclose N  E  inv N R  ( R  P ={E  nclose N}=>  R  Q)  P ={E}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Proof.
75
  iIntros {?} "#[? Hvs] ! HP". iInv N as "HR". iApply "Hvs". by iSplitL "HR".
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
77

78
Lemma vs_alloc N P :  P ={N}=> inv N P.
79
Proof. iIntros "HP". by iApply inv_alloc. Qed.
80
End vs.