# Recursive function - proof by induction

Let $$\Sigma$$ denote an alphabet and $$[ \Sigma ]$$ set of lists.

I've encountered the following function:

$$f([])=[]$$ (empty list)

$$f([x])=[x]$$, for $$x \in \Sigma$$

$$f(x:L)=f(L)$$, for $$x \in \Sigma$$ and $$L \in [ \Sigma ]$$

The function is supposed to return a tail for nonempty list. That is:

$$f([x_1,x_2,...,x_n])=[x_n]$$

How would you understand the ":" operator in the definition?

Inductive proof should be possible for showing that such a "tail function" is indeed working.

• Also posted at mathoverflow and math within a few hours. Please do not post the same question on multiple sites. Each community should have an honest shot at answering without wasting anybody's time. If you don't get a satisfying answer after a week or so, you may flag to request migration. Apr 23, 2022 at 21:59

I think it's a template match, meaning if you have some list $$L = [x_1, x_2, \dots, x_n]$$, then $$L = x:L'$$ where $$L' = [x_2, x_3, \dots, x_n]$$.
So you can imagine what that definition is saying is that $$f(x:L)$$ is equivalent to operating on the rest of the list, i.e. $$L$$ in this case, hence $$f(L)$$.
Induction follows pretty easily because once you've shown for a list of length $$n$$, to show $$n+1$$, you just use the function definition, which peels off the first element, and you immediately have a list of $$n$$, which is true by the inductive hypothesis.
• $$L:y$$ : $$y$$ is the last element
• $$x:L:y$$ : $$x$$ is the head, $$y$$ is the tail