Fix this by doing apply bi.pure_intro on the goal of said form.
Example that demonstrates the bug:
Example normalize_bug {prop:bi} P: @bi_entails prop True ⌜P⌝. (* normalize1 in this example is without the fix *) Fail timeout 3 (repeat normalize1). Ltac fixed_normalize := match goal with | |- bi_entails ?A ?B => match A with | ⌜True⌝ => apply bi.pure_intro | ⌜_⌝ => apply bi.pure_elim' end | |- ?ZZ -> ?YY => match type of ZZ with | Prop => fancy_intros true || fail 1 | _ => intros _ end end. repeat fixed_normalize. Abort.
The tactic normalize1 loops on a goal of the form True - (bi_pure phi)), due to https://github.com/PrincetonUniversity/VST/blob/726c470790d9322468f1db84f95c96b4cadf4afa/floyd/seplog_tactics.v#L1256 and https://github.com/PrincetonUniversity/VST/blob/726c470790d9322468f1db84f95c96b4cadf4afa/floyd/seplog_tactics.v#L1285.
Fix this by doing
apply bi.pure_introon the goal of said form.Example that demonstrates the bug:
Example normalize_bug {prop:bi} P: @bi_entails prop True ⌜P⌝. (* normalize1 in this example is without the fix *) Fail timeout 3 (repeat normalize1). Ltac fixed_normalize := match goal with | |- bi_entails ?A ?B => match A with | ⌜True⌝ => apply bi.pure_intro | ⌜_⌝ => apply bi.pure_elim' end | |- ?ZZ -> ?YY => match type of ZZ with | Prop => fancy_intros true || fail 1 | _ => intros _ end end. repeat fixed_normalize. Abort.