\chapter{Inductive Predicates}
\label{chap:inductive-predicates}

\emph{Inductive predicates}, or inductively defined propositions, are a
convenient way to specify functions of type \,\li{⋯ → Prop}. They are reminiscent
of formal systems (Section~\ref{sec:type-checking-and-type-inference}) and of
Prolog-style logic programming. But Lean offers a much stronger logic than
Prolog, so we need to do some work to establish theorems instead of just running
the Prolog interpreter. A possible view of Lean:
%
\[\text{Lean \texttt{=} functional programming \texttt{+} logic programming \texttt{+} more logic}\]

\section{Introductory Examples}
\label{sec:introductory-examples}

Unless you have been exposed to Prolog or logic programming, you will probably
wonder what inductive predicates are and why they are useful. We start by
reviewing three examples that demonstrate the variety of uses:\ even numbers,
tennis games, and the reflexive transitive closure.

\subsection{Even Numbers}
\label{ssec:even-numbers}

Mathematicians often define sets as the smallest set that meets some criteria.
Consider this definition:
%
\begin{quote}
The set \textit{E} of \emph{even natural numbers} is defined as the smallest set
\textit{S} closed under the following rules:
\begin{enumerate}
\item[(1)] 0 $\in$ \textit{S};
\item[(2)] for every
\textit{k} $\in$ $\mathbb{N}$, if \textit{k} $\in$ \textit{S}, then
\textit{k}~$+$~2 $\in$ \textit{S}.
\end{enumerate}
Such a set exists by the Knaster--Tarski theorem.
\end{quote}
%
(The last sentence is often left implicit.) It is easy to convince ourselves
that \textit{E} contains all the even numbers and only those. Let us put on our
mathematician's hat and prove that 4 is even:
%
\begin{quote}
By rule (1), we have 0 $\in$ \textit{E}.

Hence, by rule (2) (with \textit{k} $:=$ 0), we have 2 $\in$ \textit{E}.

Thus, by rule (2) (with \textit{k} $:=$ 2), we have 4 $\in$ \textit{E}, as
desired. \qed
\end{quote}

By contrast, computer scientists might use a formal system consisting of
two derivation rules to specify the same set:
%
\vskip\abovedisplayskip

\noindent\hbox{}\hfill
\prftree[r]{\textsc{Zero}}
  {\strut\text{0 $\in$ \textit{E}}}%
\hfill
\prftree[r]{$\textsc{AddTwo}_\textit{k}$}
  {\strut\text{\textit{k} $\in$ \textit{E}}}
  {\strut\text{\textit{k} $+$ 2 $\in$ \textit{E}}}%
\hfill\hbox{}

\vskip\belowdisplayskip

\noindent
A proof is then a derivation tree:
%
\begin{gather*}
\prftree[r]{$\textsc{AddTwo}_\text{2}$}
  {\prftree[r]{$\textsc{AddTwo}_\text{0}$}
   {\prftree[r]{\textsc{Zero}}
    {\strut\text{0 $\in$ \textit{E}}}}
   {\strut\text{2 $\in$ \textit{E}}}}
  {\strut\text{4 $\in$ \textit{E}}}
\end{gather*}
%
The proof is forward if we read it downwards and backward if we read it upwards.

Inductive predicates are the logician's way to achieve the same result. In Lean,
instead of a set, we would define a characteristic predicate inductively:

