Comenzando con coq

Una prueba sencilla

Theorem my_first_theorem : 1 + 1 = 2.
Proof.
  reflexivity.
Qed.

Pruébalo en tu navegador.

Instalación con Nix

Advertencia: esta no es la forma estándar de instalar Coq.

Para 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 mantienen mucho más actualizados que los de Debian o 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, necesita instalar Nix:

$ curl https://nixos.org/nix/install | sh

Para asegurarse de que las variables de entorno necesarias estén configuradas, 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 instalados 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

Instalar Coq en MacOS

Puede instalar el paquete completo descargando el paquete dmg desde [aquí] (https://coq.inria.fr/download).

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 también es fácil usando homebrew

preparar instalar coq

o si usa MacPorts

Puerto sudo instalar coq

No hay un buen soporte vi para Coq. Puede usar Proof General dentro de emacs que tiene una buena usabilidad.

Para instalar Proof General, elimine las versiones anteriores de Proof General, 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 agregue lo siguiente a su .emacs:

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

Asegúrese de que el Emacs que está ejecutando sea el Emacs real. Si enfrenta problemas de discrepancia de versiones, es posible que deba ejecutar makefile nuevamente especificando la ruta de Emacs explícitamente

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

Probando e instalando Coq

Probando sin instalar

Para los nuevos usuarios que deseen comenzar a probar Coq sin instalarlo en su máquina, existe un IDE en línea llamado JsCoq (presentación [aquí](https://x80.org /rhino-coq/)). La subventana del paquete permite probar varios paquetes adicionales conocidos.

Instalación

La página de descargas contiene instaladores para Windows y MacOS.

Por lo general, se recomienda a los usuarios de Linux que compilen desde la fuente usando opam, para obtener la última versión. Las instrucciones básicas sobre cómo hacerlo se dan [aquí] (https://coq.inria.fr/opam/www/using.html).

Ejemplo de demostración 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.