Dave's Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
===== Introductory Stuff ==

==== Coq Reading == 

  * [[https://coq.inria.fr/distrib/current/stdlib/|The Coq Standard Library]]
  * [[https://coq.inria.fr/distrib/current/refman/|The Coq Reference Manual]]
  * [[http://adam.chlipala.net/cpdt/|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!
  * [[https://softwarefoundations.cis.upenn.edu/|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.
  * [[https://coq.inria.fr/tutorial-nahas|A tutorial by Mike Nahas]]
  * [[https://deepspec.org/event/dsss17/|DeepSpec Summer School 2017]]
  * [[https://deepspec.org/event/dsss18/|DeepSpec Summer School 2018]]

==== 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.
  * [[https://github.com/cpitclaudel/company-coq|company-coq]] is an extension for Proof General.
  * [[https://github.com/olivierverdier/spacemacs-coq|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 [[https://madiot.fr/coq100/|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 ==

[[https://coq.inria.fr/refman/proof-engine/vernacular-commands.html|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: <code>
Inductive type_name : Set := 
| Variant1 : element1,
| Variant2 : element1.
</code>
  * ''Definition'': can be used to bind a term to a name.
    * Functions can be defined: <code>
Definition <func_name> (<arg_name> : <arg_type)... : <ret_type> := <func_body>
</code>
    * If 2 arguments have the same type they can be declared together:<code>
Definition <func_name> (arg_1_name arg_2_name arg_3_name : <arg_type>) : <ret_type> := <func_body>
</code>
  * ''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:<code>
Theorem <test_name>: [<quantifier>,] <boolean expression>.
</code>
    * Example of a quantifier:  ''forall  n:nat'':<code>
Theorem n_plus_0 : forall n:nat, 0 + n = n.
</code>
    * 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:<code>
Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
</code>                       
  * ''Proof'' Begins a proof.
  * ''Qed'' ends a proof.
    * Commands between ''Proof'' and ''Qed'' are part of the //tactics// sub-language.

==== Gallina Expressions ==

[[https://coq.inria.fr/refman/language/gallina-specification-language.html#grammar-token-match_item|The Gallina Specification]]

  * Pattern matching:<code>
match expr
| <pattern1> => <match_item>
| <pattern2> => <match_item>
end.
</code>
    * It is possible to match more than one expression at a time:<code>
match n, m with
 | O   , _    => O
 | S _ , O    => n
 | S n', S m' => minus n' m'
end.
</code>

==== Tactics == 

[[https://coq.inria.fr/refman/coq-tacindex.html|Tactic Index]]
===== 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 ==

  * [[https://coq.inria.fr/library/Coq.Init.Datatypes.html|The Standard Data Types]]
  * ''::'' list ''cons'' operator

===== 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 [[http://adam.chlipala.net/cpdt/html/Cpdt.StackMachine.html|this page]]?
  * Why are there so many synonyms of ''Theorem''? i.e. ''Lemma'', ''Remark'', ''Corollary'', ''Proposition'', ''Example''?
    * This may be partially answered [[https://divisbyzero.com/2008/09/22/what-is-the-difference-between-a-theorem-a-lemma-and-a-corollary/|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 [[http://adam.chlipala.net/cpdt/html/Cpdt.StackMachine.html#compile|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: <code>
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.
</code>
Dave's Wiki

User Tools

Site Tools

Page Tools
