Add "& T" syntax for anonymous binder "(_ : T)" and "of _ & _ & _" syntax for constructors

[proux01]

New syntactic sugar & T for anonymosu binder (_ : T) and of T & ... & T for constructors, enabling the Variant t := C1 of a & b & c | C2 x y of P x & Q y. syntax. This adds the new reserved keyword of.

This implements an old Coq call decision: https://github.com/rocq-prover/rocq/wiki/Coq-Call-2023-10-24 (just took me some time to get to it)

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged before the current PR)

• Adapt to https://github.com/rocq-prover/rocq/pull/21611 math-comp/analysis#1851
• Adapt to https://github.com/rocq-prover/rocq/pull/21611 arthuraa/deriving#37
• Adapt to https://github.com/rocq-prover/rocq/pull/21611 imdea-software/fcsl-pcm#56
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/fiat-crypto#2246
• Adapt to https://github.com/rocq-prover/rocq/pull/21611 math-comp/finmap#150
• Adapt to https://github.com/rocq-prover/rocq/pull/21611 math-comp/hierarchy-builder#576
• Adapt to https://github.com/rocq-prover/rocq/pull/21611 math-comp/math-comp#1538
• Adapt to https://github.com/rocq-prover/rocq/pull/21611 Mtac2/Mtac2#425
• Adapt to https://github.com/rocq-prover/rocq/pull/21611 Mtac2/Mtac2#426
• Adapt to https://github.com/rocq-prover/rocq/pull/21611 math-comp/odd-order#77

[SkySkimmer]

Do we really want Check (fun x of nat => x:bool). and so on to be accepted?

[SkySkimmer]

We could do something constructor specific instead with

modified   vernac/g_vernac.mlg
@@ -639,9 +639,16 @@ GRAMMAR EXTEND Gram
         { (oc,(idl,c)) } ] ]
   ;
 
+  constructor_binders: [[
+      l = binders -> { l }
+    | IDENT "of"; l = LIST1 term LEVEL "99" SEP "&" -> {
+        List.map (fun c -> CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)) l
+      }
+  ]];
+
   constructor_type:
-    [[ l = binders;
-      t= [ coe = of_type_inst; c = lconstr ->
+    [[ l = constructor_binders;
+       t = [ coe = of_type_inst; c = lconstr ->
                     { fun l attr id -> ((attr, fst coe, snd coe),(id,mkProdCN ~loc l c)) }
             |  ->
                  { fun l attr id -> ((attr,NoCoercion,NoInstance),(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None)))) } ]

(and then "of" doesn't need to be keyword AFAICT)

[proux01]

Do we really want Check (fun x of nat => x:bool). and so on to be accepted?

Yes (of course not with nat but think about phantom types for instance), combinations like & A of B & C are more dubious though, we could enfore that of can only be used at the beginning.

[SkySkimmer]

Yes

Really? You don't think that fun x of nat => seems like it should mean fun (x : nat) => but actually means fun (x : _) (_ : nat) =>?

[proux01]

No (it's not fun x of type nat =>)

[SkySkimmer]

You don't think that of sounds like it's connecting x and nat?

[gares]

We use that notation in HB, nobody complained.

Said that, I think of needs to be a keyword if you want that to work, even in constructors we use it after some initial binders as in K x of x != 0, IIRC.

[proux01]

You don't think that of sounds like it's connecting x and nat?

No, fun and of are both "keywords" (colored the same way by my editor) making of "match" with fun rather than x.

We use that notation in HB, nobody complained.

it is even more widely used in the mathcomp ecosystem for long, including code not developed by the usual mathcomp team.

Said that, I think of needs to be a keyword if you want that to work, even in constructors we use it after some initial binders as in K x of x != 0, IIRC.

Technically, Gaëtan may be right that we don't strictly need to register of as a keyword (CI will confirm). Whether it is the right thing to do, I don't know.

[SkySkimmer]

It doesn't need to be a keyword in my proposed diff where it only works if used immediately after the constructor name, which doesn't support the example @gares gave.

[proux01]

Did anyone consider not using of in the first place? That is, just use fun x & nat => instead?

The overlay cost on ssreflect users is not totally negligible (for instance: 410 lines in MathComp, 167 lines in Analysis, 151 lines in HB,...) but was deemed acceptable, so let's go for that.

Maybe a bit strange that we can still write C & foo of bar for constructors (IIUC) but probably nobody does that

Yes, I thought about that, but forbidding it would bring non negligible complexification/duplication in mlgs, so probably not worth it.

[SkySkimmer]

@coqbot merge now

[proux01]

Thanks