Commit 98b90f13 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/wp_frame_wand' into 'master'

add wp_frame_wand lemma

See merge request iris/iris!672
parents 4a59814e 771b9aed
......@@ -56,6 +56,7 @@ Coq 8.11 is no longer supported in this version of Iris.
- Use `fupd_intro _ _` for the new field `state_interp_mono` of `irisG`.
- Some proofs using lifting lemmas and adequacy theorems need to be adapted
to ignore the new step counter.
* Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement.
**Changes in `heap_lang`:**
......
......@@ -112,7 +112,7 @@ Section lemmas.
Φ, .. x, α x - (.. y, β x y - Φ (f x y)) - WP e {{ Φ }}.
Proof.
rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
iApply wp_frame_wand_l. iSplitL "HΦ"; first iAccu. iApply "Hwp".
iApply (wp_frame_wand with "HΦ"). iApply "Hwp".
iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
......
......@@ -257,6 +257,12 @@ Proof. iIntros "[H Hwp]". iApply (twp_wand with "Hwp H"). Qed.
Lemma twp_wand_r s E e Φ Ψ :
WP e @ s; E [{ Φ }] ( v, Φ v - Ψ v) - WP e @ s; E [{ Ψ }].
Proof. iIntros "[Hwp H]". iApply (twp_wand with "Hwp H"). Qed.
Lemma twp_frame_wand s E e Φ R :
R - WP e @ s; E [{ v, R - Φ v }] - WP e @ s; E [{ Φ }].
Proof.
iIntros "HR HWP". iApply (twp_wand with "HWP").
iIntros (v) "HΦ". by iApply "HΦ".
Qed.
Lemma twp_wp_step s E e P Φ :
TCEq (to_val e) None
......
......@@ -348,10 +348,10 @@ 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.
End wp.
......
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Export tactics derived_laws.
......@@ -556,9 +556,13 @@ Tactic Notation "awp_apply" open_constr(lem) :=
wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
last iAuIntro.
Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
(* Convert "list of hypothesis" into specialization pattern. *)
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
wp_apply_core lem
ltac:(fun H =>
iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H])
iApply (wp_frame_wand with
[SGoal $ SpecGoal GSpatial false [] Hs false]); [iAccu|iApplyHyp H])
ltac:(fun cont => fail);
last iAuIntro.
......
Markdown is supported
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