math:coq_notes
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
math:coq_notes [2019/02/02 22:21] dave [Questions] |
math:coq_notes [2019/02/03 19:44] (current) dave [Vernacular Commands] |
||
|---|---|---|---|
| Line 42: | Line 42: | ||
| * The sum of any two consecutive numbers is odd. | * The sum of any two consecutive numbers is odd. | ||
| + | |||
| + | For the cheaters [[https://madiot.fr/coq100/|Formalizing 100 theorems in Coq]] | ||
| ===== Language Notes == | ===== Language Notes == | ||
| Line 75: | Line 77: | ||
| * ''Fixpoint'': can be used to define recursive functions. Use it in place of ''Definition''. | * ''Fixpoint'': can be used to define recursive functions. Use it in place of ''Definition''. | ||
| * ''Theorem'': | * ''Theorem'': | ||
| - | * Synonyms that can be used interchangably with ''Theorem'': ''Lemma'', ''Remark'', ''Corollary'', ''Proposition'' | + | * Conceptually, this really looks just like a unit test. |
| - | * ''Example'': a unit test | + | * Synonyms that can be used interchangeably with ''Theorem'': ''Lemma'', ''Remark'', ''Corollary'', ''Proposition'', ''Example'' |
| - | * Syntax: ''Example <test_name>: <boolean expression>'' | + | * 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. | * ''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 == | ==== Gallina Expressions == | ||
| Line 97: | Line 113: | ||
| end. | end. | ||
| </code> | </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 == | ===== Standard Library == | ||
| Line 103: | Line 129: | ||
| * ''::'' list ''cons'' operator | * ''::'' list ''cons'' operator | ||
| + | ===== Terms == | ||
| + | |||
| + | * ''Goal'': | ||
| + | * ''unfold'': | ||
| + | * ''Context'': | ||
| + | * ''Quantifier'': | ||
| ===== Questions == | ===== Questions == | ||
| * It is said that all Coq programs terminate. Does that mean the compiler prevents infinite loops? | * 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]]? | * 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''? | + | * 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 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? | * 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? | ||
math/coq_notes.1549174915.txt.gz · Last modified: 2019/02/02 22:21 by dave
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 4.0 International
