Instituto de Computación 						     Facultad de Ingeniería
Curso de Lógica
Ejemplo de aplicación de Coq

En este documento presentamos un ejemplo concreto que pretende ilustrar cómo utilizar Coq    (en conjunto con el archivo logica.v ) para ayudarnos a construir una prueba en deducción natural, o dicho de otro modo, ayudarnos a verificar si una prueba que construimos es correcta.

Supongamos que queremos demostrar lo siguiente :   |  (p  q)  q  p
Para ello construimos la siguiente derivación :

  [ (p  q)  q (1) ]
[(p  q)  q (1)  ]                   [ p (2) ]                   p  q     (E1)
         q           (E2)                                       q                     (E)
                                           (E)
   p  (RAA) (2)
(p  q)  q  p   (I) (1)

Deseamos ahora utilizar Coq para verificar si esta derivación está bien o no. Como ya mencionamos en la breve introducción que se adjunta con este ejemplo, construiremos esta derivación en Coq “de abajo hacia arriba”. 

Esto es : Primero le indicamos a Coq que deseamos probar  (p  q)  q  p mediante (I). Luego Coq nos dirá que debemos probar  p  y que tenemos a (p  q)  q  como hipótesis.
Entonces le indicaremos que queremos probar p mediante (RAA) y  Coq nos dirá que debemos probar    y que tenemos a  (p  q)  q  y  a  p  como hipótesis, y así sucesivamente. 
Si logramos completar todas las subpruebas que Coq nos vaya presentando, entonces podremos concluir que nuestra derivación es correcta.

Comenzamos por ejecutar el programa  coqtop.exe . Al hacerlo, nos aparece la siguiente línea de comandos:

	Coq < _

Luego cargamos el archivo logica.v (que contiene nuestras reglas de deducción natural) de la siguiente manera:

	Coq < Load logica.

A continuación enunciamos el  teorema que queremos demostrar:

	Coq < Theorem miteorema: ((not p) -> q) /\ (not q) -> p.

Enseguida aparece en pantalla lo siguiente:

	1 subgoal

	==============
      (~p->q)/\~q->p

miteorema < _

Coq está esperando que le indiquemos qué regla deseamos aplicar para demostrar (~p->q)/\~q->p. 
Vamos a utilizar (I). Entonces, escribimos lo siguiente:

miteorema < SiI.

Enseguida aparece en pantalla:

	1 subgoal

	H: (~p->q)/\~q
	==============
      p

miteorema < _

Coq está esperando que le indiquemos qué regla deseamos aplicar para demostrar  p, teniendo la posibilidad de utilizar  (~p->q)/\~q  como hipótesis. 
Para probar  p, usaremos RAA. Entonces, escribimos:

miteorema < RAA.

Enseguida aparece en pantalla lo siguiente:

	1 subgoal

	H: (~p->q)/\~q
	H0: ~p
	==============
      False

miteorema < _

Coq está esperando que le digamos qué regla deseamos aplicar para demostrar  False  (o sea ), teniendo la posibilidad de utilizar  (~p->q)/\~q  y ~p como hipótesis. 
Para probar esto usaremos (E) de forma tal de concluir  False  a partir de  q->False y  q . Entonces, escribimos:
miteorema < NE ’q.
Observemos que el operando utilizado es solamente q ya que Coq puede deducir del contexto que la otra fórmula involucrada en la aplicación de la regla es  q->False ( debido a que la conclusión es False).
Enseguida aparece en pantalla lo siguiente:

	2 subgoals

	H: (~p->q)/\~q
	H0: ~p
	==============
      q->False

subgoal 2 is :
q

miteorema < _

Ahora Coq nos muestra las dos subpruebas que debemos construir, las cuales denomina  subgoal 1  y   subgoal 2. Debemos demostrar primero subgoal 1. Recién cuando lo hayamos hecho, podremos empezar a demostrar subgoal 2.

