Commit 07d25e67 by Yusuke Matsushita Committed by Robbert Krebbers

### Fix typos

parent 94152ebc
 ... ... @@ -51,7 +51,7 @@ To obtain a development version, also add the Iris opam repository: opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git Either way, you can now do opam install coq-iris. To fetch updates later, run opam update && opam upgrade. However, notice that we do not guarnatee opam update && opam upgrade. However, notice that we do not guarantee backwards-compatibility, so upgrading Iris may break your Iris-using developments. ... ... @@ -87,7 +87,7 @@ followed by make build-dep. the primitive connectives. It also contains derived constructions that are entirely independent of the choice of resources. * The subfolder [lib](theories/base_logic/lib) contains some generally useful derived constructions. Most importantly, it defines composeable derived constructions. Most importantly, it defines composable dynamic resources and ownership of them; the other constructions depend on this setup. * The folder [program_logic](theories/program_logic) specializes the base logic ... ...
 ... ... @@ -114,7 +114,7 @@ all of the redexes reduced.) ## Notation and lemmas for derived notions involving a thunk Sometimes, it is useful to define a derived notion in HeapLang that involves thunks. For example, the parallel composition e1 ||| e2 is defineable in thunks. For example, the parallel composition e1 ||| e2 is definable in HeapLang, but that requires thunking e1 and e2 before passing them to par. (This is defined in [par.v](theories/heap_lang/lib/par.v).) However, this is somewhat subtle because of the distinction between expression lambdas ... ...
 ... ... @@ -120,7 +120,7 @@ Separation logic-specific tactics This tactic solves the goal if everything in the conclusion has been framed. - iCombine "H1" "H2" as "pat" : combines H1 : P1 and H2 : P2 into H: P1 ∗ P2, then calls iDestruct H as pat on the combined hypothesis. - iAccu : solves a goal that is an evar by instantiating it with a all - iAccu : solves 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). ... ...
 ... ... @@ -7,7 +7,7 @@ This is what we do for option $\maybe\cofe$, product $(M_i)_{i \in I}$ (with $I$ \subsection{Next (Type-Level Later)} Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type): Given an OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type): \begin{align*} \latert\cofe \eqdef{}& \latertinj(x:\cofe) \\ \latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y ... ...
 ... ... @@ -78,7 +78,7 @@ As already mentioned, the persistence modality is an always-style modality: {}{\always\always\prop \provesIff \always\prop} \end{mathpar} Some further interesting derived rules include: \begin{mathparpagebreakable} \begin{mathparpagebreakable} \infer{} {\always(\prop\land\propB) \provesIff \always\prop \land \always\propB} ... ... @@ -300,8 +300,8 @@ The following rules identify the class of timeless propositions: \end{mathparpagebreakable} \subsection{Dynamic Composeable Higher-Order Resources} \label{sec:composeable-resources} \subsection{Dynamic Composable Higher-Order Resources} \label{sec:composable-resources} The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources. It turns out that we can generalize this further and permit picking cameras $\iFunc(\Prop)$'' that depend on the structure of propositions themselves. ... ... @@ -348,7 +348,7 @@ Effectively, we just defined a way to instantiate the base logic with $\Res$ as We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical propositions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic. \paragraph{Proof composability.} To make our proofs composeable, we \emph{generalize} our proofs over the family of functors. To make our proofs composable, we \emph{generalize} our proofs over the family of functors. This is possible because we made $\Res$ a \emph{product} of all the cameras picked by the user, and because we can actually work with that product pointwise''. So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}. Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors. ... ...
 ... ... @@ -4,7 +4,7 @@ This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the base logic. So in the following, we assume that some language $\Lang$ was fixed. Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composeable-resources}. Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composable-resources}. \subsection{World Satisfaction, Invariants, Fancy Updates} ... ... @@ -398,7 +398,7 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$ The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name). They, too, are lists of $\nat$, the same type as namespaces. In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\InvName$, the type of plain'' invariant names. In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structured invariant names to $\InvName$, the type of plain'' invariant names. Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\InvName$ is infinite. Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: $\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}$ ... ...
 ... ... @@ -81,7 +81,7 @@ Tactic Notation "iStartProof" uconstr(PROP) := lazymatch goal with | |- @envs_entails ?PROP' _ _ => (* This cannot be shared with the other [iStartProof], because type_term has a non-negligeable performance impact. *) type_term has a non-negligible performance impact. *) let x := type_term (eq_refl : @eq Type PROP PROP') in idtac (* We eta-expand [as_emp_valid_2], in order to make sure that ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 2, "mathjax_display_tex": 0, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.9968079924583435, "perplexity": 3401.7802771201013}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2022-21/segments/1652662675072.99/warc/CC-MAIN-20220527174336-20220527204336-00238.warc.gz"}