Induction: Proof by Induction

Induction

In this chapter, we will learn about proof by induction. Before we move on to induction itself, we can analyze simple cases where the reflection of the case already proves the theorem.

Problems.t0 (n: Nat) : Equal Nat (Plus Nat.zero n) n

When checking the theorem statement, we receive the following response:

+ INFO  Inspection.

   • Expected: (Equal Nat n n) 

   • Context: 
   •   n : Nat 

    Problems.t0 n = ?
                    ┬
                    └Here!

In Problems.t0, Kind automatically reduces the sum of 0 + n to n, and we need to prove the equality between n and n. In this case, we simply write Equal.refl and we get the confirmation response:

All terms check.

Problems.t1 (n: Nat) : Equal Nat (Plus n Nat.zero) n

After solving the first problem, the next one is very similar, it is the sum of n + 0 = n and this similarity may lead us to believe that invoking the reflection is enough. However, in the first case, Kind automatically reduces and in this one, we get the following response:

+ INFO  Inspection.

   • Expected: (Equal Nat (Plus n 0n) n) 

   • Context: 
   •   n   : Nat 

   Problems.t1 n = ?
                   ┬
                   └Here!

In the first case, Kind reduces because zero is on the right side and the Type Checker automatically reduces the sum between 0 and n to n. However, when the first input is a variable, Kind needs to check for each case and as it is a natural number, there are infinitely many cases to be tested, that is, from zero to infinity.

At first, we may think that there are so many cases and it is impossible to analyze all of them, as there are infinitely many, but soon we realize that it is possible to reduce them to two, one is the number zero and the other is a number that succeeds zero n times after.

Analyzing the case of zero, our goal is to prove that zero is equal to zero:

• Expected: Equal Nat Nat.zero Nat.zero

Now, we just need to give the Equal.refl and the zero case has been proven, we just need to respond to the successor of zero.

Our goal is to prove that for every number n, adding 0 will result in n, but we already have a new tool that helps us in this proof and it is the proof for the zero case, we just need to reduce n until the only thing needed is reflection, and we can do this by recursion and to do that we define the new n as its predecessor. In Kind, we can simply do this by defining the current n as the successor of the next n and recursively calling the function for n. This is done as follows:

Problems.t1 (Nat.succ n)   = ?

and our new goal is to prove that the successor of the sum between n and 0 is equal to the successor of n.

- Expected: Equal Nat (Nat.succ (Plus n Nat.zero)) (Nat.succ n)

To work with induction in this recursion, we must define a variable for the original case of n.

Problems.t1 (n: Nat)       : Equal (Plus n Nat.zero) n
Problems.t1 Nat.zero       = Equal.refl
Problems.t1 (Nat.succ n)   =
    let ind = Problems.t1 n
    ?

When we give the Type Check, we get the following response:

+ INFO  Inspection.

   • Expected: (Equal Nat (Nat.succ (Plus n 0n)) (Nat.succ n)) 

   • Context: 
   •   n   : Nat 
   •   ind : (Equal Nat (Plus n 0n) n) 
   •   ind = (Problems.t1 n) 

   let ind = Problems.t1 n
     ?
     ┬
     └Here!

When analyzing our goal and induction, we realize that the only difference between the goal and our variable ind is the Nat.succ. Therefore, we just need to increment the ind variable with Nat.succ. To do this, we create a new variable and use a lambda function:

let app = Equal.apply (x => (Nat.succ x)) ind

In the above case, we call the Equal.apply function to apply our lambda function to ind. The x => (Nat.succ x) function serves to add Nat.succ to every element received in the variable. Since our ind variable is a function that takes another variable n, our lambda function increments n with Nat.succ, which returns exactly our goal:

+ INFO  Inspection.

   • Expected: (Equal Nat (Nat.succ (Plus n 0n)) (Nat.succ n)) 

   • Context: 
   •   n   : Nat 
   •   ind : (Equal Nat (Plus n 0n) n) 
   •   ind = (Problems.t1 n) 
   •   app : (Equal Nat (Nat.succ (Plus n 0n)) (Nat.succ n)) 
   •   app = (Equal.apply Nat Nat (Plus n 0n) n (x => (Nat.succ x)) ind)  

   let app = Equal.apply (x => (Nat.succ x)) ind
      ?
      ┬
      └Here!

We can see that the app is exactly the same as the Expected, which is our goal, and we just need to return it, the app, for the Type Check to validate our proof:

All terms check.

There are cases where induction is even simpler - all we need to do is understand what is happening. Let's say we want to prove that a number n minus itself is always equal to zero, regardless of what that number is. How would we do it? First, we check the case where n is zero, and it is a true equality - zero minus zero is equal to zero. Then, we induct the case to the case of zero, which we know is true. Seems complicated? It's not - it's ridiculously simple. Let's see how it looks in Kind:

Minus_diag (n: Nat)     : Equal Nat (Minus  n n) Nat.zero
Minus_diag Nat.zero     = Equal.refl
Minus_diag (Nat.succ n) = Minus_diag n

Notice, this is a simple induction - we say the proof holds for the number and its predecessor, and through recursion, for all predecessors up to zero, which we verified to be true. In other words, we prove, in just three lines, that a natural number minus itself will always result in zero, regardless of what that number is.