Commit b7823a4e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tactics `wp_branch` and `wp_select` & missing proofmode file.

parent 0f4e744e
From iris.heap_lang Require Export proofmode notation.
From iris.proofmode Require Export tactics.
From osiris Require Export proto_channel.
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
(* TODO: strip laters *)
Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K N
c p (pc : TT val * iProp Σ * iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p @ N)%I
ProtoNormalize false p [] (iProto_message Receive pc)
let Δ' := envs_delete false i false Δ in
(.. x : TT,
match envs_app false
(Esnoc (Esnoc Enil j ((pc x).1.2)) i (c (pc x).2 @ N)) Δ' with
| Some Δ'' => envs_entails Δ'' (WP fill K (of_val (pc x).1.1) {{ Φ }})
| None => False
end)
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply recv_proto_spec|f_equiv].
rewrite -bi.later_intro bi_tforall_forall; apply bi.forall_intro=> x.
specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
rewrite envs_app_sound //; simpl.
by rewrite right_id HΦ bi.wand_curry.
Qed.
Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
let solve_mapsto _ :=
let c := match goal with |- _ = Some (_, (?c _ @ _)%I) => c end in
iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
wp_pures;
let Hnew := iFresh in
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
|fail 1 "wp_recv: cannot find 'recv' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <?>"
|pm_reduce; simpl; tac_intros;
tac Hnew;
wp_finish]
| _ => fail "wp_recv: not a 'wp'"
end.
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K N
c v p (pc : TT val * iProp Σ * iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p @ N)%I
ProtoNormalize false p [] (iProto_message Send pc)
let Δ' := envs_delete false i false Δ in
(.. x : TT,
match envs_split (if neg is true then Right else Left) js Δ' with
| Some (Δ1,Δ2) =>
match envs_app false (Esnoc Enil i (c (pc x).2 @ N)) Δ2 with
| Some Δ2' =>
v = (pc x).1.1
envs_entails Δ1 (pc x).1.2
envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
| None => False
end
| None => False
end)
envs_entails Δ (WP fill K (send c v) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ].
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_proto_spec|f_equiv].
rewrite bi_texist_exist -(bi.exist_intro x).
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
destruct HΦ as (-> & -> & ->). rewrite bi.pure_True // left_id.
by rewrite -bi.later_intro right_id.
Qed.
Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
let solve_mapsto _ :=
let c := match goal with |- _ = Some (_, (?c _ @ _)%I) => c end in
iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
let solve_done d :=
lazymatch d with
| true =>
done ||
let Q := match goal with |- envs_entails _ ?Q => Q end in
fail "wp_send: cannot solve" Q "using done"
| false => idtac
end in
lazymatch spec_pat.parse pat with
| [SGoal (SpecGoal GSpatial ?neg ?Hs_frame ?Hs ?d)] =>
let Hs' := eval cbv in (if neg then Hs else Hs_frame ++ Hs) in
wp_pures;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
|fail 1 "wp_send: cannot find 'send' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <!>"
|pm_reduce; simpl; tac_exist;
repeat lazymatch goal with
| |- _, _ => eexists _
end;
lazymatch goal with
| |- False => fail "wp_send:" Hs' "not fresh"
| _ => split; [try fast_done|split;[iFrame Hs_frame; solve_done d|wp_finish]]
end]
| _ => fail "wp_send: not a 'wp'"
end
| _ => fail "wp_send: only a single goal spec pattern supported"
end.
Tactic Notation "wp_send" "with" constr(pat) :=
wp_send_core (idtac) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) ")" "with" constr(pat) :=
wp_send_core (eexists x1) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) ")"
"with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
"with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4)
uconstr(x5) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) uconstr(x7) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6; eexists x7) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) uconstr(x7) uconstr(x8) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6; eexists x7; eexists x8) with pat.
Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K N
c p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p @ N)%I
ProtoNormalize false p [] (p1 <{P1}&{P2}> p2)
let Δ' := envs_delete false i false Δ in
( b : bool,
match envs_app false
(Esnoc (Esnoc Enil j (if b then P1 else P2)) i (c (if b then p1 else p2) @ N)) Δ' with
| Some Δ'' => envs_entails Δ'' (WP fill K (of_val #b) {{ Φ }})
| None => False
end)
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv].
rewrite -bi.later_intro; apply bi.forall_intro=> b.
specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
Qed.
Tactic Notation "wp_branch" "as" constr(pat1) constr(pat2) :=
let solve_mapsto _ :=
let c := match goal with |- _ = Some (_, (?c _ @ _)%I) => c end in
iAssumptionCore || fail "wp_branch: cannot find" c "↣ ? @ ?" in
wp_pures;
let Hnew := iFresh in
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_branch _ _ Hnew K))
|fail 1 "wp_branch: cannot find 'recv' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <&>"
|pm_reduce; intros [];
[iDestructHyp Hnew as pat1|iDestructHyp Hnew as pat2]; wp_finish]
| _ => fail "wp_branch: not a 'wp'"
end.
Tactic Notation "wp_branch" := wp_branch as "_" "_".
Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K N
c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p @ N)%I
ProtoNormalize false p [] (p1 <{P1}+{P2}> p2)
let Δ' := envs_delete false i false Δ in
match envs_split (if neg is true then Right else Left) js Δ' with
| Some (Δ1,Δ2) =>
match envs_app false (Esnoc Enil i (c if b then p1 else p2 @ N)) Δ2 with
| Some Δ2' =>
envs_entails Δ1 (if b then P1 else P2)
envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
| None => False
end
| None => False
end
envs_entails Δ (WP fill K (send c #b) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
rewrite -assoc; f_equiv.
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
destruct HΦ as [-> ->]. by rewrite -bi.later_intro right_id.
Qed.
Tactic Notation "wp_select" "with" constr(pat) :=
let solve_mapsto _ :=
let c := match goal with |- _ = Some (_, (?c _ @ _)%I) => c end in
iAssumptionCore || fail "wp_select: cannot find" c "↣ ? @ ?" in
let solve_done d :=
lazymatch d with
| true =>
done ||
let Q := match goal with |- envs_entails _ ?Q => Q end in
fail "wp_select: cannot solve" Q "using done"
| false => idtac
end in
lazymatch spec_pat.parse pat with
| [SGoal (SpecGoal GSpatial ?neg ?Hs_frame ?Hs ?d)] =>
let Hs' := eval cbv in (if neg then Hs else Hs_frame ++ Hs) in
wp_pures;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_select _ neg _ Hs' K))
|fail 1 "wp_select: cannot find 'send' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_select: protocol not of the shape <+>"
|pm_reduce;
lazymatch goal with
| |- False => fail "wp_select:" Hs' "not fresh"
| _ => split;[iFrame Hs_frame; solve_done d|wp_finish]
end]
| _ => fail "wp_select: not a 'wp'"
end
| _ => fail "wp_select: only a single goal spec pattern supported"
end.
Tactic Notation "wp_select" := wp_select with "[//]".
......@@ -89,8 +89,8 @@ Section list_sort.
Proof.
iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ).
wp_lam.
wp_recv (A I R ?? cmp) with "#Hcmp".
wp_recv (xs l vs) with "[Hl HI]".
wp_recv (A I R ?? cmp) as "#Hcmp".
wp_recv (xs l vs) as "[Hl HI]".
wp_load. wp_apply (llength_spec (A:=val) with "[//]"); iIntros (_).
iDestruct (big_sepL2_length with "HI") as %<-.
wp_op; case_bool_decide as Hlen; wp_if.
......@@ -110,8 +110,8 @@ Section list_sort.
wp_send with "[$Hl1 $HI1]".
wp_send with "[$Hcmp]".
wp_send with "[$Hl2 $HI2]".
wp_recv (ys1 ws1) with (??) "[Hl1 HI1]".
wp_recv (ys2 ws2) with (??) "[Hl2 HI2]".
wp_recv (ys1 ws1) as (??) "[Hl1 HI1]".
wp_recv (ys2 ws2) as (??) "[Hl2 HI2]".
do 2 wp_load.
wp_apply (lmerge_spec with "Hcmp [$HI1 $HI2]"). iIntros (ws) "HI".
wp_store.
......@@ -136,7 +136,7 @@ Section list_sort.
wp_apply (list_sort_service_spec with "Hc"); auto. }
wp_send with "[$Hcmp]".
wp_send with "[$Hl]".
wp_recv (ys ws) with "(Hsorted & Hperm & Hl & HI)".
wp_recv (ys ws) as "(Hsorted & Hperm & Hl & HI)".
wp_pures. iApply "HΦ"; iFrame.
Qed.
End list_sort.
......@@ -92,16 +92,13 @@ Section list_sort_elem.
}}}.
Proof.
iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
wp_rec. wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
- wp_recv (x v) with "HI".
wp_apply (select_spec with "[$Hc1]")=> //=; iIntros "Hc1".
wp_send with "[$HI]".
wp_rec. wp_branch; wp_pures.
- wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
wp_apply ("IH" with "Hc Hc2 Hc1").
iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
rewrite -!(assoc_L (++)).
iApply "HΨ". iFrame "Hc Hc1 Hc2". by rewrite Hxs' (comm (++) xs1') assoc_L.
- wp_apply (select_spec with "[$Hc1]")=> //=; iIntros "Hc1".
wp_apply (select_spec with "[$Hc2]")=> //=; iIntros "Hc2".
- wp_select. wp_select.
iApply ("HΨ" $! [] [] []). rewrite !right_id_L. by iFrame.
Qed.
......@@ -119,19 +116,18 @@ Section list_sort_elem.
Proof.
iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
wp_rec. wp_apply (branch_spec with "Hcin"); iIntros ([]) "[Hcin Hys']".
- iClear "Hys'". wp_recv (x v) with (Htl) "HI".
wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_send with "[$HI]"; first by auto.
wp_rec. wp_branch as "_" "Hys'".
- wp_recv (x v) as (Htl) "HI".
wp_select. wp_send with "[$HI]"; first by auto.
wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
{ done. }
{ by rewrite Hys -!assoc_L (comm _ zs). }
{ rewrite fmap_app /=. apply Sorted_snoc; auto. }
{ intros x'. rewrite !fmap_app.
inversion 1; discriminate_list || simplify_list_eq. by constructor. }
- iDestruct "Hys'" as %Hys'. wp_apply (select_spec with "[$Hc]")=> //=.
{ by rewrite Hys Hxs Hys'. }
iIntros "Hc". iApply "HΨ". iFrame.
- iDestruct "Hys'" as %Hys'. wp_select with "[]".
{ by rewrite /= Hys Hxs Hys'. }
iApply "HΨ". iFrame.
Qed.
Lemma list_sort_elem_service_merge_spec cmp c c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
......@@ -152,13 +148,11 @@ Section list_sort_elem.
iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
wp_rec. wp_apply (branch_spec with "[$Hc2]"); iIntros ([]) "[Hc2 Hys2]".
- iClear "Hys2".
wp_recv (x v) with (Htl2) "HIx".
wp_rec. wp_branch as "_" "Hys2".
- wp_recv (x v) as (Htl2) "HIx".
wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
case_bool_decide.
+ wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_send with "[$HIy1 //]".
+ wp_select. wp_send with "[$HIy1 //]".
wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx").
{ by rewrite comm. }
{ by rewrite assoc (comm _ ys2) Hys. }
......@@ -167,8 +161,7 @@ Section list_sort_elem.
{ intros x'. rewrite !fmap_app.
inversion 1; discriminate_list || simplify_list_eq. by constructor. }
iIntros "(?&?&?)". iApply "HΨ"; iFrame.
+ wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_send with "[$HIx]".
+ wp_select. wp_send with "[$HIx]".
{ iPureIntro. by apply Htl_le, total_not. }
wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
{ by rewrite Hys assoc. }
......@@ -177,8 +170,7 @@ Section list_sort_elem.
{ intros x'. rewrite !fmap_app.
inversion 1; discriminate_list || simplify_list_eq. by constructor. }
- iDestruct "Hys2" as %Hys2.
wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_send with "[$HIy1 //]".
wp_select. wp_send with "[$HIy1 //]".
wp_apply (list_sort_elem_service_move_spec with "[$Hc $Hc1]").
{ done. }
{ by rewrite Hys Hys2 -!assoc_L (comm _ xs2). }
......@@ -195,34 +187,27 @@ Section list_sort_elem.
{{{ RET #(); c END @ N }}}.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec; wp_pures.
wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
- wp_recv (x1 v1) with "HIx1".
wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
+ wp_recv (x2 v2) with "HIx2".
wp_rec; wp_pures. wp_branch; wp_pures.
- wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
+ wp_recv (x2 v2) as "HIx2".
wp_apply (start_chan_proto_spec N list_sort_elem_protocol).
{ iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"); auto. }
iIntros (cy) "Hcy".
wp_apply (start_chan_proto_spec N list_sort_elem_protocol).
{ iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
iIntros (cz) "Hcz".
wp_apply (select_spec with "[$Hcy]")=> //; iIntros "Hcy".
wp_send with "[$HIx1]".
wp_apply (select_spec with "[$Hcz]")=> //; iIntros "Hcz".
wp_send with "[$HIx2]".
wp_select. wp_send with "[$HIx1]".
wp_select. wp_send with "[$HIx2]".
wp_apply (list_sort_elem_service_split_spec with "[$Hc $Hcy $Hcz]").
iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
wp_apply (branch_spec with "Hcy"); iIntros (b) "[Hcy Hnil]".
destruct b; last first.
wp_branch as "_" "Hnil"; last first.
{ by iDestruct "Hnil" as %?%Permutation_nil_cons. }
iClear "Hnil".
wp_recv (x v) with "[_ HIx]".
wp_recv (x v) as "[_ HIx]".
wp_apply (list_sort_elem_service_merge_spec _ _ _ _ _ [] _ _ _ _ [] []
with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
{ by rewrite Hxs' Permutation_middle. }
iIntros "(Hc & Hcy & Hcz)". by iApply "HΨ".
+ wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_send with "[$HIx1]"; first by auto using TlRel_nil.
+ wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
by wp_apply (select_spec with "[$Hc]").
- by wp_apply (select_spec with "[$Hc]").
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