# Invariant vs. Induction

In the following, we consider a problem involving binary search trees. We attempt to solve the problem two ways, first iteratively, then recursively, and prove correctness for each.

Whereas proving correctness for loops, or iteration, is done using a loop invariant, for recursion, we prove correctness using induction, or in our case of structural recursion, structural induction.

# Problem:

For a value `num`

, and a binary search tree, find the largest number smaller than `num`

, if such exists, otherwise return `-1`

.

For the sake of brevity, we will refer to this value as the predecessor, or simply, `pred`

.

# Iterative solution and proof:

A solution using loops might look like this:

```
result = -1
while curr:
if curr.val < num:
result = max(result, curr.val)
curr = curr.right
else:
curr = curr.left
return result
```

**Invariant property:**

We have either `result = pred`

, or the value `pred`

exists somewhere in the tree rooted at `curr`

.

**Initialization:**

If the original tree has any values less than `num`

, then the value `pred`

exists in this tree, otherwise, `pred = -1`

, the initial value of `result`

.

**Maintenance:**

**Case 1:** `curr.val < num`

Then for any `node`

in the subtree at `curr.left`

, we have ```
node.val ≤
curr.val
```

.

Then our desired value is either in `result`

, `curr.val`

, or the subtree at `curr.right`

, and property still holds after setting ```
result =
max(result, curr.val)
```

, and `curr = curr.right`

.

**Case 2:** `curr.val ≥ num`

Then for any `node`

in the subtree at `curr.right`

, we have ```
node.val
≥ num
```

.

Then our desired value is either in `result`

or the subtree at `curr.left`

, and property still holds after setting ```
curr =
curr.left
```

.

**Termination:**

When the loop terminates, there are no values in the subtree at `curr`

, thus `result = pred`

.

# Recursive solution and proof

A recursive solution might look like this.

```
findValue :: Node -> Int
findValue node
| null node = -1
| value node < num = max (value node) (findValue (right node))
| value node >= num = findValue (left node)
```

**Claim:**

For any `node`

, if the subtree at `node`

contains any value less than `num`

, `findValue`

will return the largest such, otherwise it returns `-1`

.

**Base Case:**

If `node`

is null, then there are *no* values in the subtree at `node`

, and `findValue`

correctly returns `-1`

.

**Inductive step:**

We consider for a non-null `node`

, with value `v = value node`

.

**Case 1:** `v < num`

For any value `u`

in subtree at `left node`

we have `u ≤ v`

.

Then, if there were any values `w`

in the subtree at `node`

such that `v < w < num`

, they will be in the subtree at `right node`

.

By inductive hypothesis, `findValue`

will return the appropriate value when applied to `right node`

. Taking the `max`

as defined above, completes the inductive step for the first case.

**Case 2:** `v ≥ num`

Then for any value `w`

in the subtree at `right node`

we have `w ≥ num`

.

If there are any values `u`

in the subtree at `node`

such that ```
u <
num
```

, they will be in the subtree at `left node`

.

Inductive hypothesis ensures `findValue`

returns correct value for `left node`

.