wp_and.v

From iris.proofmode Require Import tactics.
From iris.base_logic Require Import base_logic.
From iris.program_logic Require Import weakestpre language.

Section wp_and.
  Context `{irisG Λ Σ}.
  Implicit Types s : stuckness.
  Implicit Types P : iProp Σ.
  Implicit Types Φ : val Λ → iProp Σ.
  Implicit Types v : val Λ.
  Implicit Types e : expr Λ.

  (* XXXXXXXXXXXXXXXXXXXXXXX *)
  Instance Hpers: Persistent (state_interp σ k n).
  Admitted.

  Lemma wp_and (P1 P2: val Λ → iProp Σ) e:
    ((WP e @ ∅ {{ P1 }} ) -∗ (WP e @ ∅ {{ P2 }} ) -∗ WP e @ ∅ {{ v, P1 v ∧ P2 v }})%I.
  Proof.
    iLöb as "IH" forall (e).
    iIntros "H1 H2".
    iEval (rewrite !wp_unfold /wp_pre) in "H1";
    iEval (rewrite !wp_unfold /wp_pre) in "H2";
    iEval (rewrite !wp_unfold /wp_pre).
    case_match; first by iMod "H1"; iMod "H2"; iFrame.
    iIntros (σ1 k ks n) "#Ha".

    iMod ("H1" $! σ1 k ks n with "Ha") as "[$ H1]".
    iMod ("H2" $! σ1 k ks n with "Ha") as "[% H2]".
    iIntros "!>" (e2 σ2 efs Hstep).
    iMod ("H1" $! e2 σ2 efs Hstep) as "H1";
    iMod ("H2" $! e2 σ2 efs Hstep) as "H2".
    iModIntro; iNext.
    iMod "H1" as "[$ [H1 $]]".
    iMod "H2" as "[_ [H2 _]]".
    iModIntro.
    iApply ("IH" with "H1 H2").
  Qed.
End wat.