Induction structurelle

Les listes

Les listes sont définies comme étant

• soit la liste vide ${\displaystyle {\texttt {[]}}}$,
• soit la liste obtenue par la mise en tête d'une liste ${\displaystyle \ell }$ d'un élément ${\displaystyle a}$, ce qui donne ${\displaystyle a::\ell }$.

La fonction ${\displaystyle length:listes\to \mathbb {N} }$ qui définit la longueur d'une liste par induction :

• ${\displaystyle length({\texttt {[]}})\mapsto 0}$
• ${\displaystyle length(a::\ell )\mapsto 1+length(\ell )}$.

La fonction ${\displaystyle concat:listes\times listes\to listes}$ qui concatène deux listes ${\displaystyle \ell _{1}}$ et ${\displaystyle \ell _{2}}$

• ${\displaystyle concat({\texttt {[]}},\ell _{2})\mapsto \ell _{2}}$
• ${\displaystyle concat(a::\ell 1,\ell 2)\mapsto a::(concat(\ell 1,\ell 2))}$

On peut démontrer la proposition suivante :

${\displaystyle \forall \ell _{1}\ell _{2},\;length(concat(\ell _{1},\ell _{2}))=length(\ell _{1})+length(\ell _{2})}$

On procède par induction sur ${\displaystyle \ell _{1}}$ après avoir introduit ${\displaystyle \ell _{2}}$

Cas de base (${\displaystyle \ell _{1}={\texttt {[]}}}$)

${\displaystyle length(concat({\texttt {[]}},\ell _{2}))=length(\ell _{2})=0+length(\ell _{2})=length({\texttt {[]}})+length(\ell _{2})}$

