CakeML
xsimpl is sometimes unsafe
Consider the goal
W8ARRAY av a ==>> W8ARRAY av a * &(?loc. av = Loc loc)
This goal is easily provable, but applying xsimpl reduces it to the unprovable goal ∃loc. av = Loc loc.
The reason this happens is that hpullr applies the rule hsimpl_prop, which is
∀H' H P. P ∧ H' ==>> H ⇒ H' ==>> H * &P
This rule does not seem to account for the possibility that the truth of P depends on information in H. One way to prevent situations such as the above from happening is to strengthen hsimpl_prop to say
∀H' H P. (∀h. H h ⇒ P) ∧ H' ==>> H ⇒ H' ==>> H * &P
However, this would come at the cost of slightly noisier subgoals for the 99% of situations where H is not needed to prove P.
The purpose of this issue is to discuss whether making this change would be desirable. My own feeling is yes, mostly because I would expect a tactic with "simp" in its name to be safe.
Sounds good to me. I think the usual approach people use instead currently is to call xpull at the right time before xsimpl. But a safe xsimpl would be better.
