Commit 5b43a080 authored by Ralf Jung's avatar Ralf Jung
Browse files

use wp_frame_wand in awp_apply; get rid of _l/_r variants

parent 7ee261cf
......@@ -354,12 +354,6 @@ Proof.
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 *)
......
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.
......
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