Consignes

Le rendu de ce TP se fera uniquement par TPLab et consistera en une archive (zip, tar, etc.) contenant un répertoire TP2-NOM avec :

Vous aurez compris que NOM devra être remplacé par votre nom (ou vos noms en cas de binômes) !

Tous vos fichiers doivent comporter une entête avec votre noms et votre groupe de TP.

Tout non respect d'une ou plusieurs de ces consignes entrainera automatiquement un retrait de points sur votre note !

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.

Si vous utilisez votre portable, vous devez arriver en TP avec un système fonctionnel. Pour Ubuntu, lancez la commande 

$ sudo apt install coq emacs

Vous pouvez également utiliser VsCode + vscoq, mais dans ce cas, vous devez installer et tester votre système avant la séance de TP.

Installation de Proof General

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

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 construction, 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

./TP2/emacs-1.png

Les preuves en Coq ne sont en général pas lisibles "statiquement". Avancez dans la preuve en utilisant le bouton "Next" pour observer ce qu'il se passe :

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,

./TP2/emacs-2.png

les hypothèses contiennent

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

∀y:ℕ, ∃x:ℕ, f∘g(x) = y ⊢ ∃x:ℕ, f(x) = y

Avancez dans la preuve en regardant l'évolution du but.

Emacs et Proof General offrent les raccourcis suivants :

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.

règle tactique remarques
axiome * assumption.
⇒c * intro. on peut choisir le nom de l'hypothèse avec intro H.
modus ponens apply H. H doit être une hypothèse ou un théorème de la forme P -> Q
∧c * split.
∧1 et ∧2 voir question 2
∨c,1 left.
∨c,2 right.
raisonnement par cas + destruct H. voir plus bas
¬c intro. on peut choisir le nom de l'hypothèse avec intro H.
contradiction apply H H doit être une hypothèse ou un théorème de la forme ~P
raisonnement par l'absurde apply NNPP; intro. il faut avoir la ligne Require Import Classical_Prop. au début du fichier
∀c * intro. on peut choisir le nom de la variable avec intro x.
spécialisation apply H. voir plus bas
∃c exists (u). u est le terme qui sert de témoin
utilisation du ∃ + destruct H. voir plus bas

apply permet d'appliquer la règles du modus ponens avec une petite différence. Au lieu d'avoir 2 prémisses ("P⇒Q" et "Q"), la tactique prend une preuve de P⇒Q en argument et n'a donc qu'une seule prémisse.

La situation est similaire pour les règles

Utilisation du "et"

Il n'y a pas de tactique pour l'utilisation du "et" (∧1 et ∧2), mais une tactique pour séparer une conjonction dans les hypothèses : destruct H.

Dans votre fichier mario_deduction_naturelle.v complétez les preuves suivantes : 

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

(tactiques assumption., destruct. et intro.)

et 

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

(tactiques assumption., destruct. et intro.)

Ces théorèmes permettent d'avoir les "vraies" règles ∧1 et ∧2 :

∧c,1 apply utilisation_et_1.
∧c,2 apply utilisation_et_2.

mais il est en général plus facile d'utiliser directement la tactique destruct.

1.2. Déduction naturelle, logique propositionnelle

Il est possible de faire une preuve en donnant simplement les tactiques dans l'ordre. L'interpréteur retrouve automatiquement le but courant à chaque étape, et passe au but suivant lorsqu'un but est prouvé.

Il est cependant conseillé d'utiliser les marqueurs de liste ("-", "+" et "*") pour séparer les preuves des différents buts. Ainsi, une preuve pourrait ressembler à 

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

Dans cette preuve,

  • les tactique 1 à 3 s'appliquent au but initial,

  • la tactique 3 introduit un nouveau sous-but,

  • le premier sous-but est prouvé par les tactiques 4 à 8,

    • la tactique 5 introduit un nouveau sous-but,

    • le premier "sous-sous-but" est prouvé par la tactique 6,

    • le second "sous-sous-but" est prouvé par les tactiques 7 et 8,

  • le second sous-but est prouvé par les tactiques 9 et 10.

Faites les preuves suivantes en Coq dans votre fichier mario_deduction_naturelle.v. 

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

(tactiques destruct et split) 

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

(tactiques destruct, left, right et split) 

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

(tactique apply) 

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

(tactiques destruct, left, right et split)

Plus difficile, faites la preuve de la première loi de de Morgan :

¬(P ∨ Q) ⇔ ¬P ∧ ¬Q

(tactiques apply, destruct, left, right et split)

Faites la preuve de la deuxième loi de de Morgan :

P ∨ Q ⇔ ¬(¬P ∧ ¬Q)

En plus des tactiques apply, destruct, left, right et split, vous aurez besoin du raisonnement par l'absurde : apply NNPP; intro.

1.3. Déduction naturelle, logique du premier ordre

On ajoute maintenant les quantificateurs !

Faites les preuves suivantes en Coq. 

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

(tactiques apply, destruct et split) 

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

(tactiques destruct, exists, left, right et split)

Plus dur, faite la preuve de la loi de de Morgan

¬∃ x:X, P(x) ⇔ ∀ x:X, ¬ P(x)

(tactiques apply, destruct, exists et split)

La tactique apply prend comme argument une hypothèse ou un théorème déjà démontré.

Si l'hypothèse ou le théorème est de la forme ∀ x, ..., on peut utiliser apply (H u). pour utiliser une instanciation particulière.

Faites la preuve de la loi de de Morgan

∃ x:X, P(x) ⇔ ¬(∀ x:X, ¬P(x))

En plus des tactiques apply, destruct, exists et split, vous aurez besoin du raisonnement par l'absurde : apply NNPP; intro.

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 :

La preuve complète nécessiterait l'introduction de nombreux concepts, alors nous allons nous intéresser à des programmes encore plus simples !

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 :

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.

Rappel, la concaténation en Caml peut s'écrire comme 

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].

Par définition, pour n'importe quelle liste l, on devrait avoir concat [] l = l. Dans votre fichier mario_concat.v, faites la preuve de 

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

Vous devrez utiliser la tactique simpl. pour simplifier (évaluer) une hypothèse ou un but.

Pour prouver un but évident, vous pouvez utiliser la tactique trivial.

Essayez de faire la même preuve pour 

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

et expliquez brièvement dans un commentaire pourquoi cela ne fonctionne pas.

Ne cherchez pas de preuve correcte pour cette formule. Cela sera fait dans la question suivante !

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,

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

Faite la preuve par induction du résultat suivant. 

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

  • vous devrez utiliser la tactique induction sur la liste l après avoir fait un intro.,

  • vous pouvez utiliser la tactique simpl. pour simplifier le but courant,

  • vous pouvez utiliser la tactique trivial. pour finir une preuve vraiment facile,

  • si vous avez une hypothèse H : u = v, vous pouvez remplacer chaque u par v dans le but courant avec la tactique rewrite H.

Faite la preuve par induction que la concaténation est associative : 

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

Les tactiques utilisées seront les même que pour la question précédente.

Une seule induction (sur l1) est suffisante pour faire cette preuve.

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 [].

En Caml, les fonctions correspondantes pourraient s'écrire de la manière suivante. 

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)

Essayez de faire une preuve par induction de 

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

et expliquez en quelques mots pourquoi ce n'est pas possible directement.

Avant de prouver le théorème de la question précédente, nous allons prouver un théorème plus général : 

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

Faite cette preuve par induction sur l1 en faisant attention aux points suivants :

Utilisez maintenant le théorème thm_renverse_gen pour prouver 

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

Pour cela, vous devrez :