%% \section{Equivalence of Shallow and Deep Nested Calculi}
%% \label{sec:eqshallowdeep}


We illustrate here some key steps in the formalisation of the equivalence
between $\biillsn$ and $\biilldn$. We show only the translation
from shallow nested sequent proofs to deep nested sequent proofs, which is the more difficult
part of the equivalence. %More details are available in the appendix. 
The key lemma here is that the rules $rp_i$, $drp_i$, 
$gl$ and $gr$, which are in %the shallow calculus
$\biillsn$\ but not in the deep calculus $\biilldn$, are admissible in
$\biilldn$.


%% \subsection{Proving the Deep from the Shallow Nested Sequent Calculus}
%% \begin{lemma}
%% \label{lm:dist}
%% The following rules are derivable in $\biillsn$ without cut:
%% $$
%% \infer[dist_l]
%% {(\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2), \Uc \seq \Vc}
%% {
%% (\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2), \Uc \seq \Vc
%% }
%% \qquad
%% \infer[dist_r]
%% {\Uc \seq \Vc, (\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2)}
%% {
%%  \Uc \seq \Vc, (\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2)
%% }
%% $$
%% \end{lemma}
%% Intuitively, these rules embody
%% the weak distributivity formalised by the Grishin (b) rule. 
%% % It is not surprising that these rules are derivable, as they essentially embody
%% % the weak distributivity principle formalised by the Grishin(b) rule. 

%% In the formalisation we proved the slightly less general result
%% \texttt{snb\_lem14a} and its symmetric counterpart below from which we
%% can obtain Lemma~\ref{lm:dist} with one application of
%% ???\marginpar{How to do this Jeremy?}
%% \begin{lemma}
%% The following rules are derivable in $\biillsn$ without cut:
%% $$
%% \infer[dist_l]
%% {(\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2) \seq \Vc}
%% {
%% (\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2) \seq \Vc
%% }
%% \qquad
%% \infer[dist_r]
%% {\Uc \seq (\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2)}
%% {
%%  \Uc \seq (\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2)
%% }
%% $$
%% \begin{verbatim}
%% snb_lem14a = "([($?Xa => $?Ya),,, ($?Xb => $?Yb) => $?V],
%%       ($?Xa,,, $?Xb => $?Ya,,, $?Yb) => $?V) : derl (nrulefs biillsn_cf)"
%% \end{verbatim}
%% \end{lemma}

%% \begin{lemma}
%% \label{lm:merge}
%% If $\Xc \in \Xc_1 \merge \Xc_2$ then the rules below are cut-free derivable in $\biillsn$:
%% $$
%% \infer[m_l]
%% {\Xc, \Vc \seq \Uc}
%% {
%% \Xc_1, \Xc_2, \Vc \seq \Uc
%% }
%% \qquad
%% \infer[m_r]
%% {\Uc \seq \Vc, \Xc}
%% {
%% \Uc \seq \Vc, \Xc_1, \Xc_2
%% }
%% $$\marginpar{JED, how to close the difference here ? Missing $\Vc$.}
%% \begin{verbatim}
%% rmerge_der : "(?Xa, ?Xb, ?X) : rmerge 
%%   ==> {([$?Xa,,, $?Xb => $?U], $?X => $?U),
%%        ([$?U => $?Xa,,, $?Xb], $?U => $?X)} <= derl (nrulefs fillsn_cf)"
%% \end{verbatim}
%% \end{lemma}
%% \begin{proof}
%% This follows straightforwardly from Lem.~\ref{lm:dist}.
%% \end{proof}

%% % \begin{verbatim}
%% % rmerge_der : "(?X, ?Y, ?Z) : rmerge 
%% %   ==> {([$?X,,, $?Y => $?U], $?Z => $?U),
%% %        ([$?U => $?X,,, $?Y], $?U => $?Z)} <= derl (nrulefs fillsn_cf)"
%% % \end{verbatim}

