Les preuves circulaires : une récurrence sans fin ?

La récurrence et l’induction

La force de la preuve par récurrence

La preuve par récurrence est la méthode reine de démonstration en mathématiques. En un certain sens, c’est la technique qui nous donne accès à l’infini, et donne toute leur puissance aux mathématiques. En effet, si on veut montrer qu’une propriété est vraie pour tous les nombres entiers, on ne peut pas simplement énumérer les cas en la montrant pour \(0\), puis \(1\), puis \(2\), etc. Il nous faut un moyen de les « attraper tous d’un coup ». Le principe de la récurrence est le suivant, on montre que :

• la propriété est vraie dans le cas de base \(n=0\)
• si la propriété est vraie pour un entier \(n\), alors elle est vraie pour \(n+1\)

Alors, on peut en conclure que la propriété est vraie pour tous les entiers.

Un exemple de preuve par récurrence

Supposons que l’on vous demande de montrer que pour tout entier \(n\), \(2^n\geq n+1\). Vous pouvez essayer de trouver une méthode pour comparer directement \(2^n\) à \(n+1\) et montrer que cette inégalité est toujours vraie, mais cela n’est pas garanti de fonctionner et peut nécessiter des astuces difficiles à trouver. Essayons plutôt de prouver par récurrence que \(2^n\geq n+1\) pour tout entier \(n\) :

• Cas de base : Pour \(n=0\), on a \(2^0 = 1 \geq 0+1 = 1\). Donc la propriété est vraie pour \(n=0\).
• Hérédité : On part de l’hypothèse \(2^n \geq n+1\) et on veut montrer que \(2^{n+1} \geq n+2\).
  – On sait que \(2^{n} \geq n+1\) donc \(2*2^n\geq 2*(n+1)\).
  – Comme \(2*2^n=2^{n+1}\), et \(2*(n+1)=2n+2\) qui est supérieur à \(n+2\), on a bien \(2^{n+1}\geq n+2\).
  – La propriété est donc vraie pour \(n+1\) si elle est vraie pour \(n\).

On en conclut que l’inégalité \(2^n\geq n+1\) est bien vraie pour tout entier \(n\), en ayant suivi un raisonnement quasiment « automatique ».

La définition par récurrence

La récurrence sert également à définir des objets. On peut définir par exemple une suite \(u_0,u_1,u_2\dots\) par \(u_0=10\) et pour tout \(n\), \(u_{n+1}=5u_n+4\).

Il est naturel d’utiliser la preuve par récurrence sur des objets définis de cette façon. On pourra ainsi prouver simplement par récurrence que tous les \(u_n\) sont pairs, sans avoir à calculer leur valeur :

• \(u_0\) vaut \(10\) donc il est pair
• si \(u_n\) est pair, alors \(5u_n+4\) est pair aussi, donc \(u_{n+1}\) est pair.

On peut en conclure que tous les \(u_n\) sont pairs, sans avoir besoin de se demander ce que vaut \(u_{100}\) par exemple.

Inventer l’invariant

Dans ce cas simple, la preuve est assez directe, mais la méthode de récurrence nécessite souvent de trouver un invariant : une propriété qui reste vraie à chaque étape de la construction, et qui peut être plus forte que la propriété que l’on souhaite réellement prouver. Il faut donc parfois une certaine intuition ou créativité pour trouver le bon invariant. Dans les exemples précédents, l’invariant était simplement la propriété que l’on souhaitait prouver, mais ce n’est pas toujours le cas.

Voici un exemple simple de ce phénomène : on souhaite prouver que pour tout entier \(n\), \(1+\frac{1}{4}+\dots+\frac{1}{n^2}\leq 2\). Si on essaie de prouver directement ceci par récurrence, on réalise que ça ne fonctionnera pas : en supposant la propriété pour une valeur \(n\), ce qu’on obtient pour \(n+1\) est \( 1+\frac{1}{4}+\dots+\frac{1}{n^2}+\frac{1}{(n+1)^2}\leq 2+\frac{1}{(n+1)^2}\), et non \(1+\frac{1}{4}+\dots+\frac{1}{n^2}+\frac{1}{(n+1)^2}\leq 2\) comme désiré.

