Induction and Recursion

Use the structure of natural numbers and lists to handle infinitely many cases.

15.1 Nat has two constructors

Build natural numbers from zero, Zero, and a successor, Succ(n). Nat is a built-in inductive type with the following definition:

inductive Nat: Type {
  Zero: Nat
  Succ(n: Nat): Nat
}

This represents 0, 1, 2, and so on with finitely many constructor applications. For example, 2 is Succ(Succ(Zero)), also written as the literal 2. Induction handles all natural numbers by considering the Zero and Succ(k) cases.

15.2 Start with addition

Let's write the standard-library theorem from std/Nat.taut saying that adding zero on the left leaves a number unchanged. plus is another name for +.

import std::Nat
import std::Std

theorem add_zero_left(n: Nat): plus(Zero, n) = n {
  match n: plus(Zero, n) = n {
    Zero => Refl
    Succ(k) => Eq::congr(Succ, add_zero_left(k))
  }
}

// Use the recursive theorem on the smaller natural number.

✓ theorem add_zero_left : ∀ n: Nat. plus(Zero, n) = n

tauto check src/ch15-add.taut

The expression after : in match n: proposition { ... } is the proposition you want to prove, which depends on n. In the base case Zero, both sides compute to the same term, so Refl suffices. In the Succ(k) case, call the same theorem for the smaller k to obtain the induction hypothesis, then use Eq::congr(Succ, ...) to increase both sides by one.

15.3 Induction is not a finite set of experiments

The proof does not merely test a few numbers starting at zero. It constructs evidence covering every possible natural-number structure. That is the essential distinction between many tests and a proof.

Fixed-width integers used at runtime have upper limits, unlike the natural-number type Nat. When transferring a proved property to runtime integers, consider conversions and overflow conditions separately.

15.4 Structural and well-founded recursion

Tauto supports structural recursion, which recurses into a component of a pattern, and well-founded recursion, which proves that a measure decreases at each call. The latter uses decreasing_by measure(...) and a proof of decrease.

import std::WellFounded
import std::Nat

fn id_nat(n: Nat): Nat { n }

fn half(n: Nat): Nat decreasing_by measure(id_nat) => theorem half::eq {
  match n: Nat {
    Zero => Zero
    Succ(m) => match m: Nat {
      Zero => Zero
      Succ(k) => Succ(half(k, Nat::le_succ(k)))
    }
  }
}

// Supply the decrease proof for a well-founded recursive call.

✓ def id_nat : (Nat) -> Nat
✓ def half : (Nat) -> Nat

half decreases n two at a time, so it is not merely a call on its immediate child. The final argument to half(k, Nat::le_succ(k)) proves that k is smaller than the original n. => theorem half::eq generates a theorem describing the definition of half.

The kernel rejects a recursive call that omits the required decrease proof.

Exercise 15.1: How does a function counting a list's length correspond to induction over the list's structure?