WP tactics do not `simpl` enough
See for example line 133 of ticket_lock.v
, after calling wp_cas_fail
:
|={⊤ ∖ ↑N,⊤}=> WP if: LitV false then (wait_loop #n) (#lo, #ln) else acquire (#lo, #ln) {{ v, ϕ v }}
Here, there is an of_val (LitV false)
, which should be simplified into Lit false
, which is then pretty printed properly.
I expect the problem to be related to the fact that the WP in this case is below an update modality, and as such, simpl
is not used.