9.1.1. Example: The Collatz Conjecture🔗

The Collatz Conjecture is a famous open problem in number theory.

Its statement is quite simple. First, we define a function collatzStep on numbers as follows:

Next, we look at what happens when we repeatedly apply collatzStep to some given starting number. For example, collatzStep 12 is 6, and collatzStep 6 is 3, so by repeatedly applying collatzStep we get the sequence 12, 6, 3, 10, 5, 16, 8, 4, 2, 1.

Similarly, if we start with 19, we get the longer sequence 19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8, 4, 2, 1.

Both of these sequences eventually reach 1. The question posed by Collatz was: Is the sequence starting from any positive natural number guaranteed to reach 1 eventually?

To formalize this question in Lean, we might try to define a recursive function that calculates the total number of steps that it takes for such a sequence to reach 1. You can write this definition in a standard programming language, but it is rejected by Lean's termination checker, since the argument to the recursive call, collatzStep n, is not "obviously smaller" than n.

fail to show termination for
  reaches1In
with errors
failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    reaches1In (collatzStep n)


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
n:Nat⊢ collatzStep n < n

Indeed, this isn't just a pointless limitation: functions in Lean are required to be total, to ensure logical consistency.

Moreover, we can't fix it by devising a more clever termination checker: deciding whether this particular function is total would be equivalent to settling the Collatz conjecture!

Another idea could be to express the concept "eventually reaches 1 in the Collatz sequence" as a recursively defined property of numbers CollatzHoldsFor : Nat → Prop. This is also rejected by the termination checker. In principle, we could convince Lean that div2 n is smaller than n by supplying an appropriate proof. However, we still can't convince it that (3 * n) + 1 is smaller than n!

fail to show termination for
  CollatzHoldsFor
with errors
failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    CollatzHoldsFor (div2 n)


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
n x✝:Nat⊢ div2 n < x✝

Fortunately, there is another way to do it: we can express the concept "reaches 1 eventually in the Collatz sequence" as an inductively defined property of numbers. Intuitively, this property is defined by a set of rules:

              ─────────────────── (one)
               CollatzHoldsFor 1

n.even = true     CollatzHoldsFor (div2 n)
─────────────────────────────────────────── (even)
               CollatzHoldsFor n

n.even = false    CollatzHoldsFor ((3 * n) + 1)
─────────────────────────────────────────────── (odd)
               CollatzHoldsFor n

So there are three ways to prove that a number n eventually reaches 1 in the Collatz sequence:

• n is 1;

• n is even and div2 n eventually reaches 1;

• n is odd and (3 * n) + 1 eventually reaches 1.

We can prove that a number reaches 1 by constructing a (finite) derivation using these rules. For instance, here is the derivation proving that 12 reaches 1 (where we leave out the evenness/oddness premises):

─────────────────────── (one)
  CollatzHoldsFor 1
─────────────────────── (even)
  CollatzHoldsFor 2
─────────────────────── (even)
  CollatzHoldsFor 4
─────────────────────── (even)
  CollatzHoldsFor 8
─────────────────────── (even)
  CollatzHoldsFor 16
─────────────────────── (odd)
  CollatzHoldsFor 5
─────────────────────── (even)
  CollatzHoldsFor 10
─────────────────────── (odd)
  CollatzHoldsFor 3
─────────────────────── (even)
  CollatzHoldsFor 6
─────────────────────── (even)
  CollatzHoldsFor 12

Formally in Lean, the CollatzHoldsFor property is inductively defined:

What we've done here is to use Lean's inductive definition mechanism to characterize the property "Collatz holds for..." by stating three different ways in which it can hold: (1) Collatz holds for 1, (2) if Collatz holds for div2 n and n is even, then Collatz holds for n, and (3) if Collatz holds for (3 * n) + 1 and n is odd, then Collatz holds for n. This Lean definition directly corresponds to the three rules we wrote informally above.

