Commit f400f576 authored by Robbert Krebbers's avatar Robbert Krebbers

Create eauto hint for iPvsIntro.

parent 3e0408b2
Pipeline #1793 passed with stage
......@@ -181,3 +181,6 @@ Tactic Notation "iTimeless" constr(H) :=
Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
iTimeless H; iDestruct H as Hs.
Hint Extern 2 (of_envs _ _) =>
match goal with |- _ (|={_}=> _)%I => iPvsIntro end.
......@@ -52,7 +52,7 @@ Proof.
iPvsIntro. iApply "Hf"; iSplit.
- iIntros {n} "!". wp_let.
iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
+ iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
+ iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft].
iPvs (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). }
iPvsIntro; iRight; iExists n; by iSplitL "Hl".
......@@ -79,7 +79,7 @@ Proof.
iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
iSplitL "Hl"; [iRight; by eauto|].
wp_match. iApply wp_assert'. wp_op=>?; iPvsIntro; simplify_eq/=; eauto.
wp_match. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
Qed.
Lemma hoare_one_shot (Φ : val iProp) :
......
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