Jerome Hugues (Mar 13 2024 at 01:16): Jerome Hugues (Mar 13 2024 at 01:16):Hi,
I am experimenting with the rewrite rules to be introduced in future Coq 8.20 .
The following code does not parse, with the following error : Error: Syntax error: '==>' expected after [rw_pattern] (in [rewrite_rule]).
From mathcomp Require Import ssrbool.
Symbol pplus : nat -> nat -> nat.
Notation "a ++ b" := (pplus a b).
Rewrite Rule pplus_rewrite :=
| ?n ++ 0 ==> ?n
| ?n ++ S ?m ==> S (?n ++ ?m)
| 0 ++ ?n ==> ?n
| S ?n ++ ?m ==> S (?n ++ ?m).
ssrbool defines ==> as a reserved notation, and this confuses the parser. And per https://coq.inria.fr/doc/master/refman/user-extensions/syntax-extensions.html?highlight=notation#enabling-and-disabling-notations , reserved notations cannot be disabled, so Disable Notation "==>" (all). is inoperent.
Do you have any suggestion? Shall this be reported through GitHub or moved to coq-devs zulip channel?
Thanks
Yann Leray (Mar 14 2024 at 19:04):Sorry for the late reply. I have a PR to replace ==> with >-> since this should have fewer conflicts (#18808)
Pierre Roux (Mar 14 2024 at 19:08):Why not just =>? (like in the match construct)
Jerome Hugues (Mar 14 2024 at 19:22):Pierre Roux said:
Why not just
=>? (like in the match construct)
This approach is likely to be free of future conflicts, isn't it?
Pierre Roux (Mar 14 2024 at 19:27):Sounds much more robust to me yes.
Jerome Hugues (Mar 14 2024 at 19:29):Looking at the patch, it seems >-> is used also for coercions. Wouldn't the proposed patch conflicts there? (I acknowledge
a rewrite rule on a term with coercions could be meaningless, but never doubt user's inventiveness)
Gaëtan Gilbert (Mar 14 2024 at 19:43):>-> is used in the Coercion command and in the Rewrite Rule command, they're separate commands so no conflict
Jerome Hugues (Mar 15 2024 at 01:01):Make sense, thanks.
For the record, there are instances of notations with >->, with other tokens. involved I am the opinion that these notations should not interfere, but it is worth a second opinion.
jjhugues@mac-pepperapple coq % grep -r ">->" . |grep Nota
./math-comp/mathcomp/fingroup/morphism.v:Notation "{ 'morphism' D >-> T }" := (morphism_for D (Phant T))
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Notation "{ 'morph' f : x / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'morph' f : x y / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'homo' f : x / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'homo' f : x y / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'mono' f : x / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'mono' f : x y / a >-> r }" :=
those are parenthesized so don't interfere
Notification Bot (Mar 18 2024 at 00:00):Jerome Hugues has marked this topic as unresolved.
Gaëtan Gilbert (Mar 18 2024 at 09:42):I think you need to write your own logic for this. Something like multimatch goal with H : _ |- _ => exact H end
Jerome Hugues (Mar 18 2024 at 13:27):Gaëtan Gilbert said:
I think you need to write your own logic for this. Something like
multimatch goal with H : _ |- _ => exact H end
Does this apply to this discussion thread @Gaëtan Gilbert ?
Gaëtan Gilbert (Mar 18 2024 at 13:29):no, should be https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Backtracking.20and.20assumption.20.28without.20using.20Ltac.29
Last updated: Oct 13 2024 at 01:02 UTC