Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft rewrite rules for 069-coq-roadmap.md #70

Merged
merged 3 commits into from
Jul 19, 2023
Merged

Draft rewrite rules for 069-coq-roadmap.md #70

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a3d8194
Draft rewrite rules for 069-coq-roadmap.md
TheoWinterhalter Jul 18, 2023
35f6767
069 coq roadmap: sell a bit more rewrite rules
TheoWinterhalter Jul 19, 2023
0d72bfc
Update text/069-coq-roadmap.md
Zimmi48 Jul 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions text/069-coq-roadmap.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,12 @@ to add and remove items, to reflect the evolution of the project.

#### 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`).
Copy link
Member

@jfehrle jfehrle Jul 19, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should be supported by unification and the main reduction machines (not `vm_compute` and `native_compute` for now, Coq should give a warning when those are used with rewrite rules on). Rewrite rules would propagate to any module that requires the module that defines them.

- Working Coq fork: https://github.com/Yann-Leray/coq (examples in https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v).
- CEP: https://github.com/coq/ceps/pull/50
- Yann Leray, Théo Winterhalter
- 3 to 6 month

Expand Down