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_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 ofplainly
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".