coq Tutorial
Iniziare con coq
Ricerca…
Osservazioni
Questa sezione fornisce una panoramica su cosa sia il coq e perché uno sviluppatore potrebbe volerlo utilizzare.
Dovrebbe anche menzionare qualsiasi grande argomento all'interno di coq e collegarsi agli argomenti correlati. Poiché la Documentazione per coq è nuova, potrebbe essere necessario creare versioni iniziali di tali argomenti correlati.
Test e installazione di Coq
Test senza installazione
Per i nuovi utenti che desiderano iniziare a testare Coq senza installarlo sulla propria macchina, esiste un IDE online chiamato JsCoq (presentazione qui ). La sotto finestra del pacchetto consente di testare vari pacchetti aggiuntivi ben noti.
Installazione
La pagina di download contiene programmi di installazione per Windows e MacOS.
Gli utenti di Linux sono generalmente invitati a compilare dal sorgente usando opam, al fine di ottenere l'ultima versione. Qui vengono fornite le istruzioni di base su come farlo.
Una semplice prova
Theorem my_first_theorem : 1 + 1 = 2.
Proof.
reflexivity.
Qed.
Installa Coq su MacOS
Puoi installare l'intero pacchetto scaricando il pacchetto dmg da qui .
Il pacchetto contiene un CoqIDE che può essere utilizzato per scrivere le bozze o è possibile utilizzare il comando coqtop per eseguire l'interprete sul terminale
L'installazione di Coq su MacOS è facile anche usando l'homebrew
brew install coq
o se usi MacPorts
sudo port install coq
Non c'è un buon supporto vi per Coq. È possibile utilizzare Proof General in emacs che ha una buona usabilità.
Per installare Proof General rimuovere le vecchie versioni di Proof General clonare la nuova versione da GitHub
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make
Quindi aggiungi quanto segue al tuo .emacs:
;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")
Assicurati che Emacs stia eseguendo l'Emacs vero e proprio. Se si affrontano problemi di mancata corrispondenza della versione, potrebbe essere necessario eseguire makefile specificando nuovamente il percorso di Emacs in modo esplicito
make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
Installazione con Nix
Attenzione: questo non è il modo standard per installare Coq.
Per gli utenti di Linux (e MacOS) che desiderano accedere a versioni aggiornate di Coq o essere in grado di utilizzare diverse versioni di Coq sulla stessa macchina, senza il fastidio di usare opam e senza dover compilare da fonte, questa è una soluzione alternativa.
Nix è un gestore di pacchetti per SO di tipo Unix come Linux e MacOS. Viene fornito con una propria collezione di pacchetti che è generalmente mantenuta molto più aggiornata rispetto a quella di Debian o Ubuntu. Non è in conflitto con il gestore di pacchetti della tua distribuzione perché non installa nulla in /usr/bin e così via.
Innanzitutto, è necessario installare Nix :
$ curl https://nixos.org/nix/install | sh
Per garantire che siano impostate le variabili di ambiente necessarie, accedere nuovamente o digitare:
. $HOME/.nix-profile/etc/profile.d/nix.sh
Quindi il seguente comando installerà l'ultima versione di Coq:
$ nix-env -iA nixpkgs.coq_8_6
Puoi anche eseguire CoqIDE senza aggiungere nulla al tuo PATH:
$ nix-shell -p coq_8_6 --run coqide
Allo stesso modo (supponendo che abbiate già installato Emacs e Proof-General):
$ nix-shell -p coq_8_6 --run emacs
Questo è molto utile per eseguire diverse versioni quando ne hai bisogno. Ad esempio, per eseguire Coq 8.5 utilizzare il seguente comando:
$ nix-shell -p coq_8_5 --run coqide
Esempio di prova per induzione
Ecco una semplice dimostrazione per induzione.
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.