===== 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:
Inductive type_name : Set :=
| Variant1 : element1,
| Variant2 : element1.
* ''Definition'': can be used to bind a term to a name.
* Functions can be defined:
Definition ( : :=
* If 2 arguments have the same type they can be declared together:
Definition (arg_1_name arg_2_name arg_3_name : ) : :=
* ''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 : [,] .
* 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 ==
[[https://coq.inria.fr/refman/language/gallina-specification-language.html#grammar-token-match_item|The Gallina Specification]]
* Pattern matching:
match expr
| =>
| =>
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 ==
[[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:
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.