Commit 3059ff86 authored by Robbert Krebbers's avatar Robbert Krebbers

Update ProofMode.md w.r.t. the changes to `iModIntro`.

parent 62e935b6
...@@ -114,35 +114,26 @@ Separating logic specific tactics ...@@ -114,35 +114,26 @@ Separating logic specific tactics
Modalities Modalities
---------- ----------
- `iModIntro` : introduction of a modality that is an instance of the - `iModIntro` : introduction of a modality. The type class `FromModal` is used
`FromModal` type class. Instances include: later, except 0, basic update and to specify which modalities this tactic should introduce. Instances of that
fancy update. type class include: later, except 0, basic update and fancy update,
persistently, affinely, plainly, absorbingly, absolutely, and relatively.
- `iAlways` : a deprecated alias of `iModIntro`.
- `iNext n` : introduce `n` laters by stripping that number of laters from all
hypotheses. If the argument `n` is not given, it strips one later if the
leftmost conjunct is of the shape `▷ P`, or `n` laters if the leftmost
conjunct is of the shape `▷^n P`.
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
an instance of the `ElimModal` type class. Instances include: later, except 0, an instance of the `ElimModal` type class. Instances include: later, except 0,
basic update and fancy update. basic update and fancy update.
The persistence and plainness modalities Induction
---------------------------------------- ---------
- `iAlways` : introduce a persistence or plainness modality and the spatial
context. In case of a plainness modality, the tactic will prune all persistent
hypotheses that are not plain.
The later modality
------------------
- `iNext n` : introduce `n` laters by stripping that number of laters from all
hypotheses. If the argument `n` is not given, it strips one later if the
leftmost conjunct is of the shape `▷ P`, or `n` laters if the leftmost
conjunct is of the shape `▷^n P`.
- `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by - `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
generating a hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq generating a hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq
level variables `x1 ... xn`, the hypotheses given by the selection pattern level variables `x1 ... xn`, the hypotheses given by the selection pattern
`selpat`, and the spatial context. `selpat`, and the spatial context.
Induction
---------
- `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on - `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
the Coq term `x`. The Coq introduction pattern is used to name the introduced the Coq term `x`. The Coq introduction pattern is used to name the introduced
variables. The induction hypotheses are inserted into the persistent context variables. The induction hypotheses are inserted into the persistent context
...@@ -229,8 +220,8 @@ appear at the top level: ...@@ -229,8 +220,8 @@ appear at the top level:
Items of the selection pattern can be prefixed with `$`, which cause them to Items of the selection pattern can be prefixed with `$`, which cause them to
be framed instead of cleared. be framed instead of cleared.
- `!%` : introduce a pure goal (and leave the proof mode). - `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an persistence or plainness modality (by calling `iAlways`). - `!>` : introduce a modality by calling `iModIntro`.
- `!>` : introduce a modality (by calling `iModIntro`). - `!#` : introduce a modality by calling `iModIntro` (deprecated).
- `/=` : perform `simpl`. - `/=` : perform `simpl`.
- `//` : perform `try done` on all goals. - `//` : perform `try done` on all goals.
- `//=` : syntactic sugar for `/= //` - `//=` : syntactic sugar for `/= //`
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment