\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 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 logicians' way to achieve the same result. In Lean,
instead of a set, we would define a characteristic predicate inductively:

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

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 lemma 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, if \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/love05_inductive_predicates_demo_master.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 inspection of 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.%
\footnote{We could cheat and add an axiom stating \li{even 1}, but this would be
inconsistent. Alternatively, we could add an assumption \li{even 1} to our
lemma and use it to prove \li{even 1}, but this would be tautological and hence
pointless.}

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}
constant even : ℕ → Prop
axiom even.zero    : even 0
axiom even.add_two : ∀k : ℕ, even k → even (k + 2)
\end{lstlisting}
%
replacing \li{inductive} by \li{constant} 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₂-q]{../lean/love05_inductive_predicates_demo_master.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{refl},} \li{simp}, \li{#reduce}, and
\li{#eval}. 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₃-q]{../lean/love05_inductive_predicates_demo_master.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/love05_inductive_predicates_demo_master.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/love05_inductive_predicates_demo_master.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/love05_inductive_predicates_demo_master.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}

Are there any convincing non-toy applications of inductive predicates? The
answer is yes. Consider the reflexive transitive closure
\textit{r}$^*$ of a binary relation~\textit{r}. The star (${}^*$) operator is
often defined 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/love05_inductive_predicates_demo_master.lean}
%
We represent relations as binary predicates rather than sets of pairs,
writing \hbox{\li{r a b}} for \li{(a, b) ∈ r}. The reflexive transitive closure
of \li{r} is written \li{star r}. Inside the definition, \li{r} is
omitted since it is declared as a parameter, on the left of a colon (\li{:}).
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 a b
\end{lstlisting}
%
or at the other extreme
\begin{lstlisting}
| base (a b : α) (hab : r a b) : star a b
\end{lstlisting}
%
and similarly for \li{star.refl} and \li{star.trans}. 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{|}\, \ttvar{rule-name}$_\texttt{1}$
  \,\lic{(}\ttvar{params}$_\texttt{11}$ \lic{:} \ttvar{type}$_\texttt{11}$\lic{)} $\ldots$
    \lic{(}\ttvar{params}$_{\texttt{1}\ttvar{m}}$ \lic{:} \ttvar{type}$_{\texttt{1}\ttvar{m}}$\lic{)}
  \,\lic{:}\, \rlap{\ttvar{proposition}$_\texttt{1}$} \\[-0.5\jot]
\noindent\hbox{}\phantom{\lic{|}\, \textit{co}}$\vdots$ \\
\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}$ \lic{:} \ttvar{type}$_\ttvar{nm}$\lic{)}
  \,\lic{:}\, \rlap{\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; \emph{they do not need to be constructor
patterns}. We can also use curly braces \li|{ }| instead of parentheses \li|( )|
if we wanted 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/love05_inductive_predicates_demo_master.lean}

To summarize, each introduction rule of an inductive predicate \li{p} consists
of the following components:
%
\begin{itemize}
\item an application of \li{p} to some arguments, forming a \emph{pattern};
\item zero or more \emph{conditions} that must be fulfilled, which may apply
  \li{p} recursively;
\item \emph{variables} that may appear in the pattern and the conditions.
\end{itemize}
%
Thus, for rule \li{star.base}, the pattern is \li{star 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]{../lean/love05_inductive_predicates_demo_master.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:definitions-and-statements}, 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]{../lean/love05_inductive_predicates_demo_master.lean}
%
(Strictly speaking, in Lean, some of the above definitions are actually
structures and not inductive predicates, but the difference is unimportant:
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{(λx : α, p)}} and \li{eq x y}. Notice how \li{λ} 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 only state 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 inductive predicates. Nor does it have explicit
introduction or elimination rules. The introduction principle is
\li{λ}-expression \li{λx, _}, 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/love05_inductive_predicates_demo_master.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 precisely the subgoals produced by \li{induction' h with k hk ih}.

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}), massaging
  \li{P[ ]} to make it 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}.

