Commit 662d20dc authored by Ralf Jung's avatar Ralf Jung

add bidirectional turnstile

parent 3cf0a5fc
Pipeline #289 passed with stage
...@@ -8,13 +8,13 @@ We collect here some important and frequently used derived proof rules. ...@@ -8,13 +8,13 @@ We collect here some important and frequently used derived proof rules.
{\prop \Ra \propB \proves \prop \wand \propB} {\prop \Ra \propB \proves \prop \wand \propB}
\infer{} \infer{}
{\prop * \Exists\var.\propB \Lra \Exists\var. \prop * \propB} {\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB}
\infer{} \infer{}
{\prop * \Exists\var.\propB \proves \Exists\var. \prop * \propB} {\prop * \Exists\var.\propB \proves \Exists\var. \prop * \propB}
\infer{} \infer{}
{\always(\prop*\propB) \Lra \always\prop * \always\propB} {\always(\prop*\propB) \provesIff \always\prop * \always\propB}
\infer{} \infer{}
{\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB} {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB}
...@@ -23,7 +23,7 @@ We collect here some important and frequently used derived proof rules. ...@@ -23,7 +23,7 @@ We collect here some important and frequently used derived proof rules.
{\always(\prop \wand \propB) \proves \always\prop \wand \always\propB} {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB}
\infer{} \infer{}
{\always(\prop \wand \propB) \Lra \always(\prop \Ra \propB)} {\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}
\infer{} \infer{}
{\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB} {\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB}
......
...@@ -184,6 +184,7 @@ ...@@ -184,6 +184,7 @@
\def\Lam #1.{\lambda #1.\spac}% \def\Lam #1.{\lambda #1.\spac}%
\newcommand{\proves}{\vdash} \newcommand{\proves}{\vdash}
\newcommand{\provesIff}{\mathrel{\dashv\vdash}}
\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;} \newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;}
......
...@@ -303,8 +303,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $ ...@@ -303,8 +303,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold. The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold.
We implicitly assume that an arbitrary variable context, $\vctx$, is added to every constituent of the rules. We implicitly assume that an arbitrary variable context, $\vctx$, is added to every constituent of the rules.
Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent. Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \Ra \propB$ with no assumptions. Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ can be derived.
(Bi-implications are analogous.)
\judgment{}{\vctx \mid \pfctx \proves \prop} \judgment{}{\vctx \mid \pfctx \proves \prop}
\paragraph{Laws of intuitionistic higher-order logic with equality.} \paragraph{Laws of intuitionistic higher-order logic with equality.}
...@@ -395,9 +394,9 @@ This is entirely standard. ...@@ -395,9 +394,9 @@ This is entirely standard.
\paragraph{Laws of (affine) bunched implications.} \paragraph{Laws of (affine) bunched implications.}
\begin{mathpar} \begin{mathpar}
\begin{array}{rMcMl} \begin{array}{rMcMl}
\TRUE * \prop &\Lra& \prop \\ \TRUE * \prop &\provesIff& \prop \\
\prop * \propB &\Lra& \propB * \prop \\ \prop * \propB &\provesIff& \propB * \prop \\
(\prop * \propB) * \propC &\Lra& \prop * (\propB * \propC) (\prop * \propB) * \propC &\provesIff& \prop * (\propB * \propC)
\end{array} \end{array}
\and \and
\infer[$*$-mono] \infer[$*$-mono]
...@@ -413,14 +412,14 @@ This is entirely standard. ...@@ -413,14 +412,14 @@ This is entirely standard.
\paragraph{Laws for ghosts and physical resources.} \paragraph{Laws for ghosts and physical resources.}
\begin{mathpar} \begin{mathpar}
\begin{array}{rMcMl} \begin{array}{rMcMl}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra& \ownGGhost{\melt \mtimes \meltB} \\ \ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff& \ownGGhost{\melt \mtimes \meltB} \\
\ownGGhost{\melt} &\Ra& \melt \in \mval \\ \ownGGhost{\melt} &\provesIff& \melt \in \mval \\
\TRUE &\Ra& \ownGGhost{\munit} \TRUE &\proves& \ownGGhost{\munit}
\end{array} \end{array}
\and \and
\and \and
\begin{array}{c} \begin{array}{c}
\ownPhys{\state} * \ownPhys{\state'} \Ra \FALSE \ownPhys{\state} * \ownPhys{\state'} \proves \FALSE
\end{array} \end{array}
\end{mathpar} \end{mathpar}
...@@ -439,14 +438,14 @@ This is entirely standard. ...@@ -439,14 +438,14 @@ This is entirely standard.
{\later{\Exists x:\type.\prop} \proves \Exists x:\type. \later\prop} {\later{\Exists x:\type.\prop} \proves \Exists x:\type. \later\prop}
\\\\ \\\\
\begin{array}[c]{rMcMl} \begin{array}[c]{rMcMl}
\later{(\prop \wedge \propB)} &\Lra& \later{\prop} \wedge \later{\propB} \\ \later{(\prop \wedge \propB)} &\provesIff& \later{\prop} \wedge \later{\propB} \\
\later{(\prop \vee \propB)} &\Lra& \later{\prop} \vee \later{\propB} \\ \later{(\prop \vee \propB)} &\provesIff& \later{\prop} \vee \later{\propB} \\
\end{array} \end{array}
\and \and
\begin{array}[c]{rMcMl} \begin{array}[c]{rMcMl}
\later{\All x.\prop} &\Lra& \All x. \later\prop \\ \later{\All x.\prop} &\provesIff& \All x. \later\prop \\
\Exists x. \later\prop &\Ra& \later{\Exists x.\prop} \\ \Exists x. \later\prop &\proves& \later{\Exists x.\prop} \\
\later{(\prop * \propB)} &\Lra& \later\prop * \later\propB \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB
\end{array} \end{array}
\end{mathpar} \end{mathpar}
...@@ -487,26 +486,26 @@ This is entirely standard. ...@@ -487,26 +486,26 @@ This is entirely standard.
{\always{\pfctx} \proves \always{\prop}} {\always{\pfctx} \proves \always{\prop}}
\and \and
\infer[$\always$E]{} \infer[$\always$E]{}
{\always{\prop} \Ra \prop} {\always{\prop} \proves \prop}
\and \and
\begin{array}[c]{rMcMl} \begin{array}[c]{rMcMl}
\always{(\prop * \propB)} &\Ra& \always{(\prop \land \propB)} \\ \always{(\prop * \propB)} &\proves& \always{(\prop \land \propB)} \\
\always{\prop} * \propB &\Ra& \always{\prop} \land \propB \\ \always{\prop} * \propB &\proves& \always{\prop} \land \propB \\
\always{\later\prop} &\Lra& \later\always{\prop} \\ \always{\later\prop} &\provesIff& \later\always{\prop} \\
\end{array} \end{array}
\and \and
\begin{array}[c]{rMcMl} \begin{array}[c]{rMcMl}
\always{(\prop \land \propB)} &\Lra& \always{\prop} \land \always{\propB} \\ \always{(\prop \land \propB)} &\provesIff& \always{\prop} \land \always{\propB} \\
\always{(\prop \lor \propB)} &\Lra& \always{\prop} \lor \always{\propB} \\ \always{(\prop \lor \propB)} &\provesIff& \always{\prop} \lor \always{\propB} \\
\always{\All x. \prop} &\Lra& \All x. \always{\prop} \\ \always{\All x. \prop} &\provesIff& \All x. \always{\prop} \\
\always{\Exists x. \prop} &\Lra& \Exists x. \always{\prop} \\ \always{\Exists x. \prop} &\provesIff& \Exists x. \always{\prop} \\
\end{array} \end{array}
\and \and
{ \term =_\type \term' \Ra \always \term =_\type \term'} { \term =_\type \term' \proves \always \term =_\type \term'}
\and \and
{ \knowInv\iname\prop \Ra \always \knowInv\iname\prop} { \knowInv\iname\prop \proves \always \knowInv\iname\prop}
\and \and
{ \ownGGhost{\mcore\melt} \Ra \always \ownGGhost{\mcore\melt}} { \ownGGhost{\mcore\melt} \proves \always \ownGGhost{\mcore\melt}}
\end{mathpar} \end{mathpar}
\paragraph{Laws of primitive view shifts.} \paragraph{Laws of primitive view shifts.}
......
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