GitLab

In the interface for plainly, we could have plainly_alt as an axiom. Here are the reasons this is not a completely absurd idea:

1- Most of the axioms can be removed. Namely, the only ones remaining are:

• bi_persistently_impl_plainly, bi_plainly_impl_plainly (which I find kind of arbitrary anyway),
• sbi_mixin_prop_ext (which is actually one of the few current axioms of plainly that actually /says/ something about the BI. So this is expected that it stays.
• The axioms about the updates, but I would say these are rather about the update than about bi_plainly
• sbi_mixin_later_plainly_2, which somehow I am not able to prove. But perhaps I am missing something.

Note that for some of these axioms (except bi_plainly_impl_plainly, sbi_mixin_prop_ext and the update axioms), we could replace "for all plain assertion P" by "for all equality", which make them understandable even without understanding what is plainly.

2- I would say the definition of plainly_alt is quite intuitive. Indeed, P /\ emp = emp is a way of internally saying emp |- P, which exactly means that P is valid. So this definition can directly be interpreted as the "internal validity".