Découverte de la programmation certifiée avec Coq

Tout le monde se secoue ! 

J’ai commencé (il y a 4 heures) la rédaction d’un article au doux nom de « Découverte de la programmation certifiée avec Coq » et j’ai pour objectif de proposer en validation un texte aux petits oignons. Je fais donc appel à votre bonté sans limites pour dénicher le moindre pépin, que ce soit à propos du fond ou de la forme. Vous pourrez consulter la bêta à votre guise à l’adresse suivante :

Merci !

Salut,

C’est assez abouti, donc tous types de retours sont les bienvenus ! Orthographe, structure, style, clarté, tout.

Salut,

Je ne sais pas trop à qui s’adresse l’article, parce qu’il y a des passages où tu sembles partir du principe que le lecteur ne connait pas Coq, et d’autres où sans le connaitre (ce qui est mon cas) ça devient difficile à suivre. En particulier, la partie « Démonstration du théorème de correction » m’a perdu. Je pense qu’il manque quelques détails, par exemple tu dis :

Il existe une tactique permettant de prouver n’importe quelle égalité sur un anneau, ce qui conclut la preuve : ring..

Mais ce ring. n’apparait pas dans le texte, il faut aller le chercher dans le code complet pour le trouver.

D’autre part, une question que je me pose (mais qui ne rentre peut-être pas dans le cadre de cet article), c’est que le programme Coq valide le fonctionnement du compilateur sur un programme valide, mais comment sont gérés les cas des programmes invalides ? (par exemple si tu essaie de compiler Add -5 ou Sub A ?)

Enfin, erreur classique, le lien vers l’article au début est le lien vers ta version à toi, pas vers la version publique.

Salut,

Je ne sais pas trop à qui s’adresse l’article, parce qu’il y a des passages où tu sembles partir du principe que le lecteur ne connait pas Coq, et d’autres où sans le connaitre (ce qui est mon cas) ça devient difficile à suivre. En particulier, la partie « Démonstration du théorème de correction » m’a perdu.

Je pars du principe que le lecteur ne connaît pas vraiment Coq. Mais en même temps j’aimerai bien capitaliser sur mon autre article, pour ne pas tout réexpliquer avec autant de détails et me focaliser sur l’idée de "programme prouvé" (alors que mon précédent article est plus sur la partie mathématique seule).

Ce que j’ai en tête, c’est de faire une présentation de comment ça marche, sans enseigner comment faire en détail. Faire une démonstration des grands principes.

Je pense qu’il manque quelques détails, par exemple tu dis :

Il existe une tactique permettant de prouver n’importe quelle égalité sur un anneau, ce qui conclut la preuve : ring..

Mais ce ring. n’apparait pas dans le texte, il faut aller le chercher dans le code complet pour le trouver.

Je vois ce que tu veux dire. Dans mon article précédent, ce que répondait Coq était plus simple, donc j’avais choisi de le mentionner dans les commentaires de la preuve. Ici, j’ai eu envie de montrer l’évolution du "reste à démontrer" que Coq nous donne après chaque tactique.

Je vais tenter de montrer l’échange interactif mieux dans la prochaine version, avec un genre de présentation console/réponse. C’est vraiment comme le top-level Python ou Ocaml quand on utilise Coq en console.

Effectivement, ça sort du cadre, parce que je ne souhaite pas parler d’analyse syntaxique.

Dans notre cas, un programme c’est simplement une liste (au sens de Coq) d’instructions (telles que définies par un type inductif), avec tout ce que ça signifie sur le typage. C’est impossible d’écrire un programme invalide parce qu’il serait mal typé. Coq dira par exemple que -5 est un entier relatif alors que l’argument de Add doit être un entier naturel.

Si on avait une syntaxe qu’un analyseur devait traiter, il détecterait ce genre d’erreurs ; on n’arriverait pas à fabriquer une représentation valide du programme en rencontrant ça et donc on devrait lever une erreur à un moment donné.

