Use `plainly_alt` as an axiom and replace most of the current ones
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_plainly_impl_plainly(which I find kind of arbitrary anyway),
sbi_mixin_prop_ext(which is actually one of the few current axioms of
plainlythat 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
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
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".