INFO501 : logique (et informatique)

TP 2 : systèmes de preuves, assistants de preuves

Automne 2024

• Consignes

  • Outils nécessaires, prérequis

    • Installation de Proof General (sauf pour l'interface en ligne)

• Liens utiles

• Préliminaires

  • Utiliser Coq

  • Un exemple

• 1. Déduction naturelle en Coq

  • 1.1. Règles et tactiques

    • Une première preuve

  • 1.2. Déduction naturelle, logique propositionnelle

  • 1.3. Déduction naturelle, logique du premier ordre

• 2. Initiation à la preuve de programmes

  • 2.1. Concaténation des listes

  • 2.2. Preuves par induction

  • 2.3. Deux manières de renverser une liste

Consignes

Outils nécessaires, prérequis

Pour ce TP, vous devez disposer de l'assistant de preuves Coq. Sur les machines de l'université, Coq est installé sur la partition Linux.

Nous allons utiliser l'éditeur de texte emacs avec l'extension Proof General.

$ sudo apt install coq emacs

Installation de Proof General (sauf pour l'interface en ligne)

Lancez la commande suivante depuis un terminal, pour télécharger, compiler et configurer Proof General automatiquement. Ça devrait prendre moins de une minute. (Attention, il faut copier toutes les lignes de la commande, sans le $ initial.)

$ [ -d ~/.emacs.d/lisp/PG ] ||
      git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG &&
    make -C ~/.emacs.d/lisp/PG &&
    grep -qs 'Proof General config' ~/.emacs ||
      { echo '; Proof General config' >> ~/.emacs &&
        echo '(load "~/.emacs.d/lisp/PG/generic/proof-site")' >> ~/.emacs &&
        echo '(setq inhibit-startup-screen t)' >> ~/.emacs &&
        echo '(setq proof-splash-enable nil)' >> ~/.emacs &&
        echo '(setq coq-accept-proof-using-suggestion (quote never))' >> ~/.emacs ; }

Liens utiles

• "Petit guide de survie en Coq",

• le fichier exemple_surjection.v

• le fichier mario_deduction_naturelle.v

• le fichier mario_concat.v

• Coq tactics cheatsheet

• Software Foundations, une série très complète sur l'application des assistants de preuves à l'analyse de programmes.

Préliminaires

Utiliser Coq

Coq est un assistant de preuves développé par l'INRIA. Contrairement aux SAT-solveurs (par exemple), les preuves dans un tel système ne sont en général pas automatiques : les assistants de preuves nécessitent une interaction avec l'utilisateur. Cela permet de faire de preuves plus complexes qu'on ne peut pas automatiser.

Coq est basé sur le calcul des constructions, qui peut être vu comme une extension de la déduction naturelle et des langages de programmation fonctionnelle. (Coq est d'ailleurs programmé en Caml.)

Une preuve en Coq se déroule de la manière suivante.

1. On définit (mot clé Definition) les types pour les objets que l'on veut manipuler. Coq possède de nombreuses bibliothèques avec les types des objets usuels : nombres, listes, etc.

2. On donne un énoncé que l'on veut prouver (mot clé Theorem) en donnant la proposition ("formule") correspondante.

3. On fait la preuve en utilisant des "tactiques" de preuves. Ces tactiques généralisent les "règles de démonstrations" vues en cours. L'interpréteur Coq vérifie que chaque étape est valide et affiche le but courant.

4. On termine la preuve avec le mot clé Qed (abbréviation de "Quod erat demonstrandum", càd "Ce qu'il fallait démontrer" en latin).

Un exemple

Le fichier exemple_surjection.v contient une petite preuve en Coq. Pour comprendre comment une preuve Coq fonctionne, ouvrez ce fichier dans emacs. Si vous avez bien installé Proof General, vous devriez obtenir

Les preuves en Coq ne sont en général pas lisibles "statiquement". Avancez dans la preuve en utilisant le bouton "Next" (triangle vert vers le bas dans l'interface en ligne) pour observer ce qu'il se passe :

• définition de surjective et comp,

• énoncé du théorème,

• preuve.

Lors de la preuve, Coq affiche le but courant ("goal" en anglais). Le but ressemble à un séquent, mais les hypothèses sont notées au dessus de la formule plutôt qu'à gauche. Par exemple, à cette étape de la preuve,

les hypothèses contiennent

• la liste des variables avec leurs types :

  • f et g de type ℕ → ℕ (première ligne)

  • y de type ℕ (troisième ligne),

• la formule ∀y:ℕ, ∃x:ℕ, f∘g(x) = y (deuxième ligne).

Comme les variables ne sont pas déclarées explicitement dans les séquents, ceci correspond au séquent

1. Déduction naturelle en Coq

1.1. Règles et tactiques

En utilisant les même noms utilisés en cours et en TD (voir regles.pdf), les règles de la déduction naturelle correspondent aux tactiques suivantes.

Une première preuve

Theorem et_1 : P /\ Q -> P.
Proof.
  (* ... *)

Theorem et_2 : P /\ Q -> Q.
Proof.
  (* ... *)

1.2. Déduction naturelle, logique propositionnelle

Theorem ...
Proof.
  tactique1.
  tactique2.
  tactique3.
  - tactique4.
    tactique5.
    + tactique6.
    + tactique7.
      tactique8.
  - tactique9.
    tactique10.

Theorem et_com : P /\ Q -> Q /\ P.

Theorem ou_com : P \/ Q <-> Q \/ P.

Theorem contraposition : (P -> Q) -> (~Q -> ~P).

Theorem distribution : (P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R)).

1.3. Déduction naturelle, logique du premier ordre

On ajoute maintenant les quantificateurs !

Theorem pourtout_et : (forall x:X, (P x /\ Q x)) <-> (forall x : X, P x) /\ (forall x : X, Q x).

Theorem existe_ou : (exists x:X, (P x \/ Q x)) <-> (exists x:X, P x) \/ (exists x:X, Q x).

2. Initiation à la preuve de programmes

Les assistants de preuves sont également utilisés pour faire des preuves de programmes. L'objectif est de vérifier qu'un programme satisfait sa spécification. On pourrait par exemple montrer

Theorem tri_insertion_correct :
    forall l : list nat,
    dans_l_ordre (tri_insertion l) /\ est_permutation l (tri_insertion l)

Il faudrait bien sûr commencer par :

• définir le programme tri_insertion,

• définir le prédicat dans_l_ordre,

• définir le prédicat est_permutation.

La preuve complète nécessiterait l'introduction de nombreux concepts. Nous allons donc nous intéresser à des programmes moins complexes.

2.1. Concaténation des listes

Même s'il est possible de prouver des programmes écrits en C ou en Java, il est nettement plus simple de regarder des programmes écrits dans un langage fonctionnel.

Le type des listes chainées est déjà défini en Coq. Il suffit simplement d'importer la bonne bibliothèque :

Require Import List.
Import ListNotations.

Comme en Caml, le type des listes est un type récursif avec 2 constructeurs :

• [] désigne la liste vide,

• e::l désigne l'ajout du l'élément e devant la liste l.

La concaténation s'écrit presque comme en Caml :

Fixpoint concat (l1 : list nat) (l2 : list nat) :=
  match l1 with
  | [] => l2
  | x::l1 => x :: (concat l1 l2)
  end.

let rec concat l1 l2 =
  match l1 with
  | [] -> l2
  | x::l1 -> x::(concat l1 l2)

Vous pouvez faire quelques tests dans emacs en évaluant les commandes suivantes :

Compute (concat [] []).
Compute (concat [1; 2; 3] []).
Compute (concat [] [65; 66; 67]).
Compute (concat [1; 2] [65; 66; 67; 68]).

qui donneront respectivement [], [1;2;3], [65; 66; 67] et [1; 2; 65; 66; 67; 68].

Theorem concat_vide_gauche : forall l : list nat, concat [] l = l.

Theorem concat_vide_droite : forall l : list nat, concat l [] = l.

2.2. Preuves par induction

La preuve de

Theorem concat_vide_droite : forall l : list nat, concat l [] = l.

nécessite une nouvelle tactique pour faire des preuves par récurrence :

1. si une propriété est vraie pour [],

2. et si quand cette propriété est vraie pour l, alors elle est vraie pour x::l,

alors la propriété est vraie pour n'importe quelle liste.

En effet,

• la propriété est vraie pour [] par le point 1,

• comme la propriété est vraie pour [], elle est vraie pour x::[] = [x] par le point 2,

• comme la propriété est vraie pour [x], elle est vrai pour y::[x] = [x; y] par le point 2,

• ...

Si l est une variable de liste dans le contexte, la tactique induction l. va générer 2 buts :

• un sous-but pour [],

• un sous-but pour x::l, en ajoutant l'hypothèse que le but courant est vrai pour l.

Theorem concat_vide_droite : forall l : list nat, concat l [] = l.

Theorem concat_associative : forall l1 l2 l3,
  concat (concat l1 l2) l3 = concat l1 (concat l2 l3).

2.3. Deux manières de renverser une liste

La manière "naïve" de renverser une liste consiste à prendre la tête de liste et à la concaténer à la fin du renversé de la queue de liste. En Coq :

Fixpoint renverse (l : list nat) :=
  match l with
  | [] => []
  | x::l => concat (renverse l) [x]
  end.

Une autre manière, plus efficace, est d'utiliser la fonction suivante avec un accumulateur :

Fixpoint concat_renverse (l1 : list nat) (l2 : list nat) :=
  match l1 with
  | [] => l2
  | x::l1 => concat_renverse l1 (x::l2)
  end.

On obtient alors le renversé de l avec concat_renverse l [].

let rec renverse l =
  match l with
  | [] -> []
  | x::l -> (concat (renverse l) [x])

let rec concat_renverse l1 l2 =
  match l1 with
  | [] -> l2
  | x::l1 -> concat_renverse l1 (x::l2)

Theorem thm_renverse : forall l, renverse l = concat_renverse l [].

Theorem thm_renverse_gen : forall l1 l2,
  renverse_concat l1 l2 = concat (renverse l1) l2.

Theorem thm_renverse : forall l, renverse l = concat_renverse l [].

Remarques sur la page (ou le sujet) : contact.

,

Dernière révision: le 02-10-2024 à 11:32.

mentions légales