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