
% this is the 20 minute talk for LPAR in Yogyakarta

\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{Derivability Predicates and their Induction Principles} \label{s-dp}
\begin{frame}[fragile]
  \frametitle{Derivability Predicates and their Induction Principles}

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

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}

}

\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 cut-formulae
}

\frame{
  \frametitle{The Induction Pattern in Cut-Admissibility Proofs} 
\begin{itemize}
\item 
We defined a predicate \texttt{gen\_step2ssr} (see the paper, Defnition 1),
which says that you can prove the inductive step at a point in the derivation
\item
We proved a lemma which says that if this property holds throughout a tree
for a property $P$, then $P$ holds (Theorem 1)
\item Then we proved that this predicate \texttt{gen\_step2ssr}
holds for the case where the cut-formula $A$ is parametric on the left,
subject to certain conditions:
a result applicable to many cut-elimination proofs
(Theorem 2)
\end{itemize}
}

\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}
}
  
\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}

\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}
can ``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}
}

\newcommand\muxbnpt{
\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}
}

\frame
{
  \frametitle{Defining \texttt{muxbn}}
\begin{figure}[t]
  \centering
\normalsize
\muxbnpt
\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}
\begin{lemma} \label{l-caB_muxbn'} 
  If multicut on $B$ is admissible, then \muxbn\ $B$ 0 holds.
\end{lemma}
}

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

\begin{center}
\muxbnpt
\end{center}

\begin{lemma} \label{l-caB_muxbn'} 
  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.

 If an inference \GLR($Y,C$) is
  encountered, with $B$ in $Y$, \\
  then a proof is constructed using the previous lemma
\end{proof}
}

\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$}
We then, essentially, re-do the proof, using 
\begin{itemize}
\item Admissible multicuts with $\Box A, \GLRc$
\item Admissible multicuts on cut-formula $B$
\end{itemize}
\emph{before} the \GLR($A$) step, so that the \GLR($A$) step
does not contribute to \delz.

(Several steps manipulating proofs, see paper).

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$.

\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}

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{
  }