%% \begin{lemma}
%% \label{lm:context-merge}
%% Suppose $X[~] \in X_1[~] \merge X_2[~]$ and suppose there exists $Y[~]$
%% such that for any $\Uc$ \marginpar{Not formalised by JED?}
%% and any $\rho \in \{drp_1, drp_2, rp_1, rp_2\}$,
%% the figure below left is a valid inference
%% rule in $\biillsn$:
%% \[
%% \qquad
%% \qquad\qquad
%% \infer[\rho]
%% {X[\Uc]}
%% {Y[\Uc]}
%% \qquad\qquad
%% \infer[\rho]
%% {X_1[\Uc]}
%% {Y_1[\Uc]}
%% \qquad
%% \qquad
%% \infer[\rho]
%% {X_2[\Uc]}
%% {Y_2[\Uc]}
%% \]
%% Then there exists $Y_1[~]$ and $Y_2[~]$ such that
%% $Y[~] \in Y_1[~] \merge Y_2[~]$ and the second and the third figures above 
%% are also valid instances of $\rho$ in $\biillsn$.
%% \end{lemma}
%% \begin{proof}
%% This follows from the fact that $X[~]$, $X_1[~]$ and $X_2[~]$ have exactly the same
%% nested structure, so whatever display rule applies to one also applies to the others. 
%% \end{proof}


%% % We prove in turn that the deep propagation rules (\texttt{dn\_bprs}),
%% % single-premise logical rules (\texttt{dn\_splrs})
%% % and monoid (commutativity, associativity and $\Phi$) rules (\texttt{dn\_ac0}) 
%% % are derivable in the shallow system.
%% % These proofs are simpler but have some features similar to the proofs using 

%% \begin{lemma}
%%   For any context,
%%   the deep propagation rules
%%   \texttt{dn\_bprs}, single-premise logical rules
%%   \texttt{dn\_splrs} and added monoid (commutativity, associativity and
%%   $\Phi$) rules \texttt{dn\_ac0} of $\biilldn$ are cut-free derivable in
%%   the shallow system $\biillsn$.
%% %   These proofs are simpler but have some features similar to
%% %   the proofs using \texttt{rule\_base0} and \texttt{rule\_base2}
%% %   described below.
%% \begin{verbatim}
%% ctxt_bprs_sn :
%%   "[| ([?p], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_bprs) |]
%%           ==> ?psc : derl (nrulefs fillsn_cf)"
%% ctxt_splrs_sn :
%%   "[| ([?p], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_splrs) |]
%%          ==> ?psc : derl (nrulefs fillsn_cf)"
%% ctxt_dn_ac0 :
%%   "[| ([$?pa => $?ps], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_ac0) |]
%%           ==> ?psc : derl (nrulefs fillsn_cf)" 
%% \end{verbatim}
%% \end{lemma}

%% A nested sequent $S$ satisfies \texttt{rule\_base0 rules} if, for all
%% hollow $X$, both $X \Rightarrow S$ and $S \Rightarrow X$ are derivable
%% using \texttt{rules}.

%% For the axioms, we proved that the axioms\marginpar{All this to be
%%   cleaned up.} themselves (without the context
%% $X[~]$) are derivable (\texttt{dn\_axioms\_der}),
%% and using lemmas (\texttt{dn\_axioms\_rb0} and \texttt{hctxt\_rb0}) we
%% proved that the axioms with the hollow contexts $X[~]$ are derivable.
%% Thus \texttt{dn\_axioms\_rb0} says that the axioms (without context) can be
%% extended by hollow $X$ in this way once, and \texttt{hctxt\_rb0} extends this
%% inductively to apply to any hollow extension of an axiom.

%% \begin{verbatim}
%% dn_axioms_der : "?S : dn_axioms ==> ([], ?S) : derl (nrulefs fillsn_cf)"
%% dn_axioms_rb0 : "?S : dn_axioms ==> rule_base0 fillsn_cf ?S"
%% hctxt_rb0 : "[| rule_base0 ?rules ?S; sn_idps <= ?rules;
%%   {sn_pA, sn_pS} <= ?rules; ?H : hctxt {?S} |] ==> rule_base0 ?rules ?H"
%% rule_base0_def : "rule_base0 ?rules ?S ==
%%          (ALL X:hollows. ([], $X => $?S) : derl (nrulefs ?rules)) &
%% 	 (ALL X:hollows. ([], $?S => $X) : derl (nrulefs ?rules))"
%% \end{verbatim}