On peut en revanche montrer par récurrence que pour tout \(n\), \(1+\frac14+\dots+\frac1{n^2}\leq 2-\frac1n\) (en utilisant le fait que \(\frac1{(n+1)^2} < \frac1n-\frac1{n+1}\)). C’est un invariant plus fort que ce que l’on souhaite prouver, mais il est nécessaire pour pouvoir faire la preuve par récurrence.

Définition par induction

Un autre nom de la récurrence, plus utilisé en informatique, est l’induction. Les structures inductives sont les structures définies par induction, c’est-à-dire en donnant un cas de base, et une manière de combiner des structures déjà construites pour en construire de nouvelles. On peut par exemple donner le cas des listes : une liste est soit la liste vide, soit composée d’un premier élément suivi d’une liste. On voit que cette définition des listes par induction est autoréférente : on utilise la notion de liste dans la définition de ce qu’est une liste. Spécifier que c’est une définition par induction signifie que l’on considère ici que cette construction doit partir du cas de base (ici la liste vide) et n’utiliser qu’un nombre fini d’étapes pour construire un objet donné. Chaque objet construit par induction sera donc fini. Dans notre exemple des listes, cette définition inductive permet donc de construire toutes les listes finies. Selon ce principe, on peut également définir les entiers par induction : un entier est soit \(0\), soit le successeur d’un entier.

Coinduction et preuve circulaire

Nous avons vu que l’induction ne permet de construire que des objets finis, mais nous pouvons aussi vouloir définir des objets infinis, comme les listes infinies.

La coinduction est une approche complémentaire (les mathématiciens disent « duale ») à l’induction, adaptée aux objets potentiellement infinis. Comme pour l’induction, la coinduction désigne à la fois une méthode de construction des objets et une technique de preuve sur ces objets.

La définition par coinduction

Dans la méthode de construction d’objets par coinduction, la grande différence avec l’induction est que cette fois, on ne s’oblige pas à s’appuyer sur un cas de base pour construire nos objets. Au contraire, on s’autorise des définitions d’objets infinis en utilisant une autoréférence qui ne s’arrête jamais. On peut ainsi reprendre la définition des listes, en disant qu’une liste est un premier élément suivi d’une liste. Si on n’ajoute pas de cas de base, on ne définira donc que des listes infinies, appelées flux. Si nos éléments sont des lettres, un exemple de flux est \(aabaabaab\dots\) (les points de suspension signifient que ça continue à l’infini). Les objets définis par coinduction sont appelés structures coinductives, dont les flux sont un exemple.

De même que pour la définition des flux en général, la définition par coinduction d’un flux particulier sera autoréférente, par exemple le flux infini \(f=aaaa\dots\) peut être défini comme le flux qui est égal à \(a\) suivi du flux \(f\) lui-même. On peut noter cette définition de manière concise \(f=af\). Cette définition est autoréférente, mais elle est bien suffisante pour connaître les éléments de \(f\) : on peut toujours déplier la définition autant de fois que nécessaire pour connaître chacun de ses éléments.

Preuve par coinduction

La preuve par coinduction suit la même idée que la définition par coinduction : on montre qu’une propriété est préservée au fil de la construction de l’objet (comme pour le passage de \(n\) à \(n+1\) dans l’induction), mais sans nécessairement s’appuyer sur un cas de base, et en autorisant une infinité d’étapes à la place.

Reprenons notre flux \(f\) défini par \(f=af\), et considérons maintenant le flux \(g=aag\), c’est-à-dire le flux formé de \(a\) puis \(a\) puis le flux \(g\) lui-même. Notre but va être de prouver que \(f\) et \(g\) sont en fait le même flux : simplement une suite infinie de \(a\). Cet exemple est simple, mais il permet d’illustrer le principe de preuve par coinduction.

Montrons par coinduction que les flux \(f\) et \(g\) définis ci-dessus sont égaux :

• On veut montrer \(f=g\).
• En déroulant les définitions de \(f\) et \(g\), cela revient à montrer \(af=aag\).
• Comme les deux commencent par \(a\), il suffit de montrer que \(f=ag\).
• En redéployant la définition de \(f\), cela revient à montrer que \(af=ag\).
• Les deux commencent par \(a\), il suffit donc de montrer que \(f=g\) comme au début.
• On a rebouclé sur le point de départ, c’est gagné !

