iDestruct and iPureIntro
I recently bumped into a scenario like this:
H : heapN ⊥ N
o', n' : Z
============================
"~" : heap_ctx
"~1" : inv N
(∃ o n : Z,
(l ↦ (#o, #n) ∧ ■ (o < n))
★ (auth_own γ {[o := ()]} ∨ own γ (Excl ()) ★ R))
"IH" : (locked l R -★ R -★ Φ #()) -★ WP acquire #l {{ v, Φ v }}
--------------------------------------□
"H2" : ■ (o' < n')
--------------------------------------★
■ (o' < n' + 1)
To prove this, I have to first iDestruct "H2" as "%"
to move o' < n'
to Coq context, then I can iPureIntro
and do the following proof.
My problem is, will it be good to let iPureIntro
(or invent something on top of it) to handle the iDestruct
here for me?
Or even more convenient, it is possible to apply pure theorems directly in this context?
Thanks!