Induction from n to 1

Question

I have an algorithm with a for loop that goes from i=n-1 to 1. I'm attempting to prove it's correctness.

Am I allowed to use induction like so

step 1 -- base case i = n

step 2 -- induction hypothesis, assume it works for i = n + 1

step 3 -- prove (using induction hypothesis) it works for i <= n + 1

Answer 1

As you haven't said anything about the nature of your algorithm, it's difficult to answer in a way you'll definitely find useful. But I'll attempt it, at this level of generality.

One tool you may find useful is a downward form of induction, as suggested by Nex:

For $n \in \mathbb{N}$ and statements $S_i, 1 \le i \le n$, if $S_n$ holds and so does the implication $S_{i+1} \to S_i$ for $1 < i \le n$, then $S_i$ holds for all $i \in \{1, \dots ,n\}$.

Proof: If not, then there is a greatest $i_{max} \le n$ where $S_{i_0}$ is false. We must have $i_0 < n$, as $S_n$ is true; so $i_0 + 1 \le n$. Because $i_0$ is greatest, $S_{i_0 + 1}$ is true. But $S_{i_0 + 1} \to S_{i_0}$, so $S_{i_0}$ after all.

When trying to prove a program correct, the usual approach a la Dijkstra is to attach assertions to points before and after statements or blocks of statements (preconditions and postconditions), such that the assertions are true for every execution path through the program, and such that every exit point is covered by an assertion.

When proving correctness of a loop, you want to find a precondition and a postcondition for the entire loop, as well as loop invariants – a precondition and a postcondition for the body the loop – such that at the end of the last iteration, the body postcondition implies (or just is the same thing as) the loop postcondition. For your situation, you might set this up schematically as follows (for simplicity I've change your loop limit from n-1 to n; assertions are shown within curly braces):

{loop-precond}  # assertions about initial state of in & out variables, etc. 
for i = n to 1:
    {S(i+1, n) holds}
    *body of loop*
    {S(i, n) holds} 
{S(i, n) holds for 1 ≤ i ≤ n}

The loop-invariant assertions need n as a parameter: for example, the body of the loop might process an array a[1:n] in reverse order, and S(i, n) might assert something about what has been done with a[i:n]. Assume that S(n+1, n) holds, probably trivially/vacuously.

You want to prove that the loop postcondition {S(i, n) holds for 1 ≤ i ≤ n} holds after the loop has executed. To do this, show that for any i ≤ n, if S(i+1, n) holds before the body executes, then S(i, n) holds after it executes. Because S(n+1, n) is vacuous, you may also have to show as a special case that S(n, n) holds after the first time through the loop. Now you can conclude from to the "downward induction" principle stated above that the loop postcondition holds – i.e. that the loop is "correct", whatever correctness means for your purposes.