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

Inductive predicates are reminiscent of the Horn clauses of Prolog-style logic
programming languages. But Lean offers a much stronger logic than Prolog, so
we need to do some work---interactive proving---to establish theorems instead
of just running the Prolog interpreter. A possible view of Lean:
%
\[\text{Lean \li{=} typed functional programming \li{+} logic programming \li{+} more logic}\]

\section{Introductory Example}
\label{sec:introductory-example-inductive-predicates}

\emph{Inductive predicates}, or (more precisely) inductively defined
propositions, are familiar from mathematics. Consider the example:

\begin{quote}
  The set \textit{E} of even natural numbers is defined as the smallest set
  closed under the following rules: (1)~0 $\in$ \textit{E}; and (2)~for every
  \textit{n} $\in$ $\mathbb{N}$, if \textit{n} $\in$ \textit{E}, then
  \textit{n}~$+$~2 $\in$ \textit{E}.
\end{quote}

In Lean, we write

\lstinputlisting[linerange=even-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
This should look familiar: By the Curry–Howard correspondence, what we have
done is introduce a new unary type constructor, \li{even}. Inductive types and
inductive predicates are implemented as the same mechanism in Lean.

The \li{even} predicate has two constructors:\ \li{zero} and \li{add_two}. These
can be used to build proof terms. The \li{even} predicate can be seen as a tree
type, the trees being the corresponding proof terms (or proof trees). Thanks to
the ``no junk'' guarantee of inductive definitions, \li{zero} and \li{add_two}
are the only two ways to construct \li{even}. Thus, there is no danger of
accidentally proving that \li{1} is even.

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

The truth values \li{false} and \li{true}, the connectives \li{∧} and \li{∨},
the \li{∃} quantifier, and the equality predicate \li{=} are all defined as
inductive propositions or predicates:

\begin{lstlisting}
inductive false : Prop

inductive true : Prop
| intro : true

inductive and (a b : Prop) : Prop
| intro : a → b → and

inductive or (a b : Prop) : Prop
| intro_left : a → or
| intro_right : b → or

inductive Exists {α : Type} (p : α → Prop) : Prop
| intro : ∀a : α, p a → Exists

inductive eq {α : Type} : α → α → Prop
| refl (a : α) : eq a a
\end{lstlisting}

The notations \li{∃x : α, p} and \li{x = y} are syntactic sugar for
\li{Exists (λx : α, p)} and \li{eq x y}, respectively. In contrast,
\li{∀} (\li{=} \li{Π}) and \li{→} are built directly into the logic
and are not defined as inductive predicates. Notice that there is no constructor
for \li{false}. There are no proofs of \li{false}, just like there is no proof
that \li{1} is even.

\section{Introduction, Elimination, Induction, and Inversion}
\label{sec:introduction-elimination-induction-and-inversion}

We saw in Section~\ref{sec:proofs-about-logical-connectives-and-quantifiers}
that the logical connectives and the $\exists$ quantifier are equipped with
introduction and elimination rules. The same is true for arbitrary inductive
predicates \li{p}.

\li{p}'s constructors are introduction rules. They typically have the form
\li{∀…, … → p …}\,. They can be used to prove goals of the form \li{p …}\,.

Elimination works the other way around. It extracts information from a lemma or
hypothesis of the form \li{p …}\,. Elimination takes various forms:\ pattern
matching (at the top-level of a definition or lemma, or with \li{match}), the
\li{cases} and \li{induction} tactics, or custom elimination rules (e.g.,
\li{and.elim_left}).

Just as we can perform induction on a term, we can perform induction on a
proof term using the \li{induction} tactic. This is sometimes called
\emph{rule induction}, because the induction is on the introduction rules
(i.e., the constructors of the proof term).

Often it is convenient to rewrite concrete terms of the form \li{p (c …)},
where \li{c} is typically a constructor. We can state and prove an
\emph{inversion rule} to support such eliminative reasoning. The general
format of an inversion rule (assuming a binary constructor) is as follows:
%
\[\hbox{\li{∀x y, p (c x y) → (∃…, … ∧ …) ∨ … ∨ (∃…, … ∧ …)}}\]
%
It can be useful to combine introduction and elimination in a single lemma,
which can be used for rewriting both the hypotheses and the conclusions of
goals:
%
\[\hbox{\li{∀x y, p (c x y) ↔ (∃…, … ∧ …) ∨ … ∨ (∃…, … ∧ …)}}\]
%
For example:
%
\[\hbox{\li{∀n : ℕ, even n ↔ n = 0 ∨ ∃m : ℕ, n = m + 2 ∧ even m}}\]

\section{Example: Full Binary Trees}
\label{sec:example-full-binary-trees}

We now review in turn four examples of inductive predicates. Our first
example is based on the type of binary trees introduced in
Section~\ref{sec:example-binary-trees}:

\lstinputlisting[linerange=tree-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 as follows:

\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 tree is a full tree if has two child trees that are themselves
full and that either both are empty or both are nonempty.

Syntactically, we can put the arguments on the left of the colon, as parameters,
or on the right. Here is an equivalent definition of the latter kind:

\lstinputlisting[linerange=is_full₂-q]{../lean/love05_inductive_predicates_demo_master.lean}

The tree that consists of a node with empty tree as children is a full tree.
Here is a simple proof, using the introduction rule \li{is_full.node}:

\lstinputlisting[linerange=is_full_singleton-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
The proof makes use of the \li{repeat} combinator, which applies the tactic
specified within curly braces repeatedly, as long as it succeeds. Here it
is applied twice, to eliminate the two identical goals \li{is_full empty}.

A somewhat more interesting property of full trees is that fullness is preserved
by the mirror operation. Our first proof is by structural induction on \li{t}:

\lstinputlisting[linerange=is_full_mirror-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
The key to the proof is the \li{cases} tactic invocation on the hypothesis
\li{full_t}~\li{:} \li{is_full (node a l r)}. The tactic notices, via a simple
syntactic check, that the first introduction rule (\li{is_full.empty}) cannot
have been used to derive \li{is_full} \li{(node a l r)}, so it only produces one
case, corresponding to the second introduction rule (\li{is_full.node}). As
usual, the tactical proof makes more sense if you inspect it in Visual Studio
Code, moving the cursor around.

Another way to carry out the proof is to perform pattern matching on
\li{is_full} \li{t} at the top level:

\lstinputlisting[linerange=is_full_mirror₂-q]{../lean/love05_inductive_predicates_demo_master.lean}

A third approach relies on an inversion rule. The rule is proved by a
combination of introduction and elimination steps:

\lstinputlisting[linerange=is_full_node_iff-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
The proof relies on the \li{cc} tactic, which implements an algorithm called
congruence closure. The tactic studies the equalities present in the problem
and attempts to derive a proof from them. It is described in slightly more
detail below (Section~\ref{sec:new-tactics-inductive-predicates}).

Equipped with the inversion rule, we can perform a simpler proof that relies
on the \li{simp} tactic:

\lstinputlisting[linerange=is_full_mirror₃-q]{../lean/love05_inductive_predicates_demo_master.lean}

\section{Example: Sorted Lists}
\label{sec:example-sorted-lists}

Our next 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}

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. Notice the invocation of
\li{lin}\-\li{arith}. This tactic can be invoked to solve linear arithmetic
goals. It is described below
(Section~\ref{sec:new-tactics-inductive-predicates}). A more compact proof
follows, using proof terms for everything except the arithmetic subgoal:

\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, but this time we need
to use elimination, in the form of pattern matching:

\lstinputlisting[linerange=not_sorted_17_13-q]{../lean/love05_inductive_predicates_demo_master.lean}
%
To prove a negation, we assume the unnegated formula and prove false. From the
assumption that \li{[17, 13]} is sorted, we derive that \li{17 ≤ 13}, which
together with the obvious numeric truth that \li{¬ (17 ≤ 13)} leads to a
contradiction. The contradiction is easily detected by \li{cc}.

\section{Example: Well-formed and Ground First-Order Terms}
\label{sec:example-well-formed-and-ground-first-order-terms}

Our third 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
\textit{f} applied to a list of arguments: \textit{f}(\textit{t}$_\textrm{1}$,
$\ldots$, \textit{t}$_\textrm{\textit n}$), where the metavariables
\textit{t}$_\textrm{\textit j}$ stand for the arguments, which are themselves
terms. The parameters \li{α} and \li{β} are the types of function symbols and
variables, respectively.

Not all terms are legal. For example, the term
\textit{g}(\textit{f}(\textit{a}), \textit{f}(\textit{a},\textit{b})) is
considered ill formed, because the function \textit{f} is invoked with
different number of arguments (once with one argument and once with two).
Along with \li{α} and \li{β}, we also consider the arity, represented by a
function \li{arity : α → N} indicating how many arguments each function symbol
takes. 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. Additionally, it requires 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}
%
This time, there is no \li{var} case, for obvious reasons.

\section{Example: Reflexive Transitive Closure}
\label{sec:example-reflexive-transitive-closure}

Our last example is the reflexive transitive closure of a relation, modeled
as a binary predicate \li{rtc}.

\lstinputlisting[linerange=rtc-q]{../lean/love05_inductive_predicates_demo_master.lean}

One of the key properties of \li{rtc} is that it is idempotent---applying
\li{rtc} to \li{rtc r} has no effect, for any binary predicate \li{r}:

\lstinputlisting[linerange=rtc_rtc_iff_rtc-q]{../lean/love05_inductive_predicates_demo_master.lean}

In the induction proof, we use the \li{case} syntax both to increase readability
of the proof script and to give intuitive names to the emerging variables. It is
easy to get lost in goals containing long, automatically generated names. The
goal management tactics discussed in Section~\ref{sec:goal-management-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=rtc_rtc_eq_rtc-q]{../lean/love05_inductive_predicates_demo_master.lean}

The proof requires two lemmas that are available because Lean's logic is
classical. \emph{Functional extensionality} (\li{funext}) states that two
functions that yield equal results for all inputs must be equal.
\emph{Propositional extensionality} (\li{propext}) states that equivalence of
propositions coincides with equality.

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{funext} & \noindent\llap{\li|:|~}\li|(∀x, ?f x = ?g x) → ?f = ?g| \\
\li{propext} & \noindent\llap{\li|:|~}\li|(?a ↔ ?b) → ?a = ?b| \\
\end{tabularx}

\kern\belowdisplayskip

\noindent
These properties may seem obvious, but there are proof assistants built on
weaker, intuitionistic logics in which the property do not generally hold.

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

Inductive predicates often have parameters that evolve through the induction.
Pattern matching and \li{cases} handle this gracefully, but some care is
necessary when invoking \li{induction}. Such details are often glossed over in
informal proofs, but proof assistants require us to be precise.

Suppose we have the definition

\begin{lstlisting}
inductive even : ℕ → Prop
| zero    : even 0
| add_two : ∀n, even n → even (n + 2)
\end{lstlisting}
%
If the goal has the form \li{even n → p n}, applying \li{induction} will
produce the following cases:
%
\begin{itemize}
\item \li{p 0}

\item \li{∀n, p n → p (n + 2)}
\end{itemize}
%
This works as desired.

The problem is that when the argument to \li{even} is not a variable,
\li{induction} destroys the identity of the argument. (With a variable,
there is nothing to destroy.) Thus, applying
\li{induction} on \li{even (2 * n + 1) → false} produces the subgoals
%
\begin{itemize}
\item \li{false}

\item \li{false → false}
\end{itemize}
%
The first subgoal is not provable. To solve this issue, we need to replace
\li{2 * n + 1} by a variable \li{x} and add an equation \li{x = 2 * n + 1} as
a hypothesis:
%
\[\hbox{\li{∀x, even x → x = 2 * n + 1 → false}}\]
%
This proposition is logically equivalent, but now we obtain very different
subgoals:
%
\begin{itemize}
\item \li{2 * n + 1 = 0 → false}

\item \li{∀x, (2 * n + 1 = x → false) → 2 * n + 1 = x + 2 → false}
\end{itemize}
%
Sadly, the second subgoal is not provable. The problem is that we want to
instantiate the \li{n} in the assumption with \li{n + 1} but \li{n}
is not instantiable.

The solution? We need to explicitly quantify over \li{n} to be able to
instantiate it in the induction hypothesis. We state our goal as
%
\[\hbox{\li{∀x, even x → ∀n, x = 2 * n + 1 → false}}\]
%
Now we obtain the subgoals
\begin{itemize}
\item \li{∀n, 2 * n + 1 = 0 → false};

\item \li{∀x, (∀n, 2 * n + 1 = x → false) → ∀n, 2 * n + 1 = x + 2 → false}.
\end{itemize}
%
Now the variable \li{n} in the conclusion is disconnected from the variable
\li{n} in the assumption, and we can instantiate the assumption's \li{n} with
the conclusion's \li{n + 1}.

\section{New Tactics}
\label{sec:new-tactics-inductive-predicates}

\subsection{cc}

The \li{cc} tactic applies an algorithm known as \emph{congruence closure} to
derive new equalities from those that are present in the goal. For example, if
the goal contains \li{b = a} and \li{f b ≠ f a} as hypotheses, the congruence
closure procedure will derive \li{f b = f a} from \li{b = a} and discover a
contradiction with \li{f b ≠ f a}. The tactic is also suitable for more
pedestrian work, inferring for example \li{a ∨ b ∨ c} from \li{b}.

\subsection{linarith}

The \li{linarith} tactic can be used to prove goals involving linear
arithmetic equalities or inequalities. ``Linear'' means that multiplication
and division do not occur, of if they do they one of the operand must be a
numeric constant. For example,
\li{2 * x < y} is a linear constraint---indeed, it can be rewritten as
\li{x + x < y}---whereas \li{x * y < y} is nonlinear.

\subsection{norm\_num}

The \li{norm_num} tactic can be used to prove goals requiring normalization of
arithmetic expressions. For example, it can be used to prove that
\li{1 + (x + -1) = x}.

\section{Summary of New Syntax}

\small

\subsection{Tactic Combinators}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|repeat| & repeatedly applies a tactic on all goals and subgoals until failure \\
\end{tabularx}

\subsection{Tactic}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|cc| & propagates the equalities in the goal \\
\li|linarith| & applies a procedure for linear arithmetic \\
\li|norm_num| & normalizes arithmetic expressions \\
\end{tabularx}