For particular numbers, we can now prove that the Collatz sequence reaches 1 (we'll look more closely at how it works a bit later in the chapter). Each step applies a rule and discharges the boolean evenness premise by rfl; the recursive premise is then reduced by the kernel from CollatzHoldsFor (div2 12) to CollatzHoldsFor 6, etc.

The Collatz conjecture then states that the sequence beginning from any positive number reaches 1:

If you succeed in proving this conjecture, you've got a bright future as a number theorist! But don't spend too long on it — it's been open since 1937.

9.1.2. Example: Binary Relation for Comparing Numbers🔗

A binary relation on a set α has Lean type α → α → Prop. This is a family of propositions parameterized by two elements of α — i.e., a proposition about pairs of elements of α.

For example, one familiar binary relation on Nat is Le : Nat → Nat → Prop, the less-than-or-equal-to relation, which can be inductively defined by the following two rules:

  ─────── (le_refl)
  Le n n

  Le n m
──────────── (le_step)
Le n (m + 1)

These rules say that there are two ways to show that a number is less than or equal to another: either observe that they are the same number, or, if the second has the form m + 1, give evidence that the first is less than or equal to m.

This definition is a bit simpler and more elegant than the boolean function Nat.ble we defined in Basics. As usual, Le and Nat.ble are equivalent, and there is an exercise about that later.

9.1.3. Example: Transitive Closure🔗

Another example: the transitive closure of a relation r is the smallest relation that contains r and that is transitive. This can be defined by the following two rules:

              r x y
         ─────────────── (t_step)
         TransGen r x y

TransGen r x y    TransGen r y z
──────────────────────────────────── (t_trans)
         TransGen r x z

In Lean this looks as follows:

"Gen" is short for "generated by" — TransGen r means the smallest transitive relation generated by r.

For example, suppose we define a "parent of" relation on a group of people...

In this example, sage is a parent of both cleo and ridley; and cleo is a parent of moss.

The ParentOf relation is not transitive, but we can define an "ancestor of" relation as its transitive closure:

Here is a derivation showing that sage is an ancestor of moss:

 ——————————————————— (sage_cleo) ——————————————————— (cleo_moss)
 ParentOf .sage .cleo            ParentOf .cleo .moss
————————————————————— (step)    ————————————————————— (step)
AncestorOf .sage .cleo          AncestorOf .cleo .moss
———————————————————————————————————————————————————— (trans)
                AncestorOf .sage .moss

Computing the transitive closure can be undecidable even for a relation r that is decidable (e.g., the CollatzStep relation below, whose closure is CollatzStepMulti), so in general we can't expect to define transitive closure as a boolean function. Fortunately, Lean allows us to define transitive closure as an inductive relation.

The transitive closure of a binary relation cannot, in general, be expressed in first-order logic (see the Logic chapter), since doing so would require quantifying over relations themselves. The logic of Lean is, however, much more powerful — being higher-order, as we saw there — and can easily define such inductive relations.

9.1.4. Example: Reflexive and Transitive Closure🔗

As another example, the reflexive and transitive closure of a relation r is the smallest relation that contains r and that is reflexive and transitive. This can be defined by the following three rules (where we added a reflexivity rule to TransGen):

                   r x y
         ——————————————————————— (step)
           ReflTransGen r x y

         ——————————————————————— (refl)
           ReflTransGen r x x

   ReflTransGen r x y    ReflTransGen r y z
—————————————————————————————————————————————— (trans)
           ReflTransGen r x z

For instance, this enables an equivalent definition of the Collatz conjecture. First we define a binary relation corresponding to the "Collatz step function" collatzStep:

This Collatz step relation can be used in conjunction with the reflexive and transitive closure operation to define a Collatz multi-step relation, expressing that a number n reaches another number m in zero or more Collatz steps:

This CollatzStepMulti relation defined in terms of ReflTransGen allows for more interesting derivations than the linear ones of the directly defined CollatzHoldsFor relation:

collatzStep 16 = 8          collatzStep 8 = 4          collatzStep 4 = 2          collatzStep 2 = 1
────────────────── (step)   ───────────────── (step)   ───────────────── (step)   ───────────────── (step)
CollatzStepMulti 16 8       CollatzStepMulti 8 4       CollatzStepMulti 4 2       CollatzStepMulti 2 1
──────────────────────────────────────────── (trans)   ─────────────────────────────────────────── (trans)
              CollatzStepMulti 16 4                                  CollatzStepMulti 4 1
              ───────────────────────────────────────────────────────────────────────── (trans)
                                     CollatzStepMulti 16 1

9.1.5. Example: Permutations🔗

The familiar mathematical concept of permutation also has an elegant formulation as an inductive relation. For simplicity, let's focus on permutations of lists with exactly three elements.

We can define such permutations by the following rules:

   ───────────────────────── (swap12)
   Perm3 [a, b, c] [b, a, c]

   ───────────────────────── (swap23)
   Perm3 [a, b, c] [a, c, b]

Perm3 l₁ l₂       Perm3 l₂ l₃
───────────────────────────── (trans)
         Perm3 l₁ l₃

For instance, we can derive Perm3 [1, 2, 3] [3, 2, 1] as follows:

───────────────────────── (swap12)  ─────────────────────── (swap23)
Perm3 [1, 2, 3] [2, 1, 3]            Perm3 [2, 1, 3] [2, 3, 1]
─────────────────────────────────────────────────────────────────(trans)    ───────────────────── (swap12)
Perm3 [1, 2, 3] [2, 3, 1]                                                    Perm3 [2, 3, 1] [3, 2, 1]
───────────────────────────────────────────────────────────────────────────────────────────────────────── (trans)
Perm3 [1, 2, 3] [3, 2, 1]

This definition says:

• If l₂ can be obtained from l₁ by swapping the first and second elements, then l₂ is a permutation of l₁.

• If l₂ can be obtained from l₁ by swapping the second and third elements, then l₂ is a permutation of l₁.

• If l₂ is a permutation of l₁ and l₃ is a permutation of l₂, then l₃ is a permutation of l₁.

In Lean, we can define Perm3 as follows:

9.1.6. Example: Evenness (yet again)🔗

We've already seen two ways of stating a proposition that a number n is even: We can say

(1) Nat.even n = true (using the recursive boolean function Nat.even), or

(2) ∃ k, n = Nat.double k (using an existential quantifier).

A third possibility, which we'll use as a simple running example in this chapter, is to say that a number is even if we can establish its evenness from the following two rules:

  ────────── (zero)
    Even 0

    Even n
—————————————— (succ_succ)
  Even (n + 2)

Intuitively these rules say that:

• The number 0 is even.

• If n is even, then n + 2 is even.

(Defining evenness in this way may seem a bit confusing, since we have already seen two perfectly good ways of doing it. It makes a convenient running example because it is simple and compact, but we will soon return to the more compelling examples above.)

To illustrate how this new definition of evenness works, let's imagine using it to show that 4 is even:

                 ──────── (zero)
                  Even 0
          ─────────────────────── (succ_succ)
          Even (.succ (.succ 0))
────────────────────────────────────────────── (succ_succ)
Even (.succ (.succ (.succ (.succ 0))))

In words, to show that 4 is even, by rule succ_succ, it suffices to show that 2 is even. This, in turn, is again guaranteed by rule succ_succ, as long as we can show that 0 is even. But this last fact follows directly from the zero rule.

We can translate the informal definition of evenness from above into a formal inductive declaration, where each "way that a number can be even" corresponds to a separate constructor:

Such definitions are interestingly different from previous uses of inductive for defining inductive datatypes like Nat or List. For one thing, we are defining not a Type (like Nat) or a function yielding a Type (like List), but rather a function from Nat to Prop — that is, a property of numbers. But what is really new is that, because the Nat argument of Even appears to the right of the colon on the first line, it is allowed to take different values in the types of different constructors: 0 in the type of Even.zero and (n + 2) in the type of Even.succ_succ. Accordingly, the type of each constructor must be specified explicitly (after a colon), and each constructor's type must have the form Even n for some natural number n.

In contrast, recall the definition of List:

or (equivalently but more explicitly):

This definition introduces the α parameter globally, to the left of the colon, forcing the result of List.nil and List.cons to be the same type (i.e., List α). But if we had tried to bring Nat to the left of the colon in defining Even, we would have seen an error:

Mismatched inductive type parameter in
  WrongEven 0
The provided argument
  0
is not definitionally equal to the expected parameter
  n

Note: The value of parameter `n` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.

In an inductive definition, an argument to the type constructor on the left of the colon is called a "parameter," whereas an argument on the right is called an "index" or "annotation."

For example, in inductive List (α : Type) ..., the α is a parameter, while in inductive Even : Nat → Prop ..., the unnamed Nat argument is an index.

We can think of the inductive definition of Even as defining a Lean property Even : Nat → Prop, together with two "evidence constructors":

Even : Nat → Prop

Even.zero : Even 0

Even.succ_succ {n : Nat} (h : Even n) : Even (n + 2)

These evidence constructors can be thought of as "primitive evidence of evenness," and they can be used later on just like proven theorems. In particular, we can use Lean's apply and exact tactics with the constructor names to obtain evidence for Even of particular numbers...

... or we can use function application syntax to combine several constructors:

... or we can also use the constructor tactic we saw earlier to select the appropriate inductive constructor:

In this way, we can also prove theorems that have hypotheses involving Even.

9.1.7. Constructing Evidence for Permutations🔗

Similarly, we can apply the evidence constructors to obtain evidence of Perm3 [1, 2, 3] [3, 2, 1]:

And again we can equivalently use function application syntax to combine several constructors. (Note that the Lean type checker can infer not only types, but also Nats and Lists, when they are clear from the context.)

So the informal derivation trees we drew above are not too far from what's happening formally. Formally, we're using the evidence constructors to build evidence trees, similar to the finite trees we built using the constructors of data types such as Nat, List, binary trees, etc.

9.2.1. Destructing and Inverting Evidence🔗

Suppose we are proving some fact involving a number n, and we are given Even n as a hypothesis. We already know how to perform case analysis on n using cases or induction, generating separate subgoals for the case where n = 0 and the case where n = n' + 1 for some n'. But for some proofs we may instead want to analyze the evidence for Even n directly.

As a tool for such proofs, we can formalize the intuitive characterization that we gave above for evidence of Even n, using cases.

Facts like this are often called "inversion lemmas" because they allow us to "invert" some given information to reason about all the different ways it could have been derived.

∀ (n : Nat), Even n → n = 1 → true = false

We can use the inversion lemma that we proved above to help structure proofs:

Note how the inversion lemma produces two subgoals, which correspond to the two ways of proving Even. The first subgoal is a contradiction that is discharged with contradiction. The second subgoal makes use of injections and subst. The subst tactic takes an equation x = t and replaces x by t in the context's hypotheses and in the goal, then removes that equation from the context.

We've defined a handy tactic called inversion that factors out this common pattern, saving us the trouble of explicitly stating and proving an inversion lemma for every inductive definition we make. (The details of how inversion is implemented are beyond the scope of this course. Lean provides metaprogramming facilities that its users can employ to write their own tactics, and these capabilities are powerful enough that just about any algorithmic reasoning steps can be implemented.)

Here, the inversion tactic can detect (1) that the first case, where n = 0, does not apply and (2) that the n' that appears in the Even.succ_succ case must be the same as n.

The inversion tactic can apply the principle of explosion to "obviously contradictory" hypotheses involving inductively defined properties, something that takes a bit more work using our inversion lemma. Compare:

Recall from the Logic chapter that equality (Eq) is itself an inductively defined proposition, so inversion can also be used on equality propositions.

We can use inversion to re-prove some theorems from Tactics.

For the inductively defined propositions we use, inversion behaves much like cases: it performs case analysis on the constructors of the hypothesis's inductive type. However, when the case analysis on an indexed proposition gives unsolvable equations between its indices, cases itself fails, whereas inversion leaves such equations in the context.

For example, cases would immediately fail on h:

Dependent elimination failed: Failed to solve equation
  n.mul n = 0

inversion instead leaves the equations in the context, where we can use them directly:

Here is a useful way to think about inversion. For an inductively defined hypothesis h, inversion h starts with one case for each constructor, then uses the indices of the type of h to eliminate impossible cases, and simplifies the remaining ones. In the remaining cases, it solves these equations to force some expressions or substitute some variables. If an equation cannot be solved, inversion leaves it in the context and we can use it in the rest of the proof.

∀ n, Even (2 + n) → Even n