On a l’impression ici de s’être fait entourlouper. Comment accepter une telle preuve qui semble ne faire que tourner en rond ? Une telle preuve par coinduction est pourtant bien valide. La clé ici est qu’on n’est pas simplement revenu au point de départ en tournant en rond dans la preuve, mais qu’on a ce faisant avancé dans la lecture des flux. On appelle cela un critère de progression.

Voici ci-dessous un exemple simplifié de « preuve » qui ne respecterait pas ce critère de progression.

• On veut montrer \(f=g\).
• Cela revient à montrer que \(af = ag\).
• Donc à montrer que \(f=g\).

Ce raisonnement n’est pas valide parce que la deuxième étape est obtenue en ajoutant \(a\) de chaque côté, mais on n’a jamais déplié (et donc jamais utilisé) les définitions coinductives des flux.

Les preuves circulaires

Les preuves circulaires s’inspirent des preuves par coinduction, mais ont moins de contraintes : on autorise simplement les « boucles de raisonnement », par exemple pour prouver \(A\) on peut avoir besoin d’utiliser \(B\), mais \(B\) se prouvera lui-même à partir de \(A\). De telles boucles peuvent s’imbriquer ou se combiner de manière complexe. Pour éviter de pouvoir prouver des énoncés faux, on impose ensuite un critère de validité qui permettra de vérifier a posteriori que de telles preuves sont correctes. L’idée d’un tel critère est qu’en suivant le chemin de la preuve, on doit toujours revenir vers le cas de base pour les structures inductives, ou explorer en entier les structures coinductives.

Les preuves par induction/coinduction sont toujours valides par construction : leur structure rigide ne laisse pas de place à l’erreur. Le prix à payer pour cela est qu’elles nécessitent un invariant, qu’il faut parfois inventer. Les preuves circulaires sont plus souples, en particulier pour les démonstrations impliquant en même temps des structures inductives et coinductives, mais nécessitent un critère de validité à vérifier a posteriori. On peut parfois économiser la recherche d’invariant dans ce cadre : l’idée est que l’on peut explorer « à l’aveugle » en espérant retomber sur nos pattes, et que l’invariant apparaitra alors implicitement. C’est un avantage de taille, qui justifie l’intérêt grandissant pour ce type de preuves, surtout dans la recherche de techniques pour construire des preuves automatiquement.

Exemples de preuves circulaires

Reprenons nos flux (c’est-à-dire listes infinies) \(f\) et \(g\) définis précédemment, via \(f=af\) et \(g=aag\). Voici deux preuves circulaires qui montrent que \(f\) et \(g\) sont égaux, l’une valide (elle suit en réalité la structure de la preuve par coinduction), l’autre invalide.

On utilise la notation de la théorie de la démonstration : \(\frac{~A~}{B}\) signifie que \(A\) implique \(B\). Lorsque l’on construit une preuve, on procède souvent de bas en haut : « Pour prouver \(B\), il suffit de prouver \(A\) ». On progresse donc selon les étapes numérotées. Si la preuve était par induction, on finirait par atteindre un cas de base et s’arrêter. Ici, les flèches nous indiquent qu’en remontant comme ceci, c’est-à-dire en progressant dans la preuve, on peut revenir à un point déjà vu ; autrement dit on peut continuer pour toujours.

Dans ces preuves, on a utilisé les principes suivants, tous valides :

• \(f=af\) (dans les deux preuves)
• \(g=aag\) (dans la première preuve)
• si \(x=y\) alors \(ax=ay\) (dans la première preuve, deux fois)
• si \(x=y\) alors \(y=x\) (dans la seconde preuve).

Voyons comment ces preuves peuvent être vues comme une manière de lire les flux \(f\) et \(g\) en vérifiant leur égalité. On part du bas de la preuve, c’est-à-dire l’énoncé qu’on veut montrer (ici \(f=g\)), et on remonte la preuve en suivant les opérations décrites. Le curseur rouge représente ici à partir de quand on doit vérifier l’égalité des flux restants, car on a déjà contrôlé que le début correspond bien :

