mirror of
https://github.com/janishutz/eth-summaries.git
synced 2026-07-27 21:29:09 +02:00
42 lines
2.7 KiB
TeX
42 lines
2.7 KiB
TeX
\subsection{Induction on Proof Trees}
|
|
\label{sec:induction-on-proof-trees}
|
|
This type of induction is used to prove that a statement exhibits given behaviour.
|
|
|
|
Typically, these are statements are of type $\forall \ldots \vdash \texttt{s1} \implies \vdash \texttt{s2}$.
|
|
|
|
Since often we are not restricted to just simple statements, such where we know that we are applying the $\textsc{Ass}_{\text{NS}}$ rule,
|
|
we need to perform case distinction on all possible last rules applied in the derivation tree $T$.
|
|
If all are to be proven, this will yield $7$, one for each rule of the big-step semantics.
|
|
|
|
\inlinedefinition[Subderivation] We define $T' \sqsubset T$, where $T$ is a derivation tree. $T'$ is called a \textit{subderivation} of $T$,
|
|
or more simply, a \textit{subtree} of $T$. Definition is analogous to the subterm relation.
|
|
|
|
|
|
\shade{ForestGreen}{Rundown} Below a rundown of how such proofs are expected to be laid out.
|
|
|
|
We define $P(T) \equiv \forall \sigma, \sigma', s . ({\color{red}\texttt{root}(T) \equiv \texttt{s1}} \implies {\color{ForestGreen}\vdash \texttt{s2}})$.
|
|
{\color{gray} The quantifier-bound variables / states / statements can of course differ, so adjust accordingly.
|
|
This step is the crucial step to setting up this type of induction.}
|
|
|
|
We then prove $\forall T . P(T)$ by strong induction on the shape of the derivation tree $T$.
|
|
Thus, for some arbitrary $T$, the induction hypothesis is $\forall T' \sqsubset T . P(T')$ and we prove $P(T)$.
|
|
|
|
Let $\sigma, \sigma', s$ {\color{gray} (and more, if applicable)} be arbitrary and assume the LHS of the implication.
|
|
|
|
Then, we show the RHS of the implication by case analysis on the last rule applied in $T$.
|
|
{\color{gray} We do this drawing up a derivation tree for each rule, such as $\textsc{WhT}_{\text{NS}}$, as shown below (from solutions of Exercise Session 11, FS2026):}
|
|
\begin{center}
|
|
\includegraphics[width=0.6\linewidth]{assets/proof-on-shape-of-tree.png}
|
|
\end{center}
|
|
{\color{gray} After it, we need to put final constraints and bind free variables in some way, e.g. here:}
|
|
|
|
For some $b, s', \sigma'', T_4, T_5$, such that $s \equiv \texttt{while}\; b \; \texttt{do} \; s' \; \texttt{end}$ and $\cB \llbracket b \rrbracket \sigma = \texttt{tt}$.
|
|
|
|
{\color{gray} Then use the induction hypothesis on the subderivations $T_i$ to obtain the desired result.
|
|
That is, we show that there is another tree (or possibly derivation sequence), which fulfils the RHS with the same subtrees.
|
|
|
|
Depending on our Statement, we may need to provide a second tree for the RHS.
|
|
|
|
It is also important that it's \bi{always} the last rule we are looking at. So if we are given a statement to prove where there are only a few options,
|
|
we only need to prove for those options.}
|