%% For the two-premise logical rules, we prove theorems like
%% \begin{verbatim}
%% dn_ands_sn : "[| (?Sa, ?Sb, ?Sc) : rmerge; (?Ta, ?Tb, ?Tc) : rmerge |] ==>
%%   ([$?Sa => ?A,,, $?Ta, $?Sb => ?B,,, $?Tb],
%% 	        $?Sc => ?A && ?B,,, $?Tc) : derl (nrulefs fillsn_cf)"
%% rb2_ands : "[| (?Sa, ?Sb, ?Sc) : rmerge; (?Ta, ?Tb, ?Tc) : rmerge |] ==>
%%   rule_base2 fillsn_cf 
%%     ($?Sa => ?A,,, $?Ta, $?Sb => ?B,,, $?Tb, $?Sc => ?A && ?B,,, $?Tc)"
%% deep2_ctxt : "[| sn_idps <= ?rules; {sn_pA, sn_pS} <= ?rules;
%%     rule_base2 ?rules (?Ya, ?Yb, ?Yc);
%%     (?Wa, ?Wb, ?Wc) : rmerge1 (?Ya, ?Yb, ?Yc) |] ==>
%%   rule_base2 ?rules (?Wa, ?Wb, ?Wc)"
%% \end{verbatim}
%% Then by the lemmas \texttt{rb2\_ands}, etc, and \texttt{deep2\_ctxt},
%% we are able to show from \texttt{dn\_ands\_sn} (etc)
%% that the deep two-premise logical rules are derivable in the shallow calculus.
%% Similar to \texttt{rule\_base0}, \texttt{rule\_base2} expresses that a triple
%% of sequents $(P_1, P_2, C)$ satisfies that 
%% $X \Rightarrow C$ is derivable from 
%% $X_1 \Rightarrow P_1$ and $X_2 \Rightarrow P_2$,
%% for all $(X_1, X_2, X) \in \texttt{rmerge}$, and similarly for 
%% $C \Rightarrow X$, $P_1 \Rightarrow X_1$ and $P_2 \Rightarrow X_2$.
%% So, similarly to the use of \texttt{rule\_base0} for the axioms,
%% these results are used to show that the two-premise 
%% logical rules in their contexts are derivable.

%% These results are combined to show that nested sequents derivable in the deep
%% calculus are derivable in the shallow calculus.

%% \begin{theorem}
%% \label{thm:soundness}
%% Every rule  of the deep nested sequent calculus $\biilldn$ is
%% cut-free derivable in the shallow nested sequent calculus $\biillsn.$
%% \begin{verbatim}
%% dn_sn_der : "?r : biilldn ==> ?r : derl (nrulefs fillsn_cf)" 
%% \end{verbatim}
%% \end{theorem}

%% \begin{corollary}
%% \label{thm:soundness}
%% If a sequent $X$ is provable in $\biilldn$ then it is cut-free provable in $\biillsn.$
%% \end{corollary}

%% \subsection{Proving the Shallow from the Deep Nested Sequent Calculus}
%% \label{s-dn-sn}

%% We first note that since our formulation of $\biilldn$\ involves the comma
%% as a structural connective, and explicit inclusion of the 
%% monoid rules \texttt{dn\_ac0} (see \S\ref{s-msde}),
%% it is necessary to prove that 
%% our system makes multiset-equivalent nested sequents interderivable
%% using the monoid rules, and conversely.

%% \begin{lemma}
%% If two deep nested sequents $X_a$ and $X_b$ are multiset-equivalent 
%% then the single-premise rule from $X_a$ to $X_b$ is derivable in all
%% contexts using only the monoid rules of associativity, commutativity
%% and identity. Conversely, if the deep nested sequent $X_N$ is
%% derivable from the deep nested sequent $X_M$ in all contexts using the
%% monoid rules then $X_N$ and $X_M$ are multiset-equivalent.
%% \begin{verbatim}
%% msde_derl : "(?a, ?b) : ms_deep_equiv 
%%    ==> ([?a], ?b) : derl (ctxt (nrulefs dn_ac0))"
%% dn_ac0_msde : "([?M], ?N) : ctxt (nrulefs dn_ac0) 
%%   ==> (?M, ?N) : ms_deep_equiv"
%% \end{verbatim}
%% \end{lemma}


