From f612cffc9472ba8ae640fdc19fe5260ccf388923 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 3 May 2018 15:39:40 +0200 Subject: [PATCH] awp_apply tactic. --- theories/c_translation/monad.v | 10 +++++++++ theories/c_translation/proofmode.v | 24 +++++++++++++++++++++ theories/c_translation/translation.v | 31 +++++++--------------------- 3 files changed, 41 insertions(+), 24 deletions(-) diff --git a/theories/c_translation/monad.v b/theories/c_translation/monad.v index 500b585..22a5364 100644 --- a/theories/c_translation/monad.v +++ b/theories/c_translation/monad.v @@ -66,6 +66,16 @@ End a_wp. Section a_wp_rules. Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapG Σ}. + Lemma a_wp_awp R Φ Ψ e : awp e R Φ -∗ (∀ v : val, awp v R Φ -∗ Ψ v) -∗ WP e {{ Ψ }}. + Proof. + iIntros "Hwp H". iApply (wp_wand with "Hwp"). + iIntros (v) "Hwp". iApply "H". by iApply wp_value'. + Qed. + + Lemma wp_awp_bind R Φ K e : + WP e {{ v, awp (fill K (of_val v)) R Φ }} ⊢ awp (fill K e) R Φ. + Proof. by apply: wp_bind. Qed. + Lemma awp_ret e R Φ : WP e {{ Φ }} -∗ awp (a_ret e) R Φ. Proof. diff --git a/theories/c_translation/proofmode.v b/theories/c_translation/proofmode.v index 4f87607..27c1ef0 100644 --- a/theories/c_translation/proofmode.v +++ b/theories/c_translation/proofmode.v @@ -4,6 +4,30 @@ From iris_c.lib Require Import locking_heap mset flock. From iris_c.c_translation Require Export monad lifting. From iris.proofmode Require Import coq_tactics. +Lemma tac_awp_bind `{locking_heapG Σ, heapG Σ, flockG Σ} K Δ R Φ e f : + f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *) + envs_entails Δ (WP e {{ v, awp (f (of_val v)) R Φ }})%I → + envs_entails Δ (awp (fill K e) R Φ). +Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_awp_bind. Qed. + +Ltac awp_bind_core K := + lazymatch eval hnf in K with + | [] => idtac + | _ => eapply (tac_awp_bind K); [simpl; reflexivity|lazy beta] + end. + +Tactic Notation "awp_apply" open_constr(lem) := + iPoseProofCore lem as false true (fun H => + lazymatch goal with + | |- envs_entails _ (awp ?e ?R ?Q) => + reshape_expr e ltac:(fun K e' => + awp_bind_core K; iApplyHyp H; try iNext (*; try wp_expr_simpl*) ) || + lazymatch iTypeOf H with + | Some (_,?P) => fail "awp_apply: cannot apply" P + end + | _ => fail "awp_apply: not a 'awp'" + end). + Lemma tac_awp_pure `{locking_heapG Σ, heapG Σ, flockG Σ} Δ Δ' K e1 e2 e φ R Φ : e = fill K e1 → PureExec φ e1 e2 → diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index ebce8f0..f7af137 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -85,23 +85,14 @@ Section proofs. { rewrite -bi.big_sepM_insert_override; eauto. } Qed. - Lemma a_fill R Ψ Φ K e : - awp e R Ψ -∗ - (∀ v : val, awp v R Ψ -∗ awp (fill K (of_val v)) R Φ) -∗ - awp (fill K e) R Φ. - Proof. - iIntros "Hwp H". iApply wp_bind. iApply (wp_wand with "Hwp"). - iIntros (v) "Hwp". iApply "H". iApply wp_value'. done. - Qed. - Lemma a_sequence_spec R Φ (e1 e2 : expr) : AsVal e2 → awp e1 R (λ v, U (awp (e2 v) R Φ)) -∗ awp (a_seq_bind e1 e2) R Φ. Proof. iIntros ([v2 <-%of_to_val]) "H". - iApply (a_fill _ _ _ [AppRCtx a_seq_bind; AppLCtx v2] with "H"). - iIntros (v) "H /=". rewrite /a_seq_bind. awp_lam. awp_lam. + awp_apply (a_wp_awp with "H"); iIntros (v) "H". + rewrite /a_seq_bind /=. do 2 awp_lam. iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H". awp_lam. iApply awp_bind. iApply a_seq_spec. iModIntro. by awp_lam. @@ -179,19 +170,11 @@ Section proofs. awp (a_store e1 e2) R Φ. Proof. iIntros "H1 H2 HΦ". - iApply (a_fill _ _ _ [AppRCtx a_store; AppLCtx e2] with "H1"). - iIntros (v) "H1 /=". - rewrite /a_store. awp_lam. - iApply (a_fill _ _ _ [AppRCtx (LamV "x2" ( -(a_bind (λ: "vv", a_atomic_env (λ: "env", (mset_add (Fst "vv")) "env";; Fst "vv" <- Snd "vv";; Snd "vv"))) - ((a_par v) "x2") -)%E)] with "H2"). simpl. iIntros (v2) "H2". awp_lam. -iApply awp_bind. iApply (awp_par with "H1 H2"). iNext. -iIntros (w1 w2) "H1 H2". -iDestruct "H1" as (l ->) "H1". - iNext. awp_lam. clear v. -iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]". - + awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam. + awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam. + iApply awp_bind. iApply (awp_par with "H1 H2"). + iIntros "!>" (w1 w2) "H1 H2 !>". iDestruct "H1" as (l ->) "H1". awp_lam. + iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]". iApply awp_atomic_env. iIntros (env) "Henv HR". rewrite {2}/env_inv. -- GitLab