La preuve valide suit le schéma de la preuve par coinduction vue précédemment, en dépliant \(f\) et \(g\) suffisamment pour retomber sur \(f=g\). La preuve invalide déplie \(f\), inverse le sens de l’égalité, puis replie \(f\) et inverse encore le sens de l’égalité pour retomber sur \(f=g\). On a donc ici un raisonnement circulaire, qui n’a en fait pas avancé dans la lecture des flux, et pourrait être tout aussi bien appliqué si \(g\) commençait par \(b\).

Donner ici un exemple explicite de preuve circulaire valide qui n’est pas une preuve par coinduction nous emmènerait trop loin. Les arbres de preuves que nous avons montrés n’ont qu’une seule branche. Dans la réalité les preuves ont une arborescence bien plus foisonnante. Les circularités entre les différentes parties de ces arbres peuvent être arbitrairement complexes.

Les preuves comme programmes

Il existe une correspondance entre preuves mathématiques et programmes informatiques, qui permet de voir une preuve comme un programme qui fait des calculs. Outre son intérêt théorique touchant aux aspects fondamentaux des mathématiques et de l’informatique, l’une des applications de cette correspondance est le développement de logiciels appelés assistants de preuve.

La correspondance preuve/programme

Dans cette correspondance, les énoncés mathématiques correspondent au type des données manipulées, et les preuves correspondent aux programmes qui manipulent ces données. La proposition \(p\Rightarrow q\) s’interprète alors comme un programme de type \(p\to q\), qui se nourrit d’un type de données \(p\) et renvoie un type de données \(q\). Donnons dans ce cadre une preuve de la propriété \(p\Rightarrow p\), qui est une tautologie logique, c’est-à-dire une proposition vraie. On peut voir cette preuve comme un programme qui prend un élément \(x\) de type \(p\) et renvoie simplement \(x\). En Python, cela donnerait le programme suivant, qui est bien de type \(p\to p\) si \(x\) est de type \(p\) :

def preuve(x):
    return x

Plus difficile, essayons de prouver \((p \wedge q)\Rightarrow p\), qui se lit « (\(p\) et \(q\)) implique \(p\) ». Cela revient à écrire un programme qui prend un élément \(x\) de type \(p\) et un élément \(y\) de type \(q\), et renvoie un élément de type \(p\). Il suffit pour cela de renvoyer simplement l’élément \(x\), en ignorant \(y\). En Python, cela donne le programme suivant :

def preuve(x,y):
   return x

Cette correspondance entre preuves et programmes s’appelle correspondance de Curry-Howard, et est à la base de nombreux outils informatiques pour la preuve automatique, comme Rocq (anciennement appelé Coq). En effet, prouver un théorème dans un tel assistant revient à écrire un programme, et l’assistant se contente de vérifier que le type du programme correspond bien à l’énoncé du théorème. De plus en plus d’aspects du processus sont automatisés ou guidés, pour que l’utilisateur puisse se concentrer au maximum sur les aspects intéressants et non évidents des démonstrations.

Preuves inductives et coinductives comme programmes

Dans ce cadre, les preuves inductives correspondent à des programmes récursifs, c’est-à-dire à des programmes qui peuvent se rappeler eux-mêmes, et sont censés terminer au bout d’un moment sur un cas de base. Un exemple classique de tel programme est le calcul de la factorielle d’un entier :

def factorielle(n):
    if n==0:
        return 1
    else:
        return n*factorielle(n-1)

Ici si on veut calculer la factorielle de \(5\), on lance factorielle(5), et on obtiendra \(120\), grâce au programme qui se rappelle lui-même pour calculer 5*factorielle(4), etc.

Le cas coinductif correspond également à des programmes récursifs s’appelant eux-mêmes, mais qui sont autorisés à ne jamais s’arrêter. Voici par exemple un programme qui génère la suite de Fibonacci, sans fin :

def fibo(a,b):
    print(a)
    return fibo(b,a+b)

Si on lance le programme fibo(1,1), on obtiendra la suite infinie des nombres de Fibonacci, dont chacun est égal à la somme des deux précédents : \(1,1,2,3,5,8,13,\dots\).

Le critère de progression des preuves coinductives correspond ici au fait qu’on veut vraiment imprimer une infinité de nombres, pour donner toutes les valeurs de la suite, et non se mettre au bout d’un moment à tourner en boucle sans avancer. Dans ce programme, ce critère sera garanti par le fait qu’il y a toujours une instruction print entre deux appels de la fonction fibo.

