Induction over naturals

refl proves things about concrete expressions. To prove something about every natural number, you need induction — and in a dependently typed language induction is not a tactic but an ordinary function you apply.

The shape

natind is the induction principle for naturals, taking four arguments:

natind(motive, base, step, n)

This mirrors induction as usually stated: prove the base case, prove that each case implies the next, conclude it holds throughout. The difference is that here the three parts are values you supply to a function, and the type checker verifies they fit together.

The motive

The motive is the part without an analogue in ordinary programming, and the part worth slowing down on. It is a function from a value to a type — it says what you are proving about k, for each k:

|k: Nat| Eq<Nat, 0, 0>

Feed it a number, get back a proposition. Because the result type varies with the input value, the eliminator’s own result type is determined by the value it eliminates. This is dependent elimination, and it is why the motive has to be written out rather than inferred: it is the statement being proved, and the compiler cannot guess what you intended to prove.

Worked shapes

Producing an equality proof by induction:

let p: Eq<Nat, 0, 0> = natind(
    |k: Nat| Eq<Nat, 0, 0>,
    refl,
    fn(k: Nat, ih: Eq<Nat, 0, 0>) => ih,
    0
);

The motive is the proposition, refl is the base case, and the step passes the induction hypothesis ih through unchanged.

With a computational motive, natind produces a value rather than a proof:

let n: Nat = natind(|k: Nat| Nat, 0, fn(k: Nat, ih: Nat) => ih, 0);

natrec

natrec is the non-dependent sibling: where natind takes a motive, natrec takes a plain type, because the result type does not vary:

let n: Nat = natrec(Nat, 0, fn(k: Nat, acc: Nat) => acc, 0);

Use natrec for primitive recursion where the answer is a value, and natind where the answer is a proof whose statement depends on the input.

Note on the step function

The step is written with the fn(…) => … lambda spelling rather than |…| …. Both are function values; the longer form simply reads better when the parameters are a value and an induction hypothesis.

Tactics

Written as a term, induction is an eliminator: you write the motive and both cases explicitly, which is tractable for small statements and laborious for large ones.

Since 2.0-beta the same proof can be written with tactics, which set the cases up for you:

theorem zero_add(n: Nat) -> Eq<Nat, 0 + n, n> by {
    induction n;
    refl;
    intro j;
    intro ih;
    exact cong(|x: Nat| x + 1, ih)
}

simp, ring and omega discharge routine algebra as well; the 2.0-beta release notes list them. On macOS, check a tactic proof with albite-bootstrap — the self-hosted albite does not parse by { … } yet.