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

[JasonGross]

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

• 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.

[gares]

Apparently there is a conflict in fintype

[JasonGross]

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]). *)

[CohenCyril]

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

[herbelin]

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.

[herbelin]

@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)].

[JasonGross]

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]

@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,

[JasonGross]

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)?

[JasonGross]

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

[JasonGross]

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 *)

[JasonGross]

Updated PR, seems to be working

[JasonGross]

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?

[CohenCyril]

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.

[JasonGross]

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

[proux01]

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

[JasonGross]

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

[JasonGross]

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

[JasonGross]

And now there is no CI?

[JasonGross]

Overlay for monomials: math-comp/multinomials#73

[JasonGross]

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?

[JasonGross]

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.)

[JasonGross]

Ah, maybe if someone merges math-comp/odd-order#46 then this PR will work (finally) as-is