Coq-Befehle: Übersicht und erste Schritte

Coq (seit 2024 auch unter dem Namen Rocq weiterentwickelt) ist ein interaktiver Beweisassistent auf Basis des Calculus of Inductive Constructions. Er entstand 1984 am INRIA in Rocquencourt aus einer Implementierung des Calculus of Constructions von Thierry Coquand und Gérard Huet; 1991 erweiterte Christine Paulin den Kalkül um induktive Konstruktionen. Coq wird für mathematische Beweise (z.B. Vier-Farben-Satz) und für formale Verifikation von Software (z.B. der Compiler CompCert) eingesetzt.

Erste Schritte

coqc Datei.v               # Datei kompilieren und prüfen (Verification)
coqtop                     # Interaktive REPL
coqide                     # Grafische IDE (Proof General/VS Code: VsCoq)
coq_makefile -f _CoqProject  # Makefile für Projekte erzeugen
Require Import Arith.      # Standard-Bibliothek laden
Check plus.                # Typ einer Definition anzeigen

Kernkonzepte

  • Gallina: Die eingebaute funktionale Sprache, in der Definitionen und Theoreme formuliert werden. Aus Gallina können per Extraction ausführbare Programme in OCaml, Haskell oder Scheme erzeugt werden.
  • Taktiken: Beweise werden mit kleinen Schritten geführt — intros, apply, destruct, induction, rewrite, auto und viele mehr.
  • Induktive Typen: Datentypen wie nat oder list definieren zugleich die zugehörigen Induktionsprinzipien.
  • Program Extraction: Aus konstruktiven Beweisen lassen sich lauffähige Algorithmen extrahieren — die Verbindung von Beweis und Programm.

Praxis-Tipps

  • Theorem t : forall n : nat, n + 0 = n. startet einen Beweis; Proof. intros n. simpl. reflexivity. Qed. schließt ihn ab.
  • Die SSReflect-Erweiterung (aus dem Mathematical Components-Projekt) beschleunigt große Beweise.
  • CompCert, ein formal verifizierter C-Compiler, wurde vollständig in Coq entwickelt und per Extraction nach OCaml übersetzt.
  • Für die Automatisierung stehen lia (Lineare Arithmetik) und omega-Nachfolger bereit.

Verwandte Grundlagen: Idris-Befehle, Agda-Befehle, Haskell-Befehle (alle drei Sprachen teilen die Curry-Howard-Idee).