Notas para el uso de CoqIde
---------------------------

* Acerca de la versión.
* Acerca del archivo derivaciones07.v.
* Una sesión de ejemplo.

-------------

* Acerca de la versión.

CoqIde es una interface gráfica para trabajar con el marco de desarrollo
Coq. Esta nota refiere a la siguiente versión:

---
CoqIDE: an Integrated Development Environment for Coq

Main author  : Benjamin Monate
Contributors : Jean-Christophe Filliâtre
               Pierre Letouzey, Claude Marché

Feature wish or bug report: use Web interface

	http://coq.inria.fr/bin/coq-bugs

Version information
-------------------
The Coq Proof Assistant, version 8.0pl3 (Jan 2006)
Configured on jan 13 2006 13:00:09
Architecture i686 running Unix operating system
Gtk version is 2.4.14
This is the native version (native is the best one for this architecture and OS)

---
-------------

* Acerca del archivo derivaciones07.v.

Este archivo supera al anterior Logica.v. Por ese motivo se ha eliminado dicho
documento.

Este archivo está desarrollado para la versión 8 de Coq. En él se
definen las reglas de eliminación e introducción del cálculo proposicional
y de predicados. 

Los nombres de las reglas se forman con:
 - caracteres que indican el conector,
 - caracteres que indican si la regla es de introducción o eliminación,
 - eventualmente, un índice (1 o 2),
 - eventualmente, una fórmula.

Por ejemplo: el nombre SiiE1 se refiere a 
 - una regla para el bicondicional (Sii),
 - de eliminación (E),
 - una de las dos posibilidades (1).
Al aplicar la regla es necesario explicitar la fórmula a usar.

Dos casos excepcionales a este formato de nombre son RAA, 
la reducción al absurdo, e HIP, la regla de hipótesis.

La lista siguiente es la de los nombres de las reglas.

Hip 
RAA 
YI 
YE1 f 
YE2 f
OI1
OI2
OE f
SiI
SiE f
SiiI
SiiE1 f
SiiE2 f
NoI
NoE f
BotE

-----------------

* Una sesión de ejemplo.

1. Abra la interfase gráfica.

2. Escriba
      Load "/luis/coq/derivaciones07.v".
2.a. Ejecute la instrucción mediante
2.a.i.   Navigation -> Forward, o
2.a.ii.  Ctrl+Alt+Down, o
2.a.iii. ícono de un triángulo isósceles apoyado en un vértice.
2.a. Luego de realizar la carga, estará en condiciones de usar las reglas
programadas.

3. Escriba
      Lemma pp : p -> p.
3.a. Ejecute la instrucción como antes.

4. Resuelva el lema.
3.a. Escriba
      SiI.
3.b. Ejecute.
3.c. Escriba 
      Hip.
3.d. Ejecute.
3.e. Escriba
      Qed.
3.f. Ejecute.

4. Salga de la interfase.