viewshifts.v 2.9 KB
Newer Older
1
From iris.base_logic.lib Require Export invariants.
2
From iris.proofmode Require Import tactics.
3
Set Default Proof Using "Type".
4

5
Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
6
  ( (P - |={E1,E2}=> Q))%I.
7
Arguments vs {_ _} _ _ _%I _%I.
8

9
Instance: Params (@vs) 4.
10
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
11 12 13 14 15 16
  (at level 99, E1,E2 at level 50, Q at level 200,
   format "P  ={ E1 , E2 }=>  Q") : uPred_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.

17
Notation "P ={ E1 , E2 }=> Q" := (P ={E1,E2}=> Q)%I
18 19
  (at level 99, E1,E2 at level 50, Q at level 200,
   format "P  ={ E1 , E2 }=>  Q") : C_scope.
20
Notation "P ={ E }=> Q" := (P ={E}=> Q)%I
21 22 23
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=>  Q") : C_scope.

24
Section vs.
25
Context `{invG Σ}.
26 27 28
Implicit Types P Q R : iProp Σ.
Implicit Types N : namespace.

29
Global Instance vs_ne E1 E2 : NonExpansive2 (vs E1 E2).
30 31 32 33 34 35 36 37 38 39 40 41 42
Proof. solve_proper. Qed.

Global Instance vs_proper E1 E2 : Proper (() ==> () ==> ()) (vs E1 E2).
Proof. apply ne_proper_2, _. Qed.

Lemma vs_mono E1 E2 P P' Q Q' :
  (P  P')  (Q'  Q)  (P' ={E1,E2}=> Q')  P ={E1,E2}=> Q.
Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.

Global Instance vs_mono' E1 E2 : Proper (flip () ==> () ==> ()) (vs E1 E2).
Proof. solve_proper. Qed.

Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
43
Proof. iIntros "!# []". Qed.
44
Lemma vs_timeless E P : Timeless P   P ={E}=> P.
45
Proof. by iIntros (?) "!# > ?". Qed.
46 47 48 49 50

Lemma vs_transitive E1 E2 E3 P Q R :
  (P ={E1,E2}=> Q)  (Q ={E2,E3}=> R)  P ={E1,E3}=> R.
Proof.
  iIntros "#[HvsP HvsQ] !# HP".
51
  iMod ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
52 53 54
Qed.

Lemma vs_reflexive E P : P ={E}=> P.
55
Proof. by iIntros "!# HP". Qed.
56 57 58 59

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

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

63
Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q)  P  R ={E1,E2}=> Q  R.
64 65 66 67 68
Proof. iIntros "#Hvs !# [HP $]". by iApply "Hvs". Qed.

Lemma vs_mask_frame_r E1 E2 Ef P Q :
  E1  Ef  (P ={E1,E2}=> Q)  P ={E1  Ef,E2  Ef}=> Q.
Proof.
69
  iIntros (?) "#Hvs !# HP". iApply fupd_mask_frame_r; auto. by iApply "Hvs".
70 71 72
Qed.

Lemma vs_inv N E P Q R :
73
  N  E  inv N R  ( R  P ={E∖↑N}=>  R  Q)  P ={E}=> Q.
74 75
Proof.
  iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
76
  iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
77 78 79
  by iApply "Hclose".
Qed.

80
Lemma vs_alloc N P :  P ={N}=> inv N P.
81
Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
82 83

Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}= Q)   R, R  (P  R ={E1,E2}=> Q).
84
Proof. rewrite uPred.wand_alt. by setoid_rewrite <-uPred.persistently_wand_impl. Qed.
85
End vs.