Ces exemples sont plutôt empruntés au monde de la programmation plutôt que de la preuve, mais on peut les voir comme des preuves que les fonctions factorielle et fibo sont bien définies.

Pour revenir vers les exemples des sections précédentes, voilà à quoi ressemblerait une traduction directe de la preuve par coinduction de \(f=g\), vue en Partie 2. Dans ce cadre, la définition de \(f\) selon laquelle \(f=af\) (une hypothèse que l’on pouvait utiliser dans la preuve) se traduit par un programme hypo_f qui prend \(f\) et renvoie le premier élément de \(f\) et ce qui reste, qui seront toujours égaux à \(a\) et \(f\) respectivement.

hypo_f(f)=(a,f)

De même pour \(g\), on aura

hypo_g(g)=(a,a,g)

def egaux(f,g):
    (x1,f')=hypo_f(f)
    (y1,y2,g')=hypo_g(g)
       if x1==y1:
           (x2,f'')=hypo_f(f')
           if x2==y2:
               return egaux(f'',g')
           else: return False
       else:
           return False

commentaires  
    x1 vaut a et f' vaut f
    y1 vaut a, y2 vaut a, g' vaut g
       on a bien x1==y1 : tous deux valent a
           x2 vaut a et f'' vaut f
           on a bien x2==y2 : tous deux valent a 
               on vérifie que f'' et g' sont égaux 
           
       
           

Ce programme copie complètement la structure de la preuve par coinduction vue en partie 2. Ici le critère de progression est valide, car ce programme accèdera effectivement à tous les éléments de \(f\) et \(g\) pour vérifier qu’ils sont égaux.

On notera que l’interprétation calculatoire de la coinduction correspond bien à des programmes qui ne s’arrêtent jamais. Par contre une preuve par coinduction est bien un objet fini qu’on peut vérifier complètement et qui prouve que les flux sont égaux. C’est une subtilité qu’on peut expliciter ainsi : dans le cas d’une preuve circulaire ou par coinduction, exécuter le programme n’est pas la même chose que vérifier la preuve, puisque dans le premier cas le processus ne termine pas et dans le second oui.

Les preuves circulaires comme programmes

Les preuves circulaires correspondent à des programmes GoTo, où l’on peut dire au programme de sauter n’importe où dans le code et continuer à partir de là. Voici par exemple le programme de Fibonacci en version GoTo:

a=1
b=1
debut:
print(a)
c=a
a=b
b=c+b
goto debut

Comme précédemment, le critère de validité des preuves circulaires correspond ici au fait que le programme ne doit pas tourner en rond sans avancer, et doit générer une infinité de nombres.

On voit ici que ces programmes offrent beaucoup plus de flexibilité, mais qu’il peut être plus difficile de vérifier leur validité. Pensez aux cas où l’on met des GoTo dans tous les sens, qui peuvent créer des boucles s’appelant les unes les autres de manière complexe. Cela reflète effectivement les propriétés des preuves circulaires par rapport aux preuves inductives et coinductives : elles sont plus souples mais nécessitent une vérification pour garantir leur validité.

On peut remarquer qu’il est facile de traduire un programme composé de fonctions récursives en programme GoTo, mais que l’inverse semble plus difficile. C’est exactement ce qu’il se passe pour les preuves : il est en général facile de transformer une preuve inductive ou coinductive en preuve circulaire, mais difficile de transformer une preuve circulaire en preuve utilisant l’induction et la coinduction. Pour certains systèmes de preuves particuliers, c’est même un problème ouvert de recherche. Pour d’autres systèmes de preuves, une réponse (positive ou négative en fonction du système considéré) a déjà été obtenue.

Conclusion

Les preuves circulaires sont un outil puissant, car elles peuvent permettre de contourner les difficultés liées à la recherche d’invariants dans les preuves inductives et coinductives. Cela en fait en particulier un outil privilégié pour la preuve automatique. Elles sont de plus en plus étudiées et reconnues comme des preuves à part entière, et des questions intrigantes subsistent quant à leur relation avec les preuves plus classiques.

Remerciements

Merci à Amina Doumane et Damien Pous, ainsi qu’au comité éditorial d’Interstices, pour leurs conseils et relectures attentives.