Commit 2521b1a9 authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify proof of wp_rec_locked.

parent b115ff3f
......@@ -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
......
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