Cas inductif (${\displaystyle \ell _{1}=a::\ell _{1}'}$)

On cherche à monter que ${\displaystyle length(concat(\ell _{1},\ell _{2}))=length(\ell _{1})+length(\ell _{2})}$

On dispose de l'hypothèse d'induction suivante ${\displaystyle length(concat(\ell _{1}',\ell _{2}))=length(\ell _{1}')+length(\ell _{2})}$

Donc ${\displaystyle 1+length(concat(\ell _{1}',\ell _{2}))=1+length(\ell _{1}')+length(\ell _{2})}$

Donc ${\displaystyle length(a::concat(\ell _{1}',\ell _{2}))=length(a::\ell _{1}')+length(\ell _{2})}$, par définition de ${\displaystyle length}$

Donc ${\displaystyle length(concat(a::\ell _{1}',\ell _{2}))=length(a::\ell _{1}')+length(\ell _{2})}$, par définition de ${\displaystyle concat}$

Donc ${\displaystyle length(concat(\ell _{1},\ell _{2}))=length(\ell _{1})+length(\ell _{2})}$, par définition de ${\displaystyle \ell _{1}}$

Les arbres binaires

Considérons les arbres binaires définis ainsi :

• ${\displaystyle \Box }$ pour l'arbre vide,
• B${\displaystyle _{1}}$ ${\displaystyle \bullet }$ B${\displaystyle _{2}}$ pour un arbre non vide ayant pour sous-arbre gauche B${\displaystyle _{1}}$ et pour sous-arbre droit B${\displaystyle _{2}}$.

On peut définir la fonction taille (le nombre de nœuds internes de l'arbre binaire) :

• taille(${\displaystyle \Box }$) = 0
• taille(B${\displaystyle _{1}}$ ${\displaystyle \bullet }$ B${\displaystyle _{2}}$) = taille(B${\displaystyle _{1}}$) + taille(B${\displaystyle _{2}}$) + 1

Premier principe d'induction

Sur ${\displaystyle \mathbb {N} }$, le premier principe d'induction, permet, en montrant une propriété sur un cas de base et la conservation de cette propriété de manière héréditaire, de montrer la propriété pour tous les entiers naturels si le cas de base est ${\displaystyle n_{0}=0}$.

(${\displaystyle B_{n_{0}}}$) s'appelle l'étape de base de l'induction, elle affirme que ${\displaystyle P(n_{0})}$ est vrai.

(${\displaystyle H_{n_{0}}}$) s'appelle l'étape héréditaire ou inductive, elle affirme pour tout ${\displaystyle n\geqslant n_{0}}$ que si ${\displaystyle P(n)}$ est vrai alors ${\displaystyle P(n+1)}$ est vrai aussi^[1].

Deuxième principe d'induction

Lorsque l'on a des cas plus complexes, que l'on ait besoin d'utiliser ${\displaystyle P(n_{0}),P(n_{0}+1),\dots P(n)}$ pour montrer ${\displaystyle P(n+1)}$, il est plus pratique d'utiliser le second principe d'induction.

L'étape de base est cachée dans ${\displaystyle \Gamma _{n_{0}}}$.

Sur ${\displaystyle \mathbb {N} }$, les deux principes d'induction sont équivalents, mais seul le deuxième principe d'induction se généralise à des ensembles ordonnés plus généraux^[1].

Définition par induction structurelle

Considérons une structure définie par des constructeurs ${\displaystyle f_{1},...,f_{n}}$ d'arité ${\displaystyle a_{1},...,a_{n}}$. Les constructeurs d'arité 0 sont des constantes.

La définition par induction structurelle d'une fonction ${\displaystyle g}$ s'écrit pour chaque constructeur ${\displaystyle f_{i}}$

• ${\displaystyle g(f_{i}(x_{1},..x_{a_{i}}),y_{1},...y_{n})=E_{i}(g(x_{1}),...,g(x_{a_{i}}),y_{1},...,y_{n})}$

où ${\displaystyle E_{i}}$ est une expression qui dépend de i'. On remarque que si ${\displaystyle f_{i}}$ est une constante, la définition est celle d'un cas de base:

• ${\displaystyle g(f_{i},y_{1},...y_{n})=E_{i}(y_{1},...,y_{n})}$

Raisonnement par induction structurelle

Le schéma de démonstration qu'une propriété P est valide sur toute une structure se présente sous la forme d'une règle d'inférence pour chaque constructeur ${\displaystyle f_{i}}$

${\displaystyle {\frac {P(x_{1})...P(x_{a_{i}})}{P(f_{i}(x_{1},...,x_{a_{i}}))}}}$

Il faut donc faire une démonstration d'« hérédité » pour chaque constructeur.

Le cas des entiers naturels

Le cas des entiers naturels est celui où il y a deux constructeurs: 0 d'arité 0 (donc une constante) et succ (autrement dit +1) d'arité 1. La récurrence traditionnelle se réduit donc à une récurrence structurelle sur ces deux constructeurs.

La coinduction

Grossièrement la coinduction étend l'induction en offrant la possibilité d'omettre les éléments initiaux (le jardin d'éden).

Par exemple, omettre la liste vide, transforme la liste en flux ((en) stream). : Un flux de trucs est un truc qui s'ajoute à un flux de trucs.

L'induction structurelle en Rocq

Rocq permet l'écriture de types inductifs qui représentent les ensembles inductifs. Rocq va alors générer automatiquement un principe d'induction associé à ce type.

Inductive list {A : Type} :=
    | nil
    | cons (head : A) (tail : list).

Notation "[]" := (nil).
Notation "head :: tail" := (cons head tail).

Fixpoint length {A : Type} (l : @list A) : nat :=
    match l with
    | [] => 0
    | head :: tail => 1 + length tail
    end.|lang=Rocq

Fixpoint concat {A : Type} (l1 : @list A) (l2 : @list A) : @list A :=
    match l1 with
    | [] => l2
    | head :: tail => head :: (concat tail l2)
    end.

Goal forall (A : Type) (l1 l2: @list A), 
        length (concat l1 l2) = length l1 + length l2.
Proof. intros A l1 l2.  
    induction l1 as [{{!}} a l1 IHl1].
    + simpl. reflexivity.
    + simpl. f_equal.
      apply IHl1.
Qed.

list_ind : forall (A : Type) (P : list -> Prop),
    P [] ->
    (forall (head : A) (tail : list), P tail -> P (head :: tail)) ->
        forall l : list, P l

fun (A : Type)
    (P : list -> Prop)
    (Pnil : P [])
    (Pcons : forall (head : A) (tail : list), P tail -> P (head :: tail)) 
=> fix F (l : list) : P l :=
    match l with
    | [] => Pnil
    | head :: tail => Pcons head tail (F tail)
    end