chap-minml.tex

\chapter{Simple Language with Arithmetic and Booleans}
\label{chap:basic}
\begin{quote}
``A language that doesn't affect the way you think about programming, is
not worth knowing.''
\hfill - Alan Perlis
\end{quote}

We begin our gentle introduction to mechanizing languages and proofs by
considering a simple language with arithmetic and boolean
expressions. In general, definitions of programming languages
typically cover three fundamental aspects:
the grammar  of the language  (i.e. what are syntactically well-formed terms in
the language),  its operational semantics (i.e. how do we execute and evaluate a
given term),  and its  type structure (i.e. what are  well-typed expressions).  We
revisit  these concepts  for  a small language  containing booleans  and numbers
following \citep[Ch 3,Ch 8]{TAPL} in  preparation for representing this language
together with its operational semantics and type system in \beluga.

\section{Terms}\label{sec:terms-basic}
Let  us  consider  a simple language  containing booleans,  if-expressions,  and
numbers together  with simple operations  that allow us  to test whether a given
number is zero (see \cite[Ch 3, Fig 3-1,Fig 3-2]{TAPL}). We define numbers using
$\tmzero$ and the $\tmsucc$operation.  To analyze  and manipulate numbers,  we also
provide a $\tmpred$operator.
\[
\begin{array}{ll@{\bnfas}l}
\mbox{Terms} & M & \tmtrue \bnfalt \tmfalse \bnfalt \tmif{M_1}{M_2}{M_3} \bnfalt
\tmzero \bnfalt \tmsucc M \bnfalt \tmpred M \bnfalt \tmiszero M
\end{array}
\]

The first question  we investigate is  how to define  and represent terms in the
\beluga proof  environment. To represent  terms  in \beluga,  we declare  a type
\lstinline!term!  for  terms   together  with  constants  corresponding  to  the
constructors    $\tmtrue$,   $\tmfalse$,    $\tmzero$,   $\tmsucc{\!}$,   $\tmpred{\!}$,
$\tmiszero{\!}$,  etc.   More   precisely   we   use   the   logical   framework  LF
\citep{Harper93jacm} for introducing new types such as \lstinline!term! together
with constants  \lstinline!true!,  \lstinline!false!, etc.  that  can be used to
construct terms. All constants are used as prefix operators by default.

\begin{lstlisting}
LF term : type =
| true         : term
| false        : term
| if_then_else : term -> term -> term -> term
| z            : term
| succ         : term -> term
| pred         : term -> term
| iszero       : term -> term
;
\end{lstlisting}

To illustrate, consider a few examples. We write in sans-serif font what
we would write on paper and use typewriter font for its equivalent
representation in \beluga.

\begin{center}
\begin{tabular}{l@{\quad is represented as \quad}l}
%\multicolumn{1}{c}{On paper} & & \multicolumn{1}{c}{Code}\\[0.5em]
$\tmif \tmfalse \tmzero {\tmsucc \tmzero}$ &
\lstinline!if_then_else false z (succ z)!\\
$\tmiszero (\tmpred (\tmsucc \tmzero))$ & \lstinline!iszero (pred (succ z))!.
\end{tabular}
\end{center}

% We can declare infix
% operator by using the keyword \lstinline!%infix!.

\section{Semantics}
Next, we define how to evaluate and execute a given term. Following
\cite{TAPL}, we define  a small-step semantics  for our  little language. To give  a  deterministic evaluation
strategy,  it is convenient to first define the values of our language.  In
\cite{TAPL}, we distinguish between terms and values in the grammar itself and
think of values  as a sub-class of terms; moreover, we further
distinguish between numerical values and boolean values. Here we take  a slightly different
approach and define explicitly  what it means  to be a value using the judgment
$M \Value$.  We can think of these judgments  as predicates on
terms which are defined  via  axioms and inference rules.  A term $M$ is a
a value iff we can give a derivation for $M \Value$. We also do not further
distinguish between numerical values and  booleans. Although this can
be done, such a distinction makes many of the theoretical properties
needlessly more complex.

\[
\begin{array}{c}
\multicolumn{1}{l}{\fbox{$V \Value$}: \mbox{Term $V$ is a value}}\\[1em]
\infer[\VZero]{\tmzero \Value}{} \quad
\infer[\VSucc]{(\tmsucc V) \Value}{V \Value} \quad
\infer[\VTrue]{\tmtrue \Value}{} \quad
\infer[\VFalse]{\tmfalse \Value}{}
\end{array}
\]

Here, we identify $\tmzero$ as a value; in addition, $\tmsucc V$ is a value
provided that $V$ is a value. We also identify $\tmtrue$ and $\tmfalse$ as
values. %, and say that every numeric value is a value.

We are now ready to define when a term $M$ steps to another term $N$ (using the
judgment $M \Steps N$) using congruence rules and reduction rules.

