Lecture 28: Induction

1 Purpose

A deep dive on induction.

2 Outline

At this point, you have done a lot of proofs by induction, all using the induction tactic. The intuition we’ve been using is that induction is like case analysis, except that for each constructor that has recursive data, you end up with an induction hypothesis for that subpart of the data.

Today, we will look much more closely on where induction gets that from, and an alternate way to do inductive proofs.

3 Induction tactic, in more detail

When we have a proof like:

theorem φ : forall n, Nat.add 0 n = n := 
 by intros n
    induction n
    case zero => rfl
    case succ n IH =>
      simp only [Nat.add]
      rw [IH]

If we were to prove this, on paper, one way would be to prove:

φ(0)

n: φ(n) -> φ(n+1)

t

φ(t)

e.g., to get ϕ(4), we can use the second case to conclude this if we can show ϕ(3), which we can conclude if we can show ϕ(2), which we can conclude if we can show ϕ(1), which we can conclude if we can show ϕ(0), which is the first case.

This corresponds directly to how induction works, and in particular, how the induction tactic works.

If we look carefull at the tactic state right before we run induction n, we see:

n : Nat
⊢ Nat.add 0 n = n

First, note that we always apply induction to a variable that is in the context. While informally we might say that we proceed "by natural number induction", formally, while we are using the natural number induction principle, we are particularly applying it to a given natural number. Why does that matter? And where, exactly, do the obligations come from? Informally, we’ve said that "induction is like case analysis with extra hypotheses for the recursive cases". Formally, every inductive type has what is called a "recursor"; we can print it out with, e.g.,

#print Nat.rec

This prints:

    recursor Nat.rec.{u} : {motive : Nat → Sort u} →
motive Nat.zero → ((n : Nat) → motive n → motive (Nat.succ n)) → (t : Nat) → motive t

Recursors are primitive aspects of inductive types, so the implementation is just called recursor Nat.rec.{u}, but the type is quite informative. It is a lot to read at first, but if we reformat it slightly, and add comments:

recursor Nat.rec.{u} :
{motive : Nat → Sort u} → -- what we are trying to prove
motive Nat.zero →         -- proof for Nat.zero case
((n : Nat) → motive n → motive (Nat.succ n)) → -- proof for Nat.succ case
(t : Nat) → -- the number we want the proof for
motive t -- the proof for that number

The key (and also most confusing at first) part of this is the motive argument. This is a function that takes a natural number and returns... essentially anything. For proofs, it will usually return Prop. It’s fine to read Sort u as Prop for now. What is an example of a motive?

Well, if we look at the proof we just did,

forall n, Nat.add 0 n = n

Would be something of type Nat → Prop, and in particular, it would be our motive. The first thing the induction tactic does is take the goal and turn it into a motive by replacing what we are doing induction on with a forall. This is why if we change the goal (make it more general, most likely) before we do induction, the motive that ends up being used will change, which may make the proof easier. The state of goal at the time we do induction is what determines the motive.

Once we have the motive, we have to prove cases for each of the constructors. These are derived from the definition of the inductive type. In particular, arguments for constructors will be passed in, but for arguments that are themselves instances of the type (self-referential arguments, in other words), we also get the motive applied to that argument. This is why in the successor case, to prove that motive (Nat.succ n), we get as an argument that motive n as well as just n.

But note, in contrast, that if we defined a NatList as:

    inductive NatList : Type
| nil : NatList
| cons (first : Nat) (rest : NatList) : NatList

recursor NatList.rec.{u} :
{motive : NatList → Sort u} →
motive NatList.nil →
((first : Nat) → (rest : NatList) → motive rest → motive (NatList.cons first rest)) →
(t : NatList) →
motive t

In this, for the cons case, the rest argument has the motive applied to it, but not the first argument, since the first argument is a Nat, so its not self-referential.

Once we provide all of those arguments (which amounts to proving each case), we just have to provide an element of the data type (this is the argument we were doing induction on), and we get back the motive applied to that argument, which based on how the motive was originally constructed, is enough to complete the proof.

This is, more or less, just more detail about a process that at this point should be quite familiar. But today we are going to go a bit beyond it.

4 Induction via recursion