Sinon, j’ai réglé le problème de lien.

Bonjour les agrumes !

La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :

Merci d’avance pour vos commentaires.

J’ai essayé d’améliorer la dernière partie @SpaceFox.

J’ai inclus aussi quelques autres corrections mineures au fil du texte (dont une légère simplification du code, mais elle passe presque inaperçu).

Quelques commentaires au fil de l’eau.

Une fois le comportement définit, la compilation du langage source vers le langage cible devrait être faite correctement en procédant ainsi : <description informelle du compilateur naif>

Je trouve cette phrase peu claire, car elle donne l’impression que c’est le seul choix de compilation possible. En particulier, un lecteur inattentif pourrait prouver la correction du compilateur, c’est prouver cela (que Add n génère n instructions Incr, etc.).

Je pense qu’il y aurait deux manières d’éviter cette confusion, qui amélioreraient toutes les deux le tutoriel:

1. Ne pas mélanger le paragraphe où tu parles du compilateur (ici) et celui où tu parles de la spécification du compilateur (avec la remarque sur le fait que la définition n’est pas assez fine, tout ça); parler de la spécification avant de faire la preuve mais pas trop tôt.
2. Clarifier le fait qu’il existe plusieurs choix de traduction possible, et que tu fais ici le choix le plus naïf. Il suffit peut-être de préciser qu’on pourrait imaginer un compilateur optimisant qui pour [Add 2; Sub 3] renvoie directement [Decr].

Example compile_ex: 
  compile [Add 2; Sub 3] = [Incr; Incr; Decr; Decr; Decr].
(* Démarrage de la preuve *)
Proof.

Je ne trouve pas très clair de mélanger la notion de test et la notion de preuve. Certes, on peut voir un test comme un énoncé formel avec une preuve triviale, c’est intéressant mais un débutant peut s’y perdre. Pourquoi ne pas montrer une ligne du style Compute et montrer la forme normale affichée par Coq ?

Signification des programmes

Pourquoi ne pas utiliser le terme habituel, "sémantique" ? Il me semble utile d’utiliser le terme des gens du domaine, pour qu’une personne qui a lu ton introduction s’y retrouve ensuute dans des documents plus avancés.

exec_instr_s a (exec_s prog)

J’ai l’impression qu’il y a une incohérence, au-dessus tu définis exec_instr : counter -> counter, et là tu prends deux arguments.

Il faut faire un choix entre donner une sémantique où chaque instruction renvoie un nombre, et les nombres du programme sont additionnés, et une sémantique où chaque instruction transforme un nombre, et le programme est une composition de tous ces transformateurs d’état. Je n’ai pas de préférence forte.

P.S.: Ce n’est pas normal que tu doives utiliser la commutatitivé dans ta preuve, il doit y avoir une définition à l’envers.

  destruct i ; induction n ;
  trivial ; simpl in IHn ;  unfold compile_instr ; simpl repeat ;
  unfold exec_t ; fold exec_t ;  rewrite <- IHn ; unfold exec_instr_s ;
  unfold exec_instr_t ; rewrite Nat2Z.inj_succ ; ring.

caca.

Je pense qu’il y aurait deux manières d’éviter cette confusion, qui amélioreraient toutes les deux le tutoriel: 1. Ne pas mélanger le paragraphe où tu parles du compilateur (ici) et celui où tu parles de la spécification du compilateur (avec la remarque sur le fait que la définition n’est pas assez fine, tout ça); parler de la spécification avant de faire la preuve mais pas trop tôt. 2. Clarifier le fait qu’il existe plusieurs choix de traduction possible, et que tu fais ici le choix le plus naïf. Il suffit peut-être de préciser qu’on pourrait imaginer un compilateur optimisant qui pour [Add 2; Sub 3] renvoie directement [Decr].

Oui, c’est une bonne idée, je vais tenter quelque chose dans cette direction.

