Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more
A new iModIntro
tactic that generalizes the former iAlways
, iNext
and iModIntro
. On top of that, it supports introduction of heterogeneous modalities such as bi_embed
.
This MR fixes #147 (closed) and #48 (closed).
Todo
-
Fix compilation, it needs a newer std++ but the CI is currently broken so no opam packages are published. -
Move the modality stuff from proofmode.classes
to its own file? -
Bikeshed about the name. -
What to do with the current iNext
? It is currently an alias foriModIntro
. We could a.) deprecate it b.) make it a specific version ofiModIntro
that only works for laters. -
Figure out what introduction pattern to deprecate, !#
or!>
. (I propose to keep!>
). -
The axioms are stronger than what was supported for the old iModIntro
, e.g. the current modality needs to satisfyM P ∗ M Q ⊢ M (P ∗ Q)
. This is not a problem for any of the existing instances, but the relative/subjective modality ofmonPred
does not satisfy this property. -
Fix the instance from_modal_monPred_at : FromModal P Q → MakeMonPredAt i Q 𝓠 → FromModal (P i) 𝓠
. I suppose we should give instances for specific modalities. Which? @jjourdan any idea? - The order in
proofmode.classes
andproofmode.class_instances
is a bit of a mess. I propose to reorder this later to avoid too conflicts with other MRs/master
.