Stream: math-comp users

Topic: Output not accepted as input


view this post on Zulip Julien Puydt (Nov 07 2022 at 11:31):

Here is an interesting situation:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Foo.

Variables a b c: bool.

Check a ==> b ==> c. (*  [==> a, b => c]: bool *)
Check ([==> a, b => c]).  (* refused: syntax error! *)

End Foo.

so some object gets output in some way, but can't be input like this.

Is it a non-issue? a known issue?

view this post on Zulip Pierre Roux (Nov 07 2022 at 11:58):

Note that [ ==> a, b => c] seems to work. Looks like a bug to me. Note that, since the notation is defined in this file https://github.com/coq/coq/blob/master/theories/ssr/ssrbool.v , if you report/fix the bug, it should be reported/fixed in Coq (not mathcomp).

view this post on Zulip Paolo Giarrusso (Nov 07 2022 at 12:15):

Does the bug still occur if you only import ssrbool.v? Or is it caused by some other import that adds conflicting notations?

view this post on Zulip Ana de Almeida Borges (Nov 07 2022 at 12:30):

Not this case, but I think there can be printing-only notations.

view this post on Zulip Pierre Roux (Nov 07 2022 at 12:49):

Paolo Giarrusso said:

Does the bug still occur if you only import ssrbool.v? Or is it caused by some other import that adds conflicting notations?

No, same thing with only ssrbool.v imported (and the prelude).

view this post on Zulip Pierre Roux (Nov 07 2022 at 16:36):

So I don't understand what happens here. If I just try

Local Open Scope bool_scope.

Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0,
  format "'[hv' [ ==> '['  b1 , '/'  b2 , '/'  .. , '/'  bn ']' '/'  =>  c ] ']'").

Notation "[ ==> b1 , b2 , .. , bn => c ]" :=
  (implb b1 (implb b2 .. (implb bn c) .. )) : bool_scope.

Section Foo.

Variables a b c : bool.

Check [ ==> a, b => c].
Check [==> a, b => c].  (* Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]). *)

whereas

Local Open Scope bool_scope.

Reserved Notation "[==> b1 , b2 , .. , bn => c ]" (at level 0,
  format "'[hv' [==> '['  b1 , '/'  b2 , '/'  .. , '/'  bn ']' '/'  =>  c ] ']'").

Notation "[ ==> b1 , b2 , .. , bn => c ]" :=
  (implb b1 (implb b2 .. (implb bn c) .. )) : bool_scope.

Section Foo.

Variables a b c : bool.

Check [ ==> a, b => c].
Check [==> a, b => c].  (* Error: Unknown interpretation for notation "[==> _ , _ , .. , _ => _ ]". *)

summoning @Hugo Herbelin who is the expert on notations.

view this post on Zulip Notification Bot (Nov 07 2022 at 16:53):

Julien Puydt has marked this topic as unresolved.

view this post on Zulip Julien Puydt (Nov 07 2022 at 16:56):

If the discussion goes on here, I should unmark the topic as closed.

Are those notations actually used enough to warrant having them?

view this post on Zulip Enrico Tassi (Nov 07 2022 at 19:56):

it is probably the [= notation which make this a token and breaks [==> by tokenizing it the wrong way

view this post on Zulip Pierre Roux (Nov 07 2022 at 20:03):

Yes and even if it is not used much (nobody complained until now), it's still a bug. So if it's easy to fix, let's fix it.

view this post on Zulip Julien Puydt (Nov 08 2022 at 06:06):

If those notations are both useless and problematic, why not get rid of them?

view this post on Zulip Enrico Tassi (Nov 08 2022 at 07:25):

yea, the fix seems to be to declare it as [= => for parsing, but I did not try

view this post on Zulip Pierre Roux (Nov 08 2022 at 10:25):

There seems to be a better fix: https://github.com/coq/coq/pull/16788


Last updated: Feb 08 2023 at 08:02 UTC