From: Stefano Zacchiroli Date: Mon, 21 Nov 2005 13:22:06 +0000 (+0000) Subject: split body away to ease inclusion from elsewhere X-Git-Tag: V_0_7_2_3~17 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a8a60abba413c68ee65f3322f6b4028af34ed9e6;p=helm.git split body away to ease inclusion from elsewhere --- diff --git a/helm/ocaml/tactics/doc/body.tex b/helm/ocaml/tactics/doc/body.tex new file mode 100644 index 000000000..3c537d43b --- /dev/null +++ b/helm/ocaml/tactics/doc/body.tex @@ -0,0 +1,247 @@ + +\section{Semantics} + +\subsection{Language} + +\[ +\begin{array}{rcll} + S & ::= & & \mbox{(\textbf{continuationals})}\\ + & & \TACTIC{T} & \mbox{(tactic)}\\[2ex] + & | & \DOT & \mbox{(dot)} \\ + & | & \SEMICOLON & \mbox{(semicolon)} \\ + & | & \BRANCH & \mbox{(branch)} \\ + & | & \SHIFT & \mbox{(shift)} \\ + & | & \POS{i} & \mbox{(relative positioning)} \\ + & | & \MERGE & \mbox{(merge)} \\[2ex] + & | & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\ + & | & \UNFOCUS & \mbox{(unfocus)} \\[2ex] + & | & S ~ S & \mbox{(sequential composition)} \\[2ex] + T & : := & & \mbox{(\textbf{tactics})}\\ + & & \SKIP & \mbox{(skip)} \\ + & | & \mathtt{reflexivity} & \\ + & | & \mathtt{apply}~t & \\ + & | & \dots & +\end{array} +\] + +\subsection{Status} + +\[ +\begin{array}{rcll} + \xi & & & \mbox{(proof status)} \\ + \mathit{goal} & & & \mbox{(proof goal)} \\[2ex] + + \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\ + \mathit{locator} & = & \INT\times\SWITCH & \\ + \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex] + + \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\ + \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\ + \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex] + + \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST + \\[2ex] + + \mathit{status} & = & \xi\times\mathit{stack} \\ +\end{array} +\] + +\paragraph{Utilities} +\begin{itemize} + \item $\ZEROPOS([g_1;\cdots;g_n]) = + [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$ + \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) = + [\langle 1,s_1\rangle;\cdots;\langle n,s_n\rangle]$ + \item $\ISFRESH(s) = + \left\{ + \begin{array}{ll} + \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\ + \mathit{false} & \mathrm{otherwise} \\ + \end{array} + \right.$ + \item $\FILTEROPEN(\mathit{locs})= + \left\{ + \begin{array}{ll} + [] & \mathrm{if}~\mathit{locs} = [] \\ + \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl}) + & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\ + \FILTEROPEN(\mathit{tl}) + & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\ + \end{array} + \right.$ + \item $\REMOVEGOALS(G,\mathit{locs}) = + \left\{ + \begin{array}{ll} + [] & \mathrm{if}~\mathit{locs} = [] \\ + \REMOVEGOALS(G,\mathit{tl}) + & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} + \land g\in G\\ + hd :: \REMOVEGOALS(G,\mathit{tl}) + & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\ + \end{array} + \right.$ + \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$ + it returns a new stack $S'$ identical to the given one with the exceptions + that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack + components and removed from $\tau$ and $\kappa$ components. + \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position + on a given stack $S$, appearing in an \OPEN{} switch. +\end{itemize} + +\paragraph{Invariants} +\begin{itemize} + \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s + \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in + $\tau$ and $\kappa$ components has an \OPEN~switch). + \item Unless \FOCUS{} is used the stack contains no duplicate goals. + \item $\forall~\mathrm{locator}~l\in\Gamma \mbox{(with the exception of the + top-level $\Gamma$)}, \ISFRESH(l)$. +\end{itemize} + +\subsection{Semantics} + +\[ +\begin{array}{rcll} + \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} & + \mbox{(continuationals semantics)} \\ + \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH -> + \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\ +\end{array} +\] + +\[ +\begin{array}{rcl} + \mathit{apply\_tac} & : & T -> \xi -> \GOAL -> + \xi\times\GOAL~\LIST\times\GOAL~\LIST +\end{array} +\] + +\[ +\begin{array}{rlcc} + \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\ + \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle & +\end{array} +\] + +\[ +\begin{array}{rcl} + + \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} + & = + & \langle + \xi_n, + \ENTRY{\Gamma'}{\tau'}{\kappa'}{t} +% \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t} + :: \DEEPCLOSE(G^c_n,S) + \rangle + \\[1ex] + \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1} + \\[1ex] + \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~ + \Gamma' = \ZEROPOS(G^o_n) + \land \tau' = \REMOVEGOALS(G^c_n,\tau) + \land \kappa' = \REMOVEGOALS(G^o_n,\kappa) + } + \\[1ex] + \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~ + \left\{ + \begin{array}{rcll} + \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\ + \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle + & = + & \langle\xi_i, G^o_i, G^c_i\rangle + & l_{i+1}\in G^c_i \\ + \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle + & = + & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle + & l_{i+1}\not\in G^c_i \\[1ex] + & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\ + \end{array} + \right. + } + \\[6ex] + + \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S} + & = + & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle + \\[1ex] + & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1 + \\[2ex] + + \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S} + & = + & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle + \\[1ex] + & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[] + \\[2ex] + + \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex] + + \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} + \quad + & = + & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S + \\[1ex] + & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n'] + \\[2ex] + + \SEM{~\SHIFT~} + {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'} + ::S} + & = + & \langle + \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG} + ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S + \rangle + \\[1ex] + & & \mathrm{where} ~ n\geq 1 + \\[2ex] + + \SEM{~\POS{i}~} + {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} + & = + & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle + \\[1ex] + & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l) + \\[2ex] + + \SEM{~\POS{i}~} + {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG} + ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} + & = + & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S + \rangle + \\[1ex] + & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma' + \\[2ex] + + \SEM{~\MERGE~} + {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'} + ::S} + & = + & \langle \xi, + \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'} + :: S + \rangle + \\[2ex] + + \SEM{\FOCUS{g_1,\dots,g_n}}{S} + & = + & \langle \xi, \ENTRY{\ZEROPOS([g_1;\cdots;g_n])}{[]}{[]}{\FOCUSTAG} + ::\DEEPCLOSE(S) + \rangle + \\[1ex] + & & \mathrm{where} ~ + \forall i=1,\dots,n,~g_i\in\GOALS(S) + \\[2ex] + + \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S} + & = + & \langle \xi, S\rangle \\[2ex] + +\end{array} +\] + diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index d812bcd33..00208b0c2 100644 --- a/helm/ocaml/tactics/doc/main.tex +++ b/helm/ocaml/tactics/doc/main.tex @@ -63,251 +63,7 @@ \begin{document} \maketitle -\section{Semantics} - -\subsection{Language} - -\[ -\begin{array}{rcll} - S & ::= & & \mbox{(\textbf{continuationals})}\\ - & & \TACTIC{T} & \mbox{(tactic)}\\[2ex] - & | & \DOT & \mbox{(dot)} \\ - & | & \SEMICOLON & \mbox{(semicolon)} \\ - & | & \BRANCH & \mbox{(branch)} \\ - & | & \SHIFT & \mbox{(shift)} \\ - & | & \POS{i} & \mbox{(relative positioning)} \\ - & | & \MERGE & \mbox{(merge)} \\[2ex] - & | & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\ - & | & \UNFOCUS & \mbox{(unfocus)} \\[2ex] - & | & S ~ S & \mbox{(sequential composition)} \\[2ex] - T & : := & & \mbox{(\textbf{tactics})}\\ - & & \SKIP & \mbox{(skip)} \\ - & | & \mathtt{reflexivity} & \\ - & | & \mathtt{apply}~t & \\ - & | & \dots & -\end{array} -\] - -\subsection{Status} - -\[ -\begin{array}{rcll} - \xi & & & \mbox{(proof status)} \\ - \mathit{goal} & & & \mbox{(proof goal)} \\[2ex] - - \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\ - \mathit{locator} & = & \INT\times\SWITCH & \\ - \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex] - - \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\ - \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\ - \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex] - - \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST - \\[2ex] - - \mathit{status} & = & \xi\times\mathit{stack} \\ -\end{array} -\] - -\paragraph{Utilities} -\begin{itemize} - \item $\ZEROPOS([g_1;\cdots;g_n]) = - [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$ - \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) = - [\langle 1,s_1\rangle;\cdots;\langle n,s_n\rangle]$ - \item $\ISFRESH(s) = - \left\{ - \begin{array}{ll} - \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\ - \mathit{false} & \mathrm{otherwise} \\ - \end{array} - \right.$ - \item $\FILTEROPEN(\mathit{locs})= - \left\{ - \begin{array}{ll} - [] & \mathrm{if}~\mathit{locs} = [] \\ - \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl}) - & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\ - \FILTEROPEN(\mathit{tl}) - & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\ - \end{array} - \right.$ - \item $\REMOVEGOALS(G,\mathit{locs}) = - \left\{ - \begin{array}{ll} - [] & \mathrm{if}~\mathit{locs} = [] \\ - \REMOVEGOALS(G,\mathit{tl}) - & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} - \land g\in G\\ - hd :: \REMOVEGOALS(G,\mathit{tl}) - & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\ - \end{array} - \right.$ - \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$ - it returns a new stack $S'$ identical to the given one with the exceptions - that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack - components and removed from $\tau$ and $\kappa$ components. - \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position - on a given stack $S$, appearing in an \OPEN{} switch. -\end{itemize} - -\paragraph{Invariants} -\begin{itemize} - \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s - \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in - $\tau$ and $\kappa$ components has an \OPEN~switch). - \item Unless \FOCUS{} is used the stack contains no duplicate goals. - \item $\forall~\mathrm{locator}~l\in\Gamma \mbox{(with the exception of the - top-level $\Gamma$)}, \ISFRESH(l)$. -\end{itemize} - -\subsection{Semantics} - -\[ -\begin{array}{rcll} - \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} & - \mbox{(continuationals semantics)} \\ - \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\ -\end{array} -\] - -\[ -\begin{array}{rcl} - \mathit{apply\_tac} & : & T -> \xi -> \GOAL -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST -\end{array} -\] - -\[ -\begin{array}{rlcc} - \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\ - \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle & -\end{array} -\] - -\[ -\begin{array}{rcl} - - \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} - & = - & \langle - \xi_n, - \ENTRY{\Gamma'}{\tau'}{\kappa'}{t} -% \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t} - :: \DEEPCLOSE(G^c_n,S) - \rangle - \\[1ex] - \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1} - \\[1ex] - \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~ - \Gamma' = \ZEROPOS(G^o_n) - \land \tau' = \REMOVEGOALS(G^c_n,\tau) - \land \kappa' = \REMOVEGOALS(G^o_n,\kappa) - } - \\[1ex] - \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~ - \left\{ - \begin{array}{rcll} - \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\ - \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle - & = - & \langle\xi_i, G^o_i, G^c_i\rangle - & l_{i+1}\in G^c_i \\ - \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle - & = - & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle - & l_{i+1}\not\in G^c_i \\[1ex] - & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\ - \end{array} - \right. - } - \\[6ex] - - \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S} - & = - & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle - \\[1ex] - & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1 - \\[2ex] - - \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S} - & = - & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle - \\[1ex] - & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[] - \\[2ex] - - \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex] - - \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} - \quad - & = - & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S - \\[1ex] - & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n'] - \\[2ex] - - \SEM{~\SHIFT~} - {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'} - ::S} - & = - & \langle - \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG} - ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S - \rangle - \\[1ex] - & & \mathrm{where} ~ n\geq 1 - \\[2ex] - - \SEM{~\POS{i}~} - {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} - & = - & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle - \\[1ex] - & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l) - \\[2ex] - - \SEM{~\POS{i}~} - {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG} - ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} - & = - & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S - \rangle - \\[1ex] - & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma' - \\[2ex] - - \SEM{~\MERGE~} - {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'} - ::S} - & = - & \langle \xi, - \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'} - :: S - \rangle - \\[2ex] - - \SEM{\FOCUS{g_1,\dots,g_n}}{S} - & = - & \langle \xi, \ENTRY{\ZEROPOS([g_1;\cdots;g_n])}{[]}{[]}{\FOCUSTAG} - ::\DEEPCLOSE(S) - \rangle - \\[1ex] - & & \mathrm{where} ~ - \forall i=1,\dots,n,~g_i\in\GOALS(S) - \\[2ex] - - \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S} - & = - & \langle \xi, S\rangle \\[2ex] - -\end{array} -\] +\input{body.tex} \end{document}