Je ne trouve pas très clair de mélanger la notion de test et la notion de preuve. Certes, on peut voir un test comme un énoncé formel avec une preuve triviale, c’est intéressant mais un débutant peut s’y perdre. Pourquoi ne pas montrer une ligne du style Compute et montrer la forme normale affichée par Coq ?

Je vais faire ça aussi, ça sera plus simple pour les débutants en effet.

Signification des programmes

Pourquoi ne pas utiliser le terme habituel, "sémantique" ? Il me semble utile d’utiliser le terme des gens du domaine, pour qu’une personne qui a lu ton introduction s’y retrouve ensuute dans des documents plus avancés.

C’est un choix que j’ai fait, parce que le mot "signification" est en général compris de tous, ce qui n’est pas le cas du mot "sémantique" qui est plus exotique. Je rajouterai une note pour mentionner le mot de jargon, mais je préfère ne pas utiliser le mot tout du long.

exec_instr_s a (exec_s prog)

J’ai l’impression qu’il y a une incohérence, au-dessus tu définis exec_instr : counter -> counter, et là tu prends deux arguments.

Oui, il faudra que je corrige les incohérences restantes. J’étais parti sur de la composition d’états, mais j’ai préféré finalement les additions.

P.S.: Ce n’est pas normal que tu doives utiliser la commutatitivé dans ta preuve, il doit y avoir une définition à l’envers.

Effectivement, il y avait une définition à l’envers, la réflexivité suffit. Ce sera corrigé.

On est d’accord. Je reste un bon gros novice avec Coq, donc si tu as un bon conseil pour faire ça propre, je prends.

Bonjour les agrumes !

La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :

Merci d’avance pour vos commentaires.

J’ai fait toutes les modifications mentionnées dans le message précédent. Sauf l’amélioration de la preuve crado évidemment.

J’ai essayé de trouver une preuve plus factorisée, mais ce n’est pas évident. (Le problème est que la partie commune aux deux cas est le traitement du paramètre n, mais il est caché à l’intérieur du constructeur. Si c’était une vraie preuve on changerait nos définitions pour utiliser (Add, n) à la place de Add n, et ce serait plus facile, mais ici j’ai choisi de travailler à définition fixée.)

Ma meilleure proposition pour l’instant:

Lemma Add_S:
  forall n, exec_instr_s (Add (S n)) = 1 + exec_instr_s (Add n).
Proof.
  intros n.
  simpl exec_instr_s.
  rewrite Zpos_P_of_succ_nat.
  omega.
Qed.

Lemma Sub_S:
  forall n, exec_instr_s (Sub (S n)) = -1 + exec_instr_s (Sub n).
Proof.
  intros n.
  simpl exec_instr_s.
  rewrite <- Pos2Z.opp_pos.
  rewrite Zpos_P_of_succ_nat.
  omega.
Qed.

Lemma compile_Add_S:
  forall n, compile_instr (Add (S n)) = [Incr] ++ compile_instr (Add n).
Proof. trivial. Qed.

Lemma compile_Sub_S:
  forall n, compile_instr (Sub (S n)) = [Decr] ++ compile_instr (Sub n).
Proof. trivial. Qed.

Hint Rewrite exec_t_app Add_S Sub_S compile_Add_S compile_Sub_S : zds.

Lemma compile_instr_correct:
  forall (i:instr_s), exec_instr_s i = exec_t (compile_instr i).
Proof.
  destruct i ; (induction n ; [ trivial | autorewrite with zds; rewrite <- IHn; trivial ]).
Qed.

(Je travaille avec jscoq parce que la flemme, et il n’arrive pas à utiliser la tactique ring donc j’ai dû faire un peu plus fin sur les calculs dans Z.)

OK, merci beaucoup pour la démonstration.

Je vais garder ce que j’ai actuellement pour rester court, mais je vais ajouter une note comme quoi c’est un peu brouillon.

Bonjour,

La bêta du contenu « Écrire des programmes prouvés corrects avec Coq » a été désactivée.