If you remember, we had one example where invoking the induction tactic didn’t seem to work at all.

inductive ev : Nat → Prop where
  | O : ev 0
  | SS (n : Nat) (H : ev n) : ev (Nat.succ (Nat.succ n))

def even : Nat -> Bool
  | 0 => true
  | 1 => false
  | Nat.succ (Nat.succ n) => even n

example : forall n, even n = true -> ev n :=
  by intros n H
     induction n
     case zero => constructor
     case succ n IH => sorry

The problem was that the structure of natural number induction didn’t seem to match up: evenness goes up every two numbers, not every one, so the Nat.succ case of Nat.rec doesn’t seem feasible.

Now, while recursors are fundamental (and used not only by induction, but by recursive functions as well), the semi-naive way that they are invoked by induction is not the only way that we can use them. In particular, if we use them more directly by writing recursive functions (which are compiled to calls to the recursors), we can get more control over how the induction is done.

We did this in the example for evenness:

def even_ev : forall n, even n = true -> ev n
| 0 => fun _ => ev.O
| 1 => fun H => by contradiction
| Nat.succ (Nat.succ n) => fun H => ev.SS n (even_ev n H)

Of course, we can write this in a bit more tactic-style: still using pattern matching to structure the recursion to be every two, and critically, handling the recursive case by a recursive call to the function (which will get translated to a call to the recursor).

theorem even_ev' : forall n, even n = true -> ev n
| 0 => by intros; constructor
| 1 => by intros; contradiction
| Nat.succ (Nat.succ n) => 
  by intros H; constructor; exact (even_ev' n H)

You might be tempted to write all inductive proofs like this: indeed, if you are careful, you certainly can. For example, here’s another theorem we did, rewritten that way:

def double : Nat → Nat 
    | 0 => 0
    | (Nat.succ x) => Nat.succ (Nat.succ (double x))

theorem even_double : ∀ x : Nat, even (double x) = true
| 0 => by rfl 
| Nat.succ n => by simp only [even, double]; rw [even_double n] 

But one risk with this, is you might end up trying to make recursive calls to the theorem that don’t satisfy the termination checker (satisfying the terminatior checker is actually a matter of writing things in such a way that the recursive calls can be turned into invocations of the recursor!). The nice thing about the induction tactic is that it only gives you as hypotheses things that you certainly can use to prove the goal. Recursion is a little trickier; it gives more flexibility, but some recursive patterns that seem okay may actually not be!

As an exercise, let’s rewrite the two proofs about addtail from HW7 using induction via recursion instead of the induction tactic.

namespace HW7

def Nat.add : Nat → Nat → Nat
  | Nat.zero, b   => b
  | Nat.succ a, b => Nat.succ (Nat.add a b)

def addtail (n m : Nat) : Nat :=
  match n, m with
  | Nat.zero, m => m
  | Nat.succ n', m => addtail n' (Nat.succ m)

theorem addtail_succ : forall n m, Nat.succ (addtail n m) = addtail (Nat.succ n) m
| 0, m => by simp only [addtail]
| Nat.succ n, m => 
   by simp only [addtail]
      rw [addtail_succ n (Nat.succ m)]
      rfl 

theorem add_eq : forall n m, Nat.add n m = addtail n m
| 0, m => by simp only [Nat.add, addtail]
| Nat.succ n, m =>
   by simp only [Nat.add]
      rw [add_eq n m]
      apply addtail_succ

end HW7

def eqb : Nat -> Nat → Bool
| 0, 0 => true 
| 0, Nat.succ y => false
| Nat.succ x, 0 => false
| Nat.succ x, Nat.succ y => eqb x y 

theorem eqb_sym : forall x y : Nat, eqb x y = eqb y x :=
 by intros x
    induction x <;> intros y
    case zero => cases y <;> rfl
    case succ x IH => 
      cases y <;> try rfl
      simp only [*, eqb]

theorem eqb_sym' : forall x y : Nat, eqb x y = eqb y x
| 0, 0 => by rfl
| 0, Nat.succ y => by rfl
| Nat.succ x, 0 => by rfl
| Nat.succ x, Nat.succ y => 
  by have IH : _ := eqb_sym' x y
     simp [*, eqb]