Gallo (software)

Polla

Descripción de esta imagen, también comentada a continuación

CoqIDE : el entorno de desarrollo de Coq . Información

Desarrollado por	INRIA , Universidad Diderot de París , la Escuela Politécnica , Universidad de París-Sur , Escuela Normal Superior de Lyon
Primera versión	1984
Última versión	8.13.1 (22 de febrero de 2021)
Depositar	Gallo en GitHub
Estado del proyecto	En desarrollo activo
Escrito en	OCaml
Sistema de explotación	Multiplataforma
Medio ambiente	Multiplataforma
Idiomas	inglés
Tipo	Asistente de pruebas
Política de distribución	Libre y de código abierto
Licencia	GNU LGPL 2.1
Sitio web	http://coq.inria.fr

Coq es un asistente de pruebas en el lenguaje Gallina , desarrollado por el equipo PI.R2 de Inria dentro del laboratorio PPS del CNRS y en colaboración con la École polytechnique , el CNAM , la Université Paris Diderot y la Universidad Paris-Sud (y anteriormente la École normale supérieure de Lyon ).

El nombre del software (inicialmente CoC ) es particularmente apropiado porque: es francés; se basa en el cálculo de construcciones ( CoC abreviado en inglés) introducido por Thierry Coquand . En la misma línea, su idioma es Gallina y Coq tiene un wiki dedicado, llamado Cocorico! .

Coq recibió el premio ACM SIGPLAN Programming Languages Software 2013.

Historia del proyecto

A principios de la década de 1980, Gérard Huet inició un proyecto para fabricar un demostrador interactivo de teoremas. Este es un asistente de pruebas. Thierry Coquand y Gérard Huet conciben la lógica de Coq y el cálculo de construcciones. Christine Paulin-Mohring amplía esta lógica con una nueva construcción, tipos inductivos y un mecanismo de extracción que obtiene automáticamente un programa de cero fallas a partir de una prueba.

Funciones de software

Rooster se basa en el diseño de estructuras , una teoría de tipos de orden superior , y su lenguaje de especificación es una forma de cálculo lambda mecanografiado. El cálculo de construcciones utilizado en Coq incluye directamente construcciones inductivas, de ahí su nombre de cálculo de construcciones inductivas (CIC).

Recientemente, a Coq se le ha dado una funcionalidad de automatización creciente. Citemos en particular la táctica Omega que decide la aritmética de Presburger .

Más específicamente, Coq permite:

manipular afirmaciones del cálculo;
verificar mecánicamente las pruebas de estas afirmaciones;
ayudar en la búsqueda de pruebas formales;
sintetizar programas certificados a partir de evidencia constructiva de sus especificaciones.

Es un software gratuito distribuido bajo los términos de la licencia GNU LGPL .

Entre los grandes éxitos de Coq, podemos mencionar:

Teorema de los cuatro colores: la demostración totalmente mecanizada fue completada en 2004 por Georges Gonthier y Benjamin Werner ;
Teorema de Feit-Thompson La demostración del teorema fue completada por Georges Gonthier y su equipo en septiembre de 2012;
CompCert , un compilador optimizador para el lenguaje C que está ampliamente programado y probado en Coq.

Elementos del lenguaje

Rooster usa la correspondencia Curry-Howard . La prueba de una proposición se ve como un programa cuyo tipo es esta proposición. Para definir un programa o una prueba, debe:

O escríbalo en el lenguaje Gallina, cercano al lenguaje de programación funcional OCaml .
O declare su tipo (o la proposición que queremos demostrar). El lenguaje Ltac luego hace posible definir esta prueba / programa mediante el encadenamiento hacia atrás , de forma interactiva. Se prefiere este método para pruebas matemáticas porque Coq puede adivinar ciertos pasos intermedios.

También es posible utilizar SSReflect en lugar de Ltac. Anteriormente desarrollado por separado, ahora se incluye de forma predeterminada en Coq.

Ejemplos de programas

La función factorial (con Gallina):

Require Import Arith List Bool. Fixpoint factorielle (x : nat) : nat := match x with 0 => 1 | S p => x * factorielle( p ) end.

La función factorial (con Ltac):

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

Ejemplo de demostración (con Ltac)

Cualquier número natural es par o impar.

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

Notas y referencias

" Versión 8.13.1 " ,22 de febrero de 2021(consultado el 10 de marzo de 2021 )
binario , " Christine Paulin y Zero Defect Software " , en binario ,24 de septiembre de 2015(consultado el 18 de marzo de 2020 )
La aritmética de Presburger, a diferencia de la aritmética habitual debida a Peano , es una teoría completa, es decir, para cualquier enunciado de su lenguaje se puede decidir si es un teorema de teoría o no (su negación es entonces un teorema). Esta aritmética de Presburger, que no tiene axioma para la multiplicación, por lo tanto, escapa a la incompletitud establecida por el teorema de la incompletitud .
(in) " El teorema de Feit-Thompson ha sido totalmente verificado en Coq " , Msr-inria.inria.fr,20 de septiembre de 2012(consultado el 25 de septiembre de 2012 ) .

Ver también

enlaces externos

(fr) El sitio del proyecto Coq
(es) Haan Wiki
( fr ) Informe del equipo de proyecto PI.R2 que desarrolla Coq
(es) Libro sobre gallo de Yves Bertot y Pierre Castéran