When the argument to \li{even} in \li{h} is not a variable, performing an
induction will destroy its structure. Fortunately, \hbox{\li{induction'}} (with
a prime) notices this situation and preserves the information in a hypothesis
called \li{index_eq}. Thus, given the goal \hbox{\li{h :}} \hbox{\li{even (2 * n}}
\hbox{\li{+ 1) ⊢ false},} invoking \li{induction' h with k hk ih} produces the
induction step

{\tabletfootnotesize

\kern-\baselineskip

\begin{align*}
& \hbox{\ctxt{k} \lic|: ℕ,| \ctxt{h} \lic|: even k,| \ctxt{n} \lic|: ℕ,|
  \ctxt{index\_eq} \lic|: k + 1 = 2 * n,|
  \ctxt{ih} \lic|: ∀n, ¬ k = 2 * n + 1|} \\[-\jot]
& \hbox{\lic|\⊢ false|}
\end{align*}}%
%
for \li{even.add_two}. The trivial base case \li{¬ even 1} is eliminated
automatically by basic constructor reasoning.

The hypothesis \li{index_eq} records the equality
between \li{even}'s argument in the initial goal (i.e., \li{2 * n + 1}) and
\li{even}'s argument in the \li{even.add_two} rule (i.e., \li{k +} \li{2}).
Notice that the equation is simplified by subtracting \li{1} from both sides.
To continue the proof, we need to instantiate \li{n} in the induction
hypothesis with \li{n - 1}. Here is the complete proof:
%
\lstinputlisting[linerange=not_even_two_mul_add_one-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
We use the lemma \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 lemma is very useful when we face a mixture of
\li{nat.succ} and addition.

The reflexive transitive closure \li{star r} is similar to \li{even}.
Given a goal \li{h : star} \li{r 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/love05_inductive_predicates_demo_master.lean}
%
We use the \li{case} tactic both to document which cases we are focusing on and
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 a great help when
facing 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/love05_inductive_predicates_demo_master.lean}
%
The proof requires two lemmas 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 lemma \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 normally 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 is generally not possible.

\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 lemma 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.elim_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 understand.

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 inventing the name
\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
\li{Q ∨ ¬ Q}---i.e., \li{or Q (¬ Q)} (Section~\ref{sec:logical-symbols}). Then
\li{cases'} is simply 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.intro_left hQ : Q ∨ ¬ Q]}} \\
\text{\ctxt{hnQ} \lic{: ¬ Q}} & \text{\lic{\ ⊢ P[or.intro_right hnQ : Q ∨ ¬ Q]}}
\end{align*}
%
There is no need to massage \li{P} because \li{or.intro_left hQ} and
\hbox{\li{or.intro_right}} \li{hnQ} have the same type as
\li{classical.em Q}---namely, \li{Q ∨ ¬ Q}. In practice,
the goal would be \li{⊢ P}, with no dependency on \li{classical.em Q}. We would
then have
%
\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 lemma,
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/love05_inductive_predicates_demo_master.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.

For those who have a preference for structured proofs, here is a version of the
proof with dependently typed pattern matching on \li{hn : even n}:
%
\lstinputlisting[linerange=even_iff₂-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
For technical reasons, we must pattern-match on \li{or.inl} and \hbox{\li{or.inr},}
which are constructors and which take a single explicit argument, rather than on
the variants \li{or.intro_left} and \li{or.}\allowbreak\li{intro_right}, which
are defined functions that take two explicit arguments.

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

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

\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/love05_inductive_predicates_demo_master.lean}
%
This definition captures the following mathematical intuition:
%
\begin{quote}
The set of sorted lists is defined as the smallest set \li{S} 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/love05_inductive_predicates_demo_master.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 for everything:
%
\lstinputlisting[linerange=sorted_3_5₂-q]{../lean/love05_inductive_predicates_demo_master.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/love05_inductive_predicates_demo_master.lean}

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

\lstinputlisting[linerange=not_sorted_17_13-q]{../lean/love05_inductive_predicates_demo_master.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{sorted.nil} and \hbox{\li{sorted.single}} cases, because they cannot match a two-element list. Then we
just need to invoke \li{linarith} 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/love05_inductive_predicates_demo_master.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₂-q]{../lean/love05_inductive_predicates_demo_master.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/love05_inductive_predicates_demo_master.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/love04_functional_programming_demo_master.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=is_full-q]{../lean/love05_inductive_predicates_demo_master.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=is_full_singleton-q]{../lean/love05_inductive_predicates_demo_master.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 : is_full t}:
%
\lstinputlisting[linerange=is_full_mirror-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
Since \li{is_full}'s definition follows \li{btree}'s definition, it is also
reasonable to perform structural induction on the tree \li{t}:
%
\lstinputlisting[linerange=is_full_mirror₂-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
The key is the case distinction on the hypothesis
\li{ht : is_full (node a l r)}. The \li{cases'} tactic notices that the
\li{is_full.empty} introduction rule cannot have been used to derive \li{ht},
so it only produces one case, corresponding to \li{is_full.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/love05_inductive_predicates_demo_master.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 metavariables
\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
different 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{well_formed}
predicate then checks whether the given term only contains function symbol
applications with the specified number of arguments:

\lstinputlisting[linerange=well_formed-q]{../lean/love05_inductive_predicates_demo_master.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=variable_free-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
There is no introduction rule corresponding to \li{term.var} because variables
are never variable-free.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Lemmas}

\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
