weakestpre.v 1.44 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 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32

Global Instance to_assert_wp E e P Φ :
  IntoAssert P (WP e @ E {{ Ψ }}) (|={E}=> P).
Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_wp. Qed.

Global Instance is_now_True_wp E e Φ : IsNowTrue (WP e @ E {{ Φ }}).
Proof. by rewrite /IsNowTrue -{2}pvs_wp -now_True_pvs -pvs_intro. Qed.

Global Instance elim_vs_rvs_wp E e P Φ :
  ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
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 Φ :
  ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
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 
33
  ElimVs (|={E1,E2}=> P) P
34 35
         (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
36
End weakestpre.