Dave's Wiki

• The Coq Standard Library
• The Coq Reference Manual
• Certified Programming with Dependent Types
  • There are setup instructions at the end of the introduction which are needed for running the examples. (Good thing I read the introduction!)
  • Note that the chapter “Some Quick Examples” isn't quick at all! It's very long!
• Software Foundations (Volume 1)
  • Warning: the code samples are not all copy and paste-able because whatever was used to generate the HTML combines symbols like ⇒ into ⇒ (WTH!
  • This does seem like the best book for beginners.
• A tutorial by Mike Nahas
• DeepSpec Summer School 2017
• DeepSpec Summer School 2018

• Don't bother with your distro's version of Coq/CoqIDE since these are usually outdated.
  • Version 8.9.0 is currently the latest.
• Set up ocaml & opam first.
• coqide also requires system package gtsourceview v2.x
  • On Arch and derivatives: pacman -Sy gtksourceview2
• Then, simply opam install coq coqide -y

• When saving files add the .v extension yourself–CoqIDE does not do this for you like other editors.
• Ctrl-End: plays the script to the end
• Ctrl-Home: resets the script to its beginning
• Ctrl-Down: advances the script by a single line
• Ctrl-Up: reverse the script by a single line
• Ctrl-Right: advances or reverses the script to the cursor's line

• Is an Emacs plugin for Coq and other theorem provers.
• company-coq is an extension for Proof General.
• spacemacs-coq is a spacemacs layer which loads company-coq and Proof General.

• The sum of any two consecutive numbers is odd.

• Coq is an amalgamation of 3 different languages:
  • Vernacular, which manages definitions
    • Each of its commands starts with a capital letter.
  • Tactics is used to write proofs
    • Its commands start with a lowercase letter.
  • Gallina is used to express what you want to prove
    • Its expressions use lots of operators and parens.
• Type inference is limited due to Coq's extremely expressive type system.
• All Coq programs terminate.
  • TODO: does this mean that the compiler checks to ensure there are no infinite loops?

Vernacular Command Reference. Notes on specific commands created as I learn about them below.

• Inductive: is similar to type in OCaml, but types in Coq are much more expressive than in other languages.
  • This form seems similar to OCaml's variant types:

    Inductive type_name : Set := 
    | Variant1 : element1,
    | Variant2 : element1.

• Definition: can be used to bind a term to a name.
  • Functions can be defined:

    Definition <func_name> (<arg_name> : <arg_type)... : <ret_type> := <func_body>

  • If 2 arguments have the same type they can be declared together:

    Definition <func_name> (arg_1_name arg_2_name arg_3_name : <arg_type>) : <ret_type> := <func_body>

• Fixpoint: can be used to define recursive functions. Use it in place of Definition.
• Theorem:
  • Synonyms that can be used interchangably with Theorem: Lemma, Remark, Corollary, Proposition
• Example: a unit test
  • Syntax: Example <test_name>: <boolean expression>
• Check: displays the type of an expression.

The Gallina Specification

• Pattern matching:

  match expr
  | <pattern1> => <match_item>
  | <pattern2> => <match_item>
  end.

  • It is possible to match more than one expression at a time:

    match n, m with
     | O   , _    => O
     | S _ , O    => n
     | S n', S m' => minus n' m'
    end.

• The Standard Data Types
• :: list cons operator

• It is said that all Coq programs terminate. Does that mean the compiler prevents infinite loops?
• What is the ++ operator seen on this page?
• Why are there so many synonyms of Theorem? i.e. Lemma, Remark, Corollary, Proposition?
• This text has a number of variables which seem to shadow variables defined in a parent scope, however they are suffixed with a single quote character (i.e. “ s' ”). What is the meaning of ' in this context?
  • For example:

    Definition instrDenote (i : instr) (s : stack) : option stack :=
      match i with
        | iConst n => Some (n :: s)
        | iBinop b =>
          match s with
            | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
            | _ => None
          end
      end.