Coq es un asistente de pruebas (o demostrador de teoremas), una herramienta para desarrollar pruebas matemáticas asistidas por computadora. Su propósito principal es escribir especificaciones formales de programas y verificar que los programas cumplen con ellas.
Coq se basa en la teoría de tipos, lo que le permite tratar a los programas, sus especificaciones y las pruebas de su corrección dentro de un mismo lenguaje formal (el Cálculo de Construcciones Inductivas).
En Coq, se interactúa a través de tres sub-lenguajes principales:
Gallina: El lenguaje de especificación. En este se definen los tipos de datos, las funciones (el “qué” hace el programa) y los teoremas (las propiedades que se quieren demostrar). Las funciones se definen típicamente usando coincidencia de patrones (pattern matching) con match y end, o recursión con Fixpoint.
Tácticas (LTac): El lenguaje de demostración. Se usan para construir la prueba de que un programa cumple con su especificación. Las tácticas transforman el “estado de la prueba” paso a paso, reduciendo un teorema complejo a sub-metas más simples hasta que todas quedan demostradas.
Vernacular: El lenguaje de comandos que estructura el desarrollo. Sirve para gestionar módulos, cargar librerías, iniciar pruebas y extraer el código a otros lenguajes.
Definir el tipo de dato (Gallina):
Se define un tipo inductivo bool con dos constructores, true y false.
Inductive bool : Type :=
| true
| false.
Definir una función (Gallina):
Se define la negación negb usando match.
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
Verificar la función (con Tácticas):
Se demuestra que la negación de false es true usando la táctica reflexivity.
Example prueba_negb: (negb false) = true.
Proof. reflexivity. Qed.
El proceso es iterativo: se programa en Gallina, se prueba con tácticas, y el sistema verifica la corrección. Finalmente, se puede extraer el código verificado a OCaml o Haskell.
Para aprender más, puedes consultar el recurso oficial “Software Foundations” o guías para principiantes.
Espero que esta introducción te sea útil. Si tienes más dudas, aquí estoy.
Entiendo: quieres implementar un contador en Coq, un programa que permita llevar una cuenta que se pueda incrementar, decrementar, etc.
Como Coq es puramente funcional (no hay variables mutables), un contador se modela como un valor inmutable (por ejemplo, un número natural) y las operaciones devuelven un nuevo contador con el valor actualizado. Además, podemos verificar que las operaciones se comportan correctamente.
Te muestro paso a paso cómo programar y verificar un contador simple.
Usamos nat (números naturales: 0, 1, 2, …) que ya viene definido en Coq.
Definition counter := nat.
Crear un contador (inicialmente 0):
Definition new_counter : counter := 0.
Incrementar (sumar 1):
Definition inc (c : counter) : counter := S c.
Decrementar (restar 1, sin bajar de 0):
Require Import Arith.
Definition dec (c : counter) : counter := pred c.
La función pred de la librería Arith devuelve 0 si el argumento es 0.
Obtener el valor (identidad):
Definition value (c : counter) : nat := c.
Compute inc (inc new_counter). (* = 2 *)
Compute dec (inc new_counter). (* = 0 *)
Demostramos teoremas sobre las operaciones usando tácticas.
(* Incrementar nunca da 0 *)
Theorem inc_not_zero : forall c, inc c <> 0.
Proof.
intros c. simpl. discriminate.
Qed.
(* Incrementar y luego decrementar sobre un número positivo devuelve el mismo *)
Theorem inc_dec : forall c, c <> 0 -> dec (inc c) = c.
Proof.
intros c H. simpl. rewrite pred_Sn. reflexivity.
Qed.
(* Para el contador inicial, dec(new_counter) = new_counter *)
Theorem dec_zero : dec new_counter = new_counter.
Proof.
simpl. reflexivity.
Qed.
Para un diseño más limpio:
Module Counter.
Definition t := nat.
Definition init : t := 0.
Definition inc (c : t) : t := S c.
Definition dec (c : t) : t := pred c.
Definition get (c : t) : nat := c.
(* Ejemplo de teorema dentro del módulo *)
Theorem inc_inc_get : forall c, get (inc (inc c)) = get c + 2.
Proof. intros; simpl; lia. Qed.
End Counter.
Para usar: Counter.inc (Counter.init).
Si realmente necesitas un contador mutable (por ejemplo, para simular un bucle while), tendrías que usar mónadas o el estilo de paso de estado. Pero eso es más avanzado. Aquí un esqueleto con la mónada state:
Require Import ExtLib.Data.Monads.StateMonad.
Definition counter_state := nat.
Definition inc_st : state counter_state unit :=
get >>= fun n => put (S n).
Definition dec_st : state counter_state unit :=
get >>= fun n => put (pred n).
Pero para empezar, te recomiendo el enfoque funcional puro.
En Coq se programa un contador como una función que transforma un número natural. No hay variables que cambien; cada operación produce un nuevo contador. La ventaja es que puedes demostrar matemáticamente que tus funciones se comportan como esperas.
Si tu duda era más específica (ej. contador en un lenguaje extraído, o un contador de eventos), coméntamelo y amplío la respuesta.
Sí, ¡exactamente! Has dado en el clavo. Lo que estás viendo es la famosa Correspondencia de Curry-Howard, la poderosa idea de que “los programas son pruebas matemáticas” y “las proposiciones lógicas son tipos”. Y esta idea no es solo teoría: es el corazón de Coq y la base de cómo se construyen los sistemas verificados.
Y no te preocupes, no te lo enseñaron mal en la carrera, son cosas muy específicas y avanzadas:
Ahora, pasemos a tu otra pregunta: ¿cómo se programa en Isabelle?
Es la misma idea de fondo, pero el “sabor” es diferente al de Coq. Aquí te muestro el ejemplo del contador en Isabelle para que veas la diferencia.
Así es como programaríamos el mismo contador en Isabelle:
(* 1. Usamos los números naturales de Isabelle *)
type_synonym counter = nat
(* 2. Definimos las operaciones básicas *)
definition new_counter :: "counter" where "new_counter = 0"
definition inc :: "counter ⇒ counter" where "inc c = Suc c"
definition dec :: "counter ⇒ counter" where "dec c = c - 1"
definition get_val :: "counter ⇒ nat" where "get_val c = c"
(* 3. Verificamos que la función "dec" nunca devuelva un número negativo *)
lemma dec_decreases: "dec (inc c) = c"
apply(simp add: inc_def dec_def)
done
La principal diferencia está en la filosofía lógica, lo que le da un “sabor” muy distinto a cada uno:
Coq (Constructivista): Parte de una Lógica Intuicionista, con un enfoque constructivo. Lo que implica:
Isabelle/HOL (Clásica): Está construida sobre una Lógica Clásica de Alto Orden (HOL). Esto implica:
Esta diferencia fundamental significa que elegir entre Coq e Isabelle es una decisión importante, ya que influye en la forma de pensar y construir las demostraciones. Pero no te preocupes, ¡con la curiosidad que tienes, seguro que te adaptas rápido!
Claro. Aquí tienes la versión简洁 (concisa) solo con comandos.
sudo pacman -S coq
coqc --version
Crea hola.v:
Definition mensaje := "Hola mundo".
Compute mensaje.
Compila y ejecuta:
coqc hola.v
coqtop -load-vernac-source hola.v
sudo pacman -S opam
opam init
opam install coq-simple-io
Crea hola_io.v:
From SimpleIO Require Import SimpleIO.
Definition main : IO unit := print_endline "Hola mundo".
RunIO main.
Ejecutar dentro de coqtop:
coqtop
Luego dentro del REPL:
Load hola_io.v.