Commit 71518adc authored by Léon Gondelman 's avatar Léon Gondelman

get rid of awp_bind rule in examples, use vcg_solver instead.

parent 149ef27a
...@@ -56,22 +56,22 @@ Section factorial_spec. ...@@ -56,22 +56,22 @@ Section factorial_spec.
AWP factorial #n @ R {{ v, v = #(fact n) }}%I. AWP factorial #n @ R {{ v, v = #(fact n) }}%I.
Proof. Proof.
awp_lam. awp_lam.
iApply awp_bind. awp_alloc_ret r "[Hr _]". vcg_solver.
iApply awp_bind. awp_alloc_ret c "[Hc _]". iExists 1%nat; iSplit; [ done | iIntros (r) "[Hr _]"]. vcg_continue. iIntros "Hr".
iApply a_sequence_spec'. iNext. iExists 1%nat; iSplit; [ done | iIntros (c) "[Hc _]"]. vcg_continue. iIntros "Hr Hc".
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]"). iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia. - iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro. - iIntros (?) "[Hc Hr]". vcg_continue. iModIntro. eauto.
awp_load_ret r.
Qed. Qed.
Lemma factorial_spec_with_inv (n: nat) R : Lemma factorial_spec_with_inv (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I. awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof. Proof.
awp_lam. awp_lam.
iApply awp_bind. awp_alloc_ret r "[Hr _]". vcg_solver.
iApply awp_bind. awp_alloc_ret c "[Hc _]". iExists 1%nat; iSplit; [ done | iIntros (r) "[Hr _]"]. vcg_continue. iIntros "Hr".
iApply a_sequence_spec'. iNext. do 3 awp_lam. iExists 1%nat; iSplit; [ done | iIntros (c) "[Hc _]"]. vcg_continue. iIntros "Hr Hc".
do 3 awp_lam.
iApply (a_while_inv_spec iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]"). (k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia. - iExists O. eauto with iFrame lia.
...@@ -87,8 +87,9 @@ Section factorial_spec. ...@@ -87,8 +87,9 @@ Section factorial_spec.
{ rewrite Nat.add_1_r /fact. lia. } { rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia. assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iExists (k+1)%nat. eauto with iFrame lia. iExists (k+1)%nat. eauto with iFrame lia.
+ iLeft. iSplit; eauto. do 2 iModIntro. + iLeft. iSplit; eauto. iModIntro.
iRevert "H". iIntros "%". assert (k = n) as -> by lia. iRevert "H". iIntros "%". assert (k = n) as -> by lia.
awp_load_ret r. vcg_continue. eauto.
Qed. Qed.
End factorial_spec. End factorial_spec.
...@@ -93,6 +93,15 @@ Section memcpy. ...@@ -93,6 +93,15 @@ Section memcpy.
AWP a_invoke memcpy (♯ₗp ||| (♯ₗq ||| n)) @ R {{ _, p C ls2 q C ls2 }}. AWP a_invoke memcpy (♯ₗp ||| (♯ₗq ||| n)) @ R {{ _, p C ls2 q C ls2 }}.
Proof. Proof.
iIntros (? ?) "Hp Hq". vcg_solver. awp_lam. iIntros (? ?) "Hp Hq". vcg_solver. awp_lam.
(* This can replace the proof-in-progress below:
vcg_solver. iExists 1%nat; iSplit; first done. iIntros (pp) "[Hpp _]".
vcg_continue. iIntros "Hpp". iExists 1%nat; iSplit; first done.
iIntros (qq) "[Hqq _]". vcg_continue. iIntros "Hpp Hqq".
repeat awp_proj. awp_let. set (e :=( whileᶜ (_) { _ })%E).
unfold e. vcg_solver. iIntros "Hpp Hqq". *)
iApply awp_bind. vcg_solver. iExists 1%nat; iSplit; first done. iApply awp_bind. vcg_solver. iExists 1%nat; iSplit; first done.
iIntros (pp) "[Hpp _]". vcg_continue. iIntros "Hpp". awp_let. iIntros (pp) "[Hpp _]". vcg_continue. iIntros "Hpp". awp_let.
iApply awp_bind. vcg_solver. iIntros "Hpp". iExists 1%nat; iSplit; first done. iApply awp_bind. vcg_solver. iIntros "Hpp". iExists 1%nat; iSplit; first done.
......
...@@ -42,7 +42,10 @@ Section tests_vcg. ...@@ -42,7 +42,10 @@ Section tests_vcg.
AWP (swap_with_alloc (cloc_to_val l1)) (cloc_to_val l2) @ R {{ _, l1 C v2 l2 C v1 }}. AWP (swap_with_alloc (cloc_to_val l1)) (cloc_to_val l2) @ R {{ _, l1 C v2 l2 C v1 }}.
Proof. Proof.
iIntros "Hl1 Hl2". iIntros "Hl1 Hl2".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "[Hr _]". do 2 awp_lam.
vcg_solver. iIntros "!> !> !> **". eauto with iFrame. vcg_solver.
iIntros "Hl2 Hl1". iExists 1%nat. iSplit; first done.
iIntros (l3) "[Hl3 _]". vcg_continue.
iIntros "!> !> !> **". eauto with iFrame.
Qed. Qed.
End tests_vcg. End tests_vcg.
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