Stream: Coq users

Topic: Coq 8.20 rewrite rules and reserved notations from ssrbool


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Pierre Roux (Mar 14 2024 at 19:08):

Why not just =>? (like in the match construct)

view this post on Zulip 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?

view this post on Zulip Pierre Roux (Mar 14 2024 at 19:27):

Sounds much more robust to me yes.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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 }" :=

view this post on Zulip Gaëtan Gilbert (Mar 15 2024 at 07:53):

those are parenthesized so don't interfere

view this post on Zulip Notification Bot (Mar 18 2024 at 00:00):

Jerome Hugues has marked this topic as unresolved.

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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: Jun 22 2024 at 14:01 UTC