User Tools

Site Tools


math:coq_notes

Introductory Stuff

Coq Reading

Installing Coq

  • 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

CoqIDE Notes

  • 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

Proof General

  • 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.

Stuff I'd like to Prove

  • The sum of any two consecutive numbers is odd.

For the cheaters Formalizing 100 theorems in Coq

Language Notes

  • 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 Commands

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:
    • Conceptually, this really looks just like a unit test.
    • Synonyms that can be used interchangeably with Theorem: Lemma, Remark, Corollary, Proposition, Example
    • Syntax:
      Theorem <test_name>: [<quantifier>,] <boolean expression>.
    • Example of a quantifier: forall n:nat:
      Theorem n_plus_0 : forall n:nat, 0 + n = n.
    • The above simply states: “Adding zero to every natural number results in the same natural number”
  • Check: displays the type of an expression.
  • Notation: Defines a custom operator.
    • You can even replace other operators defined in the standard libarary.
    • Example:
      Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
  • Proof Begins a proof.
  • Qed ends a proof.
    • Commands between Proof and Qed are part of the tactics sub-language.

Gallina Expressions

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.

Tactics

Oddities

  • If n is a nat, then the expression S n is the same as n + 1.
    • This is because nat modeled as a linked list with no item–the value is encoded in the number of links in the list. (This is a *very* weird way to model numbers.)
    • S is one of the constructors of nat which takes a single argument having type nat.

Standard Library

Terms

  • Goal:
  • unfold:
  • Context:
  • Quantifier:

Questions

  • 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, Example?
    • This may be partially answered here. I believe the reason is so that mathematicians can use the term that best applies–even though as far as Coq is concerned they are all functionally equivalent.
  • 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.
math/coq_notes.txt · Last modified: 2019/02/03 19:44 by dave