Commit 3b2fe797 authored by Robbert Krebbers's avatar Robbert Krebbers

iLob supports 14 args now!

parent d51bf170
......@@ -179,10 +179,8 @@ Section list_sort_elem.
list_sort_service_merge c #y1 c1 c2
{{{ RET #(); c END @ N c1 END @ N c2 END @ N}}}.
Proof.
iIntros (Hxs Hys Hsort Htl Htl_le Ψ).
iRevert (Htl_le). (* This is stupid, iLob need to support > 12 arguments *)
iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 ys1 ys2 Hxs Hys Hsort Htl).
iIntros (Htl_le) "(Hc & Hc1 & Hc2) HΨ".
iIntros (Hxs Hys Hsort Htl Htl_le Ψ) "(Hc & Hc1 & Hc2) HΨ".
iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
wp_rec.
wp_pures.
rewrite (tail_protocol_unfold xs).
......@@ -201,7 +199,7 @@ Section list_sort_elem.
wp_apply (send_proto_spec N with "Hc")=> //=.
iExists y1. iSplit; first done. iSplit; first done.
iIntros "!> Hc".
wp_apply ("IH" with "[%] [%] [%] [%] [%] [$Hc $Hc2 $Hc1]").
wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1").
{ by rewrite comm. }
{ by rewrite assoc (comm _ ys2) Hys. }
{ by apply Sorted_snoc. }
......@@ -215,7 +213,7 @@ Section list_sort_elem.
iExists x. iSplit; first done. iSplit.
{ iPureIntro. auto with lia. }
iIntros "!> Hc".
wp_apply ("IH" with "[% //] [%] [%] [%] [%] [$Hc $Hc1 $Hc2] [$]").
wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 [$]").
{ by rewrite Hys assoc. }
{ apply Sorted_snoc; auto with lia. }
{ constructor. lia. }
......
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