Add notations for patterns in `[seq ... | ... ]` notations

This allows syntax such as

Check [seq '(x, y) <- List.combine (List.seq 0 5) (List.seq 0 5) | x == y ].
Check [seq x + y | '(x, y) <- List.combine (List.seq 5 5) (List.seq 5 5) ].

to parse and print.

Motivation for this change

Without this change,

Check map (fun '(x, y) => x + y) (zip (iota 0 5) (iota 0 5)).

prints as the ugly

[seq (let '(x, y) := pat in x + y) | pat <- zip (iota 0 5) (iota 0 5)]

instead of the much more understandable

[seq x + y | '(x, y) <- zip (iota 0 5) (iota 0 5)]

Things done/to do

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries)
• ~added corresponding documentation in the headers~ (Do I need to do this? I think it's not relevant here? Can someone confirm?)

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

Apparently there is a conflict in fintype

I think I need @herbelin 's help in how to factor notations so that they work:

Require Import Coq.Lists.List.
Declare Scope seq_scope.
Open Scope seq_scope.
Notation "[ 'seq' E | i <- s ]" := (map (fun i => E) s)
  (at level 0, E at level 99, i binder,
   format "[ '[hv' 'seq'  E '/ '  |  i  <-  s ] ']'") : seq_scope.
Check [seq ?[F] i | i <- ?[enum] ?[P] ].
Reserved Notation "[ 'seq' F | x : T ]"
  (at level 0, F at level 99, x ident,
   format "'[hv' [ 'seq'  F '/ '  |  x  :  T ] ']'").
Check [seq ?[F] i | i <- ?[enum] ?[P] ].
(* Error: Syntax error: ':' expected after [name] (in [term]). *)

Hi @JasonGross @herbelin any hope to make this PR go forward?

Hi,

At first view, supporting [ 'seq' E | i <- s ] with i a binder would require to change x to binder also in [ 'seq' F | x : T ] but the latter does not seem easy to generalize because the x : T has apparently a more complex interpretation than just being a binder, see the in pred_of_simpl (@pred_of_argType T) part (what would go wrong actually by replacing this part with fun x : T => true, in which case we would get the generalization easily?).

Assuming that there is no easy way to reformulate pred_of_simpl (@pred_of_argType T) under a form referring to x : T rather than to only T, what could be tried is to only add [ 'seq' E | ' i <- s ] with i pattern, rather than generalizing [ 'seq' E | i <- s ] to i binder.

Hoping that it helps.

@CohenCyril: we would need your help to know if there is a way to reformulate pred_of_simpl (@pred_of_argType T) under a form referring to x : T rather than to only T in notation [ 'seq' F | x : T ] := [seq F | x : T in pred_of_simpl (@pred_of_argType T)].

reformulate pred_of_simpl (@pred_of_argType T) under a form referring to x : T rather than to only T in notation

@herbelin What about using the match trick for substitution to do (fun A (a : A) => A) _ (x : T)) in a way that does not leave a beta redex? (I can code up a solution that does this the next time I'm at a computer; I don't have in my head an accurate model of which zeta-redexs unification will unfold and in what order, when it needs to perform evar unification.)

@herbelin What about using the match trick for substitution to do (fun A (a : A) => A) _ (x : T)) in a way that does not leave a beta redex? (I can code up a solution that does this the next time I'm at a computer; I don't have in my head an accurate model of which zeta-redexs unification will unfold and in what order, when it needs to perform evar unification.)

I don't know if that'll work. We need x : T to occur in position of binder so that when substituted with something such as 'pat it continues to make sense,

We need x : T to occur in position of binder so that when substituted with something such as 'pat it continues to make sense,

What about the equivalent of (fun A (a : A -> True) => A) _ (fun x : T => I)?

(Of course the match form will never be used for printing, I don't know if that is an issue)

What about the equivalent of (fun A (a : A -> True) => A) _ (fun x : T => I)?

Notation "'type_of' x"
  := match _, (fun x => I) with
     | T, f
       => match match f return T -> True with f' => f' end with
          | _ => T
          end
     end
       (x binder, only parsing, at level 20).
Check type_of x : nat. (* nat *)
Check type_of '((x, y) : nat * nat). (* (nat * nat)%type *)

Updated PR, seems to be working

Two issues seem to arise:

1. This change is incompatible with Coq 8.11 and Coq 8.12. With mathcomp be dropping support for these versions on master anytime soon?
2. multinomials fails with

File "./src/freeg.v", line 207, characters 37-38:
Error:
In environment
G : zmodType
K : choiceType
s : seq (G * K)
x : K
The term "x" has type "Choice.sort K" while it is expected to have type
 "(?A * ?B)%type".

at https://github.com/math-comp/multinomials/blob/200ef66f7f892814dc7b9254f4f23bc7f59de093/src/freeg.v#L207 which is

Definition predom s: seq K := [seq x.2 | x <- s].

with

Variable G : zmodType.
Variable K : choiceType.
Implicit Types s   : seq (G * K).
Implicit Types x y : K.

The issue is that Coq now infers x : K rather than x : _ * _. There's an easy backwards-compatible fix of changing x to v on that line; is that acceptable?

1. This change is incompatible with Coq 8.11 and Coq 8.12. With mathcomp be dropping support for these versions on master anytime soon?

Coq 8.11 I think we can do it for the next release, for Coq 8.12 we might have to wait a few more month but eventually yes.

Oops, I closed and reopened to restart the CI, and coqbot removed the 1.15.0 milestone :-(

@JasonGross mathcomp now requires Coq >= 8.13, does that help here?

This PR was discussed during the last MathComp meeting (https://github.com/math-comp/math-comp/wiki/Minutes-January-11-2023) and has been considered for merging. @JasonGross Could you rebase it? Thank you.

Sorry, this fell off my todo list, I'll try to rebase shortly

I've rebased, but the CI seems extremely unhappy.

And now there is no CI?

Overlay for monomials: https://github.com/math-comp/multinomials/pull/73

I'm confused by the error in odd-order: File "./theories/PFsection3.v", line 335, characters 17-19: Error: Syntax error: ''' or [term level 99] expected after 'seq' (in [term]).

I cannot reproduce this locally. Can anyone else reproduce this?

I'm confused by the error in odd-order: File "./theories/PFsection3.v", line 335, characters 17-19: Error: Syntax error: ''' or [term level 99] expected after 'seq' (in [term]).

I cannot reproduce this locally. Can anyone else reproduce this?

Ah, this only occurs with Coq 8.13. Is odd-order planning to drop support for Coq 8.13 anytime soon? (The rest of the ecosystem seems to build fine.)

Ah, maybe if someone merges https://github.com/math-comp/odd-order/pull/46 then this PR will work (finally) as-is