Rocq

El demostrador Rocq (anteriormente llamado Coq ) es un demostrador de teoremas interactivo lanzado por primera vez en 1989. Permite la expresión de afirmaciones matemáticas, la verificación mecánica de las pruebas de estas afirmaciones, ayuda a encontrar pruebas formales mediante rutinas de automatización de pruebas y la extracción de un programa certificado a partir de la prueba constructiva de su especificación formal .

Rocq se basa en la teoría del cálculo de construcciones inductivas, una derivación del cálculo de construcciones . Rocq no es un demostrador automático de teoremas , pero incluye tácticas ( procedimientos ) de demostración automática de teoremas y diversos procedimientos de decisión .

La Association for Computing Machinery otorgó a Thierry Coquand , Gérard Huet , Christine Paulin-Mohring , Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot y Pierre Castéran el premio ACM Software System Award 2013 por Rocq (cuando se llamaba Coq).

Considerado como un lenguaje de programación , Rocq implementa un modelo de programación funcional con tipos dependientes ; ^{[ 2 ]} considerado como un sistema lógico, implementa una teoría de tipos de orden superior . El desarrollo de Rocq ha sido apoyado desde 1984 por el Instituto Francés de Investigación en Ciencias de la Computación y Automatización (INRIA), en colaboración con muchas otras instituciones de investigación francesas e internacionales. El desarrollo de Rocq fue iniciado por Gérard Huet y Thierry Coquand, y más de 200 personas, ^{[ 3 ]} principalmente investigadores, han contribuido con funcionalidades al sistema central desde su creación. El equipo de implementación ha sido coordinado sucesivamente por Gérard Huet, Christine Paulin-Mohring, Hugo Herbelin y Matthieu Sozeau. Rocq está implementado principalmente en OCaml con algo de C. El sistema central puede extenderse mediante un mecanismo de complementos . ^{[ 4 ]}

Rocq proporciona un lenguaje de especificación llamado Gallina. ^{[ 5 ]} Los programas escritos en Gallina tienen la propiedad de normalización débil , lo que implica que siempre terminan. Esta es una propiedad distintiva del lenguaje, ya que los bucles infinitos (programas que no terminan) son comunes en otros lenguajes de programación. ^{[ 6 ]}

Como ejemplo de una demostración escrita en Rocq, consideremos la demostración de un lema que establece que tomar el sucesor de un número natural invierte su paridad. La táctica de plegado-desplegado introducida por Danvy ^{[ 7 ]} se utiliza para simplificar la demostración.

Desde Stdlib Require Importar Arith Nat Bool .Fixpoint is_even ( n : nat ) : bool := match n with | 0 => true | S n' => negb ( is_even n' ) end .Lema is_even_0 : is_even 0 = verdadero . Prueba . reflexividad . Qed .Lema is_even_S n : is_even ( S n ) = negb ( is_even n ). Demostración . reflexividad . Qed .Lema successor_flips_evenness n : is_even n = negb ( is_even ( S n )). Prueba . reescribe is_even_S . destruct ( is_even n ). * simpl . reflexividad . * simpl . reflexividad . Qed .

Esta demostración primero importa la definición de booleanos y números naturales de la biblioteca estándar, y luego define una is_evenfunción que devuelve si un número es par. A continuación, se demuestran tres lemas sobre esta función. El primero simplemente reitera las ecuaciones que la definen is_even, y como Rocq conoce dichas ecuaciones, su demostración es muy breve. El último lema se demuestra con una distinción de casos tras aplicar primero el segundo lema; el asterisco *indica que comienza un nuevo subcaso.

• CompCert : un compilador optimizador para casi todo el lenguaje de programación C , programado y probado en gran medida en Rocq.
• Estructura de datos de conjuntos disjuntos : la prueba de corrección en Rocq se publicó en 2007. ^{[ 11 ]}
• Teorema de Feit-Thompson : la demostración formal utilizando Rocq se completó en septiembre de 2012. ^{[ 12 ]}
• Busy beaver : El valor del busy beaver ganador de 5 estados fue descubierto por Heiner Marxen y Jürgen Buntrock en 1989, pero solo se demostró que era el quinto busy beaver ganador —estilizado como BB(5) — en 2024 usando una demostración en Rocq. ^{[ 13 ] [ 14 ]}

Además de construir explícitamente términos de Gallina, Rocq admite el uso de tácticas escritas en el lenguaje integrado Ltac o en OCaml. Estas tácticas automatizan la construcción de pruebas, llevando a cabo pasos triviales u obvios en las mismas. ^{[ 15 ]} Varias tácticas implementan procedimientos de decisión para diversas teorías. Por ejemplo, la táctica "ring" decide la teoría de la igualdad módulo axiomas de anillo o semianillo mediante reescritura asociativa - conmutativa . ^{[ 16 ]} Por ejemplo, la siguiente prueba establece una igualdad compleja en el anillo de enteros en una sola línea de prueba: ^{[ 17 ]}

Require Import ZArith . Open Scope Z_scope . Goal forall a b c : Z , ( a + b + c ) ^ 2 = a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c . intros ; ring . Qed .

También se encuentran disponibles procedimientos de decisión integrados para la teoría vacía ("congruencia"), la lógica proposicional ("tauto"), la aritmética lineal entera sin cuantificadores ("lia") y la aritmética lineal racional/real ("lra"). ^{[ 18 ] [ 19 ]} Se han desarrollado otros procedimientos de decisión como bibliotecas, incluyendo una para álgebras de Kleene ^{[ 20 ]} y otra para ciertos objetivos geométricos . ^{[ 21 ]}

El antiguo nombre Coq significa ' gallo ' en francés y es un juego de palabras con el nombre de Thierry Coquand, cálculo de construcciones o CoC , y proviene de una tradición francesa de nombrar las herramientas de desarrollo de investigación en honor a animales. ^{[ 22 ]} Hasta 1991, Coquand estaba implementando un lenguaje llamado cálculo de construcciones y entonces simplemente se llamaba CoC . En 1991, se inició una nueva implementación basada en el cálculo extendido de construcciones inductivas y el nombre cambió de CoC a Coq en una referencia indirecta a Coquand, quien desarrolló el cálculo de construcciones junto con Gérard Huet y contribuyó al cálculo de construcciones inductivas con Christine Paulin-Mohring. ^{[ 23 ]} El 11 de octubre de 2023, el equipo de desarrollo anunció que Coq pasaría a llamarse The Rocq Prover en los meses siguientes y comenzó a actualizar la base de código, el sitio web y las herramientas relacionadas. ^{[ 24 ]} El cambio de nombre oficial se produjo con el lanzamiento de Rocq 9.0 en marzo de 2025. ^{[ 25 ]} El nuevo nombre hace referencia a Inria Rocquencourt , donde se desarrolló el sistema por primera vez, y está relacionado con el ave mítica Roc , lo que permite mantener las referencias a las aves del nombre anterior. ^{[ 26 ]}

• Premio de Ciencia Abierta 2022 para software de investigación de código abierto en la categoría "Científico y Técnico" ^{[ 27 ]}

• Cálculo de construcciones
• Correspondencia entre Curry y Howard
• Teoría de tipos intuicionista
• Lista de asistentes de prueba

• Sitio web oficial