\lstinputlisting[linerange=even-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
This should look familiar. We have used the same syntax, except with
\hbox{\li{Type}} instead of \li{Prop}, to define inductive types. Inductive
types and inductive predicates are provided by the same mechanism in Lean,
in accordance with the PAT principle.

The command above defines a unary predicate \li{Even} as well as two
introduction rules \li{Even.zero} and \li{Even.}\allowbreak\li{add_two}
that can be used to prove goals of the form \li{⊢ Even …}\,. Recall that an
introduction rule for a symbol (e.g., \li{Even}) is a theorem whose conclusion
contains that symbol
(Section~\ref{sec:forward-reasoning-about-connectives-and-quantifiers}). By the
PAT principle, \li{Even n} can be viewed as a dependent
inductive type like \hbox{\li{Vec α n}} (Section~\ref{sec:dependent-inductive-types}),
and \li{Even.zero} and \li{Even.add_two} as constructors like \li{Vec.nil} and
\li{Vec.cons}.

If we translate the Lean definition back into English, we get something similar
to the Knaster--Tarski-style definition above:

\begin{quote}
The following clauses define the even numbers.
\begin{enumerate}
\item[(1)] \li{0} is even;
\item[(2)] any number of the form \li{k + 2} is even, assuming \li{k} is even.
\end{enumerate}
Any other number is not even.
\end{quote}

It is worth nothing that inductively defined symbols have no definition. Thus,
we cannot unfold their definition using \li{simp}, any more than we can unfold
the definition of an inductive type such as \li{List α}. The only reasoning
principles available are introduction and elimination.

As a warm-up exercise, here is a proof of \li{Even 4}:

\lstinputlisting[linerange=even_4-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
For example, the proof term \li{Even.add_two _ Even_0} has type
\li{Even} \hbox{\li{(0 + 2)},} which is syntactically equal to \li{Even 2} up to
computation and hence equal from the type checker's point of view. The
underscore stands for \li{0}.

Thanks to the ``no junk'' guarantee of inductive definitions,
\hbox{\li{Even.}}\allowbreak\li{zero} and \hbox{\li{Even.}}\allowbreak\li{add_two}
are the only two ways to construct
proofs of \li{⊢ Even …}\,. By inspecting the conclusions \li{Even 0} and
\hbox{\li{Even (k +}} \hbox{\li{2)},} we see that there is no danger of ever
proving that \li{1} is even.

Another way to view the inductive definition above is as follows: The first line
introduces a predicate, whereas the second and third lines introduce axioms we
want the predicate to satisfy. Accordingly, we could have written
%
\begin{lstlisting}
opaque Even : ℕ → Prop
axiom Even.zero    : Even 0
axiom Even.add_two : ∀k : ℕ, Even k → Even (k + 2)
\end{lstlisting}
%
replacing \li{inductive} by \li{opaque} and \li{|} by \li{axiom}.
%
But this axiomatic version, apart from being dangerous, does
not give us any information about when \li{Even} is false. We cannot use it to
prove \li{¬ Even 1} or \li{¬ Even 17}. For all we know, \li{Even} could be true
for all natural numbers. In contrast, the inductive definition guarantees that
we obtain the least (i.e., the most false) predicate that satisfies the
introduction rules \li{Even.zero} and \li{Even.add_two}, and provides
elimination and induction principles that allow us to prove
\li{¬ Even 1}, \li{¬ Even 17}, or \li{¬ Even (2 * n + 1)}.

Why should we bother with inductive predicates when we can define recursive
functions? Indeed, the following definition is perfectly legitimate:
%
\lstinputlisting[linerange=even_rec-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
Each style has its strengths and weaknesses. The recursive version
forces us to specify a false case (the second equation), and it forces us to
worry about termination. On the other hand, because it is equational and
computational, it works well with \hbox{\li{rfl},} \li{simp}, \li{#eval}, and
\li{#reduce}. The inductive version is arguably more abstract and elegant. Each
introduction rule is stated independently. We can add or remove rules without
having to think about termination or executability.

Yet another way to define \li{Even} is as a nonrecursive definition, using the
modulo operator (\li|%|):
%
\lstinputlisting[linerange=even_nonrec-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
Mathematicians would likely prefer this version. But the inductive version is a
convenient ``Hello, World!''\ example that resembles many realistic inductive
definitions. It might be a toy, but it is a useful toy.

\subsection{Tennis Games}
\label{ssec:tennis-games}

Transition systems consists of transition rules that connect a ``before'' and
an ``after'' state. As a specimen of a transition system, we consider the
possible transitions in a game of tennis, starting from 0--0 (``Love all'').
Tennis games are also a toy, but in Chapter~\ref{chap:operational-semantics}, we
will define the semantics of an imperative programming language as a transition
system in a similar style.

The scoring rules for tennis from the International Tennis Federation's
\emph{Rules of Tennis} are reproduced below.
% 2007 edition of the

\begin{quote}
A standard game is scored as follows with the server's score being called first:

\hfill
\begin{tabular}{@{}l@{\extracolsep{.5em}}l@{\extracolsep{.5em}}l@{}}%
No point & -- & ``Love'' \\%
First point & -- & ``15'' \\%
Second point & -- & ``30'' \\%
Third point & -- & ``40'' \\%
Fourth point & -- & ``Game''
\end{tabular}
\hfill{}

except that if each player/team has won three points, the score is ``Deuce.''
After ``Deuce,'' the score is ``Advantage'' for the player/team who wins the
next point. If that same player/team also wins the next point, that player/team
wins the ``Game''; if the opposing player/team wins the next point, the score
is again ``Deuce.'' A player/team needs to win two consecutive points
immediately after ``Deuce'' to win the ``Game.''
\end{quote}

We first define an inductive type to represent scores:

\lstinputlisting[linerange=score-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
A score such as 30--15 is represented as \li{Score.vs 30 15}, which we will also
write in infix notation as \li{30–15}. We ignore some of the most frivolous
aspects of the scoring rules, writing \li{0} for ``Love'' and \li{40–40} for
``Deuce.'' If we really cared, we could introduce aliases such as
\li{def love : ℕ := Score.vs 0 0}.

The next stage is to introduce a binary predicate \li{Step} that
determines whether a transition is possible:
%
\lstinputlisting[linerange=step-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
Let \li{s ↝ t} abbreviate \li{Step s t}. A game is a chain
%
\li{s₀} \li{↝} \li{s₁} \li{↝} \hbox{\li{s₂}} \hbox{\li{↝}} \hbox{\li{⋯}} \li{↝} \li{s}$_\ttvar{n}$
%
where \li{s₀} $=$ \li{0–0} and no transition is possible from
\hbox{\li{s}$_\ttvar{n}$.} The predicate allows nonsensical transitions such as
\hbox{\li{15–99 ↝}} \hbox{\li{30–99},} but since the score \li{15–99} cannot be
reached from \li{0–0}, these transitions are harmless.

Equipped with a formal definition, we can ask, and formally answer, questions
such as: Do games have a maximal length? How many different final scores are
possible? Is the score 15--99 reachable from ``Love all''? And can the score
ever return to 0--0? Let us use Lean to disprove the last claim:
%
\lstinputlisting[linerange=no_step_to_0_0-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}

The diagram below summarizes which scores are reachable from which scores:%
\pagebreak[2]
%
\[\hbox{\input{images/tennis.pdf_t}}\]

\subsection{Reflexive Transitive Closure}
\label{ssec:reflexive-transitive-closure}

As a non-toy application of inductive predicates,
consider the reflexive transitive closure
\textit{r}$^*$ of a binary relation~\textit{r}. Informally,
\textit{r}$^*$ is the relation that represents zero or more steps of
\textit{r}. For example, if \textit{r} corresponds to taking one transition in
a transition system (e.g., an automaton), then \textit{r}$^*$ corresponds to
taking any number of steps, including zero. For a more concrete example,
consider the following:
%
\begin{align*}
\textit{r} & = \{(1, 2), (2, 4), (4, 8)\} \\
\textit{r}^* & = \{(\textit{n}, \textit{n}) \mid \textit{n} \in \mathbb{N}\} \cup \{(1, 2), (1, 4), (1, 8), (2, 4), (2, 8), (4, 8)\}
\end{align*}

The star (${}^*$) operator is often defined rigorously as a formal system:

\vskip\abovedisplayskip

\noindent\hbox{}\hfill
\prftree[r]{\textsc{Base}}
  {\strut\text{(\textit{a}, \textit{b}) $\in$ \textit{r}}}
  {\strut\text{(\textit{a}, \textit{b}) $\in$ \textit{r}$^*$}}%
\hfill
\prftree[r]{\textsc{Refl}}
  {\strut\text{(\textit{a}, \textit{a}) $\in$ \textit{r}$^*$}}%
\hfill
\prftree[r]{\textsc{Trans}}
  {\strut\text{(\textit{a}, \textit{b}) $\in$ \textit{r}$^*$}}
  {\strut\text{(\textit{b}, \textit{c}) $\in$ \textit{r}$^*$}}
  {\strut\text{(\textit{a}, \textit{c}) $\in$ \textit{r}$^*$}}%
\hfill\hbox{}

\vskip\belowdisplayskip

\noindent
These rules define \textit{r}$^*$ as the smallest relation that contains
\textit{r} (by \textsc{Base}) and that is reflexive (by \textsc{Refl}) and transitive
(by \textsc{Trans}). If we wanted to define the transitive closure \textit{r}$^+$
instead, we would simply omit the \textsc{Refl} rule. If we wanted the reflexive
symmetric closure, we would replace the \textsc{Trans} rule by a \textsc{Symm}
rule. With a formal system, we simply declare the properties we want to be true,
without giving a thought to termination or executability.

It is straightforward to translate the above derivation rules into introduction
rules of an inductive predicate:
%
\lstinputlisting[linerange=star-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
We represent relations as binary predicates rather than sets of pairs,
writing \hbox{\li{R a b}} for \li{(a, b) ∈ R}. Relations and predicates are
interchangeable, but predicates are often more convenient to use in a proof
assistant. The reflexive transitive closure of \li{R} is written \li{Star R}.
Notice that \li{a}, \li{b}, and \li{c} are declared as parameters of the
introduction rules, on the left of the colons. We could also have written
%
\begin{lstlisting}
| base : ∀a b : α, R a b → Star R a b
\end{lstlisting}
%
or at the other extreme
\begin{lstlisting}
| base (a b : α) (hab : R a b) : Star R a b
\end{lstlisting}
%
All these forms are logically and operationally equivalent.

The general format of inductive predicates is as follows:
%
\begin{quote}
\lic{inductive} \,{\color{procnamecolor}\ttvar{predicate-name}}
  \,\tabletbreak{\qquad}\lic{(}\ttvar{params}$_\texttt{1}$ \lic{:} \ttvar{type}$_\texttt{1}$\lic{)} $\ldots$
    \lic{(}\ttvar{params}$_{\ttvar{k}}$ \lic{:} \ttvar{type}$_{\ttvar{k}}$\lic{)}\rlap{~\,\lic{:}} \\
\noindent\phantom{\lic{|}\, }%
  \ttvar{type}$_{\ttvar{k+1}}$ \li{→ ⋯ →} \ttvar{type}$_{\ttvar{k+p}}$ \li{→} \lic{Prop} \,\lic{where} \\
\noindent\phantom{\lic{xx}}\lic{|}\, \ttvar{rule-name}$_\texttt{1}$
  \,\lic{(}\ttvar{params}$_\texttt{11}$ \lic{:} \ttvar{type}$_\texttt{11}$\lic{)} $\ldots$
    \lic{(}\ttvar{params}$_{\texttt{1}\ttvar{m}_\texttt{1}}$ \lic{:} \ttvar{type}$_{\texttt{1}\ttvar{m}_\texttt{1}}$\lic{)}
  \,\lic{:}\, \\
\noindent\phantom{\lic{xxxx}}\ttvar{proposition}$_\texttt{1}$ \\[-0.5\jot]
\noindent\phantom{\lic{xx}}\phantom{\lic{|}\, \textit{co}}$\vdots$ \\
\noindent\phantom{\lic{xx}}\lic{|}\, \ttvar{rule-name}$_\ttvar{n}$
  \,\lic{(}\ttvar{params}$_{\ttvar{n}\texttt{1}}$ \lic{:} \ttvar{type}$_{\ttvar{n}\texttt{1}}$\lic{)} $\ldots$
    \lic{(}\ttvar{params}$_{\ttvar{nm}_\ttvar{n}}$ \lic{:} \ttvar{type}$_{\ttvar{nm}_\ttvar{n}}$\lic{)}
  \,\lic{:}\, \\
\noindent\phantom{\lic{xxxx}}\ttvar{proposition}$_\ttvar{n}$
\end{quote}
%
where the conclusion of each \ttvar{proposition}$_\ttvar{j}$ must be an
application of the defined predicate \ttvar{predicate-name} to some arguments.
These arguments may be arbitrary terms; they do not need to be constructor
patterns. We can also use curly braces \li|{ }| instead of parentheses \li|( )|
if we want to make the arguments corresponding to the parameters implicit.

The above definition of \li{Star} is truly elegant. If you still doubt this, try
implementing it as a recursive function:
%
\lstinputlisting[linerange=star_rec-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}

To summarize, each introduction rule of an inductive predicate \li{P} consists
of the following components, from left to right:
%
\begin{itemize}
\item a \emph{name};
\item \emph{variables} that may appear in the rule;
\item zero or more \emph{conditions} that must be fulfilled, which may apply
  \li{P} recursively;
\item an application of \li{P} to some arguments, forming a \emph{pattern}.
\end{itemize}
%
Accordingly, for rule \li{Star.base}, the pattern is \li{Star R a b}, the
condition is \li{R a b}, and the variables are \li{a} and \li{b}.

\subsection{A Nonexample}
\label{ssec:a-example}

Not all inductive definitions admit a least solution. The simplest nonexample is
%
\lstinputlisting[linerange=Illegal-q,keywords={inductive,Prop,where}]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
If Lean accepted this definition, we could use it to prove the equivalence
\li{Illegal} \li{↔} \li{¬ Illegal}, from which we could easily derive \li{False}.
Fortunately, Lean rejects the definition:
%
\begin{quote}
\tabletsmall\ttfamily\raggedright
arg \#1 of 'Illegal.intro' has a non positive occurrence of the datatypes being declared
\end{quote}
%
The nonpositive occurrence it complains about is the occurrence of \li{Illegal}
under a negation. Mathematicians would reject the definition on the ground that
the monotonicity condition of the Knaster--Tarski theorem is not satisfied.

\section{Logical Symbols}
\label{sec:logical-symbols}

Although \li{Even} is the first openly inductive predicate in this guide, the
earlier chapters already presented other inductive predicates clandestinely.
The very first of these is equality (\li{=}), introduced in
Chapter~\ref{chap:programs-and-theorems}, followed by the logical symbols
\li{∧}, \li{∨}, \li{↔}, \li{∃}, \li{True}, and \li{False}. Their definitions
are worth studying closely:
%
\lstinputlisting[linerange=logical_symbols-q,keywords={inductive,Prop,Type}]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
(Strictly speaking, in Lean, some of the above definitions are actually
structures and not inductive predicates, but the difference is superficial.
As we saw in Section~\ref{sec:structures}, structures are essentially
single-constructor inductive predicates with some syntactic sugar.)

The traditional notations \li{∃x : α, P} and \li{x = y} are syntactic sugar for
\li{Exists} \hbox{\li{(fun x : α ↦ P)}} and \li{Eq x y}. Notice how \li{fun}
acts as an all-purpose binder. Notice also that there is no constructor for
\li{False}. There are no proofs of \li{False}, just like there is no proof of
\li{Even 1}. With inductive predicates, we state only the rules we want to be
true.

The symbol \li{∀}, including its special case \li{→}, is built directly into the
logic and is not defined as an inductive predicate. Nor does it have explicit
introduction or elimination rules. The introduction principle is
the anonymous function \li{fun x ↦} \li{_}, and the elimination principle is
function application \li{_ u}.

As for any inductive predicates, only the introduction rules are specified. The
elimination rules presented in Sections
\ref{sec:reasoning-about-connectives-and-quantifiers}~and~\ref{sec:reasoning-about-equality}
must be derived manually.

\section{Rule Induction}
\label{sec:rule-induction}

In the same way that we can perform an induction on a term of inductive type,
we can perform an induction on a proof of an inductive predicate. For example,
given the goal \li{h : Even n ⊢ P n}, we can invoke \li{induction h}
and get two subgoals, for \li{Even.zero} and \li{Even.add_two}.
This is called \emph{induction on the structure of the derivation of \li{h}} or
simply \emph{rule induction}, because the induction is on the predicate's
introduction rules (i.e., the constructors of the proof term).

There are two ways to look at rule induction:\ the ``least\hyp{}predicate\hyp{}such\hyp{}that
view'' and the ``PAT view.''
%
To understand the least\hyp{}predicate\hyp{}such\hyp{}that view, recall that an inductive
definition introduces a symbol as the least (i.e., the most false) predicate
satisfying the introduction rules. Accordingly, \li{Even} is the
least predicate \li{Q} such that the properties \li{Q 0} and
\li{∀k, Q k → Q (k + 2)} hold. Therefore, if we can show that \li{P 0} and
\li{∀k, P k} \li{→ P (k + 2)} hold for some predicate \li{P}, then \li{P} is
either \li{Even} itself or greater than (i.e., more true than) \li{Even}. As a
result, \li{Even n} implies \li{P n}, which is exactly what we need to prove
the goal \li{h : Even n} \li{⊢} \li{P n}.

The least\hyp{}predicate\hyp{}such\hyp{}that view gives a nice intuitive account of rule
induction that can be used in informal arguments, such as the following proof
that \li{Even n} implies \li|n % 2 = 0| for all \li{n}:

\begin{quote}
The proof is by rule induction on the hypothesis \hbox{\li{Even n}.}

\textsc{Case} \li{Even.zero}: \,We must show \li|0 % 2 = 0|.
This follows by computation.

\textsc{Case} \li{Even.add_two k}: \,The induction hypothesis is
\hbox{\li|k % 2|} \hbox{\li|= 0|.} We must show \li|(k + 2) % 2 = 0|. This
follows by basic arithmetic reasoning. \qed
\end{quote}
%
The Lean proof has the same structure:
%
\lstinputlisting[linerange=mod_two_eq_zero_of_even-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}

The PAT principle gives us another fruitful way to look at rule
induction. The key idea is that rule induction on \li{h} in a goal such as
\li{h : Even n} \li{⊢} \li{P[h]} is perfectly analogous to structural induction
on a value of a dependent inductive type such as \li{Vec α n}
(Section~\ref{sec:dependent-inductive-types}). Writing
\li{P}$_\texttt{u}$\li{[ ]} for the variant of \hbox{\li{P[ ]}} where
\li{n} is replaced by some term \li{u}, we get the subgoals
%
{\tabletsmall
\begin{align*}
& \hbox{\lic|\ ⊢ P|$_\texttt{0}$\li|[Even.zero : Even 0]|} \\
\hbox{\ctxt{k} \lic|: ℕ,| \ctxt{hk} \lic|: Even k,| \ctxt{ih} \lic|: P|$_\texttt{k}$\lic|[hk]|} & \hbox{\lic|\ ⊢ P|$_\texttt{k+2}$\lic|[Even.add_two k hk : Even (k + 2)]|}
\end{align*}
}%
%
These are effectively the subgoals produced by the \li{induction} tactic.

Regardless of the inductive predicate \li{Q}, the procedure to compute the
subgoals is always the same:
%
\begin{itemize}
\item[1.] Replace \li{h} in \li{P[h]} with each possible introduction rule
  applied to fresh variables (e.g., \li{Even.add_two k hk}), instantiating \li{n}
  in \li{P[ ]} to make \li{P[ ]} type-correct. This yields as many subgoals as
  there are introduction rules.

\item[2.] Add these new variables (e.g., \li{k}, \li{hk}) to the local context.

\item[3.] Add induction hypotheses for all new hypotheses that assert \li{Q …}\,.
\end{itemize}

Notice the presence of \li{hk :} \hbox{\li{Even k}} among the hypotheses above.
It was absent in the least\hyp{}predicate\hyp{}such\hyp{}that view and is not essential because
it can always be recovered by strengthening
\li{P} to be of the form \li{Even n ∧ ⋯}.

In nearly all practical cases, \li{h} will not occur in \li{P[h]}. We can then
simply write
%
\begin{align*}
& \hbox{\lic|\ ⊢ P|$_\texttt{0}$} &
\hbox{\ctxt{k} \lic|: ℕ,| \ctxt{hk} \lic|: Even k,| \ctxt{ih} \lic|: P|$_\texttt{k}$}
  & \hbox{\lic|\ ⊢ P|$_\texttt{k+2}$}
\end{align*}
%
In rare cases, \li{h} will occur in \li{P[h]}. Proofs may appear as subterms
in arbitrary terms, as we saw when we tried to extract the head of a list in
Section~\ref{sec:lists}.

The reflexive transitive closure \li{Star R} is similar to \li{Even}.
Given a goal \li{h : Star R} \li{x y ⊢ P}, rule induction on \li{h}
produces the following subgoals, where \li{P}$_\texttt{t,u}$ denotes the
variant of \li{P} where \li{x} and \li{y} are replaced by \li{t} and \li{u},
respectively:

{\tabletfootnotesize

\kern-\baselineskip

\begin{align*}
\hbox{\ctxt{a} \ctxt{b} \lic|: α,| \ctxt{hab} \lic|: R a b|} & \hbox{\lic|\ ⊢ P|$_\texttt{a,b}$} \\
\hbox{\ctxt{a} \lic|: α|} & \hbox{\lic|\ ⊢ P|$_\texttt{a,a}$} \\
\hbox{\ctxt{a} \ctxt{b} \ctxt{c} \lic|: α,| \ctxt{hab} \lic|: Star R a b,| \ctxt{hbc} \lic|: Star R b c,|
  \ctxt{ihab} \lic|: P|$_\texttt{a,b}$\lic|,| \ctxt{ihbc} \lic|: P|$_\texttt{b,c}$}
  & \hbox{\lic|\ ⊢ P|$_\texttt{a,c}$}
\end{align*}}%
%
This is where the ``assistant'' aspect of ``proof assistant'' comes into play.
One of the key properties of \li{Star} is idempotence---applying
\li{Star} to \li{Star R} has no effect. This can be proved as follows in Lean,
using rule induction for the \li{→}~direction of the equivalence:

\lstinputlisting[linerange=star_star_iff_star-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
We are careful to give intuitive names to the emerging variables. It is easy to
get lost in goals containing long, automatically generated names. The cleanup
tactics introduced in Section~\ref{sec:cleanup-tactics} can also be of help
when we face large goals.

We can state the idempotence property more standardly in terms of equality
instead of as an equivalence:

\lstinputlisting[linerange=star_star_eq_star-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
The proof uses two theorems that are available because Lean's logic is
classical:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|funext| & \lic| : (∀x, ?f x = ?g x) → ?f = ?g| \\
\lic|propext| & \lic| : (?a ↔ ?b) → ?a = ?b| \\
\end{tabular}
\end{center}
%
\emph{Functional extensionality} (\li{funext}) states that if two functions
yield equal results for all inputs, then the two functions must be equal.
\emph{Propositional extensionality} (\li{propext}) states that equivalence of
propositions coincides with equality. In these phrases, extensionality means
something like ``what you see is what you get.'' These properties may seem
obvious, and yet there exist proof assistants built on weaker, intuitionistic
logics in which the properties do not generally hold.

We register the theorem \li{Star_Star_Eq_Star} as a simp rule, because viewed as
a left-to-right rewrite rule, it genuinely replaces a complex term by a simpler
term. It is hard to imagine a situation where we would not want \li{simp} to
rewrite \li{Star (Star …)} to \li{Star …}\,.

For rule induction, we use the \li{induction} tactic. For subtle
logical reasons that will become clearer in
Chapter~\ref{chap:logical-foundations-of-mathematics}, rule induction by
pattern matching and recursion is not allowed.

In Section~\ref{sec:pattern-matching-expressions}, we saw a diagram depicting the
interpretation of \li{Bool} and \li{Prop} side by side. The diagram suggested
the existence of an infinite number of propositions, but we now know that there
are exactly two propositions:\ \li{False} and \li{True}. Here is a revised
diagram:
%
\begin{align*}
&
\hbox{\li{Bool}:~~}
\vcenter{\hbox{\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (0, 0) [shape=circle,draw,minimum size=2.9em,fill=white] {\Huge$\cdot\,\cdot$};
\end{tikzpicture}}}
&&
\hbox{\li{Prop}:~~}
\vcenter{\hbox{\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (0, 0) [shape=rectangle,draw,minimum size=3.5em,minimum width=7em,fill=gray!20] {};
  \path node at (-0.625, 0) [shape=circle,draw,minimum size=2.9em,fill=white] {};
  \path node at (+0.625, 0) [shape=circle,draw,minimum size=2.9em,fill=white] {\Huge$\!\cdot\!\cdot\!\cdot\!$};
\end{tikzpicture}}}
\end{align*}
%
We see that there are only two propositions, one which has no proofs and one
which has a number of proofs. Three proofs are shown in the diagram.

\section{Linear Arithmetic Tactic}
\label{sec:linear-arithmetic-tactic}

\subsection*{linarith}

The \li{linarith} tactic can be used to prove goals involving linear arithmetic
equalities (\li{=}), inequalities (\li{<}, \li{>}, \li{≤}, and \li{≥}), and
disequalities (\li{≠}). \emph{Linear} means that multiplication and
division do not occur, or if they do then one of the operands must be a numeric
constant. For example, \li{2 * x < y} is a linear constraint (which can be
rewritten to \li{x + x < y}), whereas \li{x * y < y} is nonlinear.

\section{Elimination}
\label{sec:elimination}

Given an inductive predicate \li{Q}, its introduction rules typically are of the
form \hbox{\li{∀…, ⋯ → Q …}} and can be used to prove goals of the form
\li{⊢ Q …}\,. Elimination works the other way around: It extracts information
from a theorem or hypothesis \li{h} \li{: Q …}\,. Elimination takes many forms:\ the
\li{cases} and \li{induction} tactics, pattern matching, and elimination
rules (e.g., \li{And.left}).

Invoked on \li{h : Q …}\,, the \li{cases h} tactic performs roughly the same rule
induction as \li{induction h} but without producing any induction hypotheses.
We encountered two idioms in Chapter~\ref{chap:functional-programming} that we
can finally analyze.

The first idiom is when \li{h} is of the form \li{l = r}---i.e., \li{Eq l r}
(Section~\ref{sec:logical-symbols}). Suppose the goal is \li{h : l = r ⊢ P[h]}.
The procedure presented in Section~\ref{sec:rule-induction} produces the subgoal
%
\[\hbox{\ctxt{a} \lic{: α ⊢ P}$_\texttt{a,a}$\lic{[Eq.refl a : a = a]}}\]
%
in which \li{P}$_\texttt{t,u}$\li{[ ]} stands for the variant of \li{P[ ]}
where \li{l} and \li{r} are replaced by \hbox{\li{t}} and~\li{u}, respectively.
(Strictly speaking, the useless hypothesis \li{h : a = a} would also appear in
the subgoal.) In practice, \li{P[h]} would likely not depend on \li{h}.
Moreover, \li{cases} reuses the name \li{l} instead of using a different name
like \li{a}. Thus, we would get
%
\[\hbox{\ctxt{l} \lic{: α ⊢ P}$_\texttt{l,l}$}\]
%
In other words, all occurrences of \li{r} in the original goal have been
replaced by \li{l}. This corresponds to the behavior we observed in
Section~\ref{sec:lists}.

The second idiom is the tactic \li{cases Classical.em Q}, where
\li{Q} is a proposition. The \li{Classical.em Q} part is a proof term for
\hbox{\li{Q ∨}} \li{¬ Q}---i.e., \li{Or Q (¬ Q)} (Section~\ref{sec:logical-symbols}). Then
\li{cases} is applied to eliminate the \li{∨} connective. Suppose the
goal is \li{⊢ P[Classical.em Q]}. By the definition of the \li{Or} predicate,
the new subgoals are
%
\begin{align*}
\text{\ctxt{hQ} \lic{: Q}} & \text{\lic{\ ⊢ P[Or.inl hQ : Q ∨ ¬ Q]}} \\
\text{\ctxt{hnQ} \lic{: ¬ Q}} & \text{\lic{\ ⊢ P[Or.inr hnQ : Q ∨ ¬ Q]}}
\end{align*}
%
There is no need to modify \li{P} because \li{Or.inl hQ} and
\hbox{\li{Or.inr}} \li{hnQ} have the same type as
\li{Classical.em Q}---namely, \li{Q ∨ ¬ Q}. In practice,
the goal would usually not contain \li{Classical.em Q} and be
simply \li{⊢ P}, and we would then have the subgoals
%
\begin{align*}
& \text{\ctxt{hQ} \lic{: Q ⊢ P}} &
& \text{\ctxt{hnQ} \lic{: ¬ Q ⊢ P}}
\end{align*}
%
Again, this is the behavior we observed in Section~\ref{sec:lists}.

In structured proofs, we can use \li{match} expressions
(Section~\ref{sec:pattern-matching-expressions}) to achieve the same effect as
\li{cases}. This works well for logical symbols. However, for predicates such
as \li{Even} and \li{Star}, with arguments that evolve through the induction,
we end up with dependently typed pattern matching, which is subtle
(Section~\ref{sec:dependent-inductive-types}). It is generally easier to let
\li{cases} figure out what the subgoals should look like than to
pattern-match. We will review an example of both styles below.

It can be useful to expand a hypothesis of the form \hbox{\li{Q (c …)},}
where \li{c} is a constructor or some other constant. We can state and prove an
\emph{inversion rule} to support such eliminative reasoning. A typical
inversion rule has the form
%
\[\hbox{\tabletsmall\lic{∀x₁ … x}$_\ttvar{n}$\lic{, Q (c x₁ … x}$_\ttvar{n}$\lic{) → (∃…, ⋯ ∧ ⋯) ∨ ⋯ ∨ (∃…, ⋯ ∧ ⋯)}}\]
%
It can be useful to combine introduction and elimination into a single theorem,
which can be used for rewriting both the hypotheses and the targets of
goals. The format is the same except for the connective \li{↔} in the middle:
%
\[\hbox{\tabletsmall\lic{∀x₁ … x}$_\ttvar{n}$\lic{, Q (c x₁ … x}$_\ttvar{n}$\lic{) ↔ (∃…, ⋯ ∧ ⋯) ∨ ⋯ ∨ (∃…, ⋯ ∧ ⋯)}}\]
%
An inversion rule for \li{Even} is given below:
%
\lstinputlisting[linerange=even_iff-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
As usual, the tactical proof is not particularly readable, but we see that
introduction rules and the eliminative \li{cases} tactic play a major role, for
both the logical symbols and the \li{Even} predicate. The \li{simp} tactic puts
the final touches.

If you prefer structured proofs, here is a version of the proof with dependently
typed pattern matching on \li{hn : Even n}:
%
\lstinputlisting[linerange=even_iff_struct-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}

\section{Further Examples}
\label{sec:further-examples}

Equipped with a better understanding of inductive predicates, we are now ready
to review four further applications in turn.

\subsection{Sorted Lists}
\label{ssec:sorted-lists}

Our first example is a predicate that checks whether a list of natural numbers
is sorted in increasing order:
%
\lstinputlisting[linerange=sorted-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
This definition captures the following mathematical intuition:
%
\begin{quote}
The set of sorted lists is defined as the smallest set closed under the
following rules:
\begin{enumerate}
\item[(1)] the list \li{[]} is sorted;
\item[(2)] given a number \li{x}, the list \li{[x]} is sorted;
\item[(3)] given two numbers \li{x}, \li{y} and a list \li{zs}, if \li{x < y}
and \li{y :: zs} is sorted, then \li{x :: y :: zs} is sorted.
\end{enumerate}
\end{quote}

It is always a good idea to test our definitions by trying it on small
examples. Is the list \li{[3, 5]} sorted? It would appear so:
%
\lstinputlisting[linerange=sorted_3_5-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
The example needs two of the introduction rules for \li{sorted}. This approach
tends to work well for expressions consisting only of closed terms. A more
compact proof follows, using proof terms:
%
\lstinputlisting[linerange=sorted_3_5_raw-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
The same idea can be used to prove that \li{[7, 9, 9, 11]} is sorted:
%
\lstinputlisting[linerange=sorted_7_9_9_11-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}

Conversely, we can show that some lists are not sorted. For this, we need
elimination:

\lstinputlisting[linerange=not_sorted_17_13-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
From the hypothesis that the list \li{[17, 13]} is sorted, we extract
the inequality \li{17} \hbox{\li{≤}} \li{13}. The \li{cases} tactic silently eliminates the
\li{nil} and \hbox{\li{single}} cases, because they cannot match a two-element list. Then we
invoke \li{simp} to exploit the impossible hypothesis \li{17 ≤ 13}.

\subsection{Palindromes}
\label{ssec:palindromes}

Palindromes are lists that read the same from left to right and from right to
left. For example, \li{[a, b, b, a]} and \li{[a, h, a]} are palindromes. The
following inductive predicate is \li{True} if and only if the list passed as
argument is a palindrome:

\lstinputlisting[linerange=palindrome-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
The definition distinguishes three cases:
%
(1)~\li{[]} is a palindrome;
(2)~for any element \li{x}, the singleton list \li{[x]} is a palindrome;
(3)~for any element \li{x} and any palindrome
  \li{[y}$_\texttt{1}$\li{, …, y}$_\ttvar{n}$\li{]}, the list
  \li{[x, y}$_\texttt{1}$\li{,} \hbox{\li{…, y}$_\ttvar{n}$\li{, x]}} is a
  palindrome.

Palindromes are another example where inductive predicates come into their own.
The following naive recursive definition cannot work because
\li{[x] ++ xs ++} \li{[x]} is not a constructor pattern, and the variable \li{x} is
repeated:
%
\lstinputlisting[linerange=palindrome_rec-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
A correct recursive definition is possible but beyond the scope of this guide.

Naturally, the reverse of a palindrome is a palindrome. It is a good exercise:
%
\lstinputlisting[linerange=reverse_palindrome-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
Informally:
%
\begin{quote}
The proof is by rule induction on the hypothesis \li{hxs}.

\textsc{Case} \li{Palindrome.nil}:
We must show \li{Palindrome} \hbox{\li{(reverse}} \li{[])}. This follows from
\li{Palindrome.nil} using \li{reverse [] = []}.

\textsc{Case} \li{Palindrome.single x}:
We must show \li{Palindrome} \li{(reverse [x])}. This follows from
\li{Palindrome.single} using \li{reverse [x] = [x]}.

\begin{sloppypar}
\textsc{Case} \li{Palindrome.sandwich x xs hxs}:
We must show \hbox{\li{Palindrome}} \hbox{\li{(reverse ([x] ++ xs ++ [x]))}} under
the hypothesis (\li{hxs}) \hbox{\li{Palindrome}} \li{xs}. The
induction hypothesis is \hbox{\li{Palindrome}} \hbox{\li{(reverse xs)}}.
By simplification, it suffices to show \hbox{\li{Palindrome ([x] ++ reverse xs ++}} \li{[x])}.
By \li{Palindrome.sandwich}, it suffices to show \li{Palindrome (reverse xs)},
which is exactly the induction hypothesis. \qed
\end{sloppypar}
\end{quote}

\subsection{Full Binary Trees}
\label{ssec:full-binary-trees}

Our third example is based on the type of binary trees introduced in
Section~\ref{sec:binary-trees}:

\lstinputlisting[linerange=BTree-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

A binary tree is \emph{full} if all its nodes have either zero or two
children. This can be encoded as an inductive predicate:

\lstinputlisting[linerange=IsFull-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
The first case states that the empty tree is a full tree. The second case
states that a nonempty tree is a full tree if it has two child trees that are
themselves full and that are both empty or both nonempty. The two cases neatly
follow the structure of the inductive type, so it is natural to reuse the names
\li{empty} and \li{node}.

The tree that consists of a node with empty trees as children is a full tree.
Here is a simple proof:

\lstinputlisting[linerange=IsFull_singleton-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}

A somewhat more interesting property of full trees is that fullness is preserved
by the mirror operation. Our first proof is by rule induction on
\li{ht : IsFull t}:
%
\lstinputlisting[linerange=IsFull_mirror-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
Since \li{IsFull}'s definition follows \li{BTree}'s definition, it is also
reasonable to perform structural induction on the tree \li{t}:
%
\lstinputlisting[linerange=IsFull_mirror_struct_induct-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
The key is the case distinction on the hypothesis
\hbox{\li{ht : IsFull}} \hbox{\li{(BTree.node a l}} \hbox{\li{r)}.} The \li{cases} tactic notices that the
\li{IsFull.}\allowbreak\li{empty} introduction rule cannot have been used to derive \li{ht},
so it only produces one case, corresponding to \li{IsFull.}\allowbreak\li{node}. As usual, the
tactical proof will make more sense if you inspect it in Visual Studio Code,
moving the cursor around.

\subsection{First-Order Terms}
\label{ssec:first-order-terms}

Our last example is based on an inductive type of first-order terms:

\lstinputlisting[linerange=term-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
A first-order term is either a variable \textit{x} or a function symbol
\relax{f} applied to a list of arguments: \relax{f}(\textit{t}$_\relax{1}$,
$\ldots$\,, \textit{t}$_\text{\textit n}$), where the mathematical variables
\textit{t}$_\text{1}$, $\ldots$, \textit{t}$_\text{\textit n}$ stand for
the arguments, which are themselves terms. Thus,
\relax{sin}(\relax{max}(\textit{x}, \textit{y})) is a first-order term. The
parameters \li{α} and \li{β} are the types of function symbols and variables,
respectively.

Not all terms are legal. For example, the term
\relax{min}(\relax{cos}(\textit{a}), \relax{cos}(\textit{a}, \textit{b})) is
considered ill-formed, because the function \relax{cos} is invoked with
inconsistent number of arguments (1 versus 2). Along with \li{α} and \li{β}, we
also consider the arity, represented by a function \li{arity : α} \li{→} \li{ℕ}
indicating how many arguments each function symbol takes.
For example, a binary symbol has arity 2.

The \li{WellFormed} predicate then checks whether the given term only contains
function symbol applications with the specified number of arguments:

\lstinputlisting[linerange=WellFormed-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
The \li{fn} case checks that the arguments \li{ts} are recursively well formed
and that the length of \li{ts} equals the specified arity for the function
symbol \li{f} in question.

Another interesting property of first-order terms is whether they contain
variables. This can be checked easily using an inductive predicate:

\lstinputlisting[linerange=VariableFree-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
There is no introduction rule corresponding to \li{Term.var} because variables
are never variable-free.

\section{Induction Pitfalls}
\label{sec:induction-pitfalls}

Some care is needed when invoking \li{induction} on inductive predicates. The
arguments of inductive predicates often evolve through the induction. Such
details are often glossed over in informal proofs, but proof assistants require
us to be precise.

Recall the definition of even numbers:

\lstinputlisting[linerange=even-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
If the goal has the form \li{h : Even n ⊢ P n}, applying \li{induction} on
\li{h} will produce the following subgoals:
%
{\tabletsmall
\begin{align*}
& \hbox{\lic|\ ⊢ P 0|} &
\hbox{\ctxt{k} \lic|: ℕ,| \ctxt{hk} \lic|: P k|} & \hbox{\lic|\ ⊢ P (k + 2)|}
\end{align*}%
}%
%
This works as desired.

The problem is when \li{Even}'s argument is not a variable. Applying
\li{induction} on the hypothesis \li{hev} in the goal
\hbox{\li{hev : Even (2 * n}} \li{+ 1) ⊢ False} fails with an error:
%
\begin{quote}
\tabletsmall\ttfamily\raggedright
index in target's type is not a variable (consider using the `cases` tactic instead)
\end{quote}%
%
To solve this issue, we need to replace \li{2 * n + 1} by a variable \li{m} and
add an equation \li{m = 2 * n + 1} as a hypothesis:
%
{\tabletsmall
\begin{align*}
\hbox{\ctxt{m} \lic|: 2 * n + 1,| \ctxt{hev} \lic|: Even m|} & \hbox{\lic|\ ⊢ False|}
\end{align*}%
}%
%
This goal is logically equivalent, but now \li{induction} produces two
subgoals:
%
{\tabletsmall
\begin{align*}
\hbox{\ctxt{m n} \lic|: ℕ,| \ctxt{hm} \lic|: 0 = 2 * n + 1|} & \hbox{\lic|\ ⊢ False|} \\
\hbox{\ctxt{m} \lic|: 2 * n + 1,| \ctxt{ih} \lic|: m = 2 * n + 1 → False,| \ctxt{hm} \lic|: m + 2 = 2 * n + 1|} & \hbox{\lic|\ ⊢ False|}
\end{align*}%
}%
%
Sadly, the second subgoal is not provable. The problem is that we want to
instantiate the \li{n} in the induction hypothesis \li{ih} with \li{n - 1} but
\li{n} is not instantiable.

The solution? We need to quantify over \li{n} to be able to
instantiate it in the induction hypothesis. This is done by specifying
\li{generalizing n} after \li{induction h}. Now we obtain the subgoals
%
{\tabletsmall
\begin{align*}
\hbox{\ctxt{m n} \lic|: ℕ,| \ctxt{hm} \lic|: 0 = 2 * n + 1|} & \hbox{\lic|\ ⊢ False|} \\
\hbox{\ctxt{m} \lic|: 2 * n + 1,| \ctxt{ih} \lic|: ∀n, m = 2 * n + 1 → False,| \ctxt{hm} \lic|: m + 2 = 2 * n + 1|} & \hbox{\lic|\ ⊢ False|}
\end{align*}%
}%
%
Now the variable \li{n} in the conclusion is disconnected from the variable
\li{n} in the induction hypothesis, and we can instantiate the hypothesis's
\li{n} with the conclusion's \li{n - 1}.

Putting all of this together, we obtain
%
\lstinputlisting[linerange=not_even_two_mul_add_one-q]{../lean/LoVe/LoVe06_InductivePredicates_DemoMaster.lean}
%
We use the theorem \li{Nat.succ_eq_add_one} to rewrite terms of the form
\li{Nat.succ} \li{n} to \li{n + 1} and the \li{linarith} tactic to perform simple
arithmetic reasoning. The theorem is very useful when we face a mixture of
\li{Nat.succ} and addition.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Theorems}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|funext| & functional extensionality \\
\li|propext| & propositional extensionality \\
\end{xltabular}

\subsection*{Tactic}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|linarith| & invokes a procedure for linear arithmetic \\
\end{xltabular}

\endgroup
