GitLab

Based on an earlier MR by @jung.

This change is slightly more invasive than expected: in monPred we were
using the embedding before the BI was defined. With the new setup, this
is no longer possible, because in order to make an instance of the
embedding, we need to know that `monPred` is a BI. As such, we define
`emp`, `⌜ _ ⌝` and friends directly in the model of `monPred` and later
prove that they are equal to a version in terms of the embedding.

This requires changing the Hint Mode of the [Frame] type class because it should not fail if its parameter is an evar, but instantiate it instead. In order to prevent all the other instances of [Frame] to intantiate this evar themselves, we create a new type class [KnwonFrame], which corresponds to the old behavior.

See the discussion in #163.

They are split into:
1- KnownMakeXXX , which only works if the parameter is not an evar. Hence, it will never force this evar to becomes e.g., emp or True.
2- MakeXXX, which works even if this is an evar, but it only has instances that will not instanciate arbitrarilly this evar.

As reported by @jjourdan: framing now no longer back tracks on whether
to strip laters or not. When framing below a later, we now only make it
strip laters of the head of the frame.

For better support for eliminating affine/absorbing separating
conjunctions in the persistent context/under a plainness/persistence
modality.

We now use the `Maybe` prefix as also used for `Frame`: it indicates
whether progress has been made by stripping of a later or not.

This reverts commit 78ba9509.

This supports Iris 2 like update modalities, as used in e.g. by @jtassaro.

This commit fixes issue #154.

These were needed pre-a63f256e.

We already supported framing under wands.

For example, framing `P` in `(P ∨ Q) ∗ R` now succeeds and turns the goal into `R`.

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.