
% this is the 50 minute talk given at ANU

\documentclass{beamer}
% \documentclass[handout]{beamer} % to print

\usetheme{Frankfurt}
\usecolortheme{seahorse}
\usepackage{proof}
\usepackage{bussproofs}
\usepackage{exptrees} 

% \usetheme{split}

\newcommand\comment[1]{} 
\comment% \AtBeginSection[]%
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection]
   \end{frame}
}
\comment% \AtBeginSubsection[]%
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection,currentsubsection]
   \end{frame}
}

\title{Generic Methods for Formalising Sequent Calculi
       Applied to Provability Logic}
\author{Jeremy Dawson and Rajeev Gor\'e}
\institute{
Logic and Computation Group
\\School of Computer Science
\\College of Engineering and Computer Science
\\ Australian National University
\\ Canberra ACT 0200, Australia
\\ \url{http://users.rsise.anu.edu.au/~jeremy/}
\ \ \url{http://users.rsise.anu.edu.au/~rpg/}
}

\begin{document}

\input{defs}

\frame{\titlepage}

% \section[Outline]{}
\frame
{
  \frametitle{Outline}
  \tableofcontents}

% \section{Section title} 
% \subsection{Subsection title} 
% \frame
% {
  % \frametitle{Frame title}
  % \framesubtitle{Frame subtitle}
% }

\section{Introduction} \label{s-intro}
\frame
{
  \frametitle{Introduction}
Formalisation of cut-admissibility for the \GLS\ sequent system
\begin{itemize}
\item cut-admissibility applies for many sequent systems
\item proofs can be tedious --- details omitted (``other cases are similar'')
\item we try to get common elements of the proofs for re-use 
\item provability logic has unusual features ($GL$ rule has formula on 
both sides of $\vdash$), proof more complex
\item previous proofs wrong, or allegedly so but actually OK
\item formalised proof in Isabelle/HOL confirms the result, omits no details,
and uses many lemmas applicable for other logics
\end{itemize}
% We formalise the cut-elimination proof in Isabelle/HOL
  }

\section{Sequents, Multisets, Sets and Provability  Logic}
\label{sec:preliminaries}
\frame
{
  \frametitle{Sequents and Multisets, Sets and Provability  Logic}
\begin{itemize}
\item
sequents  $\Gamma \vdash \Delta$ 
where $\Gamma$ and $\Delta$ are ``collections'' of formulae

\item
Our ``collections'' are multisets (unordered, but repetitions counted)

\item
Tree-shaped derivations, conclusion at the bottom

\item
Tree branches where rule has $> 1$ premise, leaf where rule has no premises
\end{itemize}

} 

\frame
{
  \frametitle{Provability  Logic}
\begin{itemize}
\item explicit weakening and contraction rules
\item usual (additive) rules for $\lnot, \land, \lor, \to$
\item additional  rule \GLR{} which characterises \GL{}:
\begin{prooftree}
  \AxiomC{$\GLRp$}
  \RightLabel{\GLR \mbox{ or } \GLRB \mbox{ or } \GLRXB}
  \UnaryInfC{$\GLRc$}
\end{prooftree}

\item in our formalisation, cut or multicut rules not part of \GLS

$$
\AxiomC{$\Gamma \vdash A, \Delta$}
  \AxiomC{$\Gamma, A \vdash \Delta$}
  \LeftLabel{(cut)}
  \BinaryInfC{$\Gamma \vdash \Delta$}
  \DisplayProof
$$ $$
  \AxiomC{$\Gamma' \vdash A^{n}, \Delta'$}
  \AxiomC{$\Gamma'', A^{m} \vdash \Delta''$}
  \LeftLabel{(multicut)}
  \BinaryInfC{$\Gamma', \Gamma'' \vdash \Delta', \Delta''$}
  \DisplayProof
$$

\end{itemize}
  }

\section{Reasoning About Derivations and Derivability}
\label{s-deriv}
\subsection{Deep and Shallow Embeddings} \label{s-dse} 
\begin{frame}[fragile]
  \frametitle{Deep and Shallow Embeddings --- Derivations}
\begin{itemize}
\item Deep or shallow embeddings of 
\emph{derivations}, \emph{rules} and \emph{variables}.
\item \emph{shallow} means that a feature in the logic is identified with the
same feature of Isabelle/HOL
\end{itemize}


Derivations:
\begin{itemize}
\item \alert{Deep:} the actual derivation tree is a data structure in HOL
\begin{verbatim}
   datatype 'a dertree = Der 'a ('a dertree list)
       | Unf 'a (* unfinished leaf not proved *)
\end{verbatim}
there is a predicate which tests whether each node of an 
 derivation tree is an instance of a rule 
\item \alert{Shallow:} no derivation tree data structure,
but an inductive definition in HOL saying what formulae are derivable;
(the course of a proof, in HOL, of a formula,
 could be described by a derivation tree)
\end{itemize}
\end{frame}
  
\frame
{
  \frametitle{Deep and Shallow Embeddings --- Rules and Variables}
Rules:
\begin{itemize}
\item \alert{Deep:} each rule is a data structure in HOL,
and the definition of derivability refers to the set of rules as a parameter
\item \alert{Shallow:} the set of rules is encoded in the definition of 
derivability
\end{itemize}

Variables (only for deep embedding of rules):
\begin{itemize}
\item \alert{Deep:} each rule contains references to names variable(s),
and HOL functions instantiate each variable as required
\item \alert{Shallow:} each ``rule'' is in fact the set of all possible 
instantiations of the ``rule'', achieved using Isabelle variables
\end{itemize}

Shallow embedding of rules seems to necessarily imply shallow embedding of 
variables and the process of instantiating them
}
  

\subsection{Generic Derivability Predicates} \label{s-dp}
\begin{frame}[fragile]
  \frametitle{Generic Derivability Predicates}
\begin{verbatim}
types 'a psc = "'a list * 'a" (* single step inference *)
consts
  derl, adm :: "'a psc set => 'a psc set"
  derrec    :: "'a psc set => 'a set => 'a set"
\end{verbatim}

\noindent
An inference rule of type \texttt{'a psc} is a list of premises % \texttt{ps}
and a conclusion. Then
\begin{itemize}
\item \texttt{derl rls} is the set of
rules derivable from the rule set \texttt{rls},
\item \texttt{adm rls} is the set of
admissible rules of the rule set \texttt{rls},
and
\item \texttt{derrec rls prems}
is the set of sequents derivable using rules \texttt{rls}
from the set \texttt{prems} of premises. 
\end{itemize}
\end{frame}

\frame{
  \frametitle{Examples : Generic Derivability Predicates}
\rm Shallow Embedding of Derivations, Deep Embedding of Rules: \\[0.6em]
 $(\{\Gamma \vdash P, ~~\Gamma \vdash Q\},
   \;\; \Gamma \vdash P \land Q) \in \mathtt{rules}$ \quad (etc for
   other rules) \\[0.4em]
 $ ~c \in \mathtt{prems} \Longrightarrow c \in \mathtt{derrec~rules~prems}$ 
 \\[0.5em]
 $ [|~(ps, c) \in \mathtt{rules} ~;~
    ps \subseteq \mathtt{derrec~rules~prems}~|] \Longrightarrow $ \\
   \qquad \qquad $ c \in \mathtt{derrec~rules~prems}$ \\[0.7em]
\rm Shallow Embedding of Derivations and of Rules: \\[0.6em]
 $ ~c \in \mathtt{prems} \Longrightarrow c \in \mathtt{ders~prems}$ \\[0.4em]
 $[|~\Gamma \vdash P \in \mathtt{ders~prems} ~;~
        \Gamma \vdash Q \in \mathtt{ders~prems}~|] \Longrightarrow $ \\
   \qquad \qquad $ \Gamma \vdash P \land Q \in \mathtt{ders~prems}$
}

\begin{frame}[fragile]
  \frametitle{Theorems about the Generic Derivability Predicates}

\begin{itemize}
\item \texttt{derl\_deriv\_eq} states that
derivability using derived rules implies derivability using the original rules
\item \texttt{derrec\_trans\_eq} states that
derivability from derivable sequents implies derivability
from the original premises.
\end{itemize}

\begin{verbatim}
derl_deriv_eq : "derl (derl ?rls) = derl ?rls"
derrec_trans_eq : "derrec ?rls (derrec ?rls ?prems)
                   = derrec ?rls ?prems"
\end{verbatim}
The induction principle (simplified) 
from the definition of \derrec\ :
$$
\frac {
\begin{array}{c}x \in derrec\ rls\ prems \qquad
   \forall c \in prems.\  P\ c \\[-0.2ex]
   \forall (ps, c) \in rls.\ (\forall p\ in\ ps.\ P\ p) \Rightarrow P\ c
\end{array}
}
   {P\ x}
$$
\end{frame}

\frame{
  \frametitle{Induction on two derivations}
Induction for a property of two derivations (eg cut-admissibility!)
$$
 \begin{array}{c}
  cl \in derrec\ rlsl\ \{\} \qquad cr \in derrec\ rlsr\ \{\}  \\
      \forall (lps, lc) \in rlsl.\ \forall (rps, rc) \in rlsr.\ \hfill \\
       \hfill \qquad \qquad
       (\forall lp \in lps.\ P~lp~rc) \land (\forall rp \in rps.\ P~lc~rp)
           \Rightarrow P~lc~rc \\
\hline { P\ cl\ cr}
\end{array}
$$
% Suppose $cl$ and $cr$ are the conclusions of the left
% and right subderivations.  Assume that for every rule pair $(lps, lc)$
% and $(rps, rc)$, if each premise $lp$ in $lps$ satisfies $P~lp ~rc$, and each
% premise $rp$ in $rps$ satisfies $P~lc~rp$, then $P~lc~rc$ holds.  Then we
% can conclude that $P~cl~cr$ holds.

to prove $P (\MC_{l}, \MC_{r})$, the
induction hypothesis is that $P (\MQ_{li}, \MC_{r})$ and $P (\MC_{l},
\MQ_{rj})$ hold for all $i$ and $j$:

\begin{center}
\begin{prooftree}
\AxiomC{$\MQ_{l1} \ldots \MQ_{ln}$}
\RightLabel{$\rho_l$}
\UnaryInfC{$\MC_{l}$}
\AxiomC{$\MQ_{r1} \ldots \MQ_{rm}$}
\RightLabel{$\rho_r$}
\UnaryInfC{$\MC_{r}$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{?}
\end{prooftree}
\end{center}

}

\subsection{Sequents, Formulae and the GLS rules} \label{s-gls}
\begin{frame}[fragile]
  \frametitle{Sequents, Formulae and Rules}

formula language: connectives, variables 
and primitive propositions:
\begin{verbatim}
datatype formula = FC string (formula list) (* connective *)
                 | FV string                (* variable *)
                 | PP string     (* primitive proposition *)
\end{verbatim}

A sequent is a pair of multisets of formulae, written
$\Gamma \vdash \Delta$.

Given a rule such as $(\vdash \land)$ in the two forms below,
$$
\MC_s = \frac{\vdash A \quad \vdash B} {\vdash A \land B}
\qquad\qquad\
\MC_e = \frac{X \vdash Y, A \quad X \vdash Y, B} {X \vdash Y, A \land B}
$$
% \begin{itemize}
 we call $\MC_e$ an \emph{extension} of $\MC_s$: 
  $X \vdash Y = \texttt{extend}\ (X \vdash Y)\ (\vdash A)$

% we define functions \texttt{pscmap} and \texttt{extend},
 \texttt{pscmap} $f$ applies $f$ to premises and conclusion,
% such that (for example), where $+$ means multiset union,

% \end{itemize}

so, using $+$ for multiset union,
%
\begin{gather*}
\texttt{extend}\ (X \vdash Y)\ (U \vdash V) = (X + U) \vdash (Y + V) \\
\MC_e = \texttt{pscmap}\ (\texttt{extend}\ (X \vdash Y))\ \MC_s
\end{gather*}

\end{frame}

\frame{
  \frametitle{The \GLS\ Rules}

Then we define \texttt{glss}, the set of rules of \GLS{} by defining:
%We define these sets of rules:
\begin{itemize}
\item \texttt{glil} and \texttt{glir}: the unextended left and right
  introduction rules, like $\MC_s$ above;
\item \texttt{wkrls} and \texttt{ctrrls} $A$: the unextended
  weakening and contraction (on $A$) rules;
\item \texttt{glne}: all of the above;
\item \texttt{glr} $B$: the \GLR(B) rule;
\item \texttt{glss}: the axiom $A \vdash A$ (not requiring $A$ to be atomic),
the \GLR(B) rule for all $B$, and all extensions of all rules in \texttt{glne}.
\end{itemize}

}
  


\section{An Axiomatic Type Class for Multisets and Sequents} \label{s-axtc}

\begin{frame}[fragile]
  \frametitle{An Axiomatic Type Class for Multisets and Sequents} 
  \framesubtitle{the class \pmz} 
ordering $\leq$ on multisets analogous to
$\subseteq$ for sets: $N \leq M$ if, for all $x$, $N$ contains no more
occurrences of $x$ than does $M$.

~

We define a type class \pmz:

~

For any type in class \pmz, the operations
$+$ and $0$ form a commutative monoid and
% the type allows the $-$ operator, and
the following two properties hold.
\begin{equation*}
A + B - A = B \qquad \qquad A - B - C = A - (B + C)
\end{equation*}

\begin{verbatim}
   axclass pm0 < comm_monoid_add, minus
     pm0_plus_minus  : "A + B - A = B"
     pm0_minus_minus : "A - B - C = A - (B + C)"
\end{verbatim}

\end{frame}

\frame{
  \frametitle{An Axiomatic Type Class for Multisets and Sequents} 
  \framesubtitle{the class \pmgez} 
 class \pmgez:
it also has $\leq$ and $0$,
axioms of \pmz\ and these:
\begin{gather*}
   0 \leq A \qquad \qquad
    B \leq A \Rightarrow B + (A - B) = A \\
   m \leq n \Leftrightarrow m - n = 0  \qquad
    x < y \Leftrightarrow x \leq y \land x \not= y \qquad
   a \sqsubseteq b \Leftrightarrow a \leq b
\end{gather*}
\begin{lemma}
  Multisets are in \pmz\ and \pmgez\ using our definition of $\leq$,
  and, if $\Gamma$ and $\Delta$ are of any type in the classes
  \pmz\ or \pmgez, then so is sequent $\Gamma \vdash \Delta$.
\end{lemma}

This class in fact gives us a lattice
\begin{lemma}
  Any type of class \pmgez\ forms a lattice,
  using the definitions \\
% {$c \land d = c - (c - d) $} and $ c \lor d = c + (d - c)$.
$$c \land d = c - (c - d) \qquad \qquad c \lor d = c + (d - c)$$
\end{lemma}
}

\frame{
  \frametitle{Simplification Procedures for Multisets and Sequents} 
Isabelle has ``simplification procedures'':
 \begin{itemize}
 \item $a - b + c + b$ to $a + c$ (integers)
\item  $a + b + c - b$ to $a + c$
(integers \emph{or} naturals)
 \end{itemize}

We applied most of the simplification procedures for naturals
to types of the classes \pmz\ and \pmgez
}

\newcommand\psl{\ensuremath\MQ_{l1} \ldots \MQ_{ln}}
\newcommand\psr{\ensuremath\MQ_{r1} \ldots \MQ_{rm}}

\section{Capturing the Core of Cut-Admissibility Proofs} \label{s-cagen}
\frame{
  \frametitle{The Induction Pattern in Cut-Admissibility Proofs} 
  \framesubtitle{Definition of \texttt{gen\_step2ssr}} 
  % \framesubtitle{The Induction Pattern} 
In the diagram below, to prove $P (\MC_{l}, \MC_{r})$, the
induction hypothesis is that $P (\MQ_{li}, \MC_{r})$ and $P (\MC_{l},
\MQ_{rj})$ hold for all $i$ and $j$:

\begin{center}
\begin{prooftree}
\AxiomC{$\MQ_{l1} \ldots \MQ_{ln}$}
\RightLabel{$\MR_l$}
\UnaryInfC{$\MC_{l}$}
\AxiomC{$\MQ_{r1} \ldots \MQ_{rm}$}
\RightLabel{$\MR_r$}
\UnaryInfC{$\MC_{r}$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{?}
\end{prooftree}
\end{center}

 \texttt{gen\_step2ssr} expresses that property $P$ holds, 
given appropriate inductive hypotheses,
for last rules on each side $\MR_l$ and $\MR_r$.

$P$ might be that cut-admissibility holds
for cut-formula $A$, rule set \texttt{rls},
assuming it holds for smaller (subformula relation \texttt{sub})
}

\frame{
  \frametitle{The Induction pattern in Cut-Admissibility Proofs} 
  \framesubtitle{Definition of \texttt{gen\_step2ssr}} 
\begin{definition}[\texttt{gen\_step2ssr}] \label{d-gen-step2ssr}
 For a formula $A$, a property $P$,
 a subformula relation \texttt{sub},
 a set of rules \texttt{rls},
 inference rule instances $\MR_l = {(\psl, \MC_l)}$
 and $\MR_r = {(\psr, \MC_r)}$,
 \texttt{gen\_step2ssr} $P\ A$ \texttt{sub rls} $(\MR_l, \MR_r)$
 means: %\\%[0.5em]
% if %all the following hold:
\begin{description}
 \item[if] forall ${A'}$ such that $(A', A) \in \texttt{sub}$
 and all \texttt{rls}-derivable sequents
 $\MD_l$ and $\MD_r$,
  ${P\ A'\ (\MD_l, \MD_r)}$ holds
 \item[ ] and for each ${\MP_{li}}$ in ${\psl}$,
 % ${\MP}$ is \texttt{rls}-derivable and
 ${P\ A\ (\MP_{li}, \MC_r)}$ holds
 \item[ ] and for each ${\MP_{rj}}$ in ${\psr}$,
 % \texttt{\MP} is \texttt{rls}-derivable and
 ${P\ A\ (\MC_l, \MP_{rj})}$ holds
 % \item ${\MC_l}$ and ${\MC_r}$ are \texttt{rls}-derivable.
\item[then] ${P\ A\ (\MC_{l}, \MC_{r})}$ holds.
\end{description}
\end{definition}
}

\frame{
  \frametitle{The Induction pattern in Cut-Admissibility Proofs} 
  \framesubtitle{Theorem using \texttt{gen\_step2ssr}}
The theorem \texttt{gen\_step2ssr\_lem} for 
$P$ states that if the step of the inductive proof
holds for all cases of final rules $\MR_l$ and $\MR_r$
 % ${(\psl, \MC_l)}$ and ${(\psr, \MC_r)}$
 on each side, then $P$ holds in all cases.

\begin{theorem}[\texttt{gen\_step2ssr\_lem}] \label{t-gen-step2ssr-lem}
 If
 \begin{itemize}
 \item \texttt{A} is in the well-founded part of the subformula relation
 \texttt{sub},
 \item sequents $\MS_l$ and $\MS_r$ are \texttt{rls}-derivable, and
 \item for all formulae $A'$, and all rules $\MR_l$ and $\MR_r$,
%  ${(\psl, \MC_l)}$ and ${(\psr, \MC_r)}$,
 our induction step condition
 \texttt{gen\_step2ssr} $P\ A'\ \texttt{sub rls}\ (\MR_l, \MR_r)$
 holds
\end{itemize}
 then ${P\ A\ (\MS_l, \MS_r)}$ holds.
\end{theorem}
}

\frame{
  \frametitle{The Induction pattern in Cut-Admissibility Proofs} 
  \framesubtitle{Lemma for the left parametric case} 

% This theorem justifies 
Inductive step where the cut-formula $A$ is
parametric on the left.

(\mbox{\texttt{prop2 mar erls} $A\ (\MC_l, \MC_r)$} means
that the conclusion of a multicut on \texttt{A} with premises 
$\MC_l$ and $\MC_r$ is derivable using rules \texttt{erls})

\begin{theorem}[\texttt{lmg\_gen\_steps}]~\label{t-gs2ssr}
 For any relation \texttt{sub} and any rule set \texttt{rls},
 given an instance of multicut with left and right subtrees
 ending with rules $\MR_l$ and $\MR_r$:
\begin{description}
 \item[if] weakening is admissible for the rule set \texttt{erls},
 \item and all extensions of some rule $(\MP, X \vdash Y)$ are in the rule set
  \texttt{erls},
  \item and $\MR_l$ is an extension of $(\MP, X \vdash Y)$,
  \item and the cut-formula $A$ is not in $Y$
  (meaning that $A$ is parametric on the left)
%  \end{itemize}
  \item[then] \texttt{gen\_step2ssr (prop2 mar erls)} $A$ \texttt{sub rls}
  $(\MR_l, \MR_r)$ holds.
\end{description}
\end{theorem}
}

\section{The Proof of Cut-Admissibility for GLS} \label{s-caglr}
\frame
{
  \frametitle{The proof of Gor\'e \& Ramanayake, and our proof}

The proof of Gor\'e \& Ramanayake
\begin{itemize}
\item  Proves admissibity of $(cut)$ (we prove admissibity of $(multicut)$)
\item  Induction on height of derivation and on ``width''
\item  Induction on size of cut-formula.
\end{itemize}
In contrast, in our proof 
\begin{itemize}
\item  we prove admissibity of $(multicut)$
\item  Induction on ``fact of'' derivation and on \delz\ 
(approximates to \delzs, related to width)
\item  Well-founded induction on immediate subformula relation
\end{itemize}
}
  
\begin{frame}[fragile]
  \frametitle{Using a deep embedding --- explicit derivation trees}

  To define \delz\ on a derivation we need an explicit derivation tree
  
~

A \textit{valid} tree is one whose inferences are in the set of rules
and which as a whole has no premises.
\begin{lemma} \label{l-derrec-valid}
  Sequent $X \vdash Y$ is derivable, shallowly,
  from the empty set of premises using rules \texttt{rls}
  (ie, is in \texttt{derrec rls} $\{\}$)
 %(ie, according to the definitions of \S\ref{s-dp})
  iff some explicit derivation tree
  \texttt{dt} is valid wrt.\ \texttt{rls} and has a conclusion
  $X \vdash Y$.
\end{lemma}
\begin{verbatim}
"(?a : derrec ?rls {}) =
   (EX dt. valid ?rls dt & conclDT dt = ?a)"
\end{verbatim}
``mix and match'' a deep embedding (derivation trees) with a shallow
embedding (inductively defined sets of derivable sequents)

\end{frame}

\frame
{
  \frametitle{Defining \delz}

\begin{definition}[\delz] \label{d-del0}
For derivation tree \texttt{dt} and formula $B$,
define \delz\ $B$ \texttt{dt}: %  is as follows:
% \delz\ $B$ \texttt{dt} is given by:
\begin{itemize}
\item if the bottom rule of \texttt{dt} is % \GLR\ (for \emph{any} $B,X$),
\GLR($Y,A$) (for \emph{any} $Y,A$),
then \delz\ $B$ \texttt{dt} is 1 (0) if $\Box B$ is (is not) in the antecedent
of the conclusion of \texttt{dt}
\item if the bottom rule of \texttt{dt} is not \GLR, then \delz\ $B$
\texttt{dt}
is obtained by summing \delz\ $B$ \texttt{dt'} over all premise subtrees
\texttt{dt'} of \texttt{dt}.
\end{itemize}
\end{definition}

\begin{tabular}{p{18em}c}
ie, you go up each branch of an explicit
derivation tree until you find an instance of the \GLR\ rule, and
count 1 where $B$ is in $Y$
&
$\begin{array}{c}
~ \\[2ex]
{\Box Y, Y, \Box A \vdash A} \\
\hline \\[-2ex]
{\Box Y \vdash \Box A}
\end{array}$
\end{tabular}
}

\frame
{
  \frametitle{The Proof}

\begin{lemma} \label{l-gr19e} If $\mu$ is a valid
  derivation tree with conclusion \GLRp{}, and \delz\ $B\ \mu = 0$, then
  \lxxc\ is derivable.
\end{lemma}

\begin{proof}
  Applying the \GLR\ rule to the \GLRp\ gives \GLRc.
Tracing upwards, 
  change each $\Box B$ to $\Box X$ in the usual way.
Contraction is not problematic since we use, as the
  inductive hypothesis, that \emph{all} occurrences of $\Box B$ can be
  replaced by $\Box X$. 
\end{proof}
}

\frame
{
  \frametitle{Defining \texttt{muxbn}}
\begin{figure}[t]
  \centering
\normalsize
\begin{prooftree}
\AxiomC{$\displaystyle \mu\left\{\ \frac{\Pi_l}{\GLRp}\right.$}
\RightLabel{\GLRB}
\UnaryInfC{\GLRc}
\AxiomC{$\Pi_r$}
\RightLabel{$\rho$}
\UnaryInfC{${\Box B^k, Y \vdash Z}$}
\dottedLine
\RightLabel{(\textit{multicut ?})}
\BinaryInfC{${\Box X, Y \vdash Z}$}
\end{prooftree}
\caption{A multicut on cut formula $\Box B$ where $\Box B$ is
  left-principal via \GLR{}}
\label{f-muxbn}
\end{figure}

\begin{definition}[\muxbn] \label{d-muxbn}
\muxbn\ $B\ n$ holds iff:
for all instances of Figure~\ref{f-muxbn} (for fixed $B$) such that
 \delz\ $B\ \mu \leq n$, the multicut in Figure~\ref{f-muxbn}
 is admissible.
\end{definition}
}

\frame
{
  \frametitle{Proofs of \texttt{muxbn}}

\begin{lemma} \label{l-caB_muxbn'} If
  $\mu$ is a valid derivation tree with conclusion \GLRp, and \delz\
  $B\ \mu = 0$, and multicut on $B$ is admissible, and $\Box B^k, Y
  \vdash Z$ is derivable, then $\Box X, Y \vdash Z$ is derivable.

  That is, if multicut on $B$ is admissible, then \muxbn\ $B$ 0 holds.
\end{lemma}

\begin{proof}
  \GLRc{} is derivable from \GLRp{} via \GLRXB.  By
  Lemma~\ref{l-gr19e}, \lxxc\ is derivable. The rest of the proof is
  by induction on the derivation of $\Box B^k, Y \vdash Z$, in effect,
  by tracing relevant occurrences of $\Box B$ up that
  derivation.

 Suppose an inference \GLR($Y,C$) is
  encountered, with $B$ in $Y$.
(see next slide)
\end{proof}
}

\frame
{

\begin{prooftree}
 \AxiomC{$\Box B^k, B^k, \Box Z, Z, \Box C \vdash C$}
 \RightLabel{\GLR($Y,C$)}
 \UnaryInfC{$\Box B^k , \Box Z \vdash \Box C$}
\end{prooftree}

$Z$ is $Y$ with
  $B$ deleted.

By induction, 
${\Box X, B^k, \Box Z, Z, \Box C \vdash C}$ is derivable. \\
From there we have the derivation shown below.

\begin{prooftree}
\AxiomC{Lemma~\ref{l-gr19e}}
\UnaryInfC{\lxxc}
\AxiomC{${\Box X, B^k, \Box Z, Z, \Box C \vdash C}$}
% following lines for context-sharing multicut
% \BinaryInfC{${\Box X, X, \Box Z, Z, \Box C \vdash C}$} 
% \RightLabel{$\textit{mcut}^*(B)$}
\RightLabel{$\textit{mcut}(B)$}
\BinaryInfC{${\Box X, \Box X, X, \Box Z, Z, \Box C \vdash C}$}
\RightLabel{\textit{ctr}}
\UnaryInfC{${\Box X, X, \Box Z, Z, \Box C \vdash C}$}
\RightLabel{\GLR($C$)}
\UnaryInfC{${\Box X, \Box Z \vdash \Box C}$}
\end{prooftree}

Additional weakening steps necessary
if $\Box B$ in $Z$ or if $B$ in $\Box Z$
(shown by machine-checking!)
}

\frame
{
  \frametitle{From \texttt{muxbn} $B\ n$ to \texttt{muxbn} $B\ (n+1)$}
\begin{prooftree}
\AxiomC{$\displaystyle \mu\left\{\ \frac{\Pi_l}{\GLRp}\right.$}
\RightLabel{\GLRB}
\UnaryInfC{\GLRc}
\end{prooftree}
Suppose \delz\ $B\ \mu = n + 1$.

Since \delz\ $B\ \mu > 0$, the tree $\mu / \GLRc$ contains
one or more branches with a \GLR\ rule, with $\Box B$ in the antecedent.
(one such branch shown).
\begin{prooftree}
\AxiomC{${\Box G, G, \Box B^k, B^k, \Box A\vdash A} $}
\RightLabel{\GLR($A$)}
\UnaryInfC{\gbna}
\UnaryInfC{\vdots}
\UnaryInfC{\GLRp}
\RightLabel{\GLR($X,B$)}
\UnaryInfC{\GLRc}
\end{prooftree}
}

\frame
{
  \frametitle{From \texttt{muxbn} $B\ n$ to \texttt{muxbn} $B\ (n+1)$}
\begin{prooftree}
\AxiomC{${\Box G, G, \Box B^k, B^k, \Box A\vdash A} $}
\RightLabel{\GLR($A$) (delete this)}
\UnaryInfC{\gbna}
\UnaryInfC{\vdots}
\UnaryInfC{\GLRp}
\RightLabel{\GLR($X,B$)}
\UnaryInfC{\GLRc}
\end{prooftree}

Delete top step, adjoin $\Box A$ on the left, extra weakening step:

\begin{prooftree}
% \AxiomC{$\mu^A \left\{ {
\AxiomC{$\Box A, \gbna$}
\UnaryInfC{\vdots}
\UnaryInfC{$\Box A, \GLRp$}
\RightLabel{(\textit{weakening}) (extra step)}
\UnaryInfC{$\Box A, A, \GLRp$}
% \DisplayProof} % \right. $}
\RightLabel{\GLR($B$)}
\UnaryInfC{$\Box A, \GLRc$}
\end{prooftree}

Call this $\mu^A / \Box A, \GLRc$, then 
\delz\ $B\ \mu > \mbox{\delz}\ B\ \mu^A$,
so $\mu^A / \Box A, \GLRc$ can be
left branch of an admissible multicut.
}

\frame
{
  \frametitle{Multicutting with $\Box A, \GLRc$}
\begin{prooftree}
\AxiomC{$\Box A, \GLRc$}
\AxiomC{}
\UnaryInfC{\GLRp}
\dottedLine
\RightLabel{(\textit{multicut} + $ctr$)}
\BinaryInfC{$\Box A, \lxxc$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Box A, \GLRc$}
\AxiomC{}
\UnaryInfC{${\Box G, G, \Box B^k, B^k, \Box A\vdash A} $}
\dottedLine
\RightLabel{(\textit{multicut} + $ctr$)}
\BinaryInfC{${\Box G,
  G, \Box X, B^k, \Box A\vdash A}$}
\end{prooftree}

Now, multicut on $B$ (smaller cut-formula), and contraction, gives
\begin{prooftree}
\AxiomC{$\Box G, G, \Box A, \Box X, X \vdash A$}
\RightLabel{\GLR}
\UnaryInfC{$\Box G, \Box X \vdash \Box A$}
\RightLabel{(\textit{weakening})}
\UnaryInfC{$\Box G, \Box X, \Box B^k \vdash \Box A$}
\end{prooftree}
}

\frame
{
  \frametitle{From \delz\ $B\ \mu = n + 1$ to \delz\ $B\ \mu' = n$}
\begin{prooftree}
\AxiomC{}
\UnaryInfC{\gbna}
\UnaryInfC{\vdots}
\UnaryInfC{\GLRp}
% \RightLabel{\GLR($X,B$)}
% \UnaryInfC{\GLRc}
\end{prooftree}
We use this proof again, now adjoin $\Box X$ on the left, to get

\begin{prooftree}
\AxiomC{previous slide}
\UnaryInfC{$\Box X, \gbna$}
\UnaryInfC{\vdots}
\UnaryInfC{$\Box X, \GLRp$}
\RightLabel{(\textit{contraction})}
\UnaryInfC{$\GLRp$}
% \RightLabel{\GLR}
% \UnaryInfC{\GLRc}
\end{prooftree}
That is, given a derivation $\mu$ of \GLRp\, with
\delz\ $B\ \mu = n + 1$, we have a derivation $\mu'$ % of \GLRp\ 
with \delz\ $B\ \mu' = n$.
}

\frame
{
  \frametitle{Wrapping it up}

\begin{lemma} \label{l-gr19bc} Assume that
  multicut-admissibility holds for cut-formula $B$, and
  that \muxbn\ $B$ $n$ holds.
Then \muxbn\ $B$ $(n+1)$ holds.
\end{lemma}

\begin{proof} See the Figure: 
 given $\mu$, where \delz\ $B\ \mu = n + 1$, 
we can replace it by by $\mu'$, where \delz\ $B\ \mu' = n$.
  Since \muxbn\ $B$ $n$ holds, the multicut in the 
Figure is admissible, as required.
\end{proof}

Now, since \muxbn\ $B$ $0$ holds, repeated use of this Lemma gives that 
\muxbn\ $B$ $n$ for all $n$.

}

\frame
{
  \frametitle{The cut-admissibility theorem}
\begin{theorem} \label{t-glss-ca}
Multicut is admissible in \GLS.
\end{theorem}

\begin{proof}
Most of the proof is as usual for cut-elimination proofs,
using induction on the size (or structure) of the cut-formula. 
The difficult case is with a multicut as in the Figure, 
which is handled by the previous lemma.
\end{proof}
}

\section{Conclusion}
\frame
{
  \frametitle{Conclusion : value of the formalisation}
  
\begin{itemize}
\item proofs usually tedious, with many details varying only slightly
\item many cases or details usually omitted in paper proofs
\item this may lead to erroneous proofs
\item formal proof avoids this risk
\end{itemize}

Our formalisation includes:
\begin{itemize}
\item formalisation includes general treatment of derivation trees 
\item general theorem expressing the appropriate inductive principle
\item general lemmas for many cases in this and other proofs
\end{itemize}


}
\end{document}
\comment{
  }

