From a3d819427155e6091df924033505cceb13c10762 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= Date: Tue, 18 Jul 2023 17:16:23 +0200 Subject: [PATCH 1/3] Draft rewrite rules for 069-coq-roadmap.md --- text/069-coq-roadmap.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index dec524c5..122640db 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -89,6 +89,10 @@ to add and remove items, to reflect the evolution of the project. #### Rewrite rules +The goal is to add (unsafe) user-defined rewrite rules. It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should 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 From 35f6767a4ef51c88e87ffb569f8a9a08c5c32bcb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= Date: Wed, 19 Jul 2023 15:01:11 +0200 Subject: [PATCH 2/3] 069 coq roadmap: sell a bit more rewrite rules --- text/069-coq-roadmap.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 122640db..b7ee7bd6 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -89,7 +89,9 @@ to add and remove items, to reflect the evolution of the project. #### Rewrite rules -The goal is to add (unsafe) user-defined rewrite rules. It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should 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. +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`). + +It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should 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 From 0d72bfcc9545aa8d819c4b6ce0002f847ef5fbf6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Wed, 19 Jul 2023 15:40:15 +0200 Subject: [PATCH 3/3] Update text/069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index b7ee7bd6..a4b912c8 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -91,7 +91,7 @@ to add and remove items, to reflect the evolution of the project. 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`). -It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should 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. +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