pviewshifts.v 2.14 KB
Newer Older
1
2
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics ghost_ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5
6
From iris.program_logic Require Export pviewshifts.
Import uPred.

Section pvs.
7
8
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

10
Global Instance from_pure_pvs E P φ : FromPure P φ  FromPure (|={E}=> P) φ.
11
Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
12

13
Global Instance from_assumption_pvs E p P Q :
14
15
16
  FromAssumption p P (|=r=> Q)  FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.

17
18
19
20
Global Instance into_wand_pvs E1 E2 R P Q :
  IntoWand R P Q  IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.

21
22
23
Global Instance from_sep_pvs E P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
24

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
26
27
  FromOr P Q1 Q2  FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
28
29

Global Instance exists_split_pvs {A} E1 E2 P (Φ : A  iProp Σ) :
30
  FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Proof.
32
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Qed.
34

35
36
Global Instance frame_pvs E1 E2 R P Q :
  Frame R P Q  Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.

39
40
Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
41

42
43
Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
Proof. by rewrite /FromVs -rvs_pvs. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
44

45
Global Instance elim_vs_rvs_pvs E1 E2 P Q :
46
  ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 2.
47
48
Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
49
  ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q) | 1.
50
Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
End pvs.

53
Hint Extern 2 (of_envs _  _) =>
54
  match goal with |- _  |={_}=> _ => iVsIntro end.