Draft rewrite rules for 069-coq-roadmap.md#70
Draft rewrite rules for 069-coq-roadmap.md#70Zimmi48 merged 3 commits intorocq-prover:coq-roadmapfrom TheoWinterhalter:patch-1
Conversation
|
Thanks, @TheoWinterhalter! FWIW, in a recent private chat with @jfehrle, he was suggesting (and I agree) that explicating the main use cases would be really useful for readers who do not know about the feature, and to understand why this is an important feature which is on the roadmap. His example template was with rewrite rules:
On the other hand, since there is already a CEP about rewrite rules, maybe a link to it would be sufficient. In terms of technical details, I think this is also sufficient like this (referring to the CEP for additional detail / additional discussion). |
|
I tried to add a bit of that. :) |
|
Thanks! |
|
|
||
| #### Rewrite rules | ||
|
|
||
| The goal is to add (unsafe) user-defined rewrite rules. This features allows users to add computation rules to axioms which can be useful for prototyping. It also allows for different kinds of computation rules with respect to what Coq currently permits: non-linearity, overlapping left-hand sides (*eg* one can write an addition on natural numbers that reduces on both sides: `0 + n` and `n + 0` both reducing to `n`). |
There was a problem hiding this comment.
"prototyping" isn't mentioned in the CEP (#50). It suggests that there are later steps to make something "final" or "production". Perhaps you could explain what you have in mind in the CEP with a brief explanation of those later steps?
What fraction of our users will be willing/able to use this feature for important projects if it's unsafe?
I assume prototyping is meant for users and not just Coq developers.
There was a problem hiding this comment.
I don't understand why it should be mentioned in the CEP. These are just examples of what people want to do with rewrite rules: in particular we already have people using the fork of @yannl35133 to try out various type theories that are not otherwise encodable in Coq.
This use case has nothing to do with the status of rewrite rules.
It is true however, that the first instance we propose is something that is unsafe—in the sense that Coq may not terminate, or be incomplete for conversion if the user did not choose the right rewrite rules—and that the user must know that. To me this is the same as unsetting guard checking or using Type : Type, these are features used by actual people in actual projects even though they are not safe.
There was a problem hiding this comment.
It's that "prototyping" is unclear. As I said:
It suggests that there are later steps to make something "final" or "production".
What are those steps? Or is it a misleading choice of word? Can you clarify?
There was a problem hiding this comment.
I think there is a misunderstanding. A user may want to use rewrite rules for prototyping before they actually implement something, but it's up to the user so I don't have to explain the steps for this hypothetical user work.
|
@Zimmi48 FWIW, the rendering where you quote me above omitted "make it possible/much easier to do <some technical thing>". This '<' needed to have a backslash escape :-( |
3 participants
I'm not entirely sure about style so I did something. Please tell me whether this is what you expected or not.