Commit 0fa4f300 authored by Léon Gondelman's avatar Léon Gondelman

factoring (a_store (a_ret _) _)

parent f1899ad2
......@@ -312,6 +312,19 @@ Section Derived.
iApply awp_ret. by wp_value_head.
Qed.
Lemma a_store_ret (l:loc) (e: expr) `{Closed [] e} R Φ :
awp e R (λ w, v, l U v (l L w - Φ w)) -
awp (a_store (a_ret #l) e) R Φ.
Proof.
iIntros "H".
iApply ((a_store_spec _ _
(λ l1, l1 = l)%I
(λ w, v, (l U v (l L w - Φ w)))%I ) with "[] [H] []").
- iApply awp_ret; iApply wp_value; eauto.
- done.
- iIntros (? w) "-> H". eauto with iFrame.
Qed.
End Derived.
Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
......
......@@ -39,17 +39,14 @@ Section factorial_spec.
Proof.
iIntros "Hl HΦ".
awp_lam.
iApply (a_store_spec _ _
(λ r, r = l)%I (λ v, v = #(n+1) l U #n)%I with "[] [Hl]").
{ awp_ret_value. }
{ iApply (a_bin_op_spec _ _
(λ v, v = #n l U #n )%I (λ v, v = #1)%I with "[-]").
+ awp_load_ret l #n.
+ awp_ret_value.
+ iIntros (? ?) "(% & Hc) %"; subst. iExists #(n+1). by iFrame. }
iIntros (? ? ->) "[% Hl1]"; subst.
iExists _; iFrame.
Qed.
iApply (a_store_ret with "[Hl HΦ]").
iApply (a_bin_op_spec _ _
(λ v, v = #n l U #n )%I (λ v, v = #1)%I with "[Hl] [] [HΦ]").
+ awp_load_ret l #n.
+ awp_ret_value.
+ iIntros (? ?) "(% & Hc) %"; subst.
iExists #(n+1). iSplit; eauto with iFrame.
Qed.
Lemma factorial_body_spec (n k : nat) (c r: loc) R :
(k <= n c U #k r U #(fact k)) -
......@@ -71,13 +68,8 @@ Section factorial_spec.
do 2 (awp_seq; iApply a_sequence_spec).
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq.
iApply (a_store_spec _ _
(λ l, l = r)%I
(λ v, v = #(fact (k+1))
c U #(k + 1)
r U #(fact k))%I with "[] [Hr Hc]").
{ awp_ret_value. }
{ iApply (a_bin_op_spec _ _
iApply (a_store_ret with "[Hr Hc]").
iApply (a_bin_op_spec _ _
(λ v, v = #(fact k) r U #(fact k))%I
(λ v, v = #(k + 1) c U #(k+1))%I with "[Hr] [Hc]").
* awp_load_ret r #(fact k).
......@@ -87,12 +79,10 @@ Section factorial_spec.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
iExists #(fact (k+1)); repeat (iSplit; eauto).
by iFrame. }
iIntros (? ? ->) "(% & Hc & Hr)"; simplify_eq.
iExists _; iFrame. iIntros "Hr".
iModIntro. awp_seq.
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iApply ("IH" $! n (k+1)%nat with "[] Hc Hr"). iPureIntro. lia.
iExists #(fact k). iFrame. iIntros "Hr".
iModIntro. awp_seq.
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iApply ("IH" $! n (k+1)%nat with "[] Hc Hr"). iPureIntro. lia.
+ iRight. iSplit; eauto.
iApply a_seq_spec. iModIntro.
assert (k = n) as -> by lia. by iFrame.
......
......@@ -50,38 +50,20 @@ Section test.
awp (swap #l1 #l2) R (λ _, l1 U v2 l2 U v1).
Proof.
iIntros "Hl1 Hl2".
do 2 awp_lam.
iApply awp_bind.
awp_alloc_ret #0 r "Hr".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret #0 r "Hr".
iApply a_sequence_spec.
iApply (a_store_spec _ _ (λ l, l = r)%I
(λ v, v = v1 l1 U v1)%I with "[] [Hl1]").
{ awp_ret_value. }
{ awp_load_ret l1 v1. }
iIntros (? ? ->) "[% Hl1]"; subst.
iExists _; iFrame. iIntros "Hr". iModIntro.
awp_seq.
iApply a_sequence_spec.
iApply (a_store_spec _ _ (λ l, l = l1)%I
(λ v, v = v2 l2 U v2)%I with "[] [Hl2]").
{ awp_ret_value. }
{ awp_load_ret l2 v2. }
iIntros (? ? ->) "[% Hl2]"; subst.
iExists _; iFrame. iIntros "Hl1". iModIntro.
awp_seq.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l1 v1. iIntros "Hl1". iExists #0. iFrame.
iIntros "Hr". iModIntro. awp_seq. iApply a_sequence_spec.
iApply awp_bind.
iApply (a_store_spec _ _ (λ l, l = l2)%I
(λ v, v = v1 r U v1)%I with "[] [Hr]").
{ awp_ret_value. }
{ awp_load_ret r v1. }
iIntros (? ? ->) "[% Hr]"; subst.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l2 v2. iIntros "Hl2". iExists v1. iFrame.
iIntros "Hl1". iModIntro. awp_seq. iApply awp_bind.
iExists _; iFrame. iIntros "Hl2".
awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret r v1. iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
Qed.
End test.
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