Skip to content
  • Robbert Krebbers's avatar
    Generic `iAlways` tactic. · 6dc83bcb
    Robbert Krebbers authored
    This commit 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:
    
    ```coq
    Inductive always_intro_spec (PROP : bi) :=
      | AIEnvIsEmpty
      | AIEnvForall (C : PROP → Prop)
      | AIEnvFilter (C : PROP → Prop)
      | AIEnvClear
      | AIEnvId.
    ```
    
    An always-style modality is then a record `always_modality` packing together the
    modality with the laws it should satisfy to justify the given actions for both
    contexts.
    6dc83bcb