Rocq (logiciel) 📖 Wikipedia

Au début des années 1980, Gérard Huet lance un projet de fabrication d’un démonstrateur interactif de théorème. Il s'agit d'un assistant de preuve. Thierry Coquand et Gérard Huet conçoivent la logique de Rocq (appelé Coq à l'époque) et le calcul des constructions. Christine Paulin-Mohring étend cette logique avec une nouvelle construction, les types inductifs et un mécanisme d’extraction qui permet d’obtenir automatiquement un programme zéro défaut à partir d’une preuve^[5].

L'ancien nom Coq fait à la fois référence au calcul des constructions (CoC abrégé en anglais) développé par Thierry Coquand, au nom de famille Coquand lui-même et au fait qu'il est français (coq gaulois) :

« The name Coq comes from the French word for rooster, CoC (the Calculus of Constructions) and Thierry Coquand, one of the initial authors of Coq. But it is also close to the word "cock" which has a slang meaning that some English speakers consider offensive (it also means a male bird or the firing lever in a gun). This similarity has already led to some women turning away from Coq and others getting harassed when they said they were working on Coq. It also makes some English conversations about Coq with lay persons simply more difficult^[6]. » (« Mais il est également proche du mot « cock », dont le sens argotique est jugé offensant par certains anglophones (il désigne aussi un oiseau mâle ou le levier de tir d'un fusil). Cette similitude a déjà conduit certaines femmes à se détourner de Coq, et d'autres à être harcelées lorsqu'elles disaient travailler sur Coq. Cela rend également plus difficiles certaines conversations en anglais sur Coq avec des profanes. »)

Un certain nombre de nouveaux noms ont donc été proposés. Rocq a été retenu, notamment car c'est un diminutif de Rocquencourt qui accueillait un site de l'INRIA où Thierry Coquand a commencé à développer Rocq et qu'il reste proche du nom Coq^[6].

Rocq est fondé sur le calcul des constructions, une théorie des types d'ordre supérieur, et son langage de spécification est une forme de lambda-calcul typé. Le calcul des constructions utilisé dans Rocq comprend directement les constructions inductives, d'où son nom de calcul des constructions inductives (CIC).

Rocq a été récemment doté de fonctionnalités d'automatisation croissantes. Citons notamment la tactique lia qui décide l'arithmétique de Presburger^[7], les tactiques field et ring pour manipuler des expressions polynomiales et rationnelles.

Plus particulièrement, Rocq permet :

• de manipuler des assertions du calcul ;
• de vérifier mécaniquement des preuves de ces assertions ;
• d'aider à la recherche de preuves formelles ;
• de synthétiser des programmes certifiés à partir de preuves constructives de leurs spécifications.

C'est un logiciel libre distribué selon les termes de la licence GNU LGPL.

Parmi les grands succès de Rocq, on peut citer :

• le théorème des quatre couleurs, dont une démonstration complètement mécanisée a été terminée en 2004 par Georges Gonthier et Benjamin Werner ;
• le théorème de Feit-Thompson, dont une preuve a été terminée par Georges Gonthier et son équipe en septembre 2012^[8] après six ans d'efforts^[9] ;
• CompCert, un compilateur optimisant pour le langage C qui est en grande partie programmé et prouvé en Rocq ;
• la démonstration inédite, par une équipe réunie autour de Tristan Stérin, que le castor affairé à 5 états s'exécute en 47 176 870 étapes^[10].

Rocq utilise la correspondance de Curry-Howard. La preuve d'une proposition est vue comme un programme dont le type est cette proposition. Pour définir un programme ou une preuve, il faut :

• soit l'écrire dans le langage Gallina, proche du langage de programmation fonctionnelle OCaml ;
• soit déclarer son type (ou la proposition que l'on veut démontrer). Le langage Ltac permet alors de définir cette preuve/programme par chaînage arrière, de façon interactive. Cette méthode est privilégiée pour les preuves mathématiques car Rocq est alors capable de deviner certaines étapes intermédiaires. Des procédures entièrement automatiques existent pour certains fragments de logique ou d'arithmétique.

Diverses fonctionnalités permettent par ailleurs de définir un programme en Gallina en y laissant des trous correspondant à des preuves à fournir, et ensuite compléter ces trous à l'aide de l'assistant de preuve interactif.

Il est aussi possible d'utiliser SSReflect à la place de Ltac. Autrefois développé séparément, il est maintenant inclus par défaut dans Rocq.

• La fonction factorielle (avec Gallina) :

Require Import Nat.

Fixpoint factorielle n :=
  match n with
  | 0 => 1
  | S p => n * factorielle p
  end.

• La fonction factorielle (avec Ltac) :

Require Import Nat.

Definition factorielle (n : nat) : nat.
  (* On fait une définition par récurrence *)
  induction n.
  - (* Si l'argument est 0, on retourne 1 *)
    exact 1.
  - (* Si l'argument de la forme (S n), on retourne un produit *)
    apply Nat.mul.
    + (* 1er facteur du produit : le successeur de n *)
      exact (S n).
    + (* 2nd facteur du produit : valeur de factorielle en n *)
      exact IHn.
  (* On indique que la définition est terminée et que l'on souhaite pouvoir calculer cette fonction. *)
Defined.

• Tout entier naturel est soit pair, soit impair, par récurrence, avec la tactique lia.

Require Import Lia.

Lemma odd_or_ind : forall (n : nat),
    (exists (p : nat), n = 2 * p) \/ (exists (p : nat), n = 1 + 2 * p).
Proof.
  intro n.
  induction n.
  - (* Cas 0 *) left. now exists 0.
  - (* Cas (n + 1) *)
    destruct IHn as [[p Hpair] | [p Himpair]].
    + (* n est pair *)
      right. exists p. auto.
    + (* n est impair *)
      left. exists (S p). lia.
  (* On indique que la preuve est terminée et qu'elle ne sera pas utilisée comme un programme. *)
Qed.

• Démonstration automatique de théorèmes
• Lean, un assistant de preuve basé sur une théorie des types très voisine de celle de Rocq
• Isabelle
• Mizar
• PhoX
• PVS

• (en) Site officiel 
• (en) Compte-rendu de l'équipe-projet PI.R2 qui développe Rocq
• (fr) Livre sur Rocq de Yves Bertot et Pierre Castéran

•   Portail de la programmation informatique
•   Portail des logiciels libres
•   Portail des mathématiques
•   Portail de la logique