Instituto de Computación 						     Facultad de Ingeniería
Curso de Lógica
Breve introducción  a Coq
¿Qué es Coq?

Coq es un ambiente que permite expresar lógicas y construir y verificar demostraciones de enunciados mediante la aplicación de ciertas reglas. Nosotros lo utilizaremos para construir y verificar derivaciones de teoremas en deducción natural.

El archivo logica.v  (disponible en la página web del curso) contiene una especificación de las reglas de deducción natural utilizadas en el curso de Lógica. Utilizando dicho archivo (en conjunto con la versión 7.2 de Coq) podemos verificar si una derivación que hemos construido es correcta o no.  Para ello, hemos de ejecutar el programa  coqtop.exe desde una ventana de comandos. Al hacerlo, aparecerá en la pantalla una línea de comandos que luce así:

	Coq < _

A continuación, hemos de cargar el archivo logica.v a efectos de poder trabajar con nuestras reglas de deducción natural:

	Coq < Load logica.

Para que lo anterior funcione, el archivo logica.v debe incluirse en el mismo directorio que el ejecutable coqtop . Una vez cargado, ya estamos en condiciones de utilizar las reglas descriptas en el archivo, las cuales se resumen a continuación:

Hip (Assumption)	SiI (I)		OI1  ( I 1 )		SiiE1   (E1)
YI   (I)		SiE (E)		OI2  ( I 2 )		SiiE2   (E2)
YE1 (E1)		NI   (I)		OE    (E )		FalseE (E)
YE2 (E2)		NE   (E)		SiiI (I)		RAA

El archivo logica.v también contiene una enumeración de letras proposicionales que podemos utilizar:
p,q,r
p0,p1,p2,p3,p4,p5,p6,p7,p8,p9
q0,q1,q2,q3,q4,q5,q6,q7,q8,q9
r0,r1,r2,r3,r4,r5,r6,r7,r8,r9
Si deseamos utilizar otras letras de proposición basta con editar el archivo logica.v  e incluirlas junto con las anteriores. Las conectivas disponibles en el ambiente son las siguientes:
	False (), True (), ~ (), ->, /\, \/, <->
La negación también puede ser expresada como  not.

¿Cómo funciona Coq?

A continuación presentamos algunas consideraciones generales a tener en cuenta a la hora de trabajar con Coq.  Las mismas pretenden explicar brevemente la forma en la cual se trabaja con Coq para verificar demostraciones. En el documento titulado Ejemplo que se adjunta con esta introducción se presenta un ejemplo concreto que ilustra con mayor claridad las consideraciones que aquí se mencionan.

Para usar Coq como herramienta para verificar si una demostración es correcta o no, tenemos que indicarle paso a paso la estrategia que utilizamos en la construcción de nuestra prueba. En cada paso, lo que hacemos es indicarle a Coq qué reglas deseamos aplicar para demostrar nuestro objetivo. Coq nos muestra las subpruebas que debemos completar y cuáles son las hipótesis podemos usar en el proceso, pero no construye la prueba por nosotros. Sólo nos garantiza que, si logramos completar las subpruebas pedidas, la prueba será correcta. Este esquema de razonamiento es el que usamos en papel cuando construimos una derivación “de abajo hacia arriba”.

La forma general que utiliza Coq para indicarnos qué debemos demostrar es la siguiente:

H1: 1
H2: 2
				.
				.
				.
Hn: n
==========

donde  1,...,n  son la hipótesis que tenemos disponibles (etiquetadas H1,...,Hn) y   es la fórmula que debemos demostrar.

Cuando Coq  nos presenta un esquema de este tipo, lo que debemos hacer es indicarle qué regla deseamos aplicar para demostrar  (en el ejemplo que se adjunta se ve con detalle cómo hacer esto). Dada la indicación, Coq verifica que la sintaxis de la regla que deseamos aplicar es correcta.  Como resultado, Coq puede decirnos 3 cosas:
1)	Que la prueba de  ha sido completada con éxito.
2)	Que la regla se ha aplicado con éxito, pero ello generó alguna(s) nueva(s) subprueba(s) que debemos completar. En este caso, Coq nos indicará cuál(es) es(son), para lo cual también usará la forma general vista antes. 
3)	Que hemos aplicado mal la regla y/o usado mal alguna hipótesis, en cuyo caso Coq despliega un mensaje de error.

