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/03 13:55] dave [Questions] |
math:coq_notes [2019/02/03 19:44] (current) dave [Vernacular Commands] |
||
|---|---|---|---|
| Line 77: | 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. | * ''Notation'': Defines a custom operator. | ||
| Line 111: | Line 117: | ||
| [[https://coq.inria.fr/refman/coq-tacindex.html|Tactic Index]] | [[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 120: | Line 133: | ||
| * ''Goal'': | * ''Goal'': | ||
| * ''unfold'': | * ''unfold'': | ||
| - | * | + | * ''Context'': |
| + | * ''Quantifier'': | ||
| ===== Questions == | ===== Questions == | ||
math/coq_notes.1549230954.txt.gz · Last modified: 2019/02/03 13:55 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
