From d6e6d71e9c2b1a88cd2c5b3e9c386f7dc4406c90 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 30 Jun 2016 14:01:54 +0200 Subject: [PATCH] Bring back wp_bindi I know we don't use it. Stating theorems also serves to document things, and IMHO this one is informative. It also costs us nothing. --- heap_lang/heap.v | 1 + heap_lang/lifting.v | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/heap_lang/heap.v b/heap_lang/heap.v index ff7f0c78..a9dad272 100644 --- a/heap_lang/heap.v +++ b/heap_lang/heap.v @@ -148,6 +148,7 @@ Section heap. Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed. (** Weakest precondition *) + (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *) Lemma wp_alloc N E e v Φ : to_val e = Some v → nclose N ⊆ E → heap_ctx N ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}. diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index 934fd473..ea1e9076 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -17,6 +17,11 @@ Lemma wp_bind {E e} K Φ : WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}. Proof. exact: wp_ectx_bind. Qed. +Lemma wp_bindi {E e} Ki Φ : + WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢ + WP fill_item Ki e @ E {{ Φ }}. +Proof. exact: weakestpre.wp_bind. Qed. + (** Base axioms for core primitives of the language: Stateful reductions. *) Lemma wp_alloc_pst E σ e v Φ : to_val e = Some v → -- 2.24.1