Commit 07d25e67 authored by Yusuke Matsushita's avatar Yusuke Matsushita Committed by Robbert

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!
Please register or to comment