From 34674c61fab8d1c7d8fd8652baafa8c62a54e61d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 24 Jun 2016 13:39:12 -0400 Subject: first draft of a "folk wisdom" document --- folkwisdom.md | 263 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 263 insertions(+) create mode 100644 folkwisdom.md diff --git a/folkwisdom.md b/folkwisdom.md new file mode 100644 index 000000000..e1c52351c --- /dev/null +++ b/folkwisdom.md @@ -0,0 +1,263 @@ +The purpose of this document is to document which design heuristics have +resulted in tolerable code, and which patterns might be indicative of a dead +end. The intent is to document experience (imperical results), not comprehensive +truth. For each guideline here, there probably exists some situation where it is +best to deviate from the said guideline. Yet incomplete wisdom is better than no +wisdom, so let's note down the trade-offs we have faced and how we have resolved +them. + +# Data representations + +## Validity + +### Obvious validity + +For some data, the obvious simple type can only take meaningful values -- +a natural number is either zero or the successor of another natural number, and +that is all there is to it. This section covers the cases when the choice of +correct representation is not obvious. + +### Validity by a well-engineered simple type structure + +If using a representation where the type only admits semantically valid values +would not make the functions that operate that type look horrendous, use that +representation. For example, the Coq standard library represents a rational +number as a pair of a integer numerator and `positive` denominator, and it works +out okay. Fractions with 0 denominator can not be represented because there is +no value of type `positive` that would be interpreted as zero. + +On the other hand, an elliptic curve point in Edwards coordinates is informally +defined as a pair `(x, y)` s.t. `x^2 + y^2 = 1 + d*x^2*y^2`. It is no longer +obvious how one would hack up a simple type that only represents valid points. +A solution that gets quite close would be to use "point compression": store `y` +and the sign bit of `x`; solve for `x` each time it is needed. Yet this +representation is not unique (there are two ways to represent a point with +`x=0`), and solving for `x` would clutter all functions that operate on `x` and +`y`. Uniqueness can still be restored at the cost of cluttering the functions +even more: one could make a type that has three cases `Xpositive`, that takes +a `y`, `Xnegative` that takes a `y`, and `Xzero` that represents the point `(0, +1)` but does not allow a superfluous y to be specified. + +The alternative is to first write down a type that can represent all valid +values and some invalid ones, and then disallow the invalid ones. Sometimes +disallowing the invalid values can be circumvented by redefining validity: it +may be possible to extend an algorithm that only operates on positive numbers to +work with all natural numbers or even all integers. Sometimes the validity +condition is crucial: the group law for combining two Edwards curve points is +only proven to be associative for points that are on the curve, not for all +pairs of numbers. + +### Validity using dependent types + +If nontrivial data validity invariants are required, the intuitive "value such +that" definition can be encoded as a sigma type: `Definition point := { P | let +'(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2 }`. In this encoding, every time +a value of type `point` is constructed out of the `x` and `y` coordinates, +a proof that the point is valid will need to be provided. Code that manipulates +point using functions that are already known to return points does not need to +deal with the invariant: a value that comes out of a function that returns +`point` is valid because wherever it was that the value was constructed from +coordinates, a validity proof must have been provided. Using sigma types this +way moves proof obligations from one place in the code to another, hopefully +more convenient place. + +Dependent types are not a free lunch, we have encountered three types of issues +when dealing with them. + +#### Rewriting + +The `rewrite` tactic does not work in equations that construct a point from +its coordinates and a proof. This is because after rewriting just the +coordinates, the proof would still refer to the old coordinates, and thus the +construction would not be valid. It might be possible to make rewriting work by +showing an equivalence relation on values such that the invariant does not +become invalidated when replacing one equivalent value with another, and the +rewrite only changes the value within an equivalence class. It might even be +possible to hook this argument with the `setoid_rewrite` tactic to automate it. +However, a more lightweight rule has been successful enough to keep us from +pursuing that strategy: when non-trivial equational reasoning on the value is +required, split this up the invariant preservation proof. For example, when an +optimized `add : point -> point -> point`, first define `add_coordinates : F*F +-> F*F -> F*F` that operates on arbitrary pairs of coordinates, do all the +rewriting you want, and then define `add` in terms of `add_coordinates`. In +analogy to Java's `public` and `private` annotations, users of the Edwards curve +`point`s never operate on the coordinates alone, while the implementation +of point addition operates on coordinates and proves invariant preservation +separately. + +#### Computation inside Coq + +Computing values of a proof-carrying type inside Coq often runs unreasonably +long or uses unreasonably much memory. However, computing the coordinates of the +same point that itself would take too long to compute seems to work fine. In +cases were the evaluation heuristics do not manage to make this okay, rewriting +the expression before evaluating it has not been too difficult. + +#### Equality and Equivalence + +Equality and invariant preservation proofs do not play nice by default. Under +Leibniz equality, showing that two points with equal coordinates are equal +requires showing that the invariant preservation proofs are equal. This can be +done using the `UIP_dec` lemma if the invariant itself is an equality and that +for all values of coordinates it is decidable to compute whether the invariant +holds on them or or not. These conditions tend to be met for the invariants this +project uses. Otherwise, two points can be defined to be equivalent (not equal) +if they have the same coordinates (working with custom equivalence relations +involves nontrivial considerations of its own). + +#### Note on defining values + +The most reliable way to make a value of a sigma type is to start the +`Definition` in proof mode (ending the first line with a dot like `Definition +zero : point.`) and then do `refine (exist _ value _); abstract +(tacticThatProvesInvariant)`. Some of the time, `Program Definition` will do the +same thing without explicit proof mode (as the Edwards curve spec) but it tends +to over-eagerly rewrite `if` and `match` statements (as in the Weierstrass curve +spec). Neatness of the value that is defined takes priority over neatness of the +code that performs the definition. + +## Equivalence + +Terms can be equivalent in different ways. In this list, each kind of equality +is stricter than the one right after it. + +- syntactic: they are literally the same expression. Proof automation is +sensitive to syntactic changes. +- definitional: one term can be transformed into the other by applying rules of +computation only. Proof checking considers two syntactically different +expressions interchangeable as long as they are definitionally equal. +- propositional: as established by a proof (which can use lemmas in addition to +rules of computation), these two terms would compute to the exact same vale. It +is always possible to rewrite using a propositional equality +- custom equivalence relations: for example, two fractions `a/b` and `c/d` can +be defined equivalent iff `a*d = b*c`. Given `x == y`, it is possible to rewrite +`f(g(x))` to `f(g(y))` if there is some equivalence relation `===` such that the +output of `f` does not change when one `===`-equivalent thing is replaced with +another, and the output of `g` only changes within a `===`-equivalence class +when the input changes within a `==`-equivalence class. This is what `Proper` +instances are about; the last statement can be written `Proper((==)=>(===))g`. + +### Which equivalence to use? + +When defining a datatype from scratch, try to define it in a way that makes +propositional equality coincide with the desired notion of equivalence. However, +as with sigma types, it is not worth garbling the code itself to use the +propositional equality + +When defining a datatype that has a field of a type that is used with a custom +equivalence, it is probably a good idea to define the obvious custom equivalence +relation for the new type right away (and make and `Equivalence` instance for +the relation and `Proper` instances for constructors and projections. When +defining a type parametrized over some other type, and it is likely that some +use of the parametric type will be set the parameter to a type with a custom +equivalence relation, define an equivalence relation for the new type, +parametrized over an equivalence relation for the parameter type. + +When writing a module that is parametric over a type, require the weakest +sufficient equivalence. In particular, if there is a chance that the module will +be instantiated with a type whose propositional equivalence makes little sense, +it is well worth requiring additional parameters for `Proper` and `Equivalence` +(and maybe `Decidable`) instances. See the Algebra library for an example. + +When writing a tactic, specify on the form of the input goal format with +syntactic precision -- trying to be insensitive to syntactic changes and only +require definitional equality can lead to arbitrary amounts of computation and +is usually not worth it. One possible exception is the +reification-by-typeclasses pattern which has not yet had issues even when it +works up to definitional equivalence to the extent typeclass resolution does. + +### Custom Equivalence Relations and Tactics + +The primary reason for avoiding custom equivalence relations is that the tactic +support for them is incomplete and sometimes brittle. This does not mean that +custom equivalence relations are useless: battling with a buggy tactic can be +bad; reformulating a proof to bypass using custom equivalence relations is often +worse. Here are some suggestions. + +1. The number one reason for hitting issues with custom equivalence relations is +that either the goal or the givens contain a typo that switched one equivalence +relation with another. In particular, `<>` refers to negation of propositional +quality by default. This can be avoided with good conventions: when introducing +a type that will be used with a custom equivalence relation, introduce the +equivalence relation (and its `Equivalence` instance) right away. When +introducing a function involving a such type, introduce a `Proper` instance +right away. Define local notations for the equivalences used in the file. Note +that while introducing the tooling may clutters the source code, section +parameters introduced using `Context {x:type}` are required for the definitions +in the section only if the definition actually refers to them. +2. Use normal `rewrite` by default -- it can deal with custom equivalence +relations and `Proper` instances. +3. To rewrite under a binder (e.g. `E` in `Let_In x (fun x => E)` or `E` in `map +(fun x => E) xs`) use `setoid_rewrite`. However, `setoid_rewrite` tries to be +oblivious to definitional equality -- and in doing so, it sometimes goes on +a wild goose chase trying to unfold definitions to find something that can be +rewritten deep down in the structure. This can cause arbitrary slowdowns and +unexpected behavior. To dodge the issues, mark the definitions as `Local Opaque` +before the `setoid_rewrite` and re-set to `Local Transparent` after. +4. When a `rewrite` fails (probably with an inexplicable error message), +double-check that the conventions from (1) are followed correctly. If this does +not reveal the issue, try `setoid_rewrite` instead for troubleshooting (it +sometimes even gives sensible error messages in Coq 8.5) but revert to `rewrite` +once the issue has been found and fixed. If rewriting picks the wrong +`Equivalence` or `Proper` instance for some type or function (or fails to find +one altogether), troubleshoot that separately: check that `pose (_:@Equivalence +T equiv)` or `pose(_:Proper (equiv1==>equiv2) f)` give the right answer, and if +not, `Set Typeclasses Debug` and read the log (which is in the hidden `*coq*` +buffer in `proofgeneral`). A useful heuristic for reading that log is to look +for the first place where the resolution backtracks and then read backwards from +there. +5. To perform multiple rewrites at once, make rewrite hint database and call +`idtac; (rewrite_strat topdown hints dbname).` where `topdown` can be replaced +with `bottomup` for different behavior. This does not seem to unfold +definitions, so it may be a reasonable alternative to using `Local Opaque` to +protect definitions from `setoid_rewrite`. + +# Generality and Abstraction + +Coq has ample facilities for abstraction and generality. The main issue we have +faced is that undisciplined use of them can clutter definitions even when only +the properties of the definitions are to be abstracted. We are not sure that the +strategy we are currently working with is optimal (in particular, it results in +verbose code), but it definitely dodges some issues other approaches do not. In +particular, we want to relate a specific set of types and operations to an +abstract structure (e.g., a group) without changing the definitions of any of +the type or operations involved. This reduces the interlock between concrete +definitions and abstractions and also enables relating the same definitions to +an abstract structure in multiple ways (e.g., integers can be a semiring under +`+` and `*` or under `max` and `+`). Furthermore, we require that it be possible +to manipulate abstractions using tactics. + +To define an abstraction, fist open a module with no parameters to make a new +namespace for the abstraction (even if the entire file is dedicated to one +abstraction). Then open a new section and add to the context parameters for all +definitions. The requirements which need to be satisfied by the definitions to +fit the structure can be defined using a typeclass record. When a one of the +requirements is a typeclass, mark the field name as a `Global Existing Instance` +right after declaring the new record. To prove lemmas about everything of that +structure, introduce an instance of that typeclass to the context (in additions +to the parameters). To relate a specific set of definitions to an abstract +structure, create a `Global Instance` of the parametric typeclass for that +structure, with the specific definitions filled in. To use a lemma proven about +an abstract structure in a specific context, just apply or rewrite using it -- +typeclass resolution will most likely determine that the specific definitions +indeed fit the structure. If not, specify the parameters to lemma manually (a +definitive description of what parameters are required and in what form can be +seen using `About lemma_name.`). + +Compared to other means of abstraction, this one does not create common notation +for all instances of the same structure. We define notations for each specific +definition, and separate them using notation scopes (which are often named after +datatypes). It would be possible to add a typeclass field that aliases the +specific definition and define a global notation for it, but definitions that +use that notation would then gain an extra layer of definitions: each underlying +operator would be wrapped in the abstract one for which the notation was +defined. Furthermore, this interferes with having one definition satisfy the +same structure in multiple ways. + +Another alternative is to use the Coq module system (which can be understood by +reading the documentation of the Ocaml module system documentation), and when +applicable, this is usually a good idea. When parameters are set once and used +very many times, the module system can be quite convenient. However, if the +number of parameters and the number of places where the values of them are +determined are comparable to the number of uses of abstractly proven lemmas, the +module system can be cumbersome. Modules cannot be instantiated automatically. -- cgit v1.2.3 From 54e43d2c5f8c2f095bda4ff19ad56153369f2630 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 24 Jun 2016 14:09:48 -0400 Subject: incorporate `Program Definition` match statement handling advice from @mattam82 --- folkwisdom.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/folkwisdom.md b/folkwisdom.md index e1c52351c..d87174115 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -110,11 +110,15 @@ involves nontrivial considerations of its own). The most reliable way to make a value of a sigma type is to start the `Definition` in proof mode (ending the first line with a dot like `Definition zero : point.`) and then do `refine (exist _ value _); abstract -(tacticThatProvesInvariant)`. Some of the time, `Program Definition` will do the -same thing without explicit proof mode (as the Edwards curve spec) but it tends -to over-eagerly rewrite `if` and `match` statements (as in the Weierstrass curve -spec). Neatness of the value that is defined takes priority over neatness of the -code that performs the definition. +(tacticThatProvesInvariant)`. Another way of doing this is to first do +`Obligation Tactic := tacticThatProvesInvariant.` and then `Program Definition +zero : point := exist _ value _.` which will call the tactic to fill in the +holes that implicit argument inference does not fill. By default, `Program +Definition` rewrites all match statements using the convoy pattern, and this can +clutter definitions quite badly. Neatness of resulting definitions takes +priority over neatness of source code. To prevent `Program Definition` to +rewriting a match statement, specify an explicit return clause: `match x return +_ with ... end.` ## Equivalence -- cgit v1.2.3 From 3c36b589a01bce19063872544bca132f3daf947d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 24 Jun 2016 17:15:59 -0400 Subject: folkwisdom: remove redundant idtac --- folkwisdom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/folkwisdom.md b/folkwisdom.md index d87174115..c6190a460 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -211,7 +211,7 @@ buffer in `proofgeneral`). A useful heuristic for reading that log is to look for the first place where the resolution backtracks and then read backwards from there. 5. To perform multiple rewrites at once, make rewrite hint database and call -`idtac; (rewrite_strat topdown hints dbname).` where `topdown` can be replaced +`(rewrite_strat topdown hints dbname).` where `topdown` can be replaced with `bottomup` for different behavior. This does not seem to unfold definitions, so it may be a reasonable alternative to using `Local Opaque` to protect definitions from `setoid_rewrite`. -- cgit v1.2.3 From 796c806bdf64490e6ef04df7e2c01e7aa94ccb86 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:46:25 -0400 Subject: add sigma type proof irrelevance wisdom from ssreflect --- folkwisdom.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/folkwisdom.md b/folkwisdom.md index c6190a460..c53ad5160 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -100,10 +100,13 @@ Leibniz equality, showing that two points with equal coordinates are equal requires showing that the invariant preservation proofs are equal. This can be done using the `UIP_dec` lemma if the invariant itself is an equality and that for all values of coordinates it is decidable to compute whether the invariant -holds on them or or not. These conditions tend to be met for the invariants this -project uses. Otherwise, two points can be defined to be equivalent (not equal) -if they have the same coordinates (working with custom equivalence relations -involves nontrivial considerations of its own). +holds on them or or not. A principled way of representing an invariant `P : T -> +Prop` as an equality is to define `check_P : T -> bool` s.t. `check_P x = true +<-> P x` and use `{x | is_true (check_P x) }` as the type of valid values^[This +technique is used extensively in `ssreflect`.]. Alternatively, two points can be +defined to be equivalent (not equal) if they have the same coordinates (working +with custom equivalence relations involves nontrivial considerations of its +own). #### Note on defining values -- cgit v1.2.3 From dddfd5a61ad8d399032f67898424f16e5d7a8790 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:50:04 -0400 Subject: wording change near "split this up" --- folkwisdom.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/folkwisdom.md b/folkwisdom.md index c53ad5160..47c5c036d 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -76,14 +76,14 @@ rewrite only changes the value within an equivalence class. It might even be possible to hook this argument with the `setoid_rewrite` tactic to automate it. However, a more lightweight rule has been successful enough to keep us from pursuing that strategy: when non-trivial equational reasoning on the value is -required, split this up the invariant preservation proof. For example, when an -optimized `add : point -> point -> point`, first define `add_coordinates : F*F --> F*F -> F*F` that operates on arbitrary pairs of coordinates, do all the -rewriting you want, and then define `add` in terms of `add_coordinates`. In -analogy to Java's `public` and `private` annotations, users of the Edwards curve -`point`s never operate on the coordinates alone, while the implementation -of point addition operates on coordinates and proves invariant preservation -separately. +required, it can be done separately from the invariant preservation proof. For +example, when aiming to implement an optimized `add : point -> point -> point`, +first define `add_coordinates : F*F -> F*F -> F*F` that operates on arbitrary +pairs of coordinates, do all the rewriting you want, and then define `add` in +terms of `add_coordinates`. In analogy to Java's `public` and `private` +annotations, users of the Edwards curve `point`s never operate on the +coordinates alone, while the implementation of point addition operates on +coordinates and proves invariant preservation separately. #### Computation inside Coq -- cgit v1.2.3 From b83a7384a3846a62bc2719567f1f0ce455787c36 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:50:55 -0400 Subject: typo near "and make and" --- folkwisdom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/folkwisdom.md b/folkwisdom.md index 47c5c036d..e8ac0faa1 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -153,7 +153,7 @@ propositional equality When defining a datatype that has a field of a type that is used with a custom equivalence, it is probably a good idea to define the obvious custom equivalence -relation for the new type right away (and make and `Equivalence` instance for +relation for the new type right away (and make an `Equivalence` instance for the relation and `Proper` instances for constructors and projections. When defining a type parametrized over some other type, and it is likely that some use of the parametric type will be set the parameter to a type with a custom -- cgit v1.2.3 From 3b535970442c9065a57bf4e23ad5c2c4c0b667b6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:52:56 -0400 Subject: s/be// --- folkwisdom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/folkwisdom.md b/folkwisdom.md index e8ac0faa1..de72c76f4 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -156,7 +156,7 @@ equivalence, it is probably a good idea to define the obvious custom equivalence relation for the new type right away (and make an `Equivalence` instance for the relation and `Proper` instances for constructors and projections. When defining a type parametrized over some other type, and it is likely that some -use of the parametric type will be set the parameter to a type with a custom +use of the parametric type will set the parameter to a type with a custom equivalence relation, define an equivalence relation for the new type, parametrized over an equivalence relation for the parameter type. -- cgit v1.2.3 From 37382028bef1b752482fb18c9550384e0e9bf0a9 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:53:38 -0400 Subject: s/quality/equality/ --- folkwisdom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/folkwisdom.md b/folkwisdom.md index de72c76f4..92f15036e 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -184,7 +184,7 @@ worse. Here are some suggestions. 1. The number one reason for hitting issues with custom equivalence relations is that either the goal or the givens contain a typo that switched one equivalence relation with another. In particular, `<>` refers to negation of propositional -quality by default. This can be avoided with good conventions: when introducing +equality by default. This can be avoided with good conventions: when introducing a type that will be used with a custom equivalence relation, introduce the equivalence relation (and its `Equivalence` instance) right away. When introducing a function involving a such type, introduce a `Proper` instance -- cgit v1.2.3 From fb7b8555839b38a36ca877650b2198685f9ffa34 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:54:20 -0400 Subject: add closing parenthesis to "(and make" --- folkwisdom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/folkwisdom.md b/folkwisdom.md index 92f15036e..687b09993 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -154,7 +154,7 @@ propositional equality When defining a datatype that has a field of a type that is used with a custom equivalence, it is probably a good idea to define the obvious custom equivalence relation for the new type right away (and make an `Equivalence` instance for -the relation and `Proper` instances for constructors and projections. When +the relation and `Proper` instances for constructors and projections). When defining a type parametrized over some other type, and it is likely that some use of the parametric type will set the parameter to a type with a custom equivalence relation, define an equivalence relation for the new type, -- cgit v1.2.3 From ce8a5c3804c50a4ee33f54b6f2fd8c6421b8cca1 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:55:33 -0400 Subject: s/on// --- folkwisdom.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/folkwisdom.md b/folkwisdom.md index 687b09993..079056439 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -166,12 +166,12 @@ be instantiated with a type whose propositional equivalence makes little sense, it is well worth requiring additional parameters for `Proper` and `Equivalence` (and maybe `Decidable`) instances. See the Algebra library for an example. -When writing a tactic, specify on the form of the input goal format with -syntactic precision -- trying to be insensitive to syntactic changes and only -require definitional equality can lead to arbitrary amounts of computation and -is usually not worth it. One possible exception is the -reification-by-typeclasses pattern which has not yet had issues even when it -works up to definitional equivalence to the extent typeclass resolution does. +When writing a tactic, specify the form of the input goal format with syntactic +precision -- trying to be insensitive to syntactic changes and only require +definitional equality can lead to arbitrary amounts of computation and is +usually not worth it. One possible exception is the reification-by-typeclasses +pattern which has not yet had issues even when it works up to definitional +equivalence to the extent typeclass resolution does. ### Custom Equivalence Relations and Tactics -- cgit v1.2.3 From 1554ea63676e285b8e8959bba6331a5ad11810d6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:58:01 -0400 Subject: recommend pose proof instead of pose --- folkwisdom.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/folkwisdom.md b/folkwisdom.md index 079056439..4f6d354eb 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -207,12 +207,12 @@ not reveal the issue, try `setoid_rewrite` instead for troubleshooting (it sometimes even gives sensible error messages in Coq 8.5) but revert to `rewrite` once the issue has been found and fixed. If rewriting picks the wrong `Equivalence` or `Proper` instance for some type or function (or fails to find -one altogether), troubleshoot that separately: check that `pose (_:@Equivalence -T equiv)` or `pose(_:Proper (equiv1==>equiv2) f)` give the right answer, and if -not, `Set Typeclasses Debug` and read the log (which is in the hidden `*coq*` -buffer in `proofgeneral`). A useful heuristic for reading that log is to look -for the first place where the resolution backtracks and then read backwards from -there. +one altogether), troubleshoot that separately: check that `pose proof +(_:@Equivalence T equiv)` or `pose(_:Proper (equiv1==>equiv2) f)` give the right +answer, and if not, `Set Typeclasses Debug` and read the log (which is in the +hidden `*coq*` buffer in `proofgeneral`). A useful heuristic for reading that +log is to look for the first place where the resolution backtracks and then read +backwards from there. 5. To perform multiple rewrites at once, make rewrite hint database and call `(rewrite_strat topdown hints dbname).` where `topdown` can be replaced with `bottomup` for different behavior. This does not seem to unfold -- cgit v1.2.3 From e61d477caa079526842d23a24aba4bdd9a2a8362 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:59:18 -0400 Subject: s/`proofgeneral`/Proof General/ --- folkwisdom.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/folkwisdom.md b/folkwisdom.md index 4f6d354eb..a41d1532f 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -210,8 +210,8 @@ once the issue has been found and fixed. If rewriting picks the wrong one altogether), troubleshoot that separately: check that `pose proof (_:@Equivalence T equiv)` or `pose(_:Proper (equiv1==>equiv2) f)` give the right answer, and if not, `Set Typeclasses Debug` and read the log (which is in the -hidden `*coq*` buffer in `proofgeneral`). A useful heuristic for reading that -log is to look for the first place where the resolution backtracks and then read +hidden `*coq*` buffer in Proof General). A useful heuristic for reading that log +is to look for the first place where the resolution backtracks and then read backwards from there. 5. To perform multiple rewrites at once, make rewrite hint database and call `(rewrite_strat topdown hints dbname).` where `topdown` can be replaced -- cgit v1.2.3 From a31c716507d5373251dbd1ddfaf6f8e4f83d3a0a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:59:47 -0400 Subject: s/fist/first/ --- folkwisdom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/folkwisdom.md b/folkwisdom.md index a41d1532f..3530a517a 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -234,7 +234,7 @@ an abstract structure in multiple ways (e.g., integers can be a semiring under `+` and `*` or under `max` and `+`). Furthermore, we require that it be possible to manipulate abstractions using tactics. -To define an abstraction, fist open a module with no parameters to make a new +To define an abstraction, first open a module with no parameters to make a new namespace for the abstraction (even if the entire file is dedicated to one abstraction). Then open a new section and add to the context parameters for all definitions. The requirements which need to be satisfied by the definitions to -- cgit v1.2.3 From 4a7d857dfb7733c103d944dfad82bd688037f721 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 19:50:33 -0400 Subject: actually fix pose proof --- folkwisdom.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/folkwisdom.md b/folkwisdom.md index 3530a517a..2234af646 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -208,11 +208,11 @@ sometimes even gives sensible error messages in Coq 8.5) but revert to `rewrite` once the issue has been found and fixed. If rewriting picks the wrong `Equivalence` or `Proper` instance for some type or function (or fails to find one altogether), troubleshoot that separately: check that `pose proof -(_:@Equivalence T equiv)` or `pose(_:Proper (equiv1==>equiv2) f)` give the right -answer, and if not, `Set Typeclasses Debug` and read the log (which is in the -hidden `*coq*` buffer in Proof General). A useful heuristic for reading that log -is to look for the first place where the resolution backtracks and then read -backwards from there. +(_:@Equivalence T equiv)` or `pose proof (_:Proper (equiv1==>equiv2) f)` give +the right answer, and if not, `Set Typeclasses Debug` and read the log (which is +in the hidden `*coq*` buffer in Proof General). A useful heuristic for reading +that log is to look for the first place where the resolution backtracks and then +read backwards from there. 5. To perform multiple rewrites at once, make rewrite hint database and call `(rewrite_strat topdown hints dbname).` where `topdown` can be replaced with `bottomup` for different behavior. This does not seem to unfold -- cgit v1.2.3 From 1336828c3069d33dca36366c03648af85f395ce5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 27 Jun 2016 14:56:20 -0400 Subject: Update folkwisdom.md --- folkwisdom.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/folkwisdom.md b/folkwisdom.md index 2234af646..3c8d92036 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -268,3 +268,20 @@ very many times, the module system can be quite convenient. However, if the number of parameters and the number of places where the values of them are determined are comparable to the number of uses of abstractly proven lemmas, the module system can be cumbersome. Modules cannot be instantiated automatically. + +# Omissions + +Considerations not (yet) covered in this document include the following: + +- structuring proofs: bullets, braces, `Focus` (a la http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html) +- conflicts in notation levels (as resolved by having files import `Util/Notations.v`) +- tactic engineering + - tactic expression evaluation vs tactic running + - how to write tactics that are debuggable + - how to write tactics that are robust against small changes + - reification: ltac, typeclasses, canonical structures (maybe reference an existing document) +- performance of proofs and proof checking + - `simpl`, `cbn`, `cbv` + - `Qed slowness, `change` vs `rewrite` + - which things fail in what ways as terms get big +- how to migrate across versions of Coq -- cgit v1.2.3