Merge BI and SBI canonical structures
This MR flattens the BI hierarchy by merging the
sbi canonical structures. This gives significant performance benefits on developments that nest BI formers (e.g., use
monPred). For, example it gives a performance gain of 37% overall on lambdarust-weak, with improvements for individual files up to 72%, see Iris issue #303. The concrete changes are as follows:
sbicanonical structure has been removed.
bicanonical structure contains the later modality. For non step-indexed BIs the later modality can simply be defined as the identity function, as the
bicanonical structure does not require the later modality to be contractive, or to satisfy the Löb rule.
- There is a smart constructor
bi_later_mixin_idthat allows getting the later axioms for "free" if later is defined as the identity function.
- There is a separate class
BiLöb, and a "free" instance of that class if the later modality is contractive. A
BiLöbinstance is required for the
iLöbtactic, and for timeless instances of implication and wand.
- Since the
sbicanonical structure has been removed, there is a separate type class
BiInternalEqfor BIs with a notion of internal equality. An instance of this class is needed for the
iRewritetactic and the various lemmas about internal equality.
- The class
SbiEmbedhas been removed and been replaced by classes
- The class
BiPlainlyhas been generalized to BIs without internal equality. As a consequence, there is a separate class
BiPropExtfor BIs with propositional extensionality (i.e.,
■ (P ∗-∗ Q) ⊢ P ≡ Q).
- The class
BiEmbedPlainlyis a bi-entailment (i.e.,
⎡■ P⎤ ⊣⊢ ■ ⎡P⎤instead of
■ ⎡P⎤ ⊢ ⎡■ P⎤) as it has been generalized to BIs without a internal equality. In the past, the left-to-right direction was obtained for "free" using the rules of internal equality.
Some prior discussion points
Should we keep the
SbiMixin, or merge them?
No longer relevant.
SbiMixinhas been renamed into
Should we keep the files
derived_laws_sbi, or merge them? These files are large, so maybe we should split them in a different way.
Let's do that in a subsequent clean up MR.
Does the class
SbiEmbedstill make sense? I expect that embeddings exist for which we not have
⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤, but maybe those are somewhat esoteric to justify the existence of this additional type class.
No longer relevant. This class has been split up into
There are still some sections left that are called
sbi_*. Should we merge those with other sections?
Most of them have been removed, some that are left require more invasive changes to files. Let's do this in a separate cleanup MR.