El nombre "Coq" es un juego de palabras con el nombre de Thierry Coquand, Cálculo de construcciones o "CoC" y sigue la tradición informática francesa de nombrar software con nombres de animales ( coq en francés significa gallo). [2] El 11 de octubre de 2023, el equipo de desarrollo anunció que Coq pasará a llamarse "The Rocq Prover" en los próximos meses y ha comenzado a actualizar el código base, el sitio web y las herramientas asociadas. [3]
Descripción general
Cuando se ve como un lenguaje de programación, Coq implementa un lenguaje de programación funcional escrito de forma dependiente ; [4] cuando se ve como un sistema lógico, implementa una teoría de tipos de orden superior . El desarrollo de Coq ha contado con el apoyo desde 1984 de INRIA , ahora en colaboración con la École Polytechnique , la Universidad Paris-Sud , la Universidad Paris Diderot y el CNRS . En los años 1990, la ENS Lyon también formó parte del proyecto. El desarrollo de Coq fue iniciado por Gérard Huet y Thierry Coquand, y más de 40 personas, principalmente investigadores, han contribuido con funciones al sistema central desde su inicio. El equipo de implementación ha sido coordinado sucesivamente por Gérard Huet, Christine Paulin-Mohring, Hugo Herbelin y Matthieu Sozeau. Coq se implementa principalmente en OCaml con un poco de C. El sistema central se puede ampliar mediante un mecanismo enchufable . [5]
El nombre coq significa " gallo " en francés y proviene de una tradición francesa de nombrar las herramientas de desarrollo de investigación con nombres de animales. [6] Hasta 1991, Coquand estaba implementando un lenguaje llamado Cálculo de Construcciones y en ese momento simplemente se llamaba CoC. En 1991, se inició una nueva implementación basada en el Cálculo de Construcciones Inductivas extendido y se cambió el nombre 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. [7]
Coq proporciona un lenguaje de especificación llamado Gallina [8] (" gallina " en latín, español, italiano y catalán). 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 sin terminación) son comunes en otros lenguajes de programación, [9]
y es una forma de evitar el problema de la detención .
plus_comm = fun n m : nat => nat_ind ( fun n0 : nat => n0 + m = m + n0 ) ( plus_n_0 m ) ( fun ( y : nat ) ( H : y + m = m + y ) => eq_ind ( S ( m + y )) ( fun n0 : nat => S ( y + m ) = n0 ) ( f_equal S H ) ( m + S y ) ( plus_n_Sm m y )) n : forall n m : nat , n + metro = metro + norte
nat_indrepresenta la inducción matemática , eq_indla sustitución de iguales y f_equalla toma de la misma función en ambos lados de la igualdad. Se hace referencia a teoremas anteriores que muestran y .
Usos notables
Teorema de los cuatro colores y extensión SSReflect
Georges Gonthier de Microsoft Research en Cambridge , Inglaterra y Benjamin Werner de INRIA utilizaron Coq para crear una prueba encuestable del teorema de los cuatro colores , que se completó en 2002. [10] Su trabajo condujo al desarrollo del SSReflect ("Reflexión a pequeña escala"). "), que fue una extensión significativa de Coq. [11] A pesar de su nombre, la mayoría de las características agregadas a Coq por SSReflect son características de propósito general y no se limitan al estilo de prueba de reflexión computacional. Estas características incluyen:
Argumentos implícitos para funciones aplicadas a argumentos cero, lo cual es útil al programar con funciones de orden superior
Argumentos anónimos concisos
Una táctica mejorada setcon combinaciones más poderosas.
Apoyo a la reflexión
SSReflect 1.11 está disponible gratuitamente, tiene doble licencia bajo la licencia de código abierto CeCILL-B o CeCILL-2.0 y es compatible con Coq 8.11. [12]
Otras aplicaciones
CompCert : un compilador optimizador para casi todo el lenguaje de programación C que en gran medida está programado y ha demostrado ser correcto en Coq.
Teorema de Feit-Thompson : la prueba formal utilizando Coq se completó en septiembre de 2012. [14]
Castor ocupado : El valor del castor ocupado ganador de 5 estados fue descubierto por Heiner Marxen y Jürgen Buntrock en 1989, pero solo resultó ser el quinto castor ocupado ganador, estilizado como BB(5) , en 2024 usando una prueba en Coq. [15] [16]
lenguaje táctico
Además de construir términos de Gallina explícitamente, Coq 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 pruebas. [17] Varias tácticas implementan procedimientos de decisión para diversas teorías. Por ejemplo, la táctica del "anillo" decide la teoría de la igualdad de los axiomas de módulo de anillo o semianillo mediante reescritura asociativa - conmutativa . [18] Por ejemplo, la siguiente prueba establece una igualdad compleja en el anillo de números enteros en una sola línea de prueba: [19]
Requerir importar ZARith . Abra el ámbito Z_scope . Objetivo para todos a b c : Z , ( a + b + c ) ^ 2 = a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c . introducciones ; anillo . Qed .
Los procedimientos de decisión incorporados también están disponibles para la teoría vacía ("congruencia"), la lógica proposicional ("tauto"), la aritmética lineal de enteros sin cuantificadores ("lia") y la aritmética lineal racional/real ("lra"). [20] [21] Se han desarrollado otros procedimientos de decisión como bibliotecas, incluida una para álgebras de Kleene [22] y otra para ciertos objetivos geométricos . [23]
^ Avigad, Jeremy; Mahboubi, Assia (3 de julio de 2018). Demostración interactiva de teoremas: Novena Conferencia Internacional, ITP 2018, celebrada como... Springer. ISBN9783319948218. Consultado el 21 de octubre de 2018 .
^ "Preguntas frecuentes". GitHub . Consultado el 8 de mayo de 2019 .
↑ «Introducción al Cálculo de Construcciones Inductivas» . Consultado el 21 de mayo de 2019 .
^
Adán Chlipala. "Programación certificada con tipos dependientes": "Universos de biblioteca".
^
Adán Chlipala. "Programación certificada con tipos dependientes": "Biblioteca GeneralRec". "Biblioteca de tipos inductivos".
^ Gonthier, Georges; Mahboubi, Assia (2010). "Una introducción a la reflexión a pequeña escala en Coq". Revista de razonamiento formalizado . 3 (2): 95-152. doi :10.6092/ISSN.1972-5787/1979.
^ "La biblioteca de componentes matemáticos 1.11.0". GitHub .
^ Conchón, Sylvain; Filliâtre, Jean-Christophe (2007). "Una estructura de datos persistente para encontrar sindicatos". En Russo, Claudio V.; Dreyer, Derek (eds.). Actas del taller ACM sobre ML, 2007, Friburgo, Alemania, 5 de octubre de 2007. Asociación de Maquinaria de Computación. págs. 37–46. doi :10.1145/1292535.1292541.
^ "El teorema de Feit-Thompson ha sido totalmente comprobado en Coq". msr-inria.inria.fr. 2012-09-20. Archivado desde el original el 19 de noviembre de 2016 . Consultado el 25 de septiembre de 2012 .
^ "[2 de julio de 2024] Hemos demostrado" BB(5) = 47.176.870"". El desafío del castor ocupado . 2024-07-02 . Consultado el 2 de julio de 2024 .
^ "El desafío del castor ocupado". bbchallenge.org . Consultado el 2 de julio de 2024 .
^ Kaiser, Jan-Oliver; Ziliani, Beta; Krebbers, Robbert; Régis-Gianas, Yann; Dreyer, Derek (30 de julio de 2018). "Mtac2: tácticas escritas para el razonamiento hacia atrás en Coq". Actas de la ACM sobre lenguajes de programación . 2 (CIFP): 78:1–78:31. doi : 10.1145/3236773 . hdl : 21.11116/0000-0003-2E8E-B .
^ Grégoire, Benjamín; Mahboubi, Assia (2005). "Demostración de igualdades en un anillo conmutativo hecho correctamente en Coq". En Hurd, Joe; Melham, Tom (eds.). Demostración de teoremas en lógica de orden superior: 18ª Conferencia Internacional, TPHOLs 2005, Oxford, Reino Unido, 22 al 25 de agosto de 2005, Actas. Apuntes de conferencias sobre informática. Berlín, Heidelberg: Springer. págs. 98-113. doi :10.1007/11541868_7. ISBN978-3-540-31820-0.
^ "Las familias de tácticas de anillo y campo: documentación de Coq 8.11.1". coq.inria.fr . Consultado el 4 de diciembre de 2023 .
^ Besson, Federico (2007). "Tácticas aritméticas reflexivas rápidas en el caso lineal y más allá". En Altenkirch, Thorsten; McBride, Conor (eds.). Tipos de pruebas y programas: taller internacional, TIPOS 2006, Nottingham, Reino Unido, 18 al 21 de abril de 2006, artículos seleccionados revisados . Apuntes de conferencias sobre informática. vol. 4502. Berlín, Heidelberg: Springer. págs. 48–62. doi :10.1007/978-3-540-74464-1_4. ISBN978-3-540-74464-1.
^ "Micromega: solucionadores de objetivos aritméticos sobre anillos ordenados - documentación de Coq 8.18.0". coq.inria.fr . Consultado el 4 de diciembre de 2023 .
^ Braibant, Thomas; Pous, Damián (2010). Kaufmann, Matt; Paulson, Lawrence C. (eds.). Una táctica Coq eficaz para decidir las álgebras de Kleene. Demostración interactiva de teoremas: Primera conferencia internacional, ITP 2010 Edimburgo, Reino Unido, 11 al 14 de julio de 2010, Actas. Apuntes de conferencias sobre informática. Berlín, Heidelberg: Springer. págs. 163-178. doi :10.1007/978-3-642-14052-5_13. ISBN978-3-642-14052-5. S2CID 3566183.
^ Narboux, Julien (2004). "Un procedimiento de decisión para la geometría en Coq". En Slind, Konrad; Búnker, Annette; Gopalakrishnan, Ganesh (eds.). Demostración de teoremas en lógica de orden superior: 17ª Conferencia Internacional, TPHOLS 2004, Park City, Utah, EE. UU., 14 al 17 de septiembre de 2004, Actas . Apuntes de conferencias sobre informática. vol. 3223. Berlín, Heidelberg: Springer. págs. 225–240. doi :10.1007/978-3-540-30142-4_17. ISBN978-3-540-30142-4. S2CID 11238876.
enlaces externos
Wikimedia Commons tiene medios relacionados con Coq (lenguaje de programación) .
Sistema interactivo en línea JsCoq: permite que Coq se ejecute en un navegador web, sin necesidad de instalar software adicional
Alectryon: una biblioteca para procesar fragmentos de Coq incrustados en documentos, que muestra objetivos y mensajes para cada oración de Coq.
Wiki Coq
Biblioteca de componentes matemáticos: biblioteca de estructuras matemáticas ampliamente utilizada, parte de la cual es el lenguaje de prueba SSReflect.