= Solution
For finite, defined <lists>, <structural induction> requires $P([])$ and $P(xs)\Rightarrow P(x:xs)$ for every head $x$ and tail $xs$. This proves $P$ for every finite <list>.
An infinite <list> cannot be reached by finitely many constructor steps. For <structural induction on lazy lists>, also check $P(\bot)$, where $\bot$ is the <bottom value>, and require an <admissible predicate on lazy lists>: if increasingly defined finite approximations all satisfy $P$, their limit does too. Together with the empty-list and constructor cases this covers finite, partial and infinite <lists>. Merely asserting the two finite-list cases is insufficient; “the list is finite” itself satisfies those cases but fails on infinite lists.
Back to article page
