sep_apply unable to handle some expressions with propositions.

[roconnor-blockstream]

Require Import VST.floyd.proofauto.

Goal forall A B C P, (P && B) |-- C -> A * (P && B) |-- A * C.
intros A B C P H.
sep_apply H.
entailer!.
Qed.

Goal forall A B C P, (!!P && B) |-- C -> A * (!!P && B) |-- C.
intros A B C P H.
sep_apply H. (*sep_apply fails*)

The above (tested in VST 2.9.1) illustrates how sep_apply fails to operate on an expression that uses a proposition, but does succeed on a similar, more general, expression.

I would expect sep_apply to be able to handle this case.

[QinshiWang]

sep_apply has special manipulation for assumptions in the form of !! ?P && _ (see here). So for (!!P && B) |-- C, sep_apply treats it as P -> B |-- C and it cannot find B to apply. I'm not sure if it is a good design.