GitLab

The advantage is that we can directly use a Coq introduction pattern
`cpat` to perform actions to the pure assertion. Before, this had
to be done in several steps:

  iDestruct ... as "[Htmp ...]"; iDestruct "Htmp" as %cpat.

That is, one had to introduce a temporary name.

I expect this to be quite useful in various developments as many of
e.g. our invariants are written as:

  ∃ x1 .. x2, ⌜ pure stuff ⌝ ∗ spacial stuff.

For obsolete reasons, that no longer seem to apply, we used ∅ as the
unit.

This makes it easier to frame or introduce some modalities before introducing
universal quantifiers.

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.

No longer `put box_own_prop γ P` in the invariant, it is persistent.

    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.

We need instances like EqDecision and Countable for it. We could
redeclare those instead, though.

The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk *
was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was
a random choice from a unicode chart.

The new symbol ∗ (as proposed by David Swasey) corresponds better to
conventional practise and matches the symbol we use on paper.

There are now two proof mode tactics for dealing with modalities:

- `iModIntro` : introduction of a modality
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality

The behavior of these tactics can be controlled by instances of the `IntroModal`
and `ElimModal` type class. We have declared instances for later, except 0,
basic updates and fancy updates. The tactic `iMod` is flexible enough that it
can also eliminate an updates around a weakest pre, and so forth.

The corresponding introduction patterns of these tactics are `!>` and `>`.

These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`.

Source of backwards incompatability: the introduction pattern `!>` is used for
introduction of arbitrary modalities. It used to introduce laters by stripping
of a later of each hypotheses.