En general, la forma de trabajar con Coq para verificar demostraciones se resume así: Dados un enunciado y un conjunto de hipótesis, le indicamos a Coq qué reglas utilizar para probarlo. En el proceso pueden aparecer otras subpruebas que debemos completar trabajando de la misma manera. Si logramos completarlas todas, la prueba será correcta. Si, en cambio no logramos hacerlo,  puede ser por dos motivos:
1)	Lo que queremos demostrar en realidad no se cumple.
2)	Las reglas que estamos aplicando no nos están llevando por buen camino, en cuyo caso tal vez sea mejor repensar la estrategia de la prueba (como cuando no se nos ocurre una derivación en papel).

¿Cómo utilizar las reglas?

Veremos a continuación cómo es la sintaxis de cada una de las reglas contenidas en el archivo logica.v. y cómo se aplican. 

Las reglas  Hip, YI, OI1, OI2, sii, NI, siii, RAA, FalseE  se aplican en forma “directa”. 
Por  ejemplo, si la fórmula a probar está entre las hipótesis, se puede utilizar la regla Hip para probarla de la siguiente manera:

Línea de comandos:  < Hip.

Las reglas  sie, NE, YE1, YE2, siie1, SiiE2 se aplican con una fórmula que sirve para proveer la información necesaria para su aplicación.
Por ejemplo, si la fórmula a demostrar es q, y se la quiere probar usando E con las fórmulas pq  y  p, basta con indicarle a Coq la fórmula p, del siguiente modo: 

Línea de comandos:  < SiE ’p.

La regla  OE se aplica a dos fórmulas. 
Por  ejemplo, para demostrar una fórmula cualquiera usando E con la fórmula pq, debemos indicarle a Coq las fórmulas p y q del siguiente modo:

Línea de comandos:  < OE ’p ’q.

Note que la aplicación de cada regla finaliza con un punto (.) y que cada operando va antepuesto de una comilla simple (’). 

En el documento titulado Ejemplo  que se adjunta con esta introducción se presenta un ejemplo concreto que ilustra con mayor claridad el “significado” de las reglas. 

Algunos comandos que debemos manejar...

Para finalizar esta breve introducción presentaremos una enumeración de algunos comandos que pueden ser de utilidad a la hora de trabajar con Coq. Por mayor información sobre estos u otros comandos, remitirse al sitio web de Coq (hay un link en el sitio web del curso de Lógica).

•	Comando Load: Sirve para cargar en el ambiente un archivo con extensión.v
Ejemplo:  < Load logica.

•	Comando Theorem: Sirve para indicarle a Coq que deseamos probar un teorema.
Ejemplo:  < Theorem nombreteorema: (p->q)->(~q->~p).

•	Comando Show Script: Sirve para desplegar una lista de todas las reglas y/o tácticas empleadas hasta el momento en la construcción de nuestra prueba.
Ejemplo:  < Show Script.
		SiI.
		Hip.

•	Comando Qed: Sirve para indicarle a Coq que hemos completado la prueba que queríamos. Lo que hace es guardarla y dejar el ambiente disponible para que construyamos otra. La prueba guardada puede eventualmente ser utilizada en la prueba de otro teorema. Sólo puede aplicarse si está completa.

•	Comando Abort: Sirve para indicarle a Coq que deseamos abandonar la prueba que estamos construyendo. Deja el ambiente disponible para que construyamos otra.

•	Comando Restart: Sirve para indicarle a Coq que deseamos recomenzar la construcción de nuestra prueba. Lo que hace es “desechar” los pasos desarrollados hasta el momento y dejar el ambiente disponible para que comencemos la prueba nuevamente.

•	Comando Quit: Lo que hace es cerrar la sesión y salir del ambiente.