Commit 5b78fb97 authored by Léon Gondelman's avatar Léon Gondelman

fix factorial_spec

parent 8a6c5109
......@@ -108,19 +108,17 @@ Section factorial_spec.
Lemma factorial_spec (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam. iApply awp_bind. iApply (a_alloc_spec _ _ (λ v, v = #1)%I).
{ iApply awp_ret. by iApply wp_value. }
iIntros (? r ->) "Hr". awp_lam. iApply awp_bind.
iApply (a_alloc_spec _ _ (λ v, v = #0)%I).
{ iApply awp_ret. by iApply wp_value. }
iIntros (? c ->) "Hc". awp_lam.
awp_lam.
iApply awp_bind. iApply a_alloc_spec. iApply awp_ret. iApply wp_value.
iIntros (r) "Hr". awp_lam.
iApply awp_bind. iApply a_alloc_spec. iApply awp_ret. iApply wp_value.
iIntros (c) "Hc". awp_lam.
iApply a_sequence_spec.
iApply (awp_wand _ (λ _, c U #n r U #(fact n))%I with "[Hr Hc]").
- iApply (factorial_body_spec n 0 c r R). iFrame. iPureIntro. lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
iApply (a_load_spec _ _ (λ v, v = r)%I).
+ iApply awp_ret. iApply wp_value; eauto.
+ iIntros (? ->). iExists _; iFrame. eauto.
iApply a_load_spec. iApply awp_ret. iApply wp_value; eauto.
iExists _,_; iFrame. eauto.
Qed.
End factorial_spec.
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