Induction structurelle sur les listes

Les définitions, qui sont le squelette des preuves :

let rec longueur = function [] -> 0 | _ :: r -> 1 + longueur r
let rec concat l1 l2 = match l1 with [] -> l2 | x :: r -> x :: concat r l2
let rec miroir = function [] -> [] | x :: r -> concat (miroir r) [x]

Première identité, par induction sur ${\ell }_1$ — et non sur ${\ell }_2$, car c'est ${\ell }_1$ que concat décompose.

Cas ${\ell }_1=\text{[]}$. $|\text{[]}@{\ell }_2|=|{\ell }_2|=0+|{\ell }_2|$.

Cas ${\ell }_1=x::r$. Alors ${\ell }_1@{\ell }_2=x::(r@{\ell }_2)$, donc

$$|{\ell }_1@{\ell }_2|=1+|r@{\ell }_2|\stackrel{\text{H.I.}}{=}1+|r|+|{\ell }_2|=|{\ell }_1|+|{\ell }_2|.$$

L'hypothèse d'induction est appliquée à $r$, qui est un argument du constructeur : c'est la seule chose que l'ordre induit autorise.

Seconde identité, encore par induction sur ${\ell }_1$.

Cas ${\ell }_1=\text{[]}$. Le membre de gauche vaut $\text{miroir}({\ell }_2)$. Celui de droite vaut $\text{miroir}({\ell }_2)@\text{[]}$. Il faut donc le lemme $\ell @\text{[]}=\ell$, qui n'est pas une évidence : il se prouve lui-même par induction sur $\ell$, et c'est l'occasion de remarquer que $\text{[]}@\ell =\ell$, lui, est vrai par définition. La concaténation n'est pas symétrique dans son code, et les deux neutres ne coûtent donc pas le même prix.

Cas ${\ell }_1=x::r$.

$$\begin{array}{rl}\text{miroir}((x::r)@{\ell }_2)& =\text{miroir}(x::(r@{\ell }_2))=\text{miroir}(r@{\ell }_2)@[x]\\ & \stackrel{\text{H.I.}}{=}(\text{miroir}({\ell }_2)@\text{miroir}(r))@[x]=\text{miroir}({\ell }_2)@(\text{miroir}(r)@[x])\\ & =\text{miroir}({\ell }_2)@\text{miroir}(x::r).\end{array}$$

L'avant-dernière égalité est l'associativité de la concaténation — second lemme, prouvé lui aussi par induction sur son premier argument.

Vérification. Les deux identités, plus $\text{miroir}(\text{miroir}(\ell ))=\ell$ et $|\text{miroir}(\ell )|=|\ell |$, ont été testées sur $3000$ couples de listes tirées au hasard : toutes vraies.

Le point de méthode, et il vaut pour tout le chapitre. Une preuve par induction structurelle en appelle presque toujours d'autres : ici, deux lemmes ($\ell @\text{[]}=\ell$ et l'associativité) qu'on ne voit pas avant d'être bloqué. Le bon réflexe est de mener le calcul jusqu'à l'obstacle, et de nommer alors le lemme manquant — plutôt que de chercher à tout prévoir.

Une remarque de coût, pour finir. miroir tel qu'écrit ici est en $\Theta (n^2)$ : mesures $0,036$ s pour $n=2000$, puis $0,636$, $3,00$ et $15,96$ s pour $8000$, $16000$ et $32000$ — un facteur $4$ à chaque doublement, la signature du quadratique. La version à accumulateur, let rec miroir_acc l acc = match l with [] -> acc | x :: r -> miroir_acc r (x :: acc), reste sous la milliseconde à $32000$. La preuve d'une fonction ne dit rien de son coût, et réciproquement : ce sont deux obligations distinctes, et le programme les demande toutes les deux.