coq Tutorial
Empezando con coq
Buscar..
Observaciones
Esta sección proporciona una descripción general de qué es coq y por qué un desarrollador puede querer usarlo.
También debe mencionar cualquier tema grande dentro de coq, y vincular a los temas relacionados. Dado que la Documentación para coq es nueva, es posible que deba crear versiones iniciales de esos temas relacionados.
Prueba e instalación de Coq.
Pruebas sin instalar
Para los usuarios nuevos que deseen comenzar a probar Coq sin instalarlo en su máquina, hay un IDE en línea llamado JsCoq (presentación aquí ). La subventana del paquete permite probar varios paquetes adicionales conocidos.
Instalación
La página de descarga contiene instaladores para Windows y MacOS.
En general, se recomienda a los usuarios de Linux que compilen desde la fuente usando opam, para obtener la última versión. Aquí se dan instrucciones básicas sobre cómo hacerlo.
Una prueba sencilla
Theorem my_first_theorem : 1 + 1 = 2.
Proof.
reflexivity.
Qed.
Instala Coq en MacOS
Puede instalar todo el paquete descargando el paquete dmg desde aquí .
El paquete contiene un CoqIDE que puede usarse para escribir sus pruebas o puede usar el comando coqtop para ejecutar el intérprete en su terminal
La instalación de Coq en MacOS es fácil de usar también en Homebrew
brew install coq
o si usas MacPorts
sudo port install coq
No hay buen soporte vi para Coq. Puedes usar Proof General dentro de emacs que tiene una buena usabilidad.
Para instalar Proof General, elimine las versiones anteriores de Proof General y clone la nueva versión de GitHub.
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make
Luego agrega lo siguiente a tu .emacs:
;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")
Asegúrese de que los emacs están ejecutando el Emacs real. Si enfrenta problemas de discrepancia de versión, es posible que tenga que ejecutar makefile nuevamente especificando la ruta de Emacs explícitamente
make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
Instalación con Nix
Advertencia: esta no es la forma estándar de instalar Coq.
Para los usuarios de Linux (y MacOS) que deseen obtener acceso a versiones actualizadas de Coq o poder usar varias versiones de Coq en la misma máquina, sin la molestia de usar opam, y sin tener que compilar desde Fuente, esta es una solución alternativa.
Nix es un administrador de paquetes para sistemas operativos tipo Unix, como Linux y MacOS. Viene con su propia colección de paquetes que generalmente se mantiene mucho más actualizada que la de Debian o la de Ubuntu. No entra en conflicto con el administrador de paquetes de su distribución porque no instala nada en /usr/bin y demás.
Primero, necesitas instalar Nix :
$ curl https://nixos.org/nix/install | sh
Para asegurarse de que las variables de entorno necesarias estén establecidas, vuelva a iniciar sesión o escriba:
. $HOME/.nix-profile/etc/profile.d/nix.sh
Luego el siguiente comando instalará la última versión de Coq:
$ nix-env -iA nixpkgs.coq_8_6
También puede ejecutar CoqIDE sin agregar nada a su RUTA:
$ nix-shell -p coq_8_6 --run coqide
Del mismo modo (suponiendo que ya tiene instalado Emacs y Proof-General):
$ nix-shell -p coq_8_6 --run emacs
Esto es muy útil para ejecutar diferentes versiones cuando las necesite. Por ejemplo, para ejecutar Coq 8.5 use el siguiente comando:
$ nix-shell -p coq_8_5 --run coqide
Ejemplo de prueba por inducción.
Aquí hay una prueba simple por inducción.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Arith.Lt.
(* A number is less than or equal to itself *)
Theorem aLTEa : forall a,
a <= a.
auto with arith. (* This follows by simple arithmetic *)
Qed.
Theorem simplALTE : forall a b,
S a <= S b <-> a <= b. (* If a <= b, then a + 1 <= b + 1 *)
Proof.
Admitted.
Theorem ltAlwaysLt: forall a b,
a <= a + b.
Proof.
intros. (* Introduce relevant variables *)
induction a, b. (* Induction on every variable *)
simpl. apply aLTEa. (* 0 <= 0 + S b *)
rewrite -> plus_O_n. auto with arith. (* 0 <= S b *)
rewrite <- plus_n_O. apply aLTEa. (* S a <= S a + 0 *)
rewrite <- simplALTE in IHa. (* IHa: a <= a + S b. Goal: S a <= S a + S b. *)
apply IHa. (* We rewrote the induction hypothesis to be in the same form as the goal, so it applies immediately now *)
Qed.