From 511f26a4808a0411a575b579383a85b04a938274 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sun, 31 Jan 2016 12:26:16 +0100
Subject: [PATCH] Add Dave's proof macros
---
docs/iris/locallabel.sty | 1 +
docs/iris/model.tex | 72 +++++-----
docs/iris/pfsteps.sty | 1 -
docs/iris/pftools.sty | 1 +
docs/locallabel.sty | 118 +++++++++++++++++
docs/pfsteps.sty | 279 ---------------------------------------
docs/pftools.sty | 130 ++++++++++++++++++
docs/setup.tex | 56 +-------
8 files changed, 289 insertions(+), 369 deletions(-)
create mode 120000 docs/iris/locallabel.sty
delete mode 120000 docs/iris/pfsteps.sty
create mode 120000 docs/iris/pftools.sty
create mode 100644 docs/locallabel.sty
delete mode 100644 docs/pfsteps.sty
create mode 100644 docs/pftools.sty
diff --git a/docs/iris/locallabel.sty b/docs/iris/locallabel.sty
new file mode 120000
index 000000000..b5cf84403
--- /dev/null
+++ b/docs/iris/locallabel.sty
@@ -0,0 +1 @@
+../locallabel.sty
\ No newline at end of file
diff --git a/docs/iris/model.tex b/docs/iris/model.tex
index df9905588..dd419358c 100644
--- a/docs/iris/model.tex
+++ b/docs/iris/model.tex
@@ -82,7 +82,7 @@ action on morphisms).
\begin{array}[t]{rcl}
% \protStatus &::=& \enabled \ALT \disabled \\[0.4em]
\textdom{Res} &\eqdef&
-\{\, \res = (\pres, \ghostRes) \mid
+\{\, \rs = (\pres, \ghostRes) \mid
\pres \in \textdom{State} \uplus \{\munit\} \land \ghostRes \in \mcarp{\monoid} \,\} \\[0.5em]
(\pres, \ghostRes) \rsplit
(\pres', \ghostRes') &\eqdef&
@@ -92,17 +92,17 @@ action on morphisms).
\end{cases}
\\[0.5em]
%
-\res \leq \res' & \eqdef &
-\Exists \res''. \res' = \res \rsplit \res''\\[1em]
+\rs \leq \rs' & \eqdef &
+\Exists \rs''. \rs' = \rs \rsplit \rs''\\[1em]
%
\UPred(\textdom{Res}) &\eqdef&
\{\, p \subseteq \mathbb{N} \times \textdom{Res} \mid
-\All (k,\res) \in p.
+\All (k,\rs) \in p.
\All j\leq k.
-\All \res' \geq \res.
-(j,\res')\in p \,\}\\[0.5em]
+\All \rs' \geq \rs.
+(j,\rs')\in p \,\}\\[0.5em]
\restr{p}{k} &\eqdef&
-\{\, (j, \res) \in p \mid j < k \,\}\\[0.5em]
+\{\, (j, \rs) \in p \mid j < k \,\}\\[0.5em]
p \nequiv{n} q & \eqdef & \restr{p}{n} = \restr{q}{n}\\[1em]
%
\textdom{PreProp} & \cong &
@@ -187,7 +187,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
%\typedsection{Validity}{valid : \pset{\textdom{Prop}} \in Sets}
%
%\begin{align*}
-%valid(p) &\iff \All n \in \mathbb{N}. \All \res \in \textdom{Res}. \All W \in \textdom{World}. (n, \res) \in p(W)
+%valid(p) &\iff \All n \in \mathbb{N}. \All \rs \in \textdom{Res}. \All W \in \textdom{World}. (n, \rs) \in p(W)
%\end{align*}
\typedsection{Later modality}{\later : \textdom{Prop} \to \textdom{Prop} \in {\cal U}}
@@ -213,7 +213,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
%\begin{align*}
%&\forall p, q \in \textdom{Prop}.~\\
%&\qquad
-% (\forall n \in \mathbb{N}.~\forall \res \in \textdom{Res}.~\forall W \in \textdom{World}.~(n, \res) \in p(W) \Rightarrow (n, \res) \in q(W)) \Leftrightarrow~valid(\always{(p \Rightarrow q)})
+% (\forall n \in \mathbb{N}.~\forall \rs \in \textdom{Res}.~\forall W \in \textdom{World}.~(n, \rs) \in p(W) \Rightarrow (n, \rs) \in q(W)) \Leftrightarrow~valid(\always{(p \Rightarrow q)})
%\end{align*}
%\end{lem}
@@ -232,11 +232,11 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\textdom{World} \to \psetdown{\mathbb{N}} \in {\cal U}}
\ralf{Make this Dave-compatible: Explicitly compose all the things in $s$}
\begin{align*}
- \fullSat{\state}{\mask}{\res}{W} &=
+ \fullSat{\state}{\mask}{\rs}{W} &=
\begin{aligned}[t]
- \{\, n + 1 \in \mathbb{N} \mid &\Exists \resB:\mathbb{N} \fpfn \textdom{Res}. (\res \rsplit \resB).\pres = \state \land{}\\
- &\quad \All \iota \in \dom(W). \iota \in \dom(W) \leftrightarrow \iota \in \dom(\resB) \land {}\\
- &\quad\quad \iota \in \mask \ra (n, \resB(\iota)) \in \wIso^{-1}(W(\iota))(W) \,\} \cup \{ 0 \}
+ \{\, n + 1 \in \mathbb{N} \mid &\Exists \rsB:\mathbb{N} \fpfn \textdom{Res}. (\rs \rsplit \rsB).\pres = \state \land{}\\
+ &\quad \All \iota \in \dom(W). \iota \in \dom(W) \leftrightarrow \iota \in \dom(\rsB) \land {}\\
+ &\quad\quad \iota \in \mask \ra (n, \rsB(\iota)) \in \wIso^{-1}(W(\iota))(W) \,\} \cup \{ 0 \}
\end{aligned}
\end{align*}
\begin{lem}\label{lem:fullsat-nonexpansive}
@@ -248,9 +248,9 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\MoveEqLeft
\All \state \in \Delta(\textdom{State}).
\All \mask_1, \mask_2 \in \Delta(\pset{\mathbb{N}}).
- \All \res, \resB \in \Delta(\textdom{Res}).
+ \All \rs, \rsB \in \Delta(\textdom{Res}).
\All W \in \textdom{World}. \\&
- \mask_1 \subseteq \mask_2 \implies (\fullSat{\state}{\mask_2}{\res}{W}) \subseteq (\fullSat{\state}{\mask_1}{\res}{W})
+ \mask_1 \subseteq \mask_2 \implies (\fullSat{\state}{\mask_2}{\rs}{W}) \subseteq (\fullSat{\state}{\mask_1}{\rs}{W})
\end{align*}
\end{lem}
@@ -293,11 +293,11 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\begin{align*}
\mathit{vs}_{\mask_1}^{\mask_2}(q) &= \Lam W.
\begin{aligned}[t]
- \{\, (n, \res) &\mid \All W_F \geq W. \All \res_F, \mask_F, \state. \All k \leq n.\\
+ \{\, (n, \rs) &\mid \All W_F \geq W. \All \rs_F, \mask_F, \state. \All k \leq n.\\
&\qquad
- k \in (\fullSat{\state}{\mask_1 \cup \mask_F}{\res \rsplit \res_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\
+ k \in (\fullSat{\state}{\mask_1 \cup \mask_F}{\rs \rsplit \rs_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\
&\qquad
- \Exists W' \geq W_F. \Exists \res'. k \in (\fullSat{\state}{\mask_2 \cup \mask_F}{\res' \rsplit \res_F}{W'}) \land (k, \res') \in q(W')
+ \Exists W' \geq W_F. \Exists \rs'. k \in (\fullSat{\state}{\mask_2 \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k, \rs') \in q(W')
\,\}
\end{aligned}
\end{align*}
@@ -338,10 +338,10 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
% \All \iota \in \mathbb{N}.
% \All p \in \textdom{Prop}.
% \All W \in \textdom{World}.
-% \All \res \in \textdom{Res}.
+% \All \rs \in \textdom{Res}.
% \All n \in \mathbb{N}. \\
%&
-% (n, \res) \in inv(\iota, p)(W) \implies (n, \res) \in vs_{\{ \iota \}}^{\emptyset}(\later p)(W)
+% (n, \rs) \in inv(\iota, p)(W) \implies (n, \rs) \in vs_{\{ \iota \}}^{\emptyset}(\later p)(W)
%\end{align*}
%\end{lem}
@@ -352,10 +352,10 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
% \forall \iota \in \mathbb{N}.~
% \forall p \in \textdom{Prop}.~
% \forall W \in \textdom{World}.~
-% \forall \res \in \textdom{Res}.~
+% \forall \rs \in \textdom{Res}.~
% \forall n \in \mathbb{N}.~\\
%&\qquad
-% (n, \res) \in (inv(\iota, p) * \later p)(W) \Rightarrow (n, \res) \in vs^{\{ \iota \}}_{\emptyset}(\top)(W)
+% (n, \rs) \in (inv(\iota, p) * \later p)(W) \Rightarrow (n, \rs) \in vs^{\{ \iota \}}_{\emptyset}(\top)(W)
%\end{align*}
%\end{lem}
@@ -392,22 +392,22 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\begin{align*}
\mathit{wp}_\mask(\expr, q) &\eqdef \Lam W.
\begin{aligned}[t]
- \{\, (n, \res) &\mid \All W_F \geq W; k \leq n; \res_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\fullSat{\state}{\mask \cup \mask_F}{\res \rsplit \res_F}{W_F}) \implies{}\\
+ \{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs \rsplit \rs_F}{W_F}) \implies{}\\
&\qquad
- (\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \res'. \\
+ (\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \rs'. \\
&\qquad\qquad
- k \in (\fullSat{\state}{\mask \cup \mask_F}{\res' \rsplit \res_F}{W'}) \land (k, \res') \in q(\expr)(W'))~\land \\
+ k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\
&\qquad
- (\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \res'. \\
+ (\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \rs'. \\
&\qquad\qquad
- k - 1 \in (\fullSat{\state'}{\mask \cup \mask_F}{\res' \rsplit \res_F}{W'}) \land (k-1, \res') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
+ k - 1 \in (\fullSat{\state'}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
&\qquad
- (\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \res', \res_1', \res_2'. \\
+ (\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \rs', \rs_1', \rs_2'. \\
&\qquad\qquad
- k - 1 \in (\fullSat{\state}{\mask \cup \mask_F}{\res' \rsplit \res_F}{W'}) \land \res' = \res_1' \rsplit \res_2'~\land \\
+ k - 1 \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land \rs' = \rs_1' \rsplit \rs_2'~\land \\
&\qquad\qquad
- (k-1, \res_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land
- (k-1, \res_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W'))
+ (k-1, \rs_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land
+ (k-1, \rs_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W'))
\,\}
\end{aligned}
\end{align*}
@@ -491,9 +491,9 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\semTerm{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &=
inv(\semTerm{\vctx \proves \iname : \textsort{InvName}}_\gamma, \semTerm{\vctx \proves \prop : \Prop}_\gamma) \\
\semTerm{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &=
- \Lam W. \{\, (n, \res) \mid \res.\ghostRes \geq \semTerm{\vctx \proves \melt : \textsort{Monoid}}_\gamma \,\} \\
+ \Lam W. \{\, (n, \rs) \mid \rs.\ghostRes \geq \semTerm{\vctx \proves \melt : \textsort{Monoid}}_\gamma \,\} \\
\semTerm{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &=
- \Lam W. \{\, (n, \res) \mid \res.\pres = \semTerm{\vctx \proves \state : \textsort{State}}_\gamma \,\}
+ \Lam W. \{\, (n, \rs) \mid \rs.\pres = \semTerm{\vctx \proves \state : \textsort{State}}_\gamma \,\}
\end{align*}
%
\begin{align*}
@@ -513,10 +513,10 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\MoveEqLeft
\forall n \in \mathbb{N}.\;
\forall W \in \textdom{World}.\;
-\forall \res \in \textdom{Res}.\;
+\forall \rs \in \textdom{Res}.\;
\forall \gamma \in \semSort{\vctx},\;
\\&
-\bigl(\All \propB \in \pfctx. (n, \res) \in \semTerm{\vctx \proves \propB : \Prop}_\gamma(W)\bigr)
-\implies (n, \res) \in \semTerm{\vctx \proves \prop : \Prop}_\gamma(W)
+\bigl(\All \propB \in \pfctx. (n, \rs) \in \semTerm{\vctx \proves \propB : \Prop}_\gamma(W)\bigr)
+\implies (n, \rs) \in \semTerm{\vctx \proves \prop : \Prop}_\gamma(W)
\end{aligned}
\]
diff --git a/docs/iris/pfsteps.sty b/docs/iris/pfsteps.sty
deleted file mode 120000
index 958ef7a14..000000000
--- a/docs/iris/pfsteps.sty
+++ /dev/null
@@ -1 +0,0 @@
-../pfsteps.sty
\ No newline at end of file
diff --git a/docs/iris/pftools.sty b/docs/iris/pftools.sty
new file mode 120000
index 000000000..68af43890
--- /dev/null
+++ b/docs/iris/pftools.sty
@@ -0,0 +1 @@
+../pftools.sty
\ No newline at end of file
diff --git a/docs/locallabel.sty b/docs/locallabel.sty
new file mode 100644
index 000000000..6c28e92e6
--- /dev/null
+++ b/docs/locallabel.sty
@@ -0,0 +1,118 @@
+% Locallabel
+%
+% Copyright (C) 2001, 2002, 2003 Didier Rémy
+%
+% Author : Didier Remy
+% Version : 1.1.1
+% Bug Reports : to author
+% Web Site : http://pauillac.inria.fr/~remy/latex/
+%
+% Locallabel is free software; you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either version 2, or (at your option)
+% any later version.
+%
+% Locallabel is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details
+% (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File locallabel.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%
+
+%% Identification
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{locallabel}
+ [2001/23/02 v0.92 Locallabel]
+
+%% Preliminary declarations
+
+%% Options
+
+%% More declarations
+
+%% We use two counters: The global counter is incremented at each reset.
+%% Its value is the ``group'' of a local.
+%% The local counter is the last numeric value of a bound label in the
+%% current group. The value of a label #1 is globally set to
+%% \csname llb@\the\c@llb@global-#1\endcsname
+%% The global command \csname llb@\the\c@llb@global-#1*\endcsname is
+%% use to ensure that a label is only bound once. Usually a label is
+%% bound and declared at the same time with \llabel. It may also be bound in
+%% advance, with \lbind, for instance so as to control the numbering.
+%% Then, another \llabel must be used to declare it in the text.
+%% If no \lbind has been used before, the \llabel calls \lbind implicitlt.
+
+\newcounter{llb@global}
+\newcounter{llb@local}
+
+\newcommand \llb@find [1]
+ {\expandafter \ifx \csname llb@\the\c@llb@global-#1\endcsname \relax
+ \message {*** Local label #1 undefined in this context}%
+ \edef \llb@current {#1??}%
+ \else
+ \edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname}%
+ \fi}
+
+\newcommand \llb@make [1]
+ {\expandafter \ifx \csname llb@\the\c@llb@global-#1\endcsname \relax
+ \stepcounter{llb@local}\relax \expandafter
+ \xdef \csname llb@\the\c@llb@global-#1\endcsname {\the\c@llb@local}%
+ \edef \llb@current {\the\c@llb@local}%
+ \else
+ \expandafter \ifx \csname llb@\the\c@llb@global-#1*\endcsname \relax
+ \message {*** Local label #1 already defined in this countext!}%
+ \edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname ??}%
+ \else
+ \expandafter \global \expandafter \let
+ \csname llb@\the\c@llb@global-#1*\endcsname \relax
+ \edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname}
+ \fi
+ \fi
+}
+
+%%% Redefine those macros to change typsetting
+
+\newcommand \thelocallabel {\the \c@llb@local}
+
+\newcommand \LlabelTypeset [1] {(\textrm {\bfseries #1})}
+\newcommand \LrefTypeset [1] {(\textrm {#1)}}
+\newcommand \glabel [1]{\LlabelTypeset{\softtarget {#1}{#1}}}
+\newcommand \gref [1]{\LrefTypeset{\softlink {#1}{#1}}}
+
+%%% To reset all local labels---which just increment a global prefix.
+\newcommand \locallabelreset[1][0]%
+ {\stepcounter {llb@global}\setcounter {llb@local}{#1}}
+
+%%% Make a new local label, typeset it, and bind to the given name
+\def \llb@relax {\relax}
+\newcommand {\llabel}[2][\relax]%
+ {\llb@make{#2}%
+ \def \@test {#1}\ifx \@test\llb@relax\else
+ \edef \@currentlabel {\the\c@llb@local}%
+ \def \@test {#1}\ifx \@test\empty \def \@test{#2}\fi
+ \label{\@test}%
+ \fi%
+ \LlabelTypeset {\softtarget{llb@\the\c@llb@global-#2}{\llb@current}}}
+
+%%% Retreive the local label of given name and type set it.
+\newcommand \lref [1]
+ {\llb@find {#1}%
+ \LrefTypeset {\softlink {llb@\the\c@llb@global-#1}{\llb@current}}}
+
+%%% Make a new local label and bind it to the given name but do not typeset
+%%% it. Typesetting may then be done with \llabel non locally. Useful to
+%%% control the order of numberring.
+\newcommand \lbind [1]
+ {\llb@make {#1}%
+ \expandafter \global \expandafter
+ \let \csname llb@\the\c@llb@global-#1*\endcsname \empty}
+
+\AtBeginDocument {%
+ \@ifundefined{softlink}{\let \softlink \@secondoftwo}{}%
+ \@ifundefined{softtarget}{\let \softtarget \@secondoftwo}{}%
+}
diff --git a/docs/pfsteps.sty b/docs/pfsteps.sty
deleted file mode 100644
index 203ab1543..000000000
--- a/docs/pfsteps.sty
+++ /dev/null
@@ -1,279 +0,0 @@
-%%
-%% This is file `pfsteps.sty',
-%% generated with the docstrip utility.
-%%
-%% The original source files were:
-%%
-%% pfsteps.dtx (with options: `package')
-%%
-%% Copyright (C) 2011 by Jesse A. Tov
-%%
-%% This file may be distributed and/or modified under the conditions of the
-%% LaTeX Project Public License, either version 1.2 of this license or (at
-%% your option) any later version. The latest version of this license is
-%% in:
-%%
-%% http://www.latex-project.org/lppl.txt
-%%
-%% and version 1.2 or later is part of all distributions of LaTeX
-%% version 1999/12/01 or later.
-%%
-\NeedsTeXFormat{LaTeX2e}[1999/12/01]
-\ProvidesPackage{pfsteps}
- [2011/04/04 v0.4 proof tools]
-\RequirePackage{listproc}
-\newcommand*\pfsteps@set[3][]{
- \expandafter\let\csname #1pfsteps@#2\endcsname#3
-}
-\newcommand*\pfsteps@option[2][\iffalse]{
- \pfsteps@set[if]{#2}#1
- \pfsteps@set[if]{#2@set}\iffalse
- \DeclareOption{#2}{
- \pfsteps@set[if]{#2}\iftrue
- \pfsteps@set[if]{#2@set}\iftrue
- }
- \DeclareOption{no#2}{
- \pfsteps@set[if]{#2}\iffalse
- \pfsteps@set[if]{#2@set}\iftrue
- }
-}
-\pfsteps@option[\iftrue]{atsign}
-\pfsteps@option[\iftrue]{hyperref}
-\pfsteps@option[\iftrue]{loadunicode}
-\pfsteps@option[\iftrue]{mathpartir}
-\pfsteps@option{unicode}
-\ProcessOptions
-\ifpfsteps@unicode
- \ifpfsteps@loadunicode
- \RequirePackage{ucs}
- \RequirePackage[utf8x]{inputenc}
- \fi
-\fi
-\ifpfsteps@mathpartir
- \ifpfsteps@mathpartir@set
- \RequirePackage{mathpartir}
- \fi
-\fi
-\ifpfsteps@hyperref
- \ifpfsteps@hyperref@set
- \RequirePackage{hyperref}
- \fi
-\fi
-\newcommand{\pfcounteranchor}[1]{(#1)}
-\newcommand{\pfcounterref}[1]{(#1)}
-\newcounter{pfsteps@pfc@global}
-\newcounter{pfsteps@pfc@local}
-\newcommand{\resetpfcounter}[1][0]
- {\stepcounter{pfsteps@pfc@global}\setcounter{pfsteps@pfc@local}{#1}}
-\newcommand{\thepfcounter}
- {\the\value{pfsteps@pfc@local}}
-\newcommand{\thepfsectioncounter}
- {\the\value{pfsteps@pfc@global}}
-\newcommand{\steppfcounter}[1][\relax]{%
- \addtocounter{pfsteps@pfc@local}{1}%
- \ifx\relax#1\relax\else
- \pflabel{#1}%
- \fi
-}
-\newcommand{\usepfcounter}[1][\relax]{%
- \steppfcounter[#1]%
- \pfsteps@hypertarget{pfc:\thepfsectioncounter:\thepfcounter}{%
- \pfcounteranchor{\thepfcounter}%
- }%
-}
-\newcommand{\pfsteps@pfc@cs}[1]
- {\csname\pfsteps@pfc@{\pfsteps@strip#1 \@empty}\endcsname}
-\newcommand{\pfsteps@pfc@}[1]
- {pfsteps@pfc@\pfsteps@strip#1 \@empty @\thepfsectioncounter}
-\def\pfsteps@strip#1 #2{%
- #1%
- \ifx#2\@empty\else\expandafter\pfsteps@strip\fi
- #2}
-\newcommand{\pflabel}[1]
- {\expandafter\ifx\csname\pfsteps@pfc@{#1}@thisrun\endcsname\relax
- \expandafter\xdef\csname\pfsteps@pfc@{#1}\endcsname
- {\thepfcounter}%
- \expandafter\gdef\csname\pfsteps@pfc@{#1}@thisrun\endcsname
- {}%
- \immediate\write\@auxout{
- \noexpand\pfsteps@def@label
- {#1}{\thepfsectioncounter}{\thepfcounter}
- }%
- \else
- \PackageWarning{pfsteps}
- {Proof step (#1) already defined in this section}%
- \fi}
-\newcommand*{\pfsteps@def@label}[3]{
- \expandafter\gdef
- \csname pfsteps@pfc@#1@#2\endcsname
- {#3}
-}
-\newcommand*{\pfref}[1]
-{{\ListExprTo
- {\Compress[\@apply@group\@firstoftwo]
- {\Sort[\@apply@group\@firstoftwo]
- {\Map
- {%
- {\@ifundefined{\pfsteps@pfc@{##1}}
- {-1}
- {\csname\pfsteps@pfc@{##1}\endcsname}}%
- {\@ifundefined{\pfsteps@pfc@{##1}}
- {\PackageWarning{pfsteps}
- {Proof step (##1) not yet defined in this section}%
- \textbf{?}}
- {\pfsteps@hyperlink
- {pfc:\thepfsectioncounter:\pfsteps@pfc@cs{##1}}
- {\pfsteps@pfc@cs{##1}}}}}
- {\List{#1}}}}}
- \pfsteps@pfref@list
- \let\listitem\pfsteps@pfref@listitem@first
- \def\@single##1{\@secondoftwo##1}%
- \def\@range##1##2{\@secondoftwo##1--\@secondoftwo##2}%
- \pfcounterref{\pfsteps@pfref@list}%
-}}
-\newcommand\pfsteps@pfref@listitem@first[1]{%
- #1\let\listitem\pfsteps@pfref@listitem@rest
-}
-\newcommand\pfsteps@pfref@listitem@rest[1]{%
- , #1\let\listitem\pfsteps@pfref@listitem@rest
-}
-\newcommand\pfsteps@hypertarget[2]{#2}
-\newcommand\pfsteps@hyperlink[2]{#2}
-\ifpfsteps@hyperref
- \AtBeginDocument{
- \ifcsname hypertarget\endcsname
- \let\pfsteps@hypertarget=\hypertarget
- \let\pfsteps@hyperlink=\hyperlink
- \fi
- }
-\fi
-\newlength{\proofleftskip}
-\newlength{\proofrightwidth}
-\setlength{\proofleftskip}{2pc}
-\setlength{\proofrightwidth}{0.3\linewidth}
-\newenvironment{pfsteps}
- {\begin{pfsteps@with}$}
- {\end{pfsteps@with}}
-\newenvironment{pfsteps*}
- {\begin{pfsteps@with}{}}
- {\end{pfsteps@with}}
-\newenvironment{pfsteps@with}[1]
-{
- \leavevmode\begingroup
- \setlength{\parskip}{0pt}%
- \trivlist
- \raggedright
- \setlength{\leftskip}{1.5\proofleftskip}
- \let\pfstepsSavedItem\item
- \let\pfstepsSavedLabel\label
- \let\pfstepsSavedQedhere\qedhere
- \newcommand\AND[1][and]{\mathrel{\mbox{##1}}}
- \newcommand\BY[2][by]
- {\pfsteps@unmath{\penalty-1 \mbox{~}\hfill%
- \begin{minipage}[t]{\proofrightwidth}%
- \raggedright##1 ##2%
- \end{minipage}}}
- \def\pfstepsItem{%
- \pfsteps@stopmath
- \pfstepsSavedItem\mbox{}\kern-1.25\proofleftskip
- \makebox[\proofleftskip]{\hfill\usepfcounter}\kern0.25\proofleftskip
- #1\relax}
- \def\pfstepsQedhere{\pfsteps@unmath{\pfstepsSavedQedhere}}
- \let\item\pfstepsItem
- \let\label\pflabel
- \let\qedhere\pfstepsQedhere
- \ifpfsteps@atsign
- \pfsteps@setup@atsign
- \fi
- \relax
-}
-{
- \pfsteps@stopmath
- \endtrivlist\endgroup
- \noindent\ignorespaces
-}
-\newcommand\pfsteps@stopmath{\ifmmode$\fi}
-\newcommand\pfsteps@unmath[1]{\ifmmode$\relax#1\relax$\else\relax#1\relax\fi}
-{
- \def\atsign{@}
- \catcode`\@=\active\relax
- \expandafter\gdef\csname pfsteps\atsign setup\atsign atsign\endcsname{
- \catcode`\@=\active\relax
- \gdef@##1 {\pflabel{##1}}
- }
-}
-\newcommand\pfstepsmathmode{\def\pfsteps@unicode@arg{$}}
-\newcommand\pfstepstextmode{\def\pfsteps@unicode@arg{\relax}}
-\newcommand\pfstepsSetupUnicode[3]{
- \DeclareUnicodeCharacter{#1}{\pfsteps@unicode@startpfsteps}
- \DeclareUnicodeCharacter{#3}{\pfsteps@unicode@item}
- \def\pfsteps@unicode@startpfsteps
- {\begingroup
- \ifpfsteps@atsign\catcode`\@=\active\relax\fi
- \pfsteps@unicode@startpfsteps@kont}
- \def\pfsteps@unicode@startpfsteps@kont##1#2
- {\begin{pfsteps@with}\pfsteps@unicode@arg\item##1\end{pfsteps@with}%
- \endgroup}
- \def\pfsteps@unicode@item{\item}
- \pfstepsmathmode
-}
-\ifpfsteps@unicode
- \pfstepsSetupUnicode{171}{Âť}{8226} % ÂŤ Âť â˘
-\fi
-\newcommand\byCasesEveryCase{\resetpfcounter}
-\newcommand\byCasesEveryOtherwise{\byCasesEveryCase}
-\providecommand{\byCasesOtherwiseTemplate}{\textbf{Otherwise:}}
-\providecommand{\byCasesCaseTemplate}[1]{\textbf{Case\ \ \fbox{#1}}}
-\providecommand{\byCasesWhereTemplate}{\textbf{where}}
-\newenvironment{byCases}
- {%
- \begingroup
- \let\case\byCases@case
- \let\otherwise\byCases@otherwise
- \ifpfsteps@mathpartir
- \ifcsname inferrule\endcsname\let\icase\byCases@icase\fi
- \fi
- \list{}{\labelwidth\z@ \itemindent-\leftmargin
- \let\makelabel\byCases@label}%
- }
- {%
- \endlist
- \endgroup
- }
-\newcommand*\byCases@label[1]{%
- \hspace\labelsep
- \normalfont~\strut
- \expandafter\ifx#1\relax\relax
- \byCasesOtherwiseTemplate
- \else
- \byCasesCaseTemplate{\normalfont${#1}$}%
- \fi
-}
-\newcommand*\byCases@case[2][\byCasesEveryCase]
- {\item[{\let\AND\byCases@and #2}]\strut#1\pfsteps@reallynopagebreak}
-\newcommand*\byCases@otherwise[1][\byCasesEveryOtherwise]
- {\item[]\strut#1\pfsteps@reallynopagebreak}
-\newcommand\pfsteps@reallynopagebreak{\par\nopagebreak\@nobreaktrue}
-\newcommand\byCases@and[1][and]{\mathrel{\mbox{\textbf{#1}}}}
-\newcommand*\byCases@icase{
- \@ifnextchar* \byCases@icase@star \byCases@icase@nostar
-}
-\def\byCases@icase@nostar{\byCases@icase@i{\inferrule}}
-\def\byCases@icase@star*{\byCases@icase@i{\inferrule*}}
-\newcommand*\byCases@icase@i[1]{
- \@ifnextchar [{\byCases@icase@opts{#1}}{\byCases@icase@noopts{#1}}
-}
-\def\byCases@icase@opts#1[#2]{\byCases@icase@ii{#1[#2]}}
-\def\byCases@icase@noopts#1{\byCases@icase@ii{#1}}
-\newcommand*\byCases@icase@ii[3]{
- \@ifnextchar [
- {\byCases@icase@where{#1}{#2}{#3}}
- {\byCases@icase@nowhere{#1}{#2}{#3}}
-}
-\def\byCases@icase@where#1#2#3[#4]{
- \case{#1{#2}{#3}\AND[\byCasesWhereTemplate]#4}%
-}
-\def\byCases@icase@nowhere#1#2#3{\case{#1{#2}{#3}}}
-\endinput
-%%
-%% End of file `pfsteps.sty'.
diff --git a/docs/pftools.sty b/docs/pftools.sty
new file mode 100644
index 000000000..32a8ab65f
--- /dev/null
+++ b/docs/pftools.sty
@@ -0,0 +1,130 @@
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{pftools}
+
+\RequirePackage{locallabel}
+\RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
+\RequirePackage{xparse}
+\RequirePackage{xcolor}
+\RequirePackage{locallabel}
+
+%% Biimplication inference rules
+% \biimp above below
+% The double lines obtained by the simpler
+% "\mprset{fraction={===}}" overlap the conclusion (e.g., the
+% mask E_M in an atomic triple).
+\newcommand*{\biimp}[2]{%
+ \hbox{%
+ \ooalign{%
+ $\genfrac{}{}{1.6pt}1{#1}{#2}$\cr%
+ $\color{white}\genfrac{}{}{0.8pt}1{\phantom{#1}}{\phantom{#2}}$%
+ }%
+ }%
+}
+\newcommand{\BIIMP}{\mprset{myfraction=\biimp}}
+
+
+%% inferH is infer with hyperlinked names.
+% \savelabel lab text: Arrange for \ref{lab} to print text and to link to the current spot.
+\newcommand*{\savelabel}[2]{%
+ % Think @currentlabel : text ref.
+ \edef\@currentlabel{#2}% Save text
+ \phantomsection% Correct hyper reference link
+ \label{#1}% Print text and store nameâŚtext.
+}
+% \textlabel label text: Print and label text.
+\newcommand*{\textlabel}[2]{{#2}\savelabel{#1}{#2}}
+% \rulenamestyle visible
+\newcommand*{\rulenamestyle}[1]{{\TirNameStyle{#1}}} % From mathpartir.sty.
+% \ruleref [discharged] lab
+\def\optionaldischarge#1{%
+ \if\relax\detokenize{#1}\relax\else\ensuremath{^{#1}}\fi}
+\newcommand*{\ruleref}[2][]{\textmd{\rulenamestyle{\ref{#2}}}\optionaldischarge{#1}}
+\newcommand*{\fakeruleref}[2][]{\rulenamestyle{#2}\optionaldischarge{#1}}
+% \rulename label
+\newcommand*{\rulename}[1]{\rulenamestyle{\textlabel{#1}{#1}}}
+% \inferhref name lab premise conclusion
+\newcommand*{\inferhref}[4]{%
+ \inferrule*[lab=\textlabel{#2}{#1}]{#3}{#4}%
+}
+% \infernH name premise conclusion, if name a valid label.
+\newcommand*{\inferH}[3]{\inferhref{#1}{#1}{#2}{#3}}
+\newcommand*{\axiom}[1]{\infer{}{#1}}
+\newcommand*{\axiomhref}[3]{\inferhref{#1}{#2}{}{#3}}
+\newcommand*{\axiomH}[2]{\inferH{#1}{}{#2}}
+\newcommand*{\inferhrefB}[4]{{\BIIMP\inferhref{#1}{#2}{#3}{#4}}}
+\newcommand*{\inferHB}[3]{{\BIIMP\inferH{#1}{#2}{#3}}}
+\newcommand*{\taghref}[2]{\label{#2}\tag{\rulenamestyle{#1}}}
+\newcommand*{\tagH}[1]{\taghref{#1}{#1}}
+
+% The sanity checks in \lbind and \llabel
+% don't work properly in amsmath environments
+% which perhaps lay out their contents more
+% than once. Use \lbind in such cases.
+% Sigh.
+
+\newcommand*{\tagL}[1]{\lbind{#1}\tag*{\llabel{#1}}}
+
+\newcommand*\ind[1][\quad]{#1\TAB=\TAB+}
+\newcommand*\unind{\TAB-}
+
+\newcommand\IND[1][\quad]{\\*\ind[#1]}
+\newcommand\UNIND{\unind \\}
+
+% Attribution: http://tex.stackexchange.com/questions/119473/tabbing-and-line-wrapping
+\newlength\pf@width
+\newcommand*{\CMT}[1]{%
+ \setlength\pf@width{\linewidth}%
+ \addtolength\pf@width{\@totalleftmargin}%
+ \addtolength\pf@width{-\dimen\@curtab}%
+ \parbox[t]{\pf@width}{\nobelowdisplayskip{#1}\ifhmode\strut\fi}}
+
+\colorlet{rescolor}{rgb:red,0;green,30;blue,55}
+\colorlet{ctxcolor}{black}
+\colorlet{codecolor}{rgb:red,76;green,177;blue,36}
+
+\newcommand*\res[1]{{\color{rescolor}\ensuremath{#1}}}
+%When \left\{ ⌠\right\} looks ugly, remember Dave says you want \bracket.
+\NewDocumentCommand{\RES}{s m O{}}{%
+ $\displaystyle{{\left\{\res{%
+ \IfBooleanTF{#1}{\begin{inbox}[l]#2\end{inbox}}{#2}%
+ }\right\}}_{#3}}$}
+
+\NewDocumentCommand{\ARES}{m O{}}{%
+ ${\displaystyle{\bracket\langle\rangle{\color{rescolor}{#1}}}_{#2}}$}
+
+\newcommand*{\CODE}[1]{%
+ ${\displaystyle{\color{codecolor}#1}}$}
+
+\newcommand*{\VARS}[1]{%
+ Vars: ${\color{ctxcolor}\displaystyle{#1}}$}
+\newcommand*{\CTX}[1]{%
+ Context: ${\color{ctxcolor}\displaystyle{#1}}$}
+
+\newcommand*{\GOAL}[1]{%
+ Goal: ${\displaystyle{#1}}$}
+\newcommand*{\SUFF}[1]{%
+ Suff: ${\displaystyle{#1}}$}
+
+\newcommand*{\PFHAVE}[1]{%
+ Have: ${\displaystyle{#1}}$}
+
+\let\pf@origqedhere\qedhere
+\def\pf@setup{%
+ % A version of \qedhere that accounts for tabbing.
+ \def\qedhere{\TAB`\pf@origqedhere}%
+}
+
+\newcommand*{\TAGL}[1]{\TAB`\llabel{#1}}
+
+% The starred version lacks leading and trailing vertical space.
+\newenvironment{proofoutline*}
+{\partopsep=\z@skip \topsep=\z@skip% avoid initial space
+ \parskip\z@skip% avoid trailing space
+ \pf@setup\par\begingroup\Tabbing\ignorespaces}
+{\endTabbing\endgroup\unskip\ignorespacesafterend}
+
+\newenvironment{proofoutline}
+{\pf@setup\par\begingroup\Tabbing\ignorespaces}
+{\endTabbing\endgroup\ignorespacesafterend}
+
+\endinput
diff --git a/docs/setup.tex b/docs/setup.tex
index 50500d946..07b3861ab 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -27,56 +27,6 @@
%\setlength{\dashlinegap}{1pt}
%\setlength{\dashlinedash}{3pt}
-% \biimp above below
-% The double lines obtained by the simpler
-% "\mprset{fraction={===}}" overlap the conclusion (e.g., the
-% mask E_M in an atomic triple).
-\newcommand*{\biimp}[2]{%
- \hbox{%
- \ooalign{%
- $\genfrac{}{}{1.6pt}1{#1}{#2}$\cr%
- $\color{white}\genfrac{}{}{.8pt}1{\phantom{#1}}{\phantom{#2}}$%
- }%
- }%
-}
-\newcommand{\BIIMP}{\mprset{myfraction=\biimp}}
-\newcommand{\infern}[3]{\inferrule[#1]{#2}{#3}}
-\newcommand{\infernB}[3]{{\BIIMP\inferrule*[right={#1}]{#2}{#3}}}
-\newcommand{\inferB}[2]{{\BIIMP\infer{#1}{#2}}}
-
-%% inferH is infern with hyperlinks.
-% \savelabel lab text: Arrange for \ref{lab} to print text and to link to the current spot.
-\makeatletter
- \newcommand*{\savelabel}[2]{%
- % Think @currentlabel : text ref.
- \edef\@currentlabel{#2}% Save text
- \phantomsection% Correct hyper reference link
- \label{#1}% Print text and store nameâŚtext.
- }
-\makeatother
-% \textlabel label text: Print and label text.
-\newcommand*{\textlabel}[2]{{#2}\savelabel{#1}{#2}}
-% \rulenamestyle visible
-\newcommand*{\rulenamestyle}[1]{{\TirNameStyle{#1}}} % From mathpartir.sty.
-% \ruleref [discharged] lab
-\def\optionaldischarge#1{%
- \if\relax\detokenize{#1}\relax\else\ensuremath{^{#1}}\fi}
-\newcommand*{\ruleref}[2][]{\rulenamestyle{\ref{#2}}\optionaldischarge{#1}}
-\newcommand*{\fakeruleref}[2][]{\rulenamestyle{#2}\optionaldischarge{#1}}
-% \rulename label
-\newcommand*{\rulename}[1]{\rulenamestyle{\textlabel{#1}{#1}}}
-% \inferhref name lab premise conclusion
-\newcommand*{\inferhref}[4]{%
- \inferrule*[lab=\textlabel{#2}{#1}]{#3}{#4}%
-}
-% \infernH name premise conclusion, if name a valid label.
-\newcommand*{\inferH}[3]{\inferhref{#1}{#1}{#2}{#3}}
-\newcommand*{\axiom}[1]{\infer{}{#1}}
-\newcommand*{\axiomhref}[3]{\inferhref{#1}{#2}{}{#3}}
-\newcommand*{\axiomH}[2]{\inferH{#1}{}{#2}}
-\newcommand*{\inferhrefB}[4]{{\BIIMP\inferhref{#1}{#2}{#3}{#4}}}
-\newcommand*{\inferHB}[3]{{\BIIMP\inferH{#1}{#2}{#3}}}
-
\usepackage{hyperref}
\hypersetup{%
linktocpage=true, pdfstartview=FitV,
@@ -97,7 +47,7 @@
\newcommand*{\figref}[1]{\hyperref[#1]{Figure~\ref*{#1}}}
\newcommand*{\tabref}[1]{\hyperref[#1]{Table~\ref*{#1}}}
-\usepackage{multicol}
+\usepackage{pftools}
%\usepackage{pfsteps}
%\newcommand*{\pflab}[1]{\steppfcounter[#1](\thepfcounter)}
@@ -255,8 +205,8 @@
% \newcommand{\Prop}{\mathbb{B}}
% \newcommand{\Pred}{\mathbb{P}}
-\newcommand{\res}{r}
-\newcommand{\resB}{s}
+\newcommand{\rs}{r}
+\newcommand{\rsB}{s}
%\newcommand{\propSet}{\mathcal{P}}
%\newcommand{\apropSet}{\mathcal{A}}
--
GitLab