From 81e5a30941057f06d692575600e3f30022233bda Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita
Date: Wed, 3 Mar 2021 08:29:12 +0000
Subject: [PATCH 1/3] fix typos in proof_mode.md
---
docs/proof_mode.md | 20 ++++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index dfd003581..b383aed63 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -55,7 +55,7 @@ Applying hypotheses and lemmas
conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
[proof mode terms][pm-trm] below.
If the applied term has more premises than given specialization patterns, the
- pattern is extended with `[] ... []`. As a consequence, all unused spatial
+ pattern is extended with `[] ... []`. As a consequence, all unused spatial
hypotheses move to the last premise.
Context management
@@ -126,7 +126,7 @@ Introduction of logical connectives
- `iSplit` : split a conjunction `P ∧ Q` into two goals. Also works for
separating conjunction `P ∗ Q` provided one of the operands is persistent (and both
proofs may use the entire spatial context).
-- `iExist t1, .., tn` : provide a witness for an existential quantifier `∃ x, ...`. `t1
+- `iExists t1, .., tn` : provide a witness for an existential quantifier `∃ x, ...`. `t1
... tn` can also be underscores, which are turned into evars. (In fact they
can be arbitrary terms with holes, or `open_constr`s, and all of the
holes will be turned into evars.)
@@ -149,7 +149,7 @@ Elimination of logical connectives
intuitionistic context, it will not be thrown away.
+ `iDestruct pm_trm as (x1 ... xn) "ipat"` : combine the above, first
specializing `pm_trm`, then eliminating existential quantifiers (and pure
- conjuncts) with `x1 ... xn`, and finally destructing the resulting term
+ conjuncts) with `x1 ... xn`, and finally destructing the resulting term
using the [introduction pattern][ipat] `ipat`.
+ `iDestruct pm_trm as %cpat` : destruct the pure conclusion of a term
`pr_trm` using the Coq introduction pattern `cpat`. When using this tactic,
@@ -185,10 +185,10 @@ Separation logic-specific tactics
of spatial context that matches pattern `pat`.
- `iCombine "H1 H2" as "ipat"` : combine `H1 : P1` and `H2 : P2` into `H: P1 ∗
P2` or something simplified but equivalent, then destruct the combined
- hypthesis using `ipat`. Some examples of simplifications `iCombine` knows
+ hypothesis using `ipat`. Some examples of simplifications `iCombine` knows
about are to combine `own γ x` and `own γ y` into `own γ (x ⋅ y)`, and to
combine `l ↦{1/2} v` and `l ↦{1/2} v` into `l ↦ v`.
-- `iAccu` : solves a goal that is an evar by instantiating it with all
+- `iAccu` : solve a goal that is an evar by instantiating it with all
hypotheses from the spatial context joined together with a separating
conjunction (or `emp` in case the spatial context is empty). Not commonly
used, but can be extremely useful when combined with automation.
@@ -248,7 +248,7 @@ Rewriting / simplification
equality in the proof mode goal / hypothesis `H`.
- `iRewrite -pm_trm` / `iRewrite -pm_trm in "H"` : rewrite in reverse direction
using an internal equality in the proof mode goal / hypothesis `H`.
-- `iEval (tac)` / `iEval (tac) in "selpat"` : performs a tactic `tac`
+- `iEval (tac)` / `iEval (tac) in "selpat"` : perform a tactic `tac`
on the proof mode goal / hypotheses given by the selection pattern
`selpat`. Using `%` as part of the selection pattern is unsupported.
The tactic `tac` should be a reduction or rewriting tactic like
@@ -258,7 +258,7 @@ Rewriting / simplification
running `tac`, `?evar` is unified with the resulting `P`, which in
turn becomes the new proof mode goal / a hypothesis given by
`selpat`. Note that parentheses around `tac` are needed.
-- `iSimpl` / `iSimpl in "selpat"` : performs `simpl` on the proof mode
+- `iSimpl` / `iSimpl in "selpat"` : perform `simpl` on the proof mode
goal / hypotheses given by the selection pattern `selpat`. This is a
shorthand for `iEval (simpl)`.
@@ -315,7 +315,7 @@ Introduction patterns (`ipat`)
==============================
Introduction patterns are used to perform introductions and eliminations of
-multiple connectives on the fly. The proof mode supports the following
+multiple connectives on the fly. The proof mode supports the following
_introduction patterns_:
- `H` : create a hypothesis named `H`.
@@ -356,7 +356,7 @@ _introduction patterns_:
is a no-op. If the hypothesis is not affine, an `` modality is added
to the hypothesis.
- `> ipat` : eliminate a modality (if the goal permits); commonly used to strip
- a later from the hypotheses when it is timeless and the goal is either a `WP`
+ a later from the hypothesis when it is timeless and the goal is either a `WP`
or an update modality `|={E}=>`.
Apart from this, there are the following introduction patterns that can only
@@ -435,7 +435,7 @@ _specialization patterns_ to express splitting of hypotheses:
which causes `done` to be called to close the goal.
- `[$]` : solve the premise by framing. It will first repeatedly frame and
consume the spatial hypotheses, and then repeatedly frame the intuitionistic
- hypotheses. Spatial hypothesis that are not framed are carried over to the
+ hypotheses. Spatial hypotheses that are not framed are carried over to the
subsequent goal.
- `[> $]` : like the above pattern, but this pattern can only be used if the
goal is a modality `M`, in which case the goal for the premise will be wrapped
--
GitLab
From 6434d5ff91e415997c5f26c315d5e41977f68164 Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita
Date: Wed, 3 Mar 2021 08:49:10 +0000
Subject: [PATCH 2/3] fix typos in editor.md
---
docs/editor.md | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/docs/editor.md b/docs/editor.md
index 8658cbc2b..d97f12ce2 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -364,7 +364,7 @@ Here is a `coqide.bindings` file for a variety of symbols used in Iris:
### VSCoq setup
The recommended extension as of December 2019 is [Maxime Dénès's
-VScoq](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq).
+VSCoq](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq).
Press `Ctrl Shift P` or `Cmd Shift P` and then type "coq" to see the list of Coq
commands and keyboard shortcuts.
@@ -381,8 +381,8 @@ ligatures.
Install the [Generic input method
extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-input-method).
To insert a symbol, type the code for a symbol such as `\to` and then press
-`Space` or `Tab`. To enable Iris unicode input support, open your user settings,
-press `Cmd ,` or `Ctrl ,`, and type "generic-input-methods.input-methods", then
+`Space` or `Tab`. To enable the Iris unicode input support, open your user settings,
+press `Cmd ,` or `Ctrl ,`, type "generic-input-methods.input-methods", and then
click on "Edit in settings.json" and add the following:
```
--
GitLab
From ed82db1381df2702436b0e25989e78c906979bbf Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita
Date: Wed, 3 Mar 2021 13:29:20 +0000
Subject: [PATCH 3/3] fix editor.md
---
docs/editor.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/editor.md b/docs/editor.md
index d97f12ce2..e2a052efc 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -381,7 +381,7 @@ ligatures.
Install the [Generic input method
extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-input-method).
To insert a symbol, type the code for a symbol such as `\to` and then press
-`Space` or `Tab`. To enable the Iris unicode input support, open your user settings,
+`Space` or `Tab`. To enable Iris unicode input support, open your user settings,
press `Cmd ,` or `Ctrl ,`, type "generic-input-methods.input-methods", and then
click on "Edit in settings.json" and add the following:
--
GitLab