---
title: Understanding Induction
abstract: I am fucking stupid and I can't understand this
author: 
type: theoretical
---

## Understanding Induction

There are a few assumptions to be made when performing induction proofs (in general):
- There is *some* non-decreasing property about the category we're observing (i.e. difference between elements in a sequence, length of a list, height of a tree)
- The structure needs to be *well-defined*[^1]

And then we move on to the mechanism for proofs itself:
1. Induction Base Case: The base case(s) must be **sufficient** to cover all minimal or simplest cases of the structure. 
   For instance, when proving properties of lists, we often start by showing the property holds for the empty list. 

2. Inductive Hypothesis: We assume that the property we're trying to prove holds for an arbitrary case. It must explicitly account for all necessary assumptions about the intermediate state of the structure.

3. Inductive Step: To establish the general inductive step, we should demonstrate that if the property holds for a given category (the induction hypothesis), it also holds for the next element (based on the non-decreasing property mentioned earlier).

We should be able to guarantee termination and avoid ambiguity in the process.

## Induction in Haskell
Given Haskell's [purity](Introduction%20to%20Functional%20Programming.md), we can perform induction proofs on most of its structure.

The non-decreasing property is defined by the data structure (`data` keyword) and/or the logic we have implemented (i.e. natural numbers - n > n-1 > 0, lists -> length, tree -> height).

We then proceed with the process mentioned above, although slightly altered as to fit the data structure category:
- **BC**: We must first establish a base case, which is a minimal instance of the structure that satisfies the property being proven. For example, this could be an empty list, a single element, or a tree with only one node. The base case must be simple enough to verify directly.

- **IH**: Assume that the property holds for some arbitrary but fixed instance of the structure. This is often referred to as the **induction step assumption**, where you posit[^2] that the property is valid for a smaller or simpler instance of the structure.

- **IS**: Using the inductive hypothesis, prove that the property holds for a larger or more complex instance of the structure. 
  
For example, if the property holds for a list of length $n$, you need to show it holds for a list of length $n+1$. Similarly, for a tree of height $h$, show it holds for a tree of height $h+1$. This step bridges the smaller case to the larger one.



For example, when proving that reversing twice returns the original list, we can use mathematical induction:

1. **Base Case**: We need to show the property holds for the empty list (`[]`). Here, it's clear that `reverseList [] = []` and `reverseList (reverseList [])` is also `[]` since `reverseList` appends elements to the left `(++)`, and an empty list cannot be appended to anything.

2. **Inductive Step**: Suppose the property holds for a given non-empty list `x:xs` (induction hypothesis). To prove it holds for the longer list xs (`x:xs`), we apply `reverseList` and use the defined function properties as follows:
   ```haskell
   -- Induction Hypothesis (property holds for xs)
   prop_reverseTwice xs =>

   -- Show that property also holds for x:xs (inductive step)
   prop_reverseTwice (reverseList x:xs) =
   -- Break down the list using reverseList and pattern matching
   prop_reverseTwice ((reverseList xs) ++ [x]) =
   -- Use the definition of concatenation, reverse, and the induction hypothesis
   prop_reverseTwice (xs ++ reverseList [] ++ [x]) =
   -- Use the fact that concatenating an empty list with any other list returns the original list.
   prop_reverseTwice (xs ++ [x]) =
   -- The property holds for xs by our induction hypothesis
   True
   ```
By showing the base case and inductive step, we have successfully proven that `reverseList` reverses lists twice, returning the original list.


### TL;DR
1. Base case - empty list or tree
2. Inductive hypothesis - assume it works for an arbitrary list `xs` or tree (i.e.)
```haskell
data Tree a = Empty                  -- A tree can be empty
            | Node a (Tree a) (Tree a) -- Or a node with a value and two
            deriving (Show, Eq)
            
-- when a Tree a is Empty

```
   
3. Inductive Step - show that it works for a larger list `x:xs` or a non-empty tree
   
This process involves knowing *some* implementation details of higher-order functions (or at least a vague idea as to how they work).


[^1]: Clear rules as to how it's constructed
[^2]: to propose as an explanation **:** [suggest](https://www.merriam-webster.com/dictionary/suggest)