Stream: Coq users

Topic: Recursive notation in terms of another?


view this post on Zulip Shea Levy (Oct 16 2020 at 16:25):

In trying to define one recursive notation in terms of another, I had:

Notation "[ h , g , .. , f ]" := (.. ([h] :: g) .. :: f) : comp_arg_scope.
Fail Notation "h ⊙ g ⊙ .. ⊙ f" := (compose ([ h, g .. f .. ])) (at level 40, no associativity).
Notation "h ⊙ g ⊙ .. ⊙ f" := (compose (.. ([h] :: g) .. :: f)) (at level 40, no associativity).

Is there any way to make the middle line not fail? I tried placing commas in various places, including exactly matching the LHS of the first line, to no avail.

view this post on Zulip Hugo Herbelin (Oct 16 2020 at 19:15):

Shea Levy said:

In trying to define one recursive notation in terms of another, I had:

Notation "[ h , g , .. , f ]" := (.. ([h] :: g) .. :: f) : comp_arg_scope.
Fail Notation "h ⊙ g ⊙ .. ⊙ f" := (compose ([ h, g .. f .. ])) (at level 40, no associativity).
Notation "h ⊙ g ⊙ .. ⊙ f" := (compose (.. ([h] :: g) .. :: f)) (at level 40, no associativity).

Is there any way to make the middle line not fail? I tried placing commas in various places, including exactly matching the LHS of the first line, to no avail.

Is this important that the second line works for you? What is not satisfactory with the third line?

I don't know if it is what you are looking for but a working variant of the second could be:

Notation "h ⊙ g ⊙ .. ⊙ f" := (compose ([ .. [h, g] .., f ])) (at level 40, no associativity).

view this post on Zulip Shea Levy (Oct 16 2020 at 19:25):

Hugo Herbelin said:

Shea Levy said:

In trying to define one recursive notation in terms of another, I had:

Notation "[ h , g , .. , f ]" := (.. ([h] :: g) .. :: f) : comp_arg_scope.
Fail Notation "h ⊙ g ⊙ .. ⊙ f" := (compose ([ h, g .. f .. ])) (at level 40, no associativity).
Notation "h ⊙ g ⊙ .. ⊙ f" := (compose (.. ([h] :: g) .. :: f)) (at level 40, no associativity).

Is there any way to make the middle line not fail? I tried placing commas in various places, including exactly matching the LHS of the first line, to no avail.

Is this important that the second line works for you? What is not satisfactory with the third line?

I don't know if it is what you are looking for but a working variant of the second could be:

Notation "h ⊙ g ⊙ .. ⊙ f" := (compose ([ .. [h, g] .., f ])) (at level 40, no associativity).

The only thing with the third line is that it's repeating what I already have on the first. But your example works, thanks! Now to understand it....

view this post on Zulip Hugo Herbelin (Oct 16 2020 at 19:54):

Now to understand it....

Technically, any occurrence of .. c .. in the right-hand side is interpreted as c together an indication that this has to be the end of a recursive pattern.

When you write [ h, g .. f .. ], this is expanded to [h] :: (g f) together with the indication that f is the end of the pattern, but the application is certainly not what you want.

You may want (compose ([ h, g , .. f .. ])), but, in this case, this is expanded to ([h] :: g) :: f with the indication that f is the end of the pattern.

Being the end of the pattern means being able to find a context ψ, an iterator φ, and a tail u such that ([h] :: g) :: <hole> is ψ(φ(<hole>)) and f is φ(u). Coq fails to find one. As a matter of fact, it is actually not possible to find such a φ when the end of the pattern is just a variable.


Last updated: Feb 01 2023 at 13:03 UTC