Coq

Seems more focused on the functional aspect and proving the correctness of programs (including generating certified programs from proofs of correctness for said programs).

Contents

• Mathematical Foundations
  • Additional Reading
• Coq IDEs
  • CoqIde
  • jsCoq
  • VSCoq (VSCode)

Mathematical Foundations

Coq is based on the Calculus of Inductive Constructions (CIC), defined in the section on Typing rules in the Coq Reference Manual. The CIC is an instance of type theory; the base of Coq is a type checker.

Using the Curry-Howard correspondence (propositions as types) logic can be expressed in type theory, constituting the foundation of mathematics in Coq. This means that proving a proposition $P : Prop$ is the same as providing a term $t : P$ (witness) of type $P$. The question of whether a proposition $P$ is provable is thus the same as whether the type $P$ is inhabited (has instances/terms). The section on Proof Objects in the Logical Foundations book shows how logical operators can be defined as types. Their actual definitions in Coq are in the library Coq.Init.Logic (see the file lib/coq/theories/Init/Logic.v in the Coq distribution for proofs).

Coq's core logic is intuitionistic/constructive, which means that to prove a proposition, an explicit witness of it must be constructed. For instance, a proof for $A ∨ B$ (a term $t : A ∨ B$) must be either a proof for $A$ ($t : A$) or a proof for $B$ ($t : B$). This means that some non-constructive arguments traditionally used in classical logic (like the excluded middle $A ∨ ¬A$) must be added as axioms. For more information see the sections on the Logic of Coq and useful Axioms in the Coq Wiki on GitHub.

Additional Reading

• For the canonical definition of the CIC see
  • coqref:Sorts for an explanation of the base of the type hierarchy
  • coqref:Typing rules for the main definitions
  • coqref:Theory of inductive definitions for inductive types
• wiki:Intuitionistic type theory explains some of the type theoretic basics. Note that this is not exactly how CIC is defined.
  • the entry on Intuitionistic Type Theory in the Stanford Encyclopedia of Philosophy discusses the concept more broadly
• Philip Wadler: Propositions as types (doi:10.1145/2699407) gives a short history and overview of the concept and its uses.

Coq IDEs

The available options seem to be:

• CoqIde, a part of the Coq project
• jsCoq, a web-based environment
• Jupyter with the coq_jupyter kernel
• emacs with the Proof General and Company-Coq plugins
• Visual Studio Code with the VSCoq plugin
• Vim with the Coqtail plugin

CoqIde

Similar to Isabelle/jEdit, feels even more old and clunky.

jsCoq

Web-based, interactive. See

• jsCoq demo
• jsCoq scratchpad (local storage)
• CollaCoq, "the Coq pastebin"

VSCoq (VSCode)

Seems to work well.

For basic use see the plugin page.

Note: if commands do not work, restart VSCode (do not close the tab of the opened .v file, just close VSCode and launch it again).

Settings

configure at Settings (Ctrl+,) > Extensions > Coq configuration

required

• Coqtop: Bin Path enter path to Coq/bin dir
• (for Windows) for Coqtop: Coqidetop Exe and Coqtop: Coqtop Exe, add .exe

recommended

• Coq: Auto Reveal Proof State At Cursor: enable
• Coqtop: Start On: set to open-script