Use siProp more in building the uPred (and BI) interfaces
uPred defines a few (primitive) connectives that could all be defined in terms of an
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an
siProp embedding. Going this route might also finally let us get rid of
base_logic.algebra and instead prove these lemmas in
siProp so they can be used "for free" in any BI with an
siProp embedding. We might even want to use
siProp to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
- Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
- (depends on 1) Add proof mode support for embed and emp_valid.
- (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
- (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
- (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
- (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
- (depends on 1) State uPred_entails as an siProp.
- (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
- (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
- (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use
siPropfor dinstance? Still need to derive
Prop-based version for setoid rewriting though.