Coq está esperando que le indiquemos qué regla deseamos aplicar para demostrar  q->False, teniendo la posibilidad de utilizar  (~p->q)/\~q  y ~p como hipótesis. 
Observemos que dicha fórmula es una abreviación para ~q. Por lo tanto, utilizamos la regla (E2), aplicada a nuestra hipótesis (~p->q)/\~q , a efectos de poder concluir ~q. Entonces, escribimos lo siguiente :

miteorema < YE2 ’(~p->q).

Observemos que el operando utilizado es solamente (~p->q). Una vez más, dado que Coq nos pide demostrar  ~q, al poner solamente (~p->q), se deduce del contexto que la otra “mitad” involucrada al aplicar la regla es ~q.

Enseguida aparece en pantalla lo siguiente:

	2 subgoals

	H: (~p->q)/\~q
	H0: ~p
	===================
      (~p->q)/\(q->False)

subgoal 2 is :
q

miteorema < _

Nuevamente, Coq nos indica que debemos demostrar dos cosas. Por un lado,  ~p->q)/\(q->False)  y por el otro, q  ( que es el subgoal 2 que había quedado pendiente). 
Comenzamos por demostrar (~p->q)/\(q->False). Observemos que dicha fórmula coincide exactamente con nuestra hipótesis H. Por lo tanto, para poder demostrar (~p->q)/\(q->False), basta con utilizar H. Entonces escribimos:

miteorema < Hip.

Enseguida aparece en pantalla lo siguiente:

	1 subgoal

	H: (~p->q)/\~q
	H0: ~p
	==============
      q

miteorema < _

Notemos que ya hemos completado una de las dos subpruebas. Ahora Coq está esperando que indiquemos qué regla deseamos aplicar para demostrar q , teniendo la posibilidad de utilizar (~p->q)/\~q  y ~p como hipótesis. 
Utilizamos (E) de forma tal de concluir  q  a partir de    ~p->q , ~p  . Entonces, escribimos:

miteorema < SiE ’~p.

Enseguida aparece en pantalla lo siguiente:

	2 subgoals

	H: (~p->q)/\~q
	H0: ~p
	==============
      ~p->q

subgoal 2 is :
~p

miteorema < _

Nuevamente, Coq nos indica que debemos demostrar dos cosas. Por un lado, ~p->q  y por el otro, ~p.
Comenzamos por demostrar ~p->q . Observemos que dicha fórmula coincide con la “mitad” izquierda de nuestra hipótesis H. Por lo tanto, utilizamos la regla (E1), aplicada a nuestra hipótesis (~p->q)/\~q , a efectos de poder concluir ~p->q . Entonces, escribimos:
miteorema < YE1 ’~q.

Enseguida aparece en pantalla lo siguiente :
	2 subgoals

	H: (~p->q)/\~q
	H0: ~p
	==============
      (~p->q)/\~q

subgoal 2 is :
~p

miteorema < _

Una vez más Coq nos indica que debemos demostrar dos cosas. Por un lado, (~p->q)/\~q  y por el otro, ~p (que es el subgoal 2 que había quedado pendiente). 
Comenzamos por demostrar (~p->q)/\~q . Notemos que coincide exactamente con nuestra hipótesis H. Entonces escribimos:

miteorema < Hip.

Enseguida aparece en pantalla lo siguiente:

	1 subgoal

	H: (~p->q)/\~q
	H0: ~p
	==============
      ~p

miteorema < _

Ahora sólo nos falta completar la subprueba para ~p. Notemos que coincide exactamente con nuestra hipótesis H0. Entonces escribimos:

miteorema < Hip.

y aparece en pantalla lo siguiente:

subtree proved !!

Esto significa que hemos completado la última subprueba en forma exitosa. 
Nótese que es en este punto (al final de la prueba) cuando las hipótesis H,H0 se cancelaron. Para terminar, basta con escribir:

miteorema < Qed.