Generic `iAlways` tactic.

This MR implements a generic iAlways tactic that is not tied to persistently, affinely and plainly but can be instantiated with a variety of always-style modalities.

In order to plug in an always-style modality, one has to decide for both the persistent and spatial what action should be performed upon introducing the modality:

• Introduction is only allowed when the context is empty.
• Introduction is only allowed when all hypotheses satisfy some predicate C : PROP → Prop (where C should be a type class).
• Introduction will only keep the hypotheses that satisfy some predicate C : PROP → Prop (where C should be a type class).
• Introduction will clear the context.
• Introduction will keep the context as-if.

Formally, these actions correspond to the following inductive type:

Inductive always_intro_spec (PROP : bi) :=
  | AIEnvIsEmpty
  | AIEnvForall (C : PROP → Prop)
  | AIEnvPrune (C : PROP → Prop)
  | AIEnvClear
  | AIEnvId.

An always-style modality is then a record packing together the modality with the laws it should satisfy to justify the given actions for both contexts.

Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
    (pspec sspec : always_intro_spec PROP) := {
  always_modality_mixin_persistent :
    match pspec with
    | AIEnvIsEmpty => True
    | AIEnvForall C | AIEnvPrune C => ∀ P, C P → □ P ⊢ M (□ P)
    | AIEnvClear => True
    | AIEnvId => ∀ P, □ P ⊢ M (□ P)
    end;
  always_modality_mixin_spatial :
    match sspec with
    | AIEnvIsEmpty => True
    | AIEnvForall C => ∀ P, C P → P ⊢ M P
    | AIEnvPrune C => (∀ P, C P → P ⊢ M P) ∧ (∀ P, Absorbing (M P))
    | AIEnvClear => ∀ P, Absorbing (M P)
    | AIEnvId => False
    end;
  always_modality_mixin_emp : emp ⊢ M emp;
  always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
  always_modality_mixin_and P Q : M P ∧ M Q ⊢ M (P ∧ Q);
  always_modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
}.

Record always_modality (PROP : bi) := AlwaysModality {
  always_modality_car :> PROP → PROP;
  always_modality_persistent_spec : always_intro_spec PROP;
  always_modality_spatial_spec : always_intro_spec PROP;
  always_modality_mixin_of : always_modality_mixin
    always_modality_car
    always_modality_persistent_spec always_modality_spatial_spec
}.

Todo before merging

• Make it work for monPred_all. For this, we need the class Objective P := P ⊢ monPred_all P first, for which @jjourdan will make an MR.
• Figure out how to state from_always_monPred_at and from_always_embed. I guess we just have to make a bunch of instances for these corresponding to the different modalities that commute with embeddings and monPred_at. @jjourdan I need your help here.
• Write some documentation

Todo after merging

• Figure out how to generalize the axioms to support modalities that do not enjoy emp ⊢ M emp, such as the plainly modality in the linear setting.