\[
\begin{array}{c}
\multicolumn{1}{l}{\fbox{$M \Steps N$}: \mbox{Term $M$ steps to term $N$}}
\\[1em]
\multicolumn{1}{l}{\mbox{\text{Congruence Rules}}}
\\[1em]
\infera{\ESucc}{\tmsucc M \Steps \tmsucc N}{M \Steps N}\qquad
\infera{\EPred}{\tmpred M \Steps \tmpred N}{M \Steps N}
\\[1em]
\multicolumn{1}{c}{\infera{\EIszero}{\tmiszero M \Steps \tmiszero N}{M \Steps N}}
\\[1em]
\multicolumn{1}{c}{\infera{\EIf}{\tmif{M_1}{M_2}{M_3} \Steps \tmif{M_1'}{M_2}{M_3}}{M_1 \Steps M_1'}}
\\[1em]
\multicolumn{1}{l}{\mbox{\text{Reduction Rules (Axioms)}}}
\\[1em]
\infera{\EPredZero}{\tmpred \tmzero \Steps \tmzero}{}\qquad
\infera{\EPredSucc}{\tmpred (\tmsucc V) \Steps V}{V \Value}
\\[1em]
\infera{\EIszeroZero}{\tmiszero \tmzero \Steps \tmtrue}{} \qquad
\infera{\EIszeroSucc}{\tmiszero (\tmsucc V) \Steps \tmfalse}{V \Value}
\\[1em]
\multicolumn{1}{c}{\infera{\EIfTrue }{\tmif{\tmtrue }{M_2}{M_3} \Steps M_2}{}}
\\[1em]
\multicolumn{1}{c}{\infera{\EIfFalse}{\tmif{\tmfalse}{M_2}{M_3} \Steps M_3}{}}
\end{array}
\]

Our goal is to represent the relation $M \Steps N$ and describe the derivation
trees which correspond to evaluating a given sub-term. To accomplish this we
also must be able to construct derivation trees that prove that a given term is
a value.  Clearly, inductively defined terms can be easily translated into objects of
type \lstinline!term! using the constants \lstinline!true!,
\lstinline!false!, \lstinline!if_then_else!, \lstinline!z!,
\lstinline!succ!, \lstinline!pred!, and \lstinline!iszero!.
However, we also defined inductively what it means for a
term to be a value:  we use the  axioms $\VZero$, $\VTrue$, and
$\VFalse$ together with the inference rule $\VSucc$. Similarly, we can
translate derivation trees that prove $V \Value$ and derivation trees
that show $M \Steps N$.

In \beluga, types are powerful enough to encode such definitions about
predicates and relations. To represent the judgment $V \Value$ we define a
predicate (type family) \lstinline!value! and state that it takes terms as
argument by declaring its type as \lstinline!term -> type!. Then each rule
corresponds to a constructor in our data-type definition. A derivation tree then
corresponds to an expression formed by these constructors.

\begin{lstlisting}
LF value : term -> type =
| v_z        : value z
| v_succ     : value V -> value (succ V)
| v_true     : value true
| v_false    : value false
;
\end{lstlisting}

In our definition of the constructor \lstinline!v_succ!, the capital letter
\lstinline!V! describes values and is thought of as being universally quantified on
the outside. We can hence read the constructor \lstinline!v_succ! as follows:

\begin{center}
\begin{tabular}{p{12cm}}
``For all terms \lstinline$V$, if \lstinline!D! is a derivation for
\lstinline!value V!, then we can form a derivation \lstinline!(v_succ <<V>> D)!
for \lstinline!value (succ V)!.''
\end{tabular}
\end{center}

We mark the term \lstinline!<<V>>! here in green since in practice programmers
can omit writing it and \beluga will infer it. The recipe is, ``if we do not
explicitly quantify over variables in the definition of a constructor, we do not
need to pass instantiations  for them when constructing objects  using said
constructor.''\index{Type reconstruction}\index{Implicit Arguments}

To illustrate, consider the following concrete example of proving that
$\tmsucc (\tmsucc \tmzero)$ is a value and constructing a derivation
for $(\tmsucc (\tmsucc \tmzero)) \Value$.
\begin{center}
  \[
     \infera{\VSucc} { (\tmsucc (\tmsucc \tmzero)) \Value }
   { \infera{\VSucc} { (\tmsucc \tmzero) \Value }
   { \infera{\VZero} { \tmzero \Value } {} } }
 \]
 is represented as
 \small{\lstinline!(v_succ <<(succ z)>> (v_succ <<z>> v_z))!}
\end{center}
\index{Encoding derivation trees}

In \beluga, we bind the derivation to the name \lstinline!v! by writing
\begin{lstlisting}
let v : [|- value (succ (succ z))] = [|- v_succ (v_succ v_z)];
\end{lstlisting}
Note that we write derivations using \lstinline!|-!.  On the left hand
side  of this symbol  we list assumptions, and on the right hand side
we describe what we claim can be derived from these assumptions.  For example, we might say:

\begin{lstlisting}
let w : [x: term, v: value x |- value (succ (succ x))] =
        [x: term, v: value x |- v_succ (v_succ v)];
\end{lstlisting}

The right hand side can be read as: Assuming \lstinline!x: term! and
\lstinline!v: value x! (i.e. \lstinline!v! is a derivation that states that
\lstinline!x! is a value), then \lstinline!v_succ (v_succ v)! is the witness for
the fact that \lstinline!succ (succ x)! is a value. On paper, we usually omit
$\vdash$ if there are no assumptions, i.e. the objects or derivations we
describe are closed.

We can similarly encode the small-step relation $M \Steps N$  between the terms
$M$ and $N$ using the type family/relation \lstinline!step!.

\begin{lstlisting}
LF step : term -> term -> type =
| e_if_true      : step (if_then_else true M2 M3) M2
| e_if_false     : step (if_then_else false M2 M3) M3
| e_pred_zero    : step (pred z) z
| e_pred_succ    : value V
                   -> step (pred (succ V)) V
| e_iszero_zero  : step (iszero z) true
| e_iszero_succ  : value V
                   -> step (iszero (succ V)) false
| e_if_then_else : step M1 M1'
                   -> step (if_then_else M1 M2 M3) (if_then_else M1' M2 M3)
| e_succ         : step M N
                   -> step (succ M) (succ N)
| e_pred         : step M N
                   -> step (pred M) (pred N)
| e_iszero       : step M N
                   -> step (iszero M) (iszero N)
;
\end{lstlisting}

Next, we show a few examples of how to encode and represent derivations that a
concrete term steps to another.

\begin{lstlisting}
let e1 : [|- step (pred (succ (pred z))) (pred (succ z))] =
         [|- e_pred (e_succ e_pred_zero)] ;

let e2 : [|- step (pred (succ z)) z] = [|- e_pred_succ v_z] ;
\end{lstlisting}

Here \lstinline!e1! stands for the derivation

\[
\begin{array}{c}
\infer[\EPred]{(\tmpred {(\tmsucc {(\tmpred {\tmzero})})}) \Steps (\tmpred {(\tmsucc {\tmzero})})}
{\infer[\ESucc]{(\tmsucc {(\tmpred {\tmzero})}) \Steps (\tmsucc {\tmzero} )}
 {\infer[\EPredZ]{(\tmpred {\tmzero}) \Steps \tmzero}{}}
}
\end{array}
\]

The name \lstinline!e2! stands for the derivation consisting of only
the rule $\EPredSucc$.

\section{Typing}\label{sec:types-basic}

Types allow us to approximate the runtime behaviour of programs. Types classify
expressions according to their values, i.e. the values they compute. In our
simple language with arithmetic and boolean expressions, we have only two types,
namely $\Bool$ and $\Nat$, corresponding to the two kinds of values.
\[
\begin{array}{lll}
\mbox{Types} & T \bnfas & \Bool \mid \Nat
\end{array}
\]

We encode these types in \beluga using the LF type \lstinline!tp! together with
two constants \lstinline!bool! and \lstinline!nat!.

\begin{lstlisting}
LF tp : type =
| bool : tp
| nat : tp
;
\end{lstlisting}

Typing rules relate terms to types and are described by the typing judgment
$M : T$. We recall here the typing rules from \cite{TAPL}.

\[
\begin{array}{c}
\multicolumn{1}{l}{\fbox{$M \hastype T$}: \mbox{Term $M$ has type $T$}}
\\[1em]
\infera{\TTrue} {\tmtrue  \hastype \Bool}{} \qquad
\infera{\TFalse}{\tmfalse \hastype \Bool}{} \qquad
\infera{\TZero}{\tmzero \hastype \Nat}{}
\\[1em]
\inferaaa{\TIf}{\tmif{M_1}{M_2}{M_3} \hastype T}{M_1 \hastype \Bool}{M_2 \hastype T}{M_3 \hastype T}
\\[1em]
\infera{\TSucc}{\tmsucc M \hastype \Nat}{M \hastype \Nat} \qquad
\infera{\TPred}{\tmpred M \hastype \Nat}{M \hastype \Nat} \qquad
\infera{\TIsZero}{\tmiszero M \hastype \Bool}{M \hastype \Nat}
\end{array}
\]


The typing relation between terms and types is encoded in \beluga using a
predicate (type family) \lstinline!hastype! which is declared with
\lstinline!term -> tp -> type!. Each typing rule corresponds to a constructor in
our definition.

\begin{lstlisting}
LF hastype : term -> tp -> type =
| t_true   : hastype true bool
| t_false  : hastype false bool
| t_zero   : hastype z nat

| t_if     : hastype M1 bool -> hastype M2 T -> hastype M3 T
             -> hastype (if_then_else M1 M2 M3) T

| t_succ   : hastype M nat
             -> hastype (succ M) nat
| t_pred   : hastype M nat
             -> hastype (pred M) nat
| t_iszero : hastype M nat
             -> hastype (iszero M) bool
;
\end{lstlisting}

\chapter{Proofs by Induction}\label{chap:proofs-basic}

We now discuss some standard properties about languages which are also discussed
in \cite{TAPL} and show how we can represent proofs of such properties as total functions that
manipulate and analyze derivation trees. In particular, we illustrate:

\begin{itemize}
\item How to represent inductive proofs about derivations
  \index{Inductive proofs about derivations} as total functions.
\item How to prove that a case is impossible.
\item How to state a property universally about terms and reason by induction on
  terms (rather than derivations).
\end{itemize}

We develop each example step-wise using the interactive programming features in
\beluga.

\section{Type Preservation}

The first property we revisit is type preservation. In particular, we write
$M : T$ and $M \Steps N$ to clearly state that we only consider closed terms.
Uere we label derivations with $\D$ and $\S$ by writing $\proofderiv{\D}{M : T}$
and $\proofderiv{\S}{M \Steps N}$ respectively.

\begin{theorem}
  If $\proofderiv{\D}{M : T}$ and $\proofderiv{\S}{M \Steps N}$ then $N : T$.
\end{theorem}
\begin{proof}
  By structural induction on the derivation $\proofderiv{\S}{M \Steps N}$. We
  consider here only a few cases.

  \begin{case}{$\S = \infera{\EPredZero}{\tmpred \tmzero \Steps \tmzero}{}$}
    $\proofderiv{\D~}{\tmpred {\tmzero} : T}$ \hfill by assumption\\
    $\proofderiv{\D'}{\tmzero : \Nat}$ \quad and \quad $T = \Nat$ \hfill by inversion using rule $\TPred$ \\
    $\proofderiv{~~~~}{\tmzero : \Nat}$ \hfill by rule $\TZero$.
  \end{case}

  \begin{case}{$\S = \infera{\EPred}{\tmpred M \Steps \tmpred N}{\above{\S '}{M \Steps N}}$}
    $\proofderiv{\D~}{\tmpred M : T}$ \hfill by assumption \\
    $\proofderiv{\D'}{M : \Nat}$ \quad and \quad $T = \Nat$ \hfill by inversion using rule $\TPred$ \\
    $\proofderiv{\F~}{N : \Nat}$ \hfill by IH using $\D'$ and $\S'$\\
    $\proofderiv{~~~~}{\tmpred N : \Nat}$ \hfill by rule $\TPred$.
  \end{case}

\end{proof}


An inductive proof as the one here can be interpreted as recursive function
where case analysis in the proof corresponds to case analysis in the program and
the appeal to the IH corresponds to making a recursive call. We also note that
we wrote $M : T$ (or $M \Steps N$ resp.), but to emphasize that both the typing
derivation and the stepping derivation are closed and do not depend on any
assumptions, we will write $\vdash M : T$ and $\vdash M \Steps N$ respectively. This
will scale as we generalize our language in Chapter \ref{chap:binders} to
include variables, functions, recursion, and other variable-binding constructs.

From a program point of view, we can read the type preservation theorem as:
``Given a typing derivation $\vdash M : T$ and a derivation for
$\vdash M \Steps N$, we return a typing derivation $\vdash N : T$.''

We begin by translating and representing the actual theorem statement
in \beluga. This is straightforward keeping in mind that:

\begin{center}
\begin{tabular}{l|l}
On paper judgment~~ & ~~Type in \beluga \\
\hline
$\vdash M : T$      & \lstinline![|- hastype M T]! \\
$\vdash M \Steps N$ & \lstinline![|- step M N]! \\
\end{tabular}
\end{center}

\begin{lstlisting}
rec tps: [|- hastype M T] -> [|- step M N] -> [|- hastype N T] = ? ;
\end{lstlisting}

Note that \lstinline!->! is overloaded. We have used it so far in defining the
type families \lstinline!hastype!, \lstinline!step!, \lstinline!value!, and the
type \lstinline!term!. The arrow in these definitions corresponded to
the line we draw when we write an inference rule to distinguish between the
premises and the conclusion. We were merely using the arrow to define syntactic
structures.

In \beluga, we strictly separate between the objects we are
constructing (such as derivation trees, terms, etc.) and proofs about
them. The type preservation statement \emph{makes a claim about the type of
the term we obtain when taking a single step}. In the type of the function \lstinline!tps! the
function type \lstinline!->! is much stronger; it for example allows us to write
recursive functions which analyze objects of type \lstinline![|-hastype M T]! and
\lstinline![|-step M M']! by pattern matching.

Lastly, note how we wrote \lstinline!?!. This is very useful when developing and
debugging proofs/programs, since it allows us to describe incomplete
proofs/programs and have \beluga print back to us the assumptions at
that given point and the goal which needs to be proven.
Let's fill in some of the details.

\paragraph{Introducing assumptions - Writing functions} Since we are proving an
implication, we introduce two assumptions \lstinline!d: [|-hastype M T]! and
\lstinline!s: [|-step M N]! and try to establish \lstinline![|-hastype N T]!.
From a programmer's point of view, we need to build a function that when given
\lstinline!d: [|-hastype M T]! and \lstinline!s: [|-step M N]! returns a
derivation of type \lstinline![|-hastype N T]!. We use a concrete syntax similar
to ML-like languages, writing:

\begin{lstlisting}
rec tps: [|- hastype M T] -> [|- step M N] -> [|- hastype N T] =
fn d => fn s => ? ;
\end{lstlisting}

\paragraph{Case analysis - Pattern matching} Next, we split the proof into
different cases analyzing $\proofderiv{\S}{M \Steps N}$. This corresponds to
pattern matching on \lstinline!s: [|-step M N]! in our program.

\begin{lstlisting}
fn d => fn s => case s of
| [|- e_if_true]         => ?
| [|- e_if_false]        => ?
| [|- e_if_then_else S'] => ?
| [|- e_pred_zero]       => ?
| [|- e_pred_succ _]     => ?
| [|- e_iszero_zero]     => ?
| [|- e_iszero_succ _ ]  => ?
| [|- e_pred S']         => ?
| [|- e_succ S']         => ?
| [|- e_iszero S']       => ?
;
\end{lstlisting}

\index{Underscore}
We sometimes use \lstinline!_! (underscore) for an argument if we do not need a
name for it, since it does not play a role in the proof. For example, when
representing $\S = \infera{\EPredSucc}{V \Value}{\tmpred ({\tmsucc V}) \Steps V}$
we simply write \lstinline![|-e_pred_succ _]! since the sub-derivation
representing $V \Value$ is not used in proving that types are preserved.
\\[1em]
\emph{Convention:} Variables describing sub-derivations, i.e. variables
occurring inside \lstinline![],! must be upper-case. Variables describing
proper assumptions in the proof, i.e. variables introduced by
\lstinline!fn!-abstraction, must be lower case.

\paragraph{Proving - Programming} Let us now implement the two cases in the type
preservation proof we discussed earlier. We start with the case
\lstinline![e_pred_zero]! which corresponds to the base case in our proof.
Pattern matching in \lstinline!s! has not only generated all the cases, but more
importantly it has refined what \lstinline!M! and \lstinline!N! stand for. In
this particular case, \lstinline!M = (pred z)! and \lstinline!N = z!. As a first
step in the proof, we analyzed the assumption
\lstinline!d: [|-hastype (pred z) T]! further. We case-analyzed this assumption
and we stated ``by inversion on $\TPred$'' which indicated that there was
exactly one case.

While we can write another case-expression analyzing \lstinline!d! in the proof,
\beluga provides syntactic sugar for case-expressions with one case; instead of
writing

\noindent
\lstinline!case d of [ |- t_pred D'] => ? ! we simply write
\lstinline!let [ |- t_pred D'] = d in ?!.

\noindent
We now have learned that \lstinline!T = nat!.

\begin{lstlisting}
rec tps: [|- hastype M T] -> [|- step M N] -> [|- hastype N T] =
fn d => fn s => case s of
| [|- e_if_true]         => ?
| [|- e_if_false]        => ?
| [|- e_if_then_else S'] => ?
| [|- e_pred_zero]       =>
  let [|- t_pred _ ] = d in ?
| [|- e_pred_succ _]     => ?
| [|- e_iszero_zero]     => ?
| [|- e_iszero_succ _ ]  => ?
| [|- e_pred S']         => ?
| [|- e_succ S']         => ?
| [|- e_iszero S']       => ?
;
\end{lstlisting}

\beluga will compile this partial program and print for the hole

\begin{lstlisting}
________________________________________________________________________________
- Meta-context: .
________________________________________________________________________________
- Context:
          tps: [ |-hastype M T] -> [ |-step M N] -> [ |-hastype N T]
          d: [ |-hastype (pred z) nat]
          s: [ |-step (pred z) z]

================================================================================
 - Goal: [ |-hastype z nat]
\end{lstlisting}

We now need to build an object that has type \lstinline![|- hastype z nat]!.
This can simply be achieved by providing \lstinline![|- t_zero]!.

For the step case where we considered \lstinline!s: [|- e_pred S']!,
we also proceeded by analyzing \lstinline!d: [|- hastype (pred M') T]! by pattern
matching. There is only one constructor that could have been used to build
\lstinline!d! and we hence know that it must be of the form
\lstinline![ |-t_pred D']! where \lstinline!D'! stands for a derivation
\lstinline![|- hastype N' nat]!, and we learn that \lstinline!T = nat!.

We then appeal to the induction hypothesis in the proof using \lstinline!S'!
and \lstinline!D'!. This corresponds to making a recursive call
\lstinline!tps [|- D'] [|- S']! and we name the resulting derivation
\lstinline![|- F]!. Finally, we construct our derivation
\lstinline![|- t_pred F]! for \lstinline![|- hastype (pred N') nat]!.

\begin{lstlisting}
rec tps: [|- hastype M T] -> [|- step M N] -> [|- hastype N T] =
fn d => fn s => case s of
| [|- e_if_true]         => ?
| [|- e_if_false]        => ?
| [|- e_if_then_else S'] => ?
| [|- e_pred_zero]       =>
  let [|- t_pred _ ] = d in [ |-t_zero]
| [|- e_pred_succ _]     => ?
| [|- e_iszero_zero]     => ?
| [|- e_iszero_succ _ ]  => ?
| [|- e_pred S']         =>
  let [|- t_pred D'] = d in
  let [|- F] = tps [ |-D'] [ |-S'] in
    [|- t_pred F]
| [|- e_succ S']         => ?
| [|- e_iszero S']       => ?
;
\end{lstlisting}

\paragraph{When is a program a proof?} So far we have just written a functional
program; for it to be a proof it needs to be a total function, i.e. it must be
defined on all inputs and it must be terminating. We can check that the function
is total in \beluga by writing the following annotation before
the function body: \lstinline!/ total s (tps m t n d s) /!. This
annotation states that we claim to implement program \lstinline!tps! that is
recursive in \lstinline!s!. Since in the theorem statement we implicitly quantify over
terms \lstinline!M! and \lstinline!N! as well as the type \lstinline!T! at the
outside, we write in the totality\index{Totality} declaration
\lstinline!(tps m t n d s)! indicating that we are recursively analyzing the fifth
argument (the first three are implicit) passed to \lstinline!tps!. The
order in which the implicit arguments are listed is irrelevant; what is
important is that their number is correct. The full proof is then written as
follows:
\todo{I'm not really sure I would have understood the part with the implicit
arguments. Maybe we should explain a little bit more about what these implicit
arguments are? -nj
I thought it seemed clear the first reading (having never really used a proof
assistant before). -ah}

\begin{lstlisting}
rec tps: [|- hastype M T] -> [|- step M N] -> [|- hastype N T] =
/ total s (tps m t n d s) /
fn d => fn s => case s of
| [|- e_if_true] =>
  let [|- t_if D D1 D2] = d in [|-D1]
| [|- e_if_false] =>
  let [|- t_if D D1 D2] = d in [|-D2]
| [|- e_if_then_else S] =>
  let [|- t_if D D1 D2] = d in
  let [|-D'] = tps [|-D] [|-S] in
  [|- t_if D' D1 D2]
| [|- e_pred_zero] =>
  let [|-t_pred _ ] = d in  [|-t_zero]
| [|- e_pred_succ _ ] =>
  let [|-t_pred (t_succ D) ] = d in [|-D]
| [|- e_iszero_zero] =>
  let [|-t_iszero _] = d in [|-t_true]
| [|- e_iszero_succ _ ] =>
  let [|-t_iszero _] = d in [|-t_false]
| [|- e_pred S] =>
  let [|-t_pred D] = d in
  let [|-D'] = tps [|-D] [|-S] in
  [|- t_pred D']
| [|-e_succ S] =>
  let [|-t_succ D] = d in
  let [|-D'] = tps [|-D] [|-S] in
  [|-t_succ D']
| [|-e_iszero S] =>
  let [|-t_iszero D] = d in
  let [|-D'] = tps [|-D] [|-S] in
  [|-t_iszero D']
;
\end{lstlisting}

The full proof can be found online in the example directory corresponding to
this chapter (see \verb|Part1/type-preservation.bel|).

\section{Uniqueness of Small-Step Evaluation}\label{sec:unique-eval}

Next, we consider the proof that evaluation using the small-step rules yields a
unique value. This is an interesting proof because we must argue that values do
not step, i.e. there are no rules that apply. For \lstinline!z!,
\lstinline!true! and \lstinline!false! this should be easy, since there is no
rule that applies. But how do we argue that \emph{every number} that is a value
does not step? We prove a contradiction. We show inductively that if $M$ is a
value and $M \Steps N$ then we can derive falsehood\index{Falsehood}
(written as $\bot$).

\begin{theorem}
If $\proofderiv{\S}{M \Steps N}$ and $\proofderiv{\V}{M \Value}$ then $\bot$.
\end{theorem}
\begin{proof}
By structural induction on the derivation $\proofderiv{\V}{M \Value}$.

\begin{basecase}{$\V = \ianc{}{\tmzero \Value}{}$}
$\proofderiv{\S}{\tmzero \Steps N}$ \hfill by assumption \\
By inspecting all the existing rules, there exists no $N$. Therefore, this
assumption is false, and from false we can derive anything; in particular, we
can conclude $\bot$.
\end{basecase}

\begin{stepcase}{$\V = \ianc{\above{\V'}{M' \Value}}{(\tmsucc M') \Value}{}$}
$\proofderiv{\S~}{(\tmsucc M') \Steps N}$ \hfill by assumption \\
$\proofderiv{\S'}{M' \Steps N'}$ \quad and \quad $N = (\tmsucc N')$ \hfill by inversion using $\ESucc$\\
$\bot$ \hfill by i.h. using $\S'$ and $\V'$
\end{stepcase}

\end{proof}

How do we model in a programming environment $\bot$ (falsehood)? In a
dependently typed language, we model $\bot$ indirectly. Recall that
there is no way to, for example, construct an element of the type
\lstinline!step z z!.  If we think of the set of elements belonging to the
type \lstinline!step M N!, then \lstinline!step z z! is not in it, but
for example \lstinline!step (pred z) z! is; so is
\lstinline!step (succ (pred z)) (succ z)!. Generally speaking, if we
define no elements belonging to a type, then the type is guaranteed to be empty
and models false. In \beluga, we can define types without elements simply by
declaring a type.

\begin{lstlisting}
not_possible: type.
\end{lstlisting}

We then can translate the theorem directly into a computation-level type in
\beluga; we have also included the totality \index{Totality} declaration,
stating that this function is recursively defined on values, i.e. objects of type
\lstinline![|- value M]!.

\begin{lstlisting}
rec values_dont_step : [|- step M N] -> [|- value M] -> [|- not_possible] =
/ total v (values_dont_step m n s v) /
?
;
\end{lstlisting}

As before, we introduce the assumption \lstinline!s! for
\lstinline![|- step M N]! and \lstinline!v! for
\lstinline![|- value M]!. Then we case-analyze \lstinline!v!.

\begin{lstlisting}
rec values_dont_step : [|- step M N] -> [|- value M] -> [|- not_possible] =
/ total v (values_dont_step m n s v) /
fn s => fn v => case v of
| [|- v_true]    => ?
| [|- v_false]   => ?
| [|- v_z ]      => ?
| [|- v_succ V'] => ?
;
\end{lstlisting}

Let's consider the case \lstinline![|- v_z] : [|- value zero]!. We argued in the
proof: ``By inspecting all the existing rules, there exists no $N$.'' This
corresponds to case-analyzing \lstinline!s!; however, there are no cases. In
\beluga, we write \lstinline!impossible s! for splitting \lstinline!s! in
the empty context. It is effectively a case-expression without branches.

For the step-case, the translation of the proof to a program is more
straightforward: the inversion in the proof is translated to analyzing
\lstinline!s!, and the appeal to the induction hypothesis corresponds to making a
recursive call.

\begin{lstlisting}
rec values_dont_step : [|- step M N] -> [|- value M] -> [|- not_possible] =
/ total v (values_dont_step m n s v) /
fn s => fn v => case v of
| [|- v_true]    => impossible s
| [|- v_false]   => impossible s
| [|- v_z ]      => impossible s
| [|- v_succ V'] => let [|- e_succ S'] = s in values_dont_step [|- S'] [|- V']
;
\end{lstlisting}

One may wonder whether we can ever actually execute and run this program; the
answer is no, since there is no way to provide a derivation
\lstinline![|- step M N]! and at the same time a proof \lstinline![|- value M]!.

We are now ready to prove that evaluation yields a unique result given the
small-step semantics. This will illustrate how we can use the lemma
\lstinline!values_dont_step!. We only show two cases, but the whole program is
available in the example directory corresponding to this chapter
(see \verb|Part1/unique.bel|).

\begin{lstlisting}
LF equal: term -> term -> type =
| ref: equal T T;


rec unique : [|- step M M1] -> [|- step M M2] -> [|- equal M1 M2] =
/ total s1 (unique m m1 m2 s1 s2) /
fn s1 => fn s2 => case s1 of
| [|- e_if_true] =>
  (case s2 of
   | [|- e_if_true]        => [|- ref]
   | [|- e_if_then_else D] => impossible values_dont_step [|- D] [|- v_true] )

| [|- e_if_false] =>
  (case s2 of
   | [|- e_if_false]       => [|- ref]
   | [|- e_if_then_else D] => impossible values_dont_step [|- D] [|- v_false] )

| [|- e_if_then_else D] =>
  (case s2 of
  | [|- e_if_true]        => impossible values_dont_step [|- D] [|- v_true]
  | [|- e_if_false]       => impossible values_dont_step [|- D] [|- v_false]
  | [|- e_if_then_else E] => let [|- ref] = unique [|- D] [|- E] in  [|- ref] )

| [|- e_succ D]        => ?
| [|- e_pred_zero]     => ?
| [|- e_pred_succ V]   => ?
| [|- e_pred D]        => ?
| [|- e_iszero_zero]   => ?
| [|- e_iszero_succ V] => ?
| [|- e_iszero D]      => ?
;
\end{lstlisting}

Let us consider the case where \lstinline!s1! is a derivation ending in
\lstinline![|- e_if_true]!, i.e. \lstinline!s1! stands for a derivation of
\lstinline![|- step (if_then_else true N1 N2) N1]!. At this point we know that \lstinline!s2! stands
for a derivation of \lstinline![|- step (if_then_else true N1 N2) M2]!. Splitting
\lstinline!s2! into cases gives us two sub-cases:
\begin{enumerate}
\item We have used the rule
\lstinline!e_if_true!. In this case, we learn that
\lstinline!M2 = N1!. Clearly, we can conclude \lstinline![|- equal N1 N1]! by
using \lstinline![|- ref]! as a witness.

\item We have used the rule \lstinline!e_if_then_else!. In this case, we have a
  sub-derivation \lstinline!D! that stands for \lstinline![|- step true N']! and \lstinline!M2 = (if_then_else N' N1 N2)!.
We now use the lemma \lstinline!values_dont_step!, passing \lstinline![|- D]! and \lstinline![|- v_true]! (a witness
for \lstinline![|- value true]!).
We therefore obtain an object of type \lstinline![|- not_possible]!; but no
elements of this type exist. This case is hence impossible.
\end{enumerate}

Next, consider the case where \lstinline!s1! is a derivation ending in
\lstinline![|- e_if_then_else D]!, i.e. \lstinline!s1! has type
\lstinline![|- step (if_then_else N N1 N2) (if_then_else N' N1 N2)]!. Hence \lstinline!D! stands for the sub-derivation
\lstinline![|- step N N']!. At this point we know that \lstinline!s2! stands
for a derivation \lstinline![|- step (if_then_else N N1 N2) M2]!. Splitting
\lstinline!s2! into cases gives us three sub-cases:

\begin{enumerate}
\item We have used the rule \lstinline!e_if_true!. As a consequence
  \lstinline!N = true! and \lstinline!M2 = N1!. Moreover,
  \lstinline!D! now stands for the sub-derivation \lstinline![|-step true N']!.
  Using again the lemma \lstinline!values_dont_step!, we show that this is impossible.

\item We have used the rule \lstinline!e_if_false!. This case is
  similar to the above.

\item We have used the rule \lstinline!e_if_then_else! and
  \lstinline!s2! stands for the derivation tree
\mbox{\lstinline![|- e_if_then_else E]!} where \lstinline!E! stands for a sub-derivation
\lstinline![|- step N N'']! and \lstinline!M2 = (if_then_else N'' N1 N2)!.
We now make a recursive call on the sub-derivations \lstinline!D! and
\lstinline!E!, i.e. \lstinline!unique [|- D] [|- E]!, which gives us a
witness for
\mbox{\lstinline![|- equal N' N'']!}. By inversion using \lstinline!ref!, we learn that
\lstinline!N' = N''!. To conclude the proof we thus need to provide a witness for
\lstinline![|- equal (if_then_else N' N1 N2) (if_then_else N' N1 N2)]!. This is easily
accomplished by \lstinline![|- ref]!. \\[0.5em]
It might look like we should be able to simply make a recursive call
and be done. This is
however a fallacy, since the type is incorrect. Recall that \lstinline!ref!
takes in an implicit argument for the term we are actually comparing; therefore
in the first occurrence \lstinline![|- ref]! actually stands for
\lstinline![|- ref <<N'>>]!, while in the second occurrence it
stands for \lstinline![|- ref <<(if_then_else N' N1 N2)>>]!.\index{Implicit Arguments}
\end{enumerate}



\section{Termination of Well-Typed Terms}\label{sec:termination}

Our goal is to prove that the evaluation of well-typed terms always halts. In
fact we haven already proven progress, i.e. evaluation cannot get stuck on
well-typed terms: either a well-typed term yields a value or we
can take another step. In this section we prove that we can always
evaluate a well-typed term to a final value.

\begin{theorem}\label{halts}
If $\proofderiv{\D}{M : T}$ then $M \Halts$, i.e.~there exists a value $V$ s.t. $M
\MSteps V$.
\end{theorem}

We recap our definition of multi-step relations that was the
reflexive, transitive closure over the single step relation.

\[
\begin{array}{c@{\qquad}c@{\qquad}c}
\infer[\MRef]{M \MSteps M}{} &
\infer[\MTr]{M \MSteps M'}{M \MSteps N & N \MSteps M'} &
\infer[\MStep]{M \MSteps M'}{M \Steps M'}
\end{array}
\]

\begin{lstlisting}
LF multi_step : term -> term -> type =
| ms_ref  : multi_step M M
| ms_tr   : multi_step M N -> multi_step N M'
            -> multi_step M M'
| ms_step : step M M'
            -> multi_step M M'
;
\end{lstlisting}

Clearly evaluation of a term $M$ may not yield a value in a single step; in fact we may need to chain multiple steps together.
In the proof for showing that well-typed terms terminate, we will see the need for lemmas that justify bigger steps when we evaluate a term.

\begin{lemma}[Multi Step Lemmas]~\label{lem:multi-step}
  \begin{enumerate}
  \item If $M \MSteps M'$ then $(\tmpred M) \MSteps (\tmpred M')$.
  \item If $M \MSteps M'$ then $(\tmsucc M) \MSteps (\tmsucc M')$.
  \item If $M \MSteps M'$ then $(\tmiszero M) \MSteps (\tmiszero M')$.
  \item If $M \MSteps M'$ then $(\tmif M {M_1} {M_2}) \MSteps (\tmif {M'} {M_1} {M_2})$.
  \end{enumerate}
\end{lemma}
\begin{proof}
By structural induction  on $\proofderiv{\S}{M \MSteps M'}$.  We'll only
show the proof of the last
proposition. By definition of $\MSteps$, we consider three cases:

\begin{basecase}{$\S = \ianc{M \Steps M'}{M \MSteps M'}{\MStep}$}
$\tmif{M}{M_1}{M_2} \Steps \tmif{M'}{M_1}{M_2}$ \hfill by rule $\EIf$ \\
$\tmif{M}{M_1}{M_2} \MSteps \tmif{M'}{M_1}{M_2}$ \hfill by rule $\MStep$
\end{basecase}

\begin{basecase}{$\S = \ianc{}{M \MSteps M}{\MRef}$}
$\tmif{M}{M_1}{M_2} \longrightarrow^* \tmif{M'}{M_1}{M_2}$ \hfill
by rule $\MRef$
\end{basecase}

\begin{stepcase}{$\S = \ibnc{\above{\S_1}{M \MSteps N}}{\above{\S_2}{N \MSteps M'}}{M \MSteps M'}{\MTr}$}
$\tmif{M}{M_1}{M_2} \MSteps \tmif{N}{M_1}{M_2}$ \hfill by I.H. on $\S_1$\\
$\tmif{N}{M_1}{M_2} \MSteps \tmif{M'}{M_1}{M_2}$ \hfill by I.H. on $\S_2$\\
$\tmif{M}{M_1}{M_2} \MSteps \tmif{M'}{M_1}{M_2}$ \hfill by rule $\MTr$  \\
\end{stepcase}
\end{proof}

How would we mechanize this proof in \beluga? This may seem
straightforward, but there are some subtleties. In the last statement,
we say

\begin{center}
If $M \MSteps M'$ then $(\tmif M {M_1} {M_2}) \MSteps (\tmif {M'} {M_1} {M_2})$.
\end{center}

It is important to realize that $M$, $M'$, $M_1$, and $M_2$ are all
universally quantified.  When we appeal to the induction hypothesis on
$\S_1$ we in fact instantiate and choose the appropriate $M_1$ and
$M_2$. It might be more precise to rewrite the statement to make this clearer.

\begin{center}
If $M \MSteps M'$, then for all $M_1$ and $M_2$, $(\tmif M {M_1} {M_2}) \MSteps (\tmif {M'} {M_1} {M_2})$.
\end{center}

Mechanizing proofs highlights such subtleties and forces us to
understand them and be more precise than in the on paper proof. We can
now translate the statement and the proof into
\beluga straightforwardly. We make the quantification in the
statement explicit by writing \lstinline!{M1: [|- term}{M2: [|- term}!. In the
program, we use \lstinline!mlam!-abstraction as the corresponding
proof term for introducing a universal quantifier.\index{Universal
  quantification}\index{Explicit Arguments}

\begin{lstlisting}
rec mstep_if_then_else : [|- multi_step M M'] ->
   {M1: [|- term]}{M2: [|- term]}
   [|- multi_step (if_then_else M M1 M2) (if_then_else M' M1 M2)] =
/ total ms (mstep_if_then_else m m' ms m1 m2)/
fn ms => case ms of
| [|- ms_ref ]     => mlam M1 => mlam M2 => [|- ms_ref]
| [|- ms_step S]   => mlam M1 => mlam M2 => [|- ms_step (e_if_then_else S)]
| [|- ms_tr S1 S2] => mlam M1 => mlam M2 =>
  let [|- S1'] = mstep_if_then_else [|- S1] [|- M1] [|- M2] in
  let [|- S2'] = mstep_if_then_else [|- S2] [|- M1] [|- M2] in
  [|- ms_tr S1' S2']
;
\end{lstlisting}


Let us return to the goal of this section, namely of proving that the
evaluation of a well-typed term always terminates. To prove this statement, we
need an additional lemma which justifies that the multi-step relation
preserves types.

\begin{lemma}[Type preservation for multi-step relation]
If $M : T$ and $M \MSteps M'$ then $M':T$.
\end{lemma}
\begin{proof}
By structural induction on $M \MSteps M'$, using type preservation for the single-step relation.
\end{proof}

Finally, we are ready to consider the proof that the evaluation of a well-typed term
always terminates. We first define $M \Halts$ as follows:

\[
\begin{array}{c}
\infer{M \Halts}{M \MSteps V & V \Value }
\end{array}
\]

Note that we are encoding existential quantification \index{Existential quantification} in the proposition ``there exists a value
$V$ s.t. $M \MSteps V$'' in the theorem by defining a separate judgment
$M \Halts$. This trick allows us to turn an existential into a
universal quantifier, as the rule can be read as: For all $M$, $V$, if
$M \MSteps V$ and $V \Value$ then $M \Halts$.

We can now proceed with a proof of Theorem \ref{halts}.


\begin{proof}
By structural induction on $\proofderiv{\D}{M : T}$. We show a few
representative cases.

\begin{case}{$\D = \ianc{}{ \tmzero :\Nat}{\TZero}$}
$\tmzero \MSteps \tmzero$ \hfill by $\MRef$\\
$\tmzero \Value$ \hfill by $\VZero$ rule \\
$\tmzero \Halts$ \hfill by definition of $\Halts$
\end{case}

\begin{case}{$\D = \ianc{\above{\D'}{ N : \Nat}}{ (\tmpred N) : \Nat}{\TPred}$}
$N \Halts$, i.e. $\exists V.$ s.t.$~\V'::V\Value$ ~~and~~ $\S'::N \MSteps V$ \hfill by I.H. $\D'$\\[1em]
%
\fbox{To Prove: ~~~$M\Halts$, i.e. $\exists W.$ s.t. $W \Value$ ~~and~~ $\S :: \tmpred N \MSteps W$}\\[1em]
%
\begin{subcase}{$\V' = \ianc{}{\tmzero \Value}{\VZero}$ \quad and \quad $V = \tmzero$}
$\proofderiv{\S'}{N \MSteps \tmzero}$ \hfill restating assumption $\S'$\\
$\proofderiv{\S_0}{\tmpred N \MSteps \tmpred \tmzero}$ \hfill by lemma mstep-pred \\
$\proofderiv{\S_1}{\tmpred \tmzero \MSteps \tmzero}$ \hfill by $\MStep$ using $\EPredZ$\\
$\proofderiv{\S}{\tmpred N \MSteps \tmzero}$ \hfill by $\MTr$ using $\S_0$ and $\S_1$\\
$\exists W$.s.t.$W \Value$ ~~and~~ $\S::~\tmpred N \MSteps W$ \hfill by choosing
$W = \tmzero$\\
$(\tmpred N)\Halts$ \hfill by definition of ${\!}\Halts$\\[1em]
\end{subcase}
%
\noindent
\begin{subcase}{$\V' = \ianc{\above{\W}{V'\Value}}{(\tmsucc V') \Value}{\VSucc}$ \quad and \quad $V = \tmsucc V'$}
$\proofderiv{\S'}{N \MSteps \tmsucc V'}$ \hfill restating assumption $\S'$\\
$\proofderiv{\S_0}{\tmpred N \MSteps \tmpred (\tmsucc V')}$ \hfill by lemma mstep-pred \\
$\proofderiv{\S_1}{\tmpred (\tmsucc V') \MSteps V'}$ \hfill by $\MStep$ using $\EPredSucc$ and $\W$\\
$\proofderiv{\S}{\tmpred N \MSteps V'}$ \hfill by $\MTr$ using $\S_0$ and $\S_1$\\
$\exists W$.s.t.$W \Value$ ~~and~ ~$\S::~\tmpred N \MSteps W$ \hfill by choosing
$W = V'$\\
$\tmpred N\Halts$ \hfill by definition of ${\!}\Halts$\\[1em]
\end{subcase}
%
\noindent
\begin{subcase}{$\V' = \ianc{}{\tmtrue \Value}{\VTrue}$ \quad and \quad  $V = \tmtrue$}
$\proofderiv{\S'}{N \MSteps \tmtrue}$ \hfill restating assumption $\S'$\\
$\proofderiv{\F}{\tmtrue : \Nat}$ \hfill by type preservation for multi-step relations using $\D'$\\
$~~~ \bot$ \hfill \\[1em]
\end{subcase}
%
\noindent
\begin{subcase}{$\V' = \ianc{}{\tmfalse \Value}{\VFalse}$ \quad and \quad $V = \tmfalse$}
Similar to the case where $V = \tmtrue$.
\end{subcase}
\end{case}

\begin{case}{$\D = \icnc{\above{\D_1}{M_1 \hastype \Bool}}{\above{\D_2}{M_2 \hastype T}}{\above{\D_3}{M_3 \hastype T}}{\tmif{M_1}{M_2}{M_3} \hastype T}{\TIf}$}
$M_1 \Halts$, i.e. $\exists V.$ s.t. $\V' :: V \Value$ ~~and~~ $\S' :: M_1 \MSteps V$ \hfill by I.H. $\D_1$ \\[1em]
%
\fbox{To Prove: ~~~$M\Halts$, i.e. $\exists W.$ s.t. $W \Value$ ~~and~~ $\S :: (\tmif{M_1}{M_2}{M_3}) \MSteps W$} \\[1em]
%
\begin{subcase}{$\V' = \ianc{}{\tmtrue \Value}{\VTrue}$ \quad and \quad $V = \tmtrue$}
$\proofderiv{\S_0}{\tmif{M_1}{M_2}{M_3} \MSteps \tmif{\tmtrue}{M_2}{M_3}}$ \hfill by lemma mstep-if \\
$\proofderiv{\S_1}{\tmif{\tmtrue}{M_2}{M_3} \MSteps M_2}$ \hfill by $\MStep$ using $\EIfTrue$ \\
$\proofderiv{\S_2}{\tmif{M_1}{M_2}{M_3} \MSteps M_2}$ \hfill by $\MTr$ using $\S_0$ and $\S_1$ \\
$M_2 \Halts$, i.e. $\exists V_2.$ s.t. $\V_2 :: V_2 \Value$ ~~and~~ $\S_3 :: M_2 \MSteps V_2$ \hfill by I.H. $\D_2$ 
$\proofderiv{\S}{\tmif{M_1}{M_2}{M_3} \MSteps V_2}$ \hfill by $\MTr$ using $\S_2$ and $\S_3$ \\
$\exists W.$ s.t. $W \Value$ ~~and~~ $\proofderiv{\S}{\tmif{M_1}{M_2}{M_3} \MSteps W}$ \hfill by choosing $W = V_2$ \\
$\tmif{M_1}{M_2}{M_3} \Halts$ \hfill by definition of ${\!}\Halts$
\end{subcase}\\[1em]
%
\begin{subcase}{$\V' = \ianc{}{\tmfalse \Value}{\VFalse}$ \quad and \quad $V = \tmfalse$}
Similar to the case where $V = \tmtrue$.
\end{subcase}\\[1em]
%
\begin{subcase}{$\V' = \ianc{}{\tmzero \Value}{\VZero}$ \quad and \quad $V = \tmzero$}
$\proofderiv{\S'}{M_1 \MSteps \tmzero}$ \hfill restating assumption $\S'$ \\
$\proofderiv{\F}{\tmzero : \Bool}$ \hfill by type preservation for multi-step relations using $\D_1$ \\
$~~~ \bot$
\end{subcase}\\[1em]
%
\begin{subcase}{$\V' = \ianc{\above{\W}{V'\Value}}{(\tmsucc V') \Value}{\VSucc}$ \quad and \quad $V = \tmsucc V'$}
Similar to the case were $V = \tmzero$.
\end{subcase}
\end{case}

\end{proof}


We now discuss how to mechanize this proof as a program. As a first step, we
must encode the statement of the theorem as a type.

\begin{lstlisting}
LF halts: term -> type =
| result: multi_step M V -> value V
          -> halts M;

rec terminate : [|- hastype M T] -> [|- halts M] =
/ total d (terminate m t d)/
fn d => ? ;
\end{lstlisting}

Again we encode the case analysis in the proof as a case analysis in the program
splitting on the assumption \lstinline!d!. We show below the cases we discussed
in detail above, however the full proof is implemented in the file
\lstinline!termination.bel!.

For the case where we have \lstinline!d: [|- hastype z nat]! by
\lstinline![|- t_zero]!, we return \lstinline![|- result ms_ref (v_z)]! that
stands for a proof \lstinline![|- halts z]!.

For the case where we have
\lstinline!d: [|- hastype (pred N) nat]! by \lstinline![|- t_pred D]! and
\lstinline!D! stands for a sub-derivation \lstinline![|- hastype N nat]!: by the
induction hypothesis on \lstinline!D! (i.e. modelled via the recursive call), we
obtain a proof of \lstinline![|- halts N]!.  By inversion, we know that this
proof has the shape \lstinline![|- result MS W]! where \lstinline!MS!
stands for \lstinline![|- multi_step N R]! and \lstinline!W!
stands for a proof \lstinline![|- value R]!. We now case-analyze
\mbox{\lstinline![|- value R]!}.

If \lstinline!R=z! and we have a derivation
\lstinline![|- v_z]!, we call our lemma \lstinline!mstep_pred! with
\lstinline!MS! to obtain a derivation \lstinline!MS'! for
\lstinline![|- multi_step (pred N) (pred z)]!. What remains is to build a proof
for \lstinline![|- halts (pred N)]!. First, we build a proof \lstinline![|- v_z]!
that \lstinline![|- value z]!. Second, we build a proof for
\lstinline![|- multi_step (pred N) z]! using transitivity together with
\lstinline!MS'! and the derivation \lstinline![|- ms_step e_pred_zero]! for
\mbox{\lstinline![|- multi_step (pred N) z]!}.

If \lstinline!R=succ W! and we have a derivation
\lstinline!(v_succ V)!, we call our lemma \lstinline!mstep_pred! with
\lstinline!MS! to obtain a derivation \lstinline!MS'! for
\lstinline![|- multi_step (pred N) (pred (succ W))]!. What remains is to build a proof
for \lstinline![|- halts (pred N)]! using transitivity together with
\lstinline!MS'! and the derivation
\lstinline![|- ms_step (e_pred_succ V)]!.
%for
%\mbox{\lstinline![|-multi_step (pred N) W]!}.

If \lstinline!R=true! or \lstinline!R=false! then we know by the type
preservation lemma for the multi-step relation implemented by the
function \lstinline!multi_tps! that we cannot take a step.

Finally we consider the case where we have
\lstinline!d: [|- hastype (if_then_else M M1 M2) T]! by
\lstinline![|- t_if D D1 D2]!, where
\lstinline!D! stands for a sub-derivation \lstinline![|- hastype M bool]!,
\lstinline!D1! stands for a sub-derivation \lstinline![|- hastype M1 T]!, and
\lstinline!D2! stands for a sub-derivation \lstinline![|- hastype M2 T]!. By the
induction hypothesis on \lstinline!D!, we obtain a proof for \lstinline![|- halts M]!
which has the shape \lstinline![|- result MS W]! where \lstinline!MS! stands for
\lstinline![|- multistep M R]! and \lstinline!W! stands for \lstinline![|- value R]!.
We proceed by case analysis on \lstinline![|- value R]!.

If \lstinline!R=true! and we have a derivation \lstinline![|- v_true]!, we call
our multi-step lemma \lstinline!mstep_if_then_else! with \lstinline!MS!, \lstinline!M1!, and
\lstinline!M2! to obtain a derivation \lstinline!MS0! that stands for
\lstinline![|- multi_step (if_then_else M M1 M2) (if_then_else true M1 M2)]!. By a recursive
call on \lstinline!D1!, we obtain a proof of \lstinline![|- halts M1]! that has the shape
\lstinline![|- result MS1 W']!, where \lstinline!MS1! stands for
\lstinline![|- multi_step M1 R']! and \lstinline!W'! stands for \lstinline![|- value R']!.
We build a proof for \lstinline![|- multi_step (if_then_else M M1 M2) R']! using
transitivity (along with \lstinline![|- ms_step e_if_true]!)
and combine that with \lstinline!W'! to build our proof of
\lstinline![|- halts (if_then_else M M1 M2)]!.

The case where \lstinline!R=false! proceeds similarly.

If \lstinline!R=z! or \lstinline!R=succ W!, then by the type preservation
lemma for the multi-step relation (\lstinline!multi_tps!) we cannot take a step
and so this case is impossible.

\todo{The cases for t_if are more complicated than I'd like them to be
	because the multi-step derivations like (ms_tr MS0 (ms_step e_if_true)) can't
	be factored out (presumably because M1 and M2 aren't specified in e_if_true)
	so everything needs to be done at once in the last line.
	It would be nice to make this simpler for the reader. -ah}

\begin{lstlisting}
rec terminate : [|-hastype M T] -> [ |-halts M] =
/ total d (terminate m t d)/
fn d => case d of
| [|- t_true]  => ?
| [|- t_false] => ?
| [|- t_if D D1 D2] : [|- hastype (if_then_else M M1 M2) T] =>
  (case terminate [|- D] of
  | [|- result MS v_true] =>
    let [|- MS0] = mstep_if_then_else [|- MS] [|- M1] [|- M2] in
    let [|- result MS1 W'] = terminate [|- D1] in
      [|- result (ms_tr (ms_tr MS0 (ms_step e_if_true)) MS1) W']
  | [|- result MS v_false] =>
    let [|- MS0] = mstep_if_then_else [|- MS] [|- M1] [|- M2] in
    let [|- result MS1 W'] = terminate [|- D2] in
      [|- result (ms_tr (ms_tr MS0 (ms_step e_if_false)) MS1) W']
  | [|- result MS v_z] => impossible multi_tps [|- D] [|- MS]
  | [|- result MS (v_succ V)] => impossible multi_tps [|- D] [|- MS] )
| [|- t_zero]   => [|- result ms_ref v_z]
| [|- t_succ D] => ?
| [|- t_pred D] => (case terminate [|- D] of
   | [|- result MS v_z] =>
     let [|- MS'] = mstep_pred [|- MS] in
       [|- result (ms_tr MS' (ms_step e_pred_zero)) v_z]
   | [|- result MS (v_succ V)] =>
     let [|- MS'] = mstep_pred [ |-MS] in
       [|- result (ms_tr MS' (ms_step (e_pred_succ V))) V]
   | [|- result MS v_true]  => impossible multi_tps [|- D] [|- MS]
   | [|- result MS v_false] => impossible multi_tps [|- D] [|- MS]
 )
| [|- t_iszero D] => ?
;
\end{lstlisting}

There is one very interesting aspect that arises in the
translation of the on-paper proof into the program. Revisit the line

\begin{center}
	\lstinline!| [|- t_if D D1 D2] : [|- hastype (if_then_else M M1 M2) T] =>!
\end{center}

We give a type annotation to the pattern. This is not necessary for
type reconstruction, but rather we want to be able to name the terms
\lstinline!M1! and \lstinline!M2! as we must pass them explicitly
when we use the lemma \lstinline!mstep_if_then_else!. Type annotations
can also be used in let-expressions and alternatively, we could have
written the following:

\begin{lstlisting}
| [|- t_if D D1 D2] : [|- hastype (if_then_else M M1 M2) T] =>
  let d : [|- hastype (if_then_else M M1 M2) T] = d in
  (case terminate [|- D] of
   . . .
  )
\end{lstlisting}

% \chapter{Exercise 3.5.17}

\section{Relating Small-Step and Big-Step Semantics}
\label{sec:small-to-big}
\subsection{Definition of the Big-Step semantics}

% Almost taken from TAPL:
Two styles of operational semantics are in common use. The one used so far and
most commonly used in \cite{TAPL} is called the {\em small-step} style, because
the definition of the evaluation relation shows how individual steps of
computation are used to rewrite a term, bit by bit, until it eventually becomes
a value. On top of this, we define a multi-step evaluation relation that allows
us to talk about terms evaluating (in many steps) to values. An alternative
style, called {\em big-step} semantics (or sometimes {\em natural} semantics),
directly formulates the notion of ``the term $M$ evaluates to the final value $V$'',
written $M \BSteps V$. The big-step evaluation rules for our language of
boolean and arithmetic expressions can be described as follows:

\[
\begin{array}{c@{\qquad}c}
\multicolumn{2}{l}{\fbox{$M \BSteps V$}: \mbox{Term $M$ evaluates to value $V$}}\\[1em]
  \infer[\BValue]{V \BSteps V}{V \Value} &
  \infer[\BSucc]{\tmsucc M \BSteps \tmsucc V}{M \BSteps V}
\\[0.5em]
  \infer[\BPredZero]{\tmpred M \BSteps \tmzero}{M \BSteps \tmzero} &
  \infer[\BPredSucc]{\tmpred M \BSteps V}{M \BSteps \tmsucc V}
\\[0.5em]
  \infer[\BIszeroZero]{\tmiszero M \BSteps \tmtrue} {M \BSteps \tmzero} &
  \infer[\BIszeroSucc]{\tmiszero M \BSteps \tmfalse}{M \BSteps \tmsucc V}
\\[0.5em]
  \infer[\BIfTrue] {\tmif {M_1}{M_2}{M_3} \BSteps V}{M_1 \BSteps true  & M_2 \BSteps V} &
  \infer[\BIfFalse]{\tmif {M_1}{M_2}{M_3} \BSteps V}{M_1 \BSteps false & M_3 \BSteps V} \\
\end{array}
\]

Following the previous principle of encoding judgments such as $M \BSteps V$
using predicates (type families), we define in \beluga the relation
\lstinline!bigstep! between two terms using an LF type family. In the rules, we
do not enforce that we always return a value. Rather this is a property we can
prove and often referred to as value soundness.

\begin{lstlisting}
LF bigstep : term -> term -> type =
   | b_value       : value V
		     -> bigstep V V
   | b_succ        : bigstep M V
		     -> bigstep (succ M) (succ V)

   | b_pred_zero   : bigstep M z
		     -> bigstep (pred M) z
   | b_pred_succ   : bigstep M (succ V)
		     -> bigstep (pred M) V

   | b_iszero_zero : bigstep M z
		     -> bigstep (iszero M) true
   | b_iszero_succ : bigstep M (succ V)
		     -> bigstep (iszero M) false

   | b_if_true     : bigstep M1 true  -> bigstep M2 V
		     -> bigstep (if_then_else M1 M2 M3) V
   | b_if_false    : bigstep M1 false -> bigstep M3 V
		     -> bigstep (if_then_else M1 M2 M3) V
;
\end{lstlisting}

\subsection{Value soundness}

We will now prove two interesting properties about values in the big-step semantics.
First, we prove that an expression always evaluates to a value:

\begin{lemma}[Value Soundness for the Big-step semantics]
  \label{lem:bstep-value-soundness}
  ~\\If $M \BSteps V$, then $V$ is a value.
\end{lemma}

\begin{lstlisting}
rec bstep_value : [|- bigstep M V] -> [|- value V] =
/ total b (bstep_value _ _ b) /
  fn b => case b of
  | [|- b_value E] => [|- E]
  | [|- b_succ B]  => let [|- E] = bstep_value [|- B] in [|- v_succ E]

  | [|- b_pred_zero B] => bstep_value [|- B]
  | [|- b_pred_succ B] => let [|- v_succ E] = bstep_value [|- B] in [|- E]

  | [|- b_iszero_zero B] => [|- v_true]
  | [|- b_iszero_succ B] => [|- v_false]

  | [|- b_if_true  B1 B2] => bstep_value [|- B2]
  | [|- b_if_false B1 B3] => bstep_value [|- B3]
;
\end{lstlisting}

(Note that in the totality declaration for \lstinline!bstep_value!, we
use underscores instead of naming the variables that the function
is not recursively defined on. We will continue to do this in the
future.)

Second, we  prove that evaluation yields a unique value. Note that
this is {\bf not} equivalent to saying that only the \BValue rule can
apply. For example there are two different ways of proving that
$\tmsucc \tmtrue \BSteps \tmsucc \tmtrue$:

\[
\begin{array}{c@{\qquad}c}
  \infer[\BValue]{\tmsucc \tmtrue \BSteps \tmsucc \tmtrue}
  {\infer[\VSucc]{\tmsucc \tmtrue \Value}
    {\infer[\VTrue]{\tmtrue \Value}{}}} &

  \infer[\BSucc]{\tmsucc \tmtrue \BSteps \tmsucc \tmtrue}
  {\infer[\BValue]{\tmtrue \BSteps \tmtrue}
    {\infer[\VTrue]{\tmtrue \Value}{}}}
\end{array}
\]

What we prove here for the big-step semantics is the same property as the
``values don't step'' for the small-step semantics, except that in our case,
values can continue evaluating over and over. Values always
evaluate to themselves.

\begin{lemma}
  \label{lem:bstep-values-stagnate}
  If $V_1 \BSteps V_2$ with $V_1$ a value, then $V_1 = V_2$.
\end{lemma}

\begin{lstlisting}
rec bstep_value_stagnate : [|- bigstep V1 V2] -> [|- value V1] -> [|- equal V1 V2] =
/ total e (bstep_value_stagnate _ _ _ e) /
  fn b => fn e => case e of
  | [|- v_z]       => let [|- b_value _] = b in [|- ref]
  | [|- v_true]    => let [|- b_value _] = b in [|- ref]
  | [|- v_false]   => let [|- b_value _] = b in [|- ref]
  | [|- v_succ E'] =>
    (case b of
     | [|- b_value _] => [|- ref]
     | [|- b_succ B'] =>
       let [|- ref] = bstep_value_stagnate [|- B'] [|- E'] in [|- ref]
    )
;
\end{lstlisting}

We now prove that the small-step and big-step semantics for this language
coincide, {\em i.e.} $M \MSteps V$ if and only if $M \BSteps V$, for any value
 $V$. We will prove the two directions of the ``if and only if'' separately.

\subsection{Part 1: If $M \BSteps V$ then $M \MSteps V$}

Note that in this direction, we do not need to state that $V$ is a value, since
the Value Soundness Lemma (Lemma~\ref{lem:bstep-value-soundness}) gives us this
property for free.

This part of the proof follows exactly the one described in \cite{TAPL}. In the
proof, we rely on the Multi Step Lemmas (Lemma~\ref{lem:multi-step}) which we
proved in the last section. These lemmas justify bigger steps when evaluating a
term with the small-step semantics, which will be useful when we translate a
sequence of steps to a derivation tree in our big-step semantics. Let us now
write the actual proof:

\begin{proposition}[Big-step to small-step]
  \label{prop:bstep-to-mstep}
  If $M \BSteps V$ then $M \MSteps V.$
\end{proposition}

\begin{proof}
  By induction on the proof $\proofderiv{\mathcal{B}}{M \BSteps V}$.
  We show a few representative cases.

\begin{case}{$\B = \ianc{V \Value}{V \BSteps V}{\BValue}$}
$V \MSteps V$ \hfill by reflexivity of $\MSteps$, i.e. $\MRef$
\end{case}

\begin{case}{$\B = \ianc{\above{\B'}{M \BSteps \tmzero}}{\tmpred M
  \BSteps \tmzero}{\BPredZero}$}
$M \MSteps \tmzero$ \hfill by I.H. on $\B'$\\
$\tmpred M \MSteps \tmpred z$ \hfill by lemma~\ref{lem:multi-step}\\
$\tmpred \tmzero \Steps \tmzero$ \hfill by $\EPredZero$\\
$\tmpred \tmzero \MSteps \tmzero$ \hfill by $\MStep$\\
$\tmpred M \MSteps \tmzero$ \hfill by $\MTr$
\end{case}

\begin{case}{$\B = \inferaa{\BIfTrue}{\tmif{M_1}{M_2}{M_3} \BSteps V}{\above{\B_1}{M_1 \BSteps \tmtrue}}{\above{\B_2}{M_2 \BSteps V}}$}
$M_1 \MSteps \tmtrue$ \hfill by I.H. using $\B_1$ \\
$M_2 \MSteps V$ \hfill by I.H. using $\B_2$ \\
$\tmif{M_1}{M_2}{M_3} \MSteps \tmif{\tmtrue}{M_2}{M_3}$ \hfill by lemma~\ref{lem:multi-step}\\
$\tmif{\tmtrue}{M_2}{M_3} \Steps M_2$ \hfill by $\EIfTrue$ \\
$\tmif{\tmtrue}{M_2}{M_3} \MSteps M_2$ \hfill by $\MStep$ \\
$\tmif{M_1}{M_2}{M_3} \MSteps V$ \hfill by $\MTr$
\end{case}

\end{proof}


Encoding this proof is in fact straightforward. We translate the
theorem statement into a type and the inductive proof into a recursive
program.


\begin{lstlisting}
rec bstep_to_mstep : [|- bigstep M V] -> [|- multi_step M V] =
/ total b (bstep_to_mstep _ _ b) /
  fn b => case b of
  | [|- b_value _] => [|- ms_ref]
  | [|- b_succ  B] => ?

  | [|- b_pred_zero B] =>
    let [|- S] = bstep_to_mstep [|- B] in
    let [|- S'] = mstep_pred [|- S] in
      [|- ms_tr S' (ms_step e_pred_zero)]
  | [|- b_pred_succ B] => ?

  | [|- b_iszero_zero B] => ?
  | [|- b_iszero_succ B] => ?

  | [|- b_if_true  B1 B2] : [|- bigstep (if_then_else _ M2 M3) _] =>
    let [|- S1] = bstep_to_mstep [|- B1] in
    let [|- S2] = bstep_to_mstep [|- B2] in
    let [|- S1'] = mstep_if_then_else [|- S1] [|- M2] [|- M3] in
      [|- ms_tr (ms_tr S1' (ms_step e_if_true)) S2]
  | [|- b_if_false B1 B2] => ?
;
  \end{lstlisting}



\subsection{Part 2: If $M \MSteps V$ with $V$ a value then $M \BSteps V$ }

This direction is not as immediate as the first one. This comes essentially from
the fact that the big-step semantics relates a term and a value, while the
small step semantics relates two terms. In this proof, we
exploit the fact that eventually we also reach a value using the
small step semantics and moreover that in both the small step (with multi-step)
and big step semantics, values evaluate to themselves.

% This is the reason why we will need to say that $V$ is a value (we didn't need
% it in the Part~1), and this is the reason why we will have to use lemmas that
% will take a multi-step relation between two terms, and a big-step relation
% starting from the second term and finishing the evaluation to the value.
% \todo{This is really not clear, but I don't know how to say it. -nj}

\begin{lemma}\label{lem:step-bstep-to-bstep}
  If $M \Steps N$ and $N \BSteps V$ then $M \BSteps V$.
\end{lemma}

The statement of the lemma can be directly translated into \beluga.

\begin{lstlisting}
rec step_bstep_to_bstep : [|- step M N] -> [|- bigstep N V] -> [|- bigstep M V] =
/ total s (step_bstep_to_bstep _ _ _ s _) /
  fn s => fn b => ?;
\end{lstlisting}

The proof of this lemma is the hardest part. Indeed, once we have this lemma, we will only
have to iterate over the $\Steps$ to get the same property for $\MSteps$:

\begin{lemma}\label{lem:mstep-bstep-to-bstep}
  If $M \MSteps N$ and $N \BSteps V$ then $M \Downarrow V$.
\end{lemma}

This lemma is translated into \beluga directly as

  \begin{lstlisting}
rec mstep_bstep_to_bstep : [|- multi_step M N] -> [|- bigstep N V]
			   -> [|- bigstep M V] =
/ total s (mstep_bstep_to_bstep _ _ _ s _) /
  fn s => fn b => ?;
  \end{lstlisting}

Finally we will just have to apply this lemma with $N = V$ to obtain what we
want:

\begin{proposition}\label{prop:mstep-to-bstep}
  If $M \MSteps V$ with $V$ a value then $M \BSteps V$.
\end{proposition}

Or in \beluga:

\begin{lstlisting}
rec mstep_to_bstep : [|- multi_step M V] -> [|- value V] -> [|- bigstep M V] =
/ total s (mstep_to_bstep _ _ s _) /
  fn s => fn v => ?;
\end{lstlisting}


Let us now return to the proof of Lemma \ref{lem:step-bstep-to-bstep}.

\begin{proof}[Proof of lemma~\ref{lem:step-bstep-to-bstep}]

By induction on the proof $\proofderiv{\mathcal{S}}{M \Steps N}$. We show a few representative cases.

\begin{case}{$\S = \ianc{}{\tmif{\tmtrue}{M_2}{M_3} \Steps  M_2}{\EIfTrue}$}
$\tmtrue \BSteps \tmtrue$ \hfill by $\VTrue$ and $\BValue$\\
$M_2 \BSteps V$ \hfill by assumption \\
$\tmif{\tmtrue}{M_2}{M_3} \BSteps V$ \hfill by $\BIfTrue$
\end{case}

\begin{case}{$\S = \infera{\EPredSucc}{\tmpred (\tmsucc V) \Steps V}{V \Value}$}
$V \BSteps V'$ \hfill by assumption \\
$V = V'$ \hfill by Lemma \ref{lem:bstep-values-stagnate} \\
$(\tmsucc V) \Value$ \hfill by $\VSucc$ \\
$\tmsucc V \BSteps \tmsucc V$ \hfill by $\BValue$ \\
$\tmpred (\tmsucc V) \BSteps V$ \hfill by $\BPredSucc$
\end{case}

\begin{case}{$\S = \infera{\EIf}{\tmif{M_1}{M_2}{M_3} \Steps \tmif{M_1'}{M_2}{M_3}}{\above{\S'}{M_1 \Steps M_1'}}$}
We case-analyze $\proofderiv{\mathcal{B}}{\tmif{M_1'}{M_2}{M_3} \BSteps V}$. \\[1em]
%
\begin{subcase}{$\mathcal{B} = \ianc{V \Value}{V \BSteps V}{\BValue}$ ~~and~~ $V = \tmif{M_1'}{M_2}{M_3}$}
Impossible, since $\tmif{M_1'}{M_2}{M_3}$ cannot be a value.
\end{subcase} \\[1em]
%
\begin{subcase}{$\mathcal{B} = \ibnc{\above{\mathcal{B}_1}{M_1' \BSteps \tmtrue}}{\above{\mathcal{B}_2}{M_2 \BSteps V}}{\tmif{M_1'}{M_2}{M_3} \BSteps V}{\BIfTrue}$}
$\proofderiv{\S'}{M_1 \Steps M_1'}$ \hfill restating assumption $\S'$ \\
$M_1 \BSteps \tmtrue$ \hfill by I.H. on $\S'$ and $\mathcal{B}_1$ \\
$\tmif{M_1}{M_2}{M_3} \BSteps V$ \hfill by $\mathcal{B}_2$ and $\BIfTrue$
\end{subcase} \\[1em]
%
\begin{subcase}{$\mathcal{B} = \ibnc{\above{\mathcal{B}_1}{M_1' \BSteps \tmfalse}}{\above{\mathcal{B}_2}{M_3 \BSteps V}}{\tmif{M_1'}{M_2}{M_3} \BSteps V}{\BIfFalse}$}
Similar to the case using $\BIfTrue$.
\end{subcase}
\end{case}

\begin{case}{$\S = \infera{\ESucc}{\tmsucc M \Steps \tmsucc N}{\above{\S'}{M \Steps N}}$}
We case-analyze $\proofderiv{\mathcal{B}}{\tmsucc N \BSteps V}$. \\[1em]
%
\begin{subcase}{$\mathcal{B} = \ianc{V \Value}{V \BSteps V}{\BValue}$ ~~and~~ $V = \tmsucc N$}
$\proofderiv{\S'}{M \Steps N}$ \hfill restating assumption $\S'$ \\
$N \Value$ \hfill by inversion on $\VSucc$ \\
$\proofderiv{\mathcal{B}'}{N \BSteps N}$ \hfill by $\BValue$ \\
$M \BSteps N$ \hfill by I.H. on $\S'$ and $\mathcal{B}'$ \\
$\tmsucc M \BSteps \tmsucc N$ \hfill by $\BSucc$
\end{subcase} \\[1em]
%
\begin{subcase}{$\mathcal{B} = \ianc{\above{\mathcal{B}'}{N \BSteps V'}}{\tmsucc N \BSteps \tmsucc V'}{\BSucc}$ ~~and~~ $V = \tmsucc V'$}
$\proofderiv{\S'}{M \Steps N}$ \hfill restating assumption $\S'$ \\
$M \BSteps V'$ \hfill by I.H. on $\S'$ and $\mathcal{B}'$ \\
$\tmsucc M \BSteps \tmsucc V'$ \hfill by $\BSucc$
\end{subcase}
\end{case}

\end{proof}

\begin{lstlisting}
rec step_bstep_to_bstep : [|- step M N] -> [|- bigstep N V] -> [|- bigstep M V] =
/ total s (step_bstep_to_bstep _ _ _ s _) /
  fn s => fn b =>
  let [|- B] = b in
  case s of
  | [|- e_if_true]  => [|- b_if_true (b_value v_true) B]
  | [|- e_if_false] => ?

  | [|- e_pred_zero]   => ?
  | [|- e_pred_succ E] =>
    let [|- ref] = bstep_value_stagnate [|- B] [|- E] in
      [|- b_pred_succ (b_value (v_succ E))]

  | [|- e_iszero_zero]   => ?
  | [|- e_iszero_succ V] => ?

  | [|- e_if_then_else S] =>
    (case [|- B] of
     | [|- b_value E] => impossible [|- E]
     | [|- b_if_true  B1' B2'] =>
       let [|- B1] = step_bstep_to_bstep [|- S] [|- B1'] in
         [|- b_if_true  B1 B2']
     | [|- b_if_false B1' B3'] =>
       let [|- B1] = step_bstep_to_bstep [|- S] [|- B1'] in
         [|- b_if_false B1 B3'] )

  | [|- e_succ S]   =>
    (case [|- B] of
     | [|- b_value E] =>
       let [|- v_succ E'] = [|- E] in
       let [|- B'] = step_bstep_to_bstep [|- S] [|- b_value E'] in
         [|- b_succ B']
     | [|- b_succ B]  =>
       let [|- B'] = step_bstep_to_bstep [|- S] [|- B] in
         [|- b_succ B'] )
  | [|- e_pred S]   => ?
  | [|- e_iszero S] => ?
;
\end{lstlisting}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End: