From 2521b1a99f18334ca95797cb1793b0cc8c8f7fca Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 6 Dec 2016 20:46:48 +0100 Subject: [PATCH] Simplify proof of wp_rec_locked. --- heap_lang/lifting.v | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index ee50b4a81..7d45d5501 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -111,15 +111,11 @@ Proof. intros; inv_head_step; eauto. Qed. -Lemma wp_rec_locked E f x erec (e1 e2 : expr) Φ `{!Closed (f :b: x :b: []) erec} : +Lemma wp_rec_locked E f x erec e1 e2 Φ `{!Closed (f :b: x :b: []) erec} : e1 = of_val $ locked (RecV f x erec) → is_Some (to_val e2) → ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}. -Proof. - intros -> [v2 ?]. unlock. rewrite -(wp_lift_pure_det_head_step' (App _ _) - (subst' x e2 (subst' f (Rec f x erec) erec))); eauto. - intros; inv_head_step; eauto. -Qed. +Proof. unlock. auto using wp_rec. Qed. Lemma wp_un_op E op e v v' Φ : to_val e = Some v → -- GitLab