Structural induction in haskell Notation in this question derives from Haskell as follows. Let $[A]$ denote the collection of lists whose elements are drawn from the set $A$, so e.g. $[\mathbb{Z}]$ is the set of integer lists. Denote the empty list of any type by $[]$. Denote a single-element list by by $[a]$. We may write any nonempty list as a:x, where $a \in A$ is the first element and $x \in [A]$ is the (possibly empty) tail of the list. Denote list concatenation by a ++ b. Lists are finite and allow repetitions: 1 : [1] is a valid list, which has two elements ($1$ and $1$).
The Haskell code is:
perm :: [Int] -> [[Int]] 
perm z = f([], [], z) where  
f(x, y, []) = []   
f(x, [], [a]) = [x ++ [a]]  
f(x, y, a:z) = f(x ++ [a], [], y ++ z) ++ f(x, y ++ [a], z)

How do I prove that the function returns a permutation by using structural induction?
 A: This is more of an expository hint than anything; I'm answering the "how" rather than giving an answer to the exercise.
You need to find an appropriate wellfounded partial order on $[\mathbb{Z}] \times [\mathbb{Z}] \times [\mathbb{Z}]$, such that the following relations hold for all lists $x, y, z \in [\mathbb{Z}]$ and for all $a \in \mathbb{Z}$:
(x ++ [a], [], y ++ z) < (x, y, a:z)
(x, y ++ [a], z) < (x, y, a:z)

In fact, the actual elements of the list are unimportant; your definition is completely generic on the type $\mathbb{Z}$. So we should be able to answer this question by only considering the lengths of the lists.
In fact, an equivalent formulation of your question is: prove by induction that $g : \mathbb{N}^3 \to \mathbb{N}$ is well-defined, where $g$ is given by


*

*$g(a, b, 0) = 0$

*$g(a, 0, 1) = 1$

*$g(a, b, c+1) = g(a+1, 0, b+c) + g(a, b+1, c)$.


(Moreover, you actually also want $g(0, 0, c) = c!$, but that's a story for another time.)
The way to do this is to find a function $i : \mathbb{N}^3 \to \mathbb{N}$ such that $i(a+1, 0, b+c) < i(a, b, c+1)$ (so that the first recursive call can be assumed inductively to terminate) and such that $i(a, b+1, c) < i(a, b, c+1)$ (so that the second recursive call can be assumed inductively to terminate). Once you've done this, you're done by induction on the value of $i$.
