mirror of
https://github.com/janishutz/eth-summaries.git
synced 2026-07-27 21:29:09 +02:00
33 lines
1.4 KiB
TeX
33 lines
1.4 KiB
TeX
\subsection{Structural Induction}
|
|
In this subsection, we present structural induction over lists.
|
|
The same concept also applies similarly to trees and more.
|
|
Weak Structural Induction on trees is presented in the subsequent subsection.
|
|
|
|
For both, we only provide the natural deduction rules, as the proofs proceed analogously to the ones for mathematical induction.
|
|
|
|
\subsubsection{Weak Structural Induction}
|
|
\[
|
|
\begin{prooftree}
|
|
\hypo{\Gamma \vdash P(\texttt{[]})}
|
|
\hypo{\Gamma, P(\texttt{xs}) \vdash P(\texttt{x : xs})}
|
|
\infer2[where \texttt{x}, \texttt{xs} not free in $\Gamma$]{\Gamma \vdash \forall \texttt{xs} . P(\texttt{xs})}
|
|
\end{prooftree}
|
|
\]
|
|
|
|
\subsubsection{Strong Structural Induction}
|
|
\inlinedefinition[Subterm relation] denoted $\sqsubset$ is defined as follows:
|
|
\[
|
|
\forall xs, ys . xs \sqsubset ys \Leftrightarrow (\exists x. ys = x:xs) \lor (\exists zs . xs \sqsubset zs \land zs \sqsubset ys)
|
|
\]
|
|
\begin{align*}
|
|
\begin{prooftree}
|
|
\hypo{\Gamma, \forall ys \sqsubset xs . P(ys) \vdash P(xs)}
|
|
\infer1[$xs$ not free in $\Gamma$, $ys$ not free in $P(xs)$]{\Gamma \vdash \forall xs . P(xs)}
|
|
\end{prooftree}
|
|
\end{align*}
|
|
|
|
|
|
\subsubsection{Generalizing expressions}
|
|
Sometimes, an expression can be hard to proof straight away because there is a constant in it.
|
|
In that case, replace that constant, making sure to update both sides of the expression to reflect the change.
|