Commit 226ad3bc authored by Ralf Jung's avatar Ralf Jung

wp_rec_löb: make an assumption persistent

parent 272f29d3
......@@ -223,13 +223,13 @@ Implicit Types l : loc.
induction directly, but this demonstrates that we can state the expected
reasoning principle for recursive functions, without any visible ▷. *)
Lemma wp_rec_löb s E f x e Φ Ψ :
(( v, Ψ v - WP (rec: f x := e)%V v @ s; E {{ Φ }}) -
( ( v, Ψ v - WP (rec: f x := e)%V v @ s; E {{ Φ }}) -
v, Ψ v - WP (subst' x v (subst' f (rec: f x := e) e)) @ s; E {{ Φ }}) -
v, Ψ v - WP (rec: f x := e)%V v @ s; E {{ Φ }}.
Proof.
iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
iApply lifting.wp_pure_step_later; first done.
iNext. iApply ("Hrec" with "[] HΨ"). iIntros (w) "HΨ".
iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!#" (w) "HΨ".
iApply ("IH" with "HΨ").
Qed.
......
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