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

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

11
12
Global Instance frame_wp E e R Φ Ψ :
  ( v, Frame R (Φ v) (Ψ v))  Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
13
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
14

15
16
Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
17
18

Global Instance elim_vs_rvs_wp E e P Φ :
19
  ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}) | 2.
20
21
22
Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.

Global Instance elim_vs_pvs_wp E e P Φ :
23
  ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}) | 1.
24
25
26
27
28
Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.

(* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
  atomic e 
29
  ElimVs (|={E1,E2}=> P) P
30
31
         (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
End weakestpre.