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_constrs, 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