Library iris.proofmode.weakestpre

From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export pviewshifts pstepshifts.
From iris.program_logic Require Export weakestpre.
Import uPred.

Section weakestpre.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.

Global Instance aframe_wp E e R Φ Ψ :
  AffineP R →
  (∀ v, Frame R (Φ v) (Ψ v)) →
  Frame R (WP e @ E {{ Φ }})
          (WP e @ E {{ Ψ}}).
Proof.
  rewrite /Frame⇒ HA HR. rewrite -(affine_affine R). rewrite wp_frame_l.
  apply wp_mono. intros v. rewrite affine_elim. apply HR.
Qed.
Global Instance is_afsa_wp E e Φ :
  IsAFSA (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
Proof. split. done. apply _. Qed.
End weakestpre.