Es difícil explicar para que sirve Coq desde cero. Se trata de un asistente de prueba, es decir, de un programa que nos ayuda a llevar a cabo pruebas matemáticas y que nos da la seguridad de que lo que hemos probado sea cierto. Coq tiene distintas aplicaciones:
- formalizar pruebas ya existentes para comprobar con seguridad que son ciertas,
- ayuda a demostrar nuevos teoremas,
- extraer programas correctos por construcción,
- probar que determinado programa, lenguaje, función, o sistema de tipos preserva una invariante,
- (semi)automatizar todas estas tareas.
Todo esto suena bastante abstracto, y la verdad es que los métodos formales son un área de alto contenido matemático. Pero no por esto son inútiles. En la práctica, hay muchísimos programas con errores que tienen un coste tremendo, desde fallos de seguridad, hasta errores de cálculo. En general, las metodologías de desarrollo intentan evitar estos problemas siguiendo una serie de técnicas como el uso de tests. Pero estas técnicas no pueden asegurar que el programa sea correcto; sólo que no tenga fallos conocidos.
Mediiante los métodos formales podemos asegurarnos de que un programa cumpla con determinadas propiedades matemáticamente demostrables: que una función acabe en tiempo finito, que converja correctamente a un resultado, que no traspase información que ha de permanecer secreta, etc.
Las desventajas de los métodos formales son fundamentalmente dos: por un lado, el tiempo necesario para probar que un determinado programa respeta una propiedad puede ser muy alto. De hecho, es sabido que hay propiedades que no son demostrables, aunque un programa las cumpla. Por otro lado, los métodos formales requieren de una base matemática suficiente para ponerse en práctica, que la mayoría de los programadores no tenemos, y eso aunque hayamos estudiado informática.
¿Por qué este tutorial?
Yo no soy un experto en los métodos formales ni en el uso de Coq. Lo que estudié al respecto en la carrera era sobre todo basado en el lenguaje Z y he de confesar que a penas me acuerdo. En el tema de Coq, he de admitir que soy autodidacta.
Existen buenos materiales para aprender sobre este tema (aunque todavía no tanto como me gustaría). Las razones para escribir mi propio tutorial son tres:
- Aún hay poco material sobre Coq en español.
- El material que hay sobre Coq tiende a partir de la base de una persona que sepa un mínimo de matemática discreta, lógica simbólica, etc.
- También me gustaría tratar el tema fijándome en la accesibilidad del uso de Coq.
Instalación.
La última versión estable de Coq es la 8.5pl4. Para Windows hay un instalador, y para GNU/Linux existen varias opciones. Para empezar recomiendo utilizar la que esté disponible en el repositorio de la distribución. Por ejemplo, Debian stable tiene Coq 8.4pl4, de julio de 2014. Está algo anticuada, pero para aprender a utilizar Coq sirve perfectamente, aunque se vayan introduciendo cambios y mejoras. Una vez sea necesario, puede instalarse una versión más moderna mediante el uso de OPAM, que es un gestor de paquetes específico de ocaml.
Para verificar que Coq está instalado correctamente, es necesario ejecutar “coqtop”.
$ coqtop
Welcome to Coq 8.5pl2 (July 2016)
Coq <
Para salir de Coq, podemos usar el comando “Quit.” (importante, Coq es sensible al caso) o ctrl-d en linux, y ctrl-z en Windows seguido de intro.
Empezando con Coq, desde cero.
Coqtop actúa como todo REPL (read-print-evaluate loop). Lee las declaraciones que introducimos, las evalúa, y nos imprime el resultado. Algunos ejemplos:
Coq < Check 0.
0
: nat
Check es un comando de Coq que nos da el tipo de una expresión. Otro ejemplo:
Coq < Check Nat.add.
Nat.add
: nat -> nat -> nat
Esto nos indica el tipo de Nat.add. Nat es un módulo que contiene definiciones relativas a los números naturales. El tipo de Nat.add, viene dado como nat -> nat -> nat. ¿Qué quiere decir el operador “->”? Podríamos leerlo como “hacia”. Lo que nos está diciendo es que nat toma un número natural (nat) y nos devuelve algo que toma otro número natural y devuelve un número natural (nat -> nat). Con paréntesis, nat -> (nat -> nat).
Una pequeña digresión sobre funciones y parámetros. En Coq se utiliza la noción de función de modo más formal que en otros lenguajes. Estamos acostumbrados a tener funciones que toman varios parámetros, como int suma(int a, b). En Coq las funciones toman un parámetro y devuelven un parámetro. ¿Cómo podemos trabajar con estas funciones? Mediante el uso de funciones parciales y la técnica denominada “currying”. Una función como suma, en Coq, lo que hace es tomar un número natural, y devolver como resultado una función que toma un sólo número natural, le suma el anterior, y devuelve el resultado, que es otro natural. A las funciones que toman o devuelven otras funciones como parámetros se las denomina funciones de orden superior. Hay motivos, tanto teóricos como prácticos, para utilizar esta definición de función más estricta, y una vez que uno se acostumbra no presenta mayores problemas. Simplemente, add es una función que, a efectos prácticos, toma dos naturales y nos devuelve otro, mediante una función intermedia de orden superior.
Podemos probar el uso de add.
Coq < Compute Nat.add 2 3.
= 5
: nat
Para sorpresa de nadie, 2 + 3 = 5, y 5 es un número natural. Hasta aquí todo es bastante normal. Pero en Coq los tipos son elementos de primera clase, y se construyen mediante fórmulas inductivas. Print sirve para ver la definición de un objeto.
Coq < Print nat.
Inductive nat : Set := O : nat | S : nat -> nat
Aquí las cosas ya empiezan a ser distintas. Lo que quiere decir esta definición, es que nat es un tipo inductivo (perteneciente a Set (conjunto)) que se puede formar mediante dos constructores:
- O. Esto representa el cero.
- Una función S que toma un nat y devuelve otro nat. S es la función Sucesor.
Esto supone que sólo hay dos formas de tener un nat. O bien “O”, o “S nat”, donde nat es algún natural. Por ejemplo:
Coq < Check O.
0
: nat
<!>
Coq < Check S (S (S O)).
3
: nat
El uso de 0, 1, 2, etc, es azúcar sintáctica para O, S O, S (S O), etc. Esta construcción de los números naturales se llama la construcción de Peano, y es un sistema numérico unario (sólo hay un dígito). Es poco eficiente, pero se utiliza por defecto porque nos permite realizar pruebas inductivas con facilidad. Coq dispone de otras representaciones numéricas cuando son necesarias.
Veamos ahora la definición de Nat.add.
Coq < Print Nat.add.
Nat.add =
fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end
: nat -> nat -> nat
Vamos a analizar esta definición paso a paso.
fix es un operador que se utiliza para definir funciones recursivas. Nos está advirtiendo que esta función se llama a si misma.
(n m : nat) {struct n} : nat. Esto indica que toma 2 parámetros, n y m, de tipo nat. struct n indica que la recursión es estructural en n, es decir, que cuando add se llama a si misma, n va a ser siempre inferior. Esto garantiza que add siempre devuelva un resultado en tiempo finito. El último nat es el tipo del valor de retorno de la función.
Pero, un momento, no habíamos dicho que las funciones sólo toman un valor? Todo este aspecto de funciones de orden superior es automático. Al tomar n y m, es lo mismo que si dijéramos que tomamos sólo n, y que devolvemos una función que toma m, con el valor de n rellenado. Por eso digo que a efectos prácticos la cuestión de los parámetros de las funciones no tiene importancia. Podemos escribir funciones como si tomasen varios parámetros, y se hace el currying automáticamente.
Tras el “:=”, viene el cuerpo en sí de la función.
match es un operador para encajar patrones. Indicamos la variable en la que queremos encajar, ponemos with, y los patrones. En este caso estamos encajando en n.
Según el primer patrón, si n encaja con 0, la función devuelve m. (0 + m = m).
Según el segundo patrón, si n encaja con S p, es decir, cuando n es el sucesor de otro nat p, la función devuelve S (add p m), el sucesor de añadir p a m. Aquí vemos que la función tiene recursión estructural en n, porque al llamarse a si misma, el valor de n siempre tendrá que ir disminuyendo.
Finalmente, end cierra la función, y se nos presenta el tipo, nat -> nat -> nat.
Una de las ventajas de que los tipos sean objetos de primera clase definidos por fórmulas inductivas, es que las funciones siempre son completas. De hecho, si intentásemos definir add2 sin el patrón de 0, ocurriría esto:
Coq < Fixpoint add2 (n m : nat) : nat :=
Coq < match n with
Coq < | S p => S (add2 p m)
Coq < end.
Toplevel input, characters 0-80:
> Fixpoint add2 (n m : nat) : nat :=
> match n with
> | S p => S (add2 p m)
> end.
Error: Non exhaustive pattern-matching: no clause found for pattern 0
Algunas cuestiones sobre esta definición. Utilizo Fixpoint, porque me permite definir y nombrar una función recursiva de una tacada, en vez de utilizar fix. Es azúcar sintáctica. No he puesto el {struct n} en la definición, porque no es necesario. Coq es capaz de inferirlo de la estructura de la función. Al final de end, hay un punto (.) para cerrar el comando. Al margen de esto, las dos declaraciones son iguales salvo por la falta del encaje para el patrón 0, y ese es el error que Coq nos da. De esta forma, Coq se asegura que todas las definiciones de funciones son totales y completas (es decir, terminan en tiempo finito y pueden aplicarse a todos los parámetros del tipo).
Una prueba sencilla.
Ahora que hemos utilizado números naturales y la función add que los suma, vamos a probar que 0 es el elemento neutro de la suma. Para ello tenemos que probar dos hechos: 1) que n + 0 = n, y 2) que 0 + m = m.
Coq dispone de sintaxis que nos deja decir n + m en lugar de (add n m), lo que hace las pruebas más fáciles de formular.
Coq < Theorem add_0_m: forall m:nat, 0 + m = m.
Theorem indica a Coq que vamos a intentar probar un teorema. Existen otros comandos que hacen exactamente lo mismo pero tienen otros nombres, como Lemma. La diferencia es puramente estética. Tras Theorem, indicamos el nombre que le vamos a dar al teorema, seguido de dos puntos (:) y la definición.
En este caso utilizamos forall, que es el cuantificador universal. forall m:nat viene queriendo decir “para todo m, cuando m es un número natural”. Tras la coma que finaliza la cuantificación, viene el resultado: 0 + m = m, y un punto (.).
Entonces Coq entra en modo de prueba:
1 subgoal
============================
forall m : nat, 0 + m = m
add_0_m <
Coq nos indica lo que se denomina un juicio. Primero nos da el número de submetas (ramas de la prueba), que en este caso es una sola. Luego nos da las hipótesis, o lo que sabemos que es cierto o postulamos como tal, seguido de una línea de signos de igual, y la meta que debemos probar. Finalmente, en la entrada de comandos, en lugar de decir simplemente Coq, nos dice el nombre del teorema.
A partir de aquí es necesario utilizar lo que Coq denomina tácticas. Las tácticas son órdenes a Coq que manipulan el estado del juicio (o bien de las hipótesis o bien de la meta) y nos permiten ir avanzando en la prueba.
add_0_m < intros.
m : nat
============================
0 + m = m
La táctica intros (pensemos en introducir) toma las variables que estén cuantificadas en la meta y las pasa para la hipótesis. Desde el punnto de vista matemático, es como cuando en la prueba decimos: sea un número natural m.
add_0_m < simpl.
m : nat
============================
m = m
La táctica simpl (de simplificar) intenta simplificar la meta, aplicando las funciones, y en general reduciendo los términos. En este caso, 0 + m se simplifica a m, porque all hacer add 0 m, n es 0, y encaja con el patrón que nos devuelve m. En términos matemáticos, aquí diríamos “directamente de la definición de Nat.add, 0 + m se reduce a m.”
add_0_m < reflexivity.
No more subgoals.
reflexivity es la táctica que se usa cuando tenemos una igualdad, y ambos términos coinciden. En general, reflexivity intenta hacer una simplificación previa, de forma que en este caso nos habríamos podido ahorrar la táctica simpl, pero la he puesto explícitamente para que se vea el funcionamiento de la reducción. Coq nos dice que no quedan metas por probar, y entonces podemos hacer Qed (quod era demonstrandum, latinajo que significa “lo que había que probar” y que indica el fin de la prueba).
add_0_m < Qed.
intros.
simpl.
reflexivity.
Qed.
add_0_m is defined
Coq <
Al hacer Qed, se nos da el script de las tácticas utilizadas, y el teorema queda definido para su posible uso.
Pero nos queda otra parte que probar: n + 0 = n.
Coq < Theorem add_n_0: forall n:nat, n + 0 = n.
1 subgoal
============================
forall n : nat, n + 0 = n
Veamos lo que sucede si intentamos usar la misma estrategia (voy a copiar sólo lo esencial):
n : nat
============================
n + 0 = n
add_n_0 < simpl.
n : nat
============================
n + 0 = n
Vaya, ¿y eso? simpl no nos sirve, porque no puede reducir el término n + 0. Podía reducir 0 + m, porque en el patrón 0, la función simplemente devuelve m, pero cuando n es una variable, tendría que encajar con S p, y como no sabemos el valor de n, no podemos generar p. En este caso tenemos que hacer una prueba por inducción, y aquí es donde se ve la ventaja de que nat esté definido por una fórmula inductiva.
En una prueba por inducción, lo que decimos es: si la proposición p es cierta para 0, y si en todos los casos en que la proposición p es cierta para n, también es cierta para S n, entonces la proposición es cierta para todo n.
Esto se puede hacer en Coq mediante el uso de la táctica induction. A diferencia de las tácticas que hemos visto hasta ahora, induction requiere un parámetro, que es la variable en la que vamos a llevar a cabo la inducción.
add_n_0 < induction n.
2 subgoals
============================
0 + 0 = 0
subgoal 2 is:
S n + 0 = S n
Aquí Coq nos dice que tenemos 2 submetas, es decir, la prueba se ha ramificado. Para intentar probar una cosa, tenemos que probar estas dos: que 0 + 0 = 0, y la segunda submeta, que S n + 0 = S n. La primera submeta se prueba con reflexivity, directamente de la definición de add:
add_n_0 < reflexivity.
1 subgoal
n : nat
IHn : n + 0 = n
============================
S n + 0 = S n
Al probar una meta, nos queda sólo la otra. En este meta, además de la hipótesis n:nat (sea un número natural n), también tenemos la hipótesis inductiva, de que n + 0 = n. Esto es lo que estamos intentando probar, pero no podemos usar la hipótesis directamente porque n ya es un número natural concreto, y nosotros estamos probando para todo n. Pero la inducción nos permite asumir que n + 0 = n, y probar que siempre que esto sea cierto, es cierto para S n (es decir, n + 1).
En este caso hacemos simplificación:
add_n_0 < simpl.
1 subgoal
n : nat
IHn : n + 0 = n
============================
S (n + 0) = S n
Y ahora la simplificación si que nos ayuda a reducir el término, porque S n encaja con el patrón S p en add, y la definición nos dice que el resultado es s (p + m), siendo m 0. De ahí que nos deje reducir S n + 0 a S (n + 0).
El motivo por el que esto es útil es que tenemos una hipótesis en que se nos dice que n + 0 = n. La igualdad en Coq implica que podemos reescribir un término por otro y obtener los mismos resultados. Para ello utilizamos la táctica rewrite.
add_n_0 < rewrite IHn.
1 subgoal
n : nat
IHn : n + 0 = n
============================
S n = S n
rewrite nos permite reescribir en ambas direcciones de la igualdad, pero por defecto lo hace de izquierda a derecha. Sustituye por lo tanto el término (n + 0) por (n), y nos deja con una igualdad que lógicamente se resuelve por reflexivity. Qed!
La explicación de esta prueba me ha llevado por lo menos media hora escribirla, pero la prueba, hoy por hoy, es cosa de 15 segundos.
En el próximo episodio…
Si veo que hay interés seguiré escribiendo sobre Coq, pero entiendo que es un tema bastante técnico y no se si tendrá audiencia. En cualquier caso, y si me pongo, en el próximo episodio voy a explicar lo siguiente:
- ¿Cuál es el tipo de un teorema? ¿Qué pasa si usamos Print con él?
- Isomorfismo de Curry-Howard, y por qué es importante.
- Lógica. La lógica constructiva y la clásica. Pruebas de algunos teoremas.
- Más sobre otras tácticas (destruct, rewrite de derecha a izquierda, split, left, right).
Si has llegado hasta aquí, muchísimas gracias por tu atención. Dime lo que opinas en Twitter (@modulux) o por correo electrónico.