diff --git a/spec/doc.tex b/spec/doc.tex
index 61924fc615e402045f0af5364d6d6ae8ecd7a25b..51d9d960a0aeb5363ac059437aed7cda11558701 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -977,8 +977,8 @@ If there is no anchor in $P$ then there is a step $s_i$ that has the
empty clause as its conclusion. We can perform the same induction as
in the proof of Lemma~\ref{lem:sound_subproof} with $\mathit{start} = 1$
and $\mathit{end} = i$. This shows that $V \vDash \bot$, where $V$ is the
-conclusion of the \proofType{assume} steps in $[s_1, \dots, s_i]$. We can weaken
-this by adding the conclusions of the \proofType{assume} steps in
+conclusion of the \proofRule{assume} steps in $[s_1, \dots, s_i]$. We can weaken
+this by adding the conclusions of the \proofRule{assume} steps in
$[s_i, \dots, s_n]$ to get $\varphi_1, \dots, \varphi_m \vDash \bot$.
If there are $n$ anchors in $P$ then there is an admissible subproof with
@@ -991,257 +991,8 @@ Definition~\ref{def:valid_proof}. The newly constructed proof $P'$ has
$n-1$ anchors and hence is sound due to the induction hypothesis.
\end{proof}
-\subsubsection{Abstract Inference System} % or Rules, or Rules of Inference
-\label{sec:inference-system}
-Most of the content is taken from the presentation and the correctness proof of
-the format~\cite{barbosa-2019}.
-
-The inference rules used by our framework depend on a notion of
-\emph{context} defined by the grammar
-\[\GAMMA \,::=\, \emptyctx \,\mid\, \GAMMA,\, x \,\mid\, \GAMMA,\,\bar x_n\mapsto \bar s_n\]
-The empty context $\emptyctx$ is also denoted by a blank.
-Each context entry either \emph{fixes} a variable~$x$ or defines a
-\emph{substitution} $\{\bar x_n \mapsto \bar s_n\}$. Any variables arising in
-the terms $\bar s_n$
-will typically have been introduced in the context $\GAMMA$ on the left, but
-this is not required.
-If a context introduces the same variable several times, the rightmost
-entry shadows the others.
-\par
-Abstractly, a context $\GAMMA$ fixes a set of variables
-and specifies a substitution
-$\subst{\GAMMA}$%
-. The substitution is the identity for $\emptyctx$ and is
-defined as follows in the other cases:
-%
-\begin{align*}
- \subst{\GAMMA,\, x} & = \subst{\GAMMA}[x \mapsto x]
- \, %%% TYPESETTING
-&
- \subst{\GAMMA,\, \bar x_n \mapsto \bar t_n} & = \subst{\GAMMA} \mathrel\circ \{\bar x_n \mapsto \bar t_n\}
-\end{align*}
-In the first equation,
-the $[x \mapsto x]$ update shadows any
-replacement of $x$ induced by $\GAMMA$.
-The examples below illustrate this subtlety:
-\begin{align*}
-\subst{x \mapsto 7,\, x \mapsto \sym{g}(x)} & = \{x \mapsto \sym{g}(7)\}
-\\
-\subst{x \mapsto 7,\, x,\, x \mapsto \sym{g}(x)} & = \{x \mapsto \sym{g}(x)\}
-%\\
-%\subst{x,\, y \mapsto x,\, x,\, z \mapsto x} & = \{x \mapsto \sym{g}(x)\}
-\end{align*}%
-We write $\substapp{\GAMMA}{t}$ to abbreviate
-the capture-avoiding substitution $\subst{\GAMMA}(t)$.
-
-Transformations of terms (and formulas) are justified by judgments of
-the form $\judge{\GAMMA}{\allowbreak t\simeq\nobreak u}$, where $\GAMMA$ is a context, $t$ is an unprocessed term, and $u$ is the
-corresponding processed term. The free variables in $t$ and $u$ must appear in
-the context $\GAMMA$. Semantically, the judgment expresses the equality of the
-terms $\substapp{\GAMMA}{t}$ and $u$, universally quantified on variables fixed by~$\GAMMA$.
-Crucially, the substitution applies only on the left-hand side of the equality.
-
-The inference rules for the transformations rely on equations that are presented here, then the rules are
-presented below, followed by explanations.
-\begin{gather}
- \label{eq:choicei}
- \models (\Ex{x}{\varphi[x]}) \implies \varphi[\Choice{x}{\varphi}]
- \tag{\ensuremath{\Choicename_1}}
- \\
- \label{eq:choiceii}
- \models (\forall x.\;\varphi \simeq \psi) \implies (\Choice{x}{\varphi}) \simeq (\Choice{x}{\psi})
- \tag{\ensuremath{\Choicename_2}}
- \\
- % \intertext{and}
- \label{eq:let}
- \models (\mathrm{let}~\bar x_n \simeq \bar s_n~\mathrm{in}~t[\bar x_n])
- \simeq t[\bar s_n]
- \tag{\ensuremath{\mathrm{let}}}
-\end{gather}
-
-% PF TODO: \models_{\!\!{\mathcal T}} does not look nice. Actually
-% this {\mathcal T} with the current font is ugly, without even counting
-% the space that makes \models_{\!\!{\mathcal T}} unreadable
-The rules are:
-%
-\noindent
-\begin{center}
- \AXC{\strut}
- \RL{{\footnotesize \TautT}%
- \quad\mbox{if\vthinspace{} $\models_{\!\!{\mathcal T}} {\substapp{\GAMMA}{t} \simeq u}$}}
- \UIC{\strut$\judge{\GAMMA}{t\simeq u}$}
- \DP
- \qquad
- \AXC{\strut$\judge{\GAMMA}{s\simeq t}\quad\judge{\GAMMA}{t\simeq u}$}
- \RL{{\footnotesize \Trans}\quad\mbox{if\vthinspace{} $\substapp{\GAMMA}{t} = t$}}
- \UIC{\strut$\judge{\GAMMA}{s\simeq u}$}
- \DP
-
-\vskip.7\abovedisplayskip
-
- \AXC{\strut$\bigl(\judge{\GAMMA}{t_i\simeq u_i}\bigr){}_{i=1}^n$}
- \RL{{\footnotesize \Cong}}
- \UIC{\strut$\judge{\GAMMA}{\sym{f}(\bar t_n)\simeq \sym{f}(\bar u_n)}$}
- \DP
- \ \ \
- \AXC{\strut$\judge{\GAMMA,\,y,\,x\mapsto y}{\varphi\simeq\psi}$}
- \RL{{\footnotesize \Bind}\quad\mbox{if\vthinspace{} $y \notin \FV{Qx.\>\varphi} \mathrel\cup \var{\GAMMA}$}}
- \UIC{\strut$\judge{\GAMMA}{(Qx.\>\varphi)\simeq (Qy.\>\psi)}$}
- \DP
-
-\vskip.7\abovedisplayskip
-
- \AXC{\strut$\judge{\GAMMA,\, x\mapsto (\Choice{x}{\varphi})}{\varphi\simeq \psi}$}
- \RL{{\footnotesize \SkoEx}}
- \UIC{\strut$\judge{\GAMMA}{(\Ex{x}{\varphi})\simeq \psi}$}
- \DP
- \qquad
- \AXC{\strut$\judge{\GAMMA,\, x\mapsto (\Choice{x}{\Not\varphi})}{\varphi\simeq \psi}$}
- \RL{{\footnotesize \SkoAll}}
- \UIC{\strut$\judge{\GAMMA}{(\All{x}{\varphi})\simeq \psi}$}
- \DP
-
-\vskip.7\abovedisplayskip
-
- \AXC{\strut$\bigl(\judge{\GAMMA}{r_i \simeq s_i}\bigr){}_{i=1}^n
- \quad
- \judge{\GAMMA,\,\bar x_n\mapsto \bar s_n}{t\simeq u}$}
- \RL{{\footnotesize \Let}\quad\mbox{if\vthinspace{}
- $\substapp{\GAMMA}{s_i} = s_i$ \,for all $i \in [n]$}}
- \UIC{\strut$\judge{\GAMMA}{(\mathrm{let}\ \bar x_n \simeq \bar r_n\ \mathrm{in}\ t)\simeq u}$}
- \DP
-\end{center}
-
-\noindent
-%These rules deserve some explanation:
-%
-% PF TODO it is not nice to have an itemize here. Maybe just remove, with an introductory sentence nicely saying indeed that rules deserve explanation.
-\begin{itemize}
-\item \TautT{} relies on an oracle $\models_{\mathcal T}$
-to derive arbitrary lemmas in a theory $\mathcal T\!$.
-In practice, the oracle will produce some
-kind of certificate to justify the inference.
-An important special case, for
-which we use the name \Refl{}, is syntactic equality up to renaming of bound
-variables; the side condition
-is then $\substapp{\GAMMA}{t} \eqa u$.
-(We use $\eqa$ instead of $=$ because applying a substitution can
-rename bound variables.)
-% PF TODO: maybe mention alpha-conversion: it is not clear why alpha
-
-
-\smallskip
-
-\item \Trans{} needs the side condition because the term $t$ appears both on
-the left-hand side of $\simeq$ (where it is subject to $\GAMMA$'s substitution)
-and on the right-hand side (where it is not).
-Without it, the two occurrences of $t$ in the
-antecedent could denote different terms.
-
-\smallskip
-
-\item \Cong{} can be used for any function symbol $\sym{f}$,
- including the logical connectives. % and other predicates.
-
-\smallskip
-
-\item \Bind{} is a congruence rule for quantifiers. The rule
-also justifies the renaming of the bound variable
-(from $x$ to $y$). In the antecedent, the
-renaming is expressed by a substitution in the context.
-If $x = y$,
-the context is $\GAMMA,\, x,\, x \mapsto x$, which has the same meaning as
-$\GAMMA,\, x$. The side condition prevents an unwarranted variable
-capture: The new variable should not be a free variable in the formula where the
-renaming occurs ($y \notin \FV{Qx.\>\varphi}$), and should be fresh in the
-context ($y\notin \var{\GAMMA}$, where $\var{\GAMMA}$ denotes the set of all
-variables occurring in $\GAMMA$). In particular, $y$ should not appear fixed
-or on either side of a substitution in the context.
-\smallskip
-
-\item \SkoEx{} and \SkoAll{} exploit (\ref{eq:choicei})
-to replace a quantified variable with a suitable witness, simulating
-skolemization. We can think of the $\Choicename$ expression in each rule
-abstractly as a fresh function symbol that takes any fixed variables it
-depends on as arguments. In the antecedents, the replacement is performed
-by the context.
-
-\smallskip
-
-\item \Let{} exploits (\ref{eq:let}) to expand a `let'
-expression. Again, a substitution is used.
-The terms~$\bar r_n$ assigned to the variables $\bar x_n$
-can be transformed into terms $\bar s_n$.
-\end{itemize}
-
-The antecedents of all the rules inspect subterms structurally, without
-modifying them. Modifications to the term on the left-hand side are delayed;
-the substitution is applied only in \Taut{}. This is crucial to obtain compact
-proofs that can be checked efficiently.
-Some of the side conditions may look computationally expensive,
-but there are techniques to compute them fairly efficiently. Furthermore, by
-systematically renaming variables in \Bind, we can satisfy most of the side conditions
-trivially.
-% PF TODO "there are techniques": we might want something more strict.
-
-The set of rules can be extended to cater for arbitrary transformations that
-can be expressed as equalities, using Hilbert choice to represent fresh
-symbols if necessary. The usefulness of Hilbert choice for proof
-reconstruction is well known
-\cite{de-nivelle-2005,paulson-susanto-2007,boehme-weber-2010}, but we push
-the idea further and use it to simplify the inference system and make it more
-uniform.
-
-\begin{example}
-\label{ex:let}
-The following derivation tree justifies the expansion of a `let' expression:
-%
-\[
- \AXC{\axiomstrut}
- \RL{{\footnotesize $\Cong$}}
- \UIC{\strut$\judgei{\sym{a} \simeq \sym{a}}$}
- \AXC{\axiomstrut}
- \RL{{\footnotesize \Refl}}
- \UIC{\strut$\judge{x\mapsto\sym{a}}{x\simeq \sym{a}}$}
- \AXC{\axiomstrut}
- \RL{{\footnotesize \Refl}}
- \UIC{\strut$\judge{x\mapsto\sym{a}}{x\simeq \sym{a}}$}
- \RL{{\footnotesize \Cong}}
- \BIC{\strut$\judge{x\mapsto\sym{a}}{\sym{p}(x, x)\simeq \sym{p}(\sym{a}, \sym{a})}$}
- \RL{{\footnotesize \Let}}
- \BIC{\strut$\judgei{(\mathrm{let}\ x\simeq \sym{a}\ \mathrm{in}\ \sym{p}(x
- , x))\simeq \sym{p}(\sym{a},\sym{a})}$}
- \DP
-\]
-\end{example}
-
-\subsubsection{Correctness}
-\label{sec:correctness}
-\newcommand\thys{\mathcal T_1 \mathrel\cup \cdots \mathrel\cup \mathcal T_n \mathrel\cup {\simeq} \mathrel\cup \Choicename \mathrel\cup \mathrm{let}}
-
-\begin{theorem}[Soundness of Inferences~{\cite[Theorem 11]{barbosa-2019}}]
- \label{thm:sound-calc}
- \,If the judgment\/ $\judge{\GAMMA}{t\simeq u}$ is derivable
- using the original inference system
- with the theories $\enum{\mathcal T}${\rm,} then\/
- $\models_{\mathcal T}{\substapp{\GAMMA}{t} \simeq u}$ with\/ $\mathcal T = \thys$.
-\end{theorem}
-\begin{proof}
- See~\cite[Theorem 11]{barbosa-2019}
-\end{proof}
-
-
-\subsubsection{More Concrete Rules}
-\label{sec:concrete-rules}
-
-The high-level rules presented in the previous paragraph are useful for
-presentation purpose, but they are hard to check. We specialize them by reducing
-applicability. In particular the {\Taut} rule is very hard to check and is
-specialized.
-% PF TODO: improve the previous sentence
-
\begin{figure}[t]
-\begin{minted}[linenos]{smtlib2.py -x}
+ \begin{minted}[linenos]{smtlib2.py -x}
(assume h1 (not (p a)))
(assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
...
@@ -1258,18 +1009,12 @@ specialized.
(step t16 (cl (not (forall ((vr5 U)) (p vr5))) (p a))
:rule or :premises (t15))
(step t17 (cl) :rule resolution :premises (t16 h1 t14))
-\end{minted}
-\caption{Example proof output. Assumptions are introduced (line 1--2);
-a subproof renames bound variables (line 4--8); the proof finishes with
-instantiation and resolution steps (line 10--15)}\label{fig:proof_ex}
+ \end{minted}
+ \caption{Example proof output. Assumptions are introduced (line 1--2);
+ a subproof renames bound variables (line 4--8); the proof finishes with
+ instantiation and resolution steps (line 10--15)}\label{fig:proof_ex}
\end{figure}
-% PF Don't you want to talk about the lambda interpretation of all this?
-% At first, I wanted to only use the lambda version. It is only later that
-% this syntactic sugar was introduced.
-% The above section actually does not talk much about semantics if
-% it does not relate to logic, interpretation, etc...
-
\subsection{The Syntax}
\label{sec:syntax}