\begin{lemma}
\label{lm:permute}
The rules $drp_1$, $rp_1$, $drp_2$, $rp_2$, $gl$, and $gr$ permute up over all logical rules of $\biilldn.$
\end{lemma}
This is the permutation lemma, that (in general)
where one of the shallow rules in question follows a rule of $\biilldn$\
in a derivation, then the derivation can be re-ordered so that the 
shallow rule precedes the deep rule. 
%% To prove this lemma, we need to use
%% two additional structural rules, called $eg$ and $ig$~\cite{ARXIV}, that
%% can be shown to be admissible in $\biillsn$.
%% : 
%% $$
%% \infer[eg]
%% {\Sc, \Sc' \seq \Tc, \Tc'}
%% {(\Sc \seq \Tc), \Sc' \seq \Tc'}
%% \qquad
%% \infer[ig]
%% {\Sc, \Sc' \seq \Tc, \Tc'}
%% {
%% \Sc \seq (\Sc' \seq \Tc'), \Tc
%% }
%% $$
We illustrate here a step in the proof of this 
permutation lemma, i.e., when permuting structural rules over a single-premise
logical rule. We proved theorems of the following form
{\small
\begin{verbatim}
p_irp_anda : "?c = ($?ca => $?cs) -->
  ([?p], ?c) : ctxt (nrulefs {sn_anda}) -->
  (?c, ?c') : ms_deep_equiv --> ([?c'], ?d') : nrulefs {invert sn_rp} -->
  (EX p' q q' d. (?p, p') : ms_deep_equiv &
    ([p'], q) : nrulefs {invert sn_rp} & (q, q') : ms_deep_equiv &
    ([q'], d) : dctxt (nrulefs {sn_anda}) & (d, ?d') : ms_deep_equiv)"
\end{verbatim}
}
That is, where a structural rule, e.g., $rp_1$, 
%%   among
%% $rp_1$, $drp_1$, $rp_2$, $drp_2$, $gl$, $gr$, $eg$ and $eg$
appears below a deep logical rule in a derivation,
the derivation steps may be permuted so that the logical rule follows 
the other rule.
It may be noted that this result uses \texttt{dctxt}, not \texttt{ctxt}, 
in the conclusion.  This made semi-automatic proof easier; 
the lemmas for all the logical rules concerned (6 of them) for all the
structural rules involved (6 of them) were done using just three separate sets
of tactics. 

%% Before realising we needed to use $rp_1$, $drp_1$, $eg$ and $eg$
%% instead of 
%% $rp_1$, $drp_1$, $rp_2$, $drp_2$, $gl$ and $gr$
%% we proved the twelve theorems for the six logical rules and 
%% for $rp_2$ and $drp_2$ using the tactics \texttt{mpttacs}.

%% We proved the twelve theorems 
%% for $rp_1$ and $drp_1$ using the tactics \texttt{mpttacs\_i}.
%% Having proved the twelve theorems 
%% for $gl$ and $gr$ using the tactics \texttt{mpttacs\_g}
%% we found that the same tactics worked to prove the twelve theorems 
%% for $eg$ and $ig$.


%% To use \texttt{dctxt} in this way we needed the results 
%% \texttt{dc\_anda} and \texttt{dcok\_anda} (etc).
%% \begin{verbatim}
%% dc_anda : "([?p], ?c) : dctxt (nrulefs {sn_anda}) ==>
%%   EX p' c'. (?p, p') : ms_deep_equiv & (c', ?c) : ms_deep_equiv &
%%     ([p'], c') : ctxt (nrulefs {sn_anda})" 

%% dcok_anda : "EX p' q q' d. (?p1, p') : ms_deep_equiv &
%%    ([p'], q) : nrulefs {?sn_rule1} & (q, q') : ms_deep_equiv &
%%    ([q'], d) : dctxt (nrulefs {sn_anda}) & (d, ?d'1) : ms_deep_equiv ==>
%%  EX p' q q' d. (?p1, p') : ms_deep_equiv &
%%    ([p'], q) : nrulefs {?sn_rule1} & (q, q') : ms_deep_equiv &
%%       ([q'], d) : ctxt (nrulefs {sn_anda}) & (d, ?d'1) : ms_deep_equiv"
%% \end{verbatim}

%% These results, and similar ones for the other rules of $\biilldn$,
%% will give that the rules 
%% $rp_1$, $drp_1$, $rp_2$, $drp_2$, $gl$ and $gr$ are admissible in $\biilldn$.
%% See \S\ref{s-TBA}.

%% See the file \texttt{CRotate.ML}.

The proofs of the permutation lemma involved a large number of cases,
because a sequent expression such as $X [\mathcal S \seq \mathcal T]$
can match a given sequent $Z$ in numerous ways, for two reasons:
\begin{itemize}
\item for multisets $\mathcal S$ and $\mathcal T$,
%that is, in our
%formulation), 
there can be multiple ways to achieve
$(\mathcal S, \ldots) \in$ \texttt{ms\_deep\_equiv} 
%can be achieved, and
\item the size of context $X [~]$ is arbitrary, so
$\mathcal S \seq \mathcal T$ can match any part of $Z.$
\end{itemize}
The attempted proof encounters many obviously impossible cases
such as a formula matching $\mathcal S \seq \mathcal T$.
After these are %detected and 
eliminated, we counted the cases where 
a goal (such as the conclusion of \texttt{p\_rp\_anda}) is actually solved.
These cases numbered 616, which shows the value of automating the process as
much as possible.  

%% \subsubsection{Wrapping it up}
%% From \S\ \ref{s-perm-ax}, \ref{s-one-prem-log}, \ref{s-two-prem-log},
%% \ref{s-prop-rules} and \ref{s-glr-ieg}
%% we have the $\biilldn$-admissibility of $rp_1$, $drp_1$, $eg$ and $ig$,
%% and from \S\ref{s-hollow-weak} 
%% we have $\biilldn$-admissibility of the two-premise logical rules.
%% The other rules of $\biillsn$\ are $\biilldn$-derivable,
%% so we get \texttt{sn\_dn\_der}.
%% Combining this with \texttt{dn\_sn\_der} (see \S\ref{s-dn-sn})
%% we get \texttt{sn\_dn\_equiv}.
%% These proofs made good use of the lemmas relating 
%% \texttt{derrec}, \texttt{derl}, \texttt{adm}
%% described in our LPAR 2010 (or Raj's talk in India) paper \cite{xx}

%% \begin{theorem}
%% If a sequent $X$ is cut-free $\biillsn$-derivable then it is also $\biilldn$-derivable.
%% \end{theorem}

%% \begin{corollary}\label{cor:dc=dn}
%% A formula is cut-free $\biilldc$-derivable iff it is $\biilldn$-derivable.
%% \end{corollary}

\begin{theorem}\label{thm:eqshallowdeep}
All rules cut-free derivable in $\biillsn$ are (cut-free) admissible in 
$\biilldn$.
% Every rule that is cut-free derivable in $\biillsn$ is (cut-free) admissible in 
% $\biilldn$.
{\small
\begin{verbatim}
sn_dn_der : "derl (nrulefs biillsn_cf) <= adm biilldn"
\end{verbatim}
}
\noindent A sequent is cut-free provable (derivable from the empty set of assumption
sequents) in $\biillsn$ iff it is provable $\biilldn$.
{\small
\begin{verbatim}
sn_dn_equiv : "(?r : derrec (nrulefs biillsn_cf) {}) =
               (?r : derrec biilldn {})" 
\end{verbatim}
}
\noindent The formula $A$ is cut-free provable in the display calculus iff it
is (cut-free) provable in $\biilldn$.
{\small
\begin{verbatim}
dc_dn_equiv : "((T |- ?A) : derrec (rulefs biilldc_cf) {}) =
               (($NPhi => ?A) : derrec biilldn {})"
\end{verbatim}
}
\end{theorem}

% \subsection{Lemmas about \texttt{ms\_deep\_equiv}}

% OMIT THIS SECTION

% There were a number of seemingly basic lemmas about the
% \texttt{ms\_deep\_equiv} relation which were not easy to prove. 
% For example, 

% \begin{verbatim}
% mins_msde_lem ;
% msde_ex_plus ;
% msde_mins_inv ;
% msde_plus_inv ;
% msde_commasD ;
% ctxt_nseq_lem ;
% \end{verbatim}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 
