Tutoriel : types de données, fonctions et preuves en Isabelle

Ce tutoriel présente les fonctionnalités de base que nous utiliserons pour définir la sémantique du langage Niklaus :

définition de types de données
définition de fonctions
preuves par application de règles (apply) ou structurées (bloc proof/qed en Isar)

D'autres constructions seront présentées lorsqu'elles seront nécessaires.

Note : vous pouvez télécharger le listing ci-dessous dans un fichier TutoList.thy pour l'utiliser dans Isabelle.

Installation d'Isabelle

Pour installer isabelle sur votre ordinateur, consultez https://isabelle.in.tum.de/

Introduction à Isabelle/HOL man-isabelle.pdf

Exercices

Après avoir fait ce tutoriel, faites les deux exercices suivants. Vous pouvez télécharger le fichier suivant pour démarrer : TutoExos.thy

Fonction inductive

Définissez une fonction snoc l x qui ajoute x à la fin de l, ainsi qu'une fonction rev_snoc l qui utilise snoc pour inverser l. Prouvez que rev_snoc l = rev l.

Vous pouvez utiliser la commande sledgehammer à la place d'une preuve. Cette commande utilise des solveurs externes pour essayer de trouver une preuve. En cas de succès, il ne reste qu'à remplacer l'appel à sledgehammer par la preuve qu'il a trouvée (il suffit pour cela de cliquer sur le texte de la preuve dans la console). Dans l'exemple ci-dessus, vous pouvez donc commencer par remplacer sorry par sledgehammer pour trouver les preuves.

Preuve par induction avec une hypothèse plus forte

Cet exercice est plus difficile, mais il met en évidence l'importance du choix de l'hypothèse de récurrence dans une preuve par induction.

Définissez une fonction rev_acc qui inverse une liste par accumulation dans un second argument, et prouvez que rev_acc l [] = rev l. Dans cette démonstration, l'hypothèse de récurrence est trop faible car elle ne traite que le cas ou le second argument de rev_acc est la liste vide. Il faut donc établir un lemme plus général qui permettra de faire le raisonnement par induction. De plus, pour démontrer ce lemme par induction, nous aurons besoin de l'utiliser avec une autre valeur du second argument de rev_acc, il faut donc indiquer que cet argument est une variable libre grâce à arbitrary: r si l'argument est r.

Code du tutoriel

À enregistrer dans un fichier de nom TutoList.thy.