Commit 09835135 authored by Ralf Jung's avatar Ralf Jung
Browse files

add wp_frame_wand lemma

parent 4a59814e
......@@ -348,12 +348,18 @@ Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
Lemma wp_wand_r s E e Φ Ψ :
WP e @ s; E {{ Φ }} ( v, Φ v - Ψ v) WP e @ s; E {{ Ψ }}.
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
Lemma wp_frame_wand_l s E e Q Φ :
Q WP e @ s; E {{ v, Q - Φ v }} - WP e @ s; E {{ Φ }}.
Lemma wp_frame_wand s E e Φ R :
R - WP e @ s; E {{ v, R - Φ v }} - WP e @ s; E {{ Φ }}.
Proof.
iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
iIntros "HR HWP". iApply (wp_wand with "HWP").
iIntros (v) "HΦ". by iApply "HΦ".
Qed.
Lemma wp_frame_wand_l s E e Q Φ :
Q WP e @ s; E {{ v, Q - Φ v }} - WP e @ s; E {{ Φ }}.
Proof. iIntros "[HQ HWP]". by iApply (wp_frame_wand with "HQ"). Qed.
Lemma wp_frame_wand_r s E e Q Φ :
WP e @ s; E {{ v, Q - Φ v }} Q - WP e @ s; E {{ Φ }}.
Proof. iIntros "[HWP HQ]". by iApply (wp_frame_wand with "HQ"). Qed.
End wp.
(** Proofmode class instances *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment