Add parsing and interpretation of elimination constraints

[jrosain]

This PR adds the parsing of elimination constraints as defined in the RFC rocq-prover/rfcs#111.

In particular, it adds the possibility to have sort-level constraints in definitions:

Definition foo@{s s'; | s -> s'} ...

and for global sorts.

Sort s s'.
Constraint s -> s'.

• Added / updated test-suite.

• Added / updated documentation.
  • Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged in sync with the upstream PR)

• Adapt to rocq-prover/rocq#21195 (parsing of elim constraints) mattam82/Coq-Equations#670
• Adapt to rocq-prover/rocq#21195 (add constraint kind when pushing context) rocq-community/coq-dpdgraph#156
• Adapt to rocq-prover/rocq#21195 (update univ constraints to prenex sort poly constraints) rocq-community/rocq-lean-import#47
• Adapt to rocq-prover/rocq#21195 (add quality constraint kinds) Mtac2/Mtac2#415
• Adapt to rocq-prover/rocq#21195 (add quality constraint kind) rocq-community/paramcoq#144
• Adapt to rocq-prover/rocq#21195 (add quality constraint kind) mit-plv/rewriter#182
• Adapt to rocq-prover/rocq#21195 (update evd API for UnivProblem) coq-tactician/coq-tactician#120
• Adapt to rocq-prover/rocq#21195 (Univ.ContextSet → PConstraints.ContextSet) impermeable/coq-waterproof#218
• Adapt to rocq-prover/rocq#21195 (Univ.ContextSet → PConstraints.ContextSet) MetaRocq/metarocq#1216
• Adapt to rocq-prover/rocq#21195 (Constraints->UnivConstraints, univ_decl->sort_poly_decl) LPCIC/coq-elpi#934
• https://gitlab.inria.fr/fbesson/itauto/-/merge_requests/19

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

something strange is going on in stdlib_test, the message from https://github.com/rocq-prover/stdlib/blob/e343c58314f5a902e08ec6a211f4e1b5812a8c89/test-suite/output/Fixpoint.v#L123 changed to say to produce a value in sort "Prop" even though the fixpoint is -> bool

[jrosain]

@coqbot run full CI

[jrosain]

@SkySkimmer how do i specify the itauto overlay (project on gitlab)? I tried to do the same stuff as for the others but it didn't work.

Also, I don't know how to fix the refman problem, which comes from this snippet:

.. insertprodn universe_name sort_poly_constraint

.. prodn::
   universe_name ::= @qualid
   | Set
   | Prop
   univ_annot ::= @%{ {* @univ_level_or_quality } {? {| %| | ; } {* @univ_level_or_quality } } %}
   univ_level_or_quality ::= 0
   | Set
   | SProp
   | Prop
   | Type
   | _
   | @qualid
   sort_poly_decl ::= @%{ {? {* @ident } {| %| | ; } } {* @ident } {? + } {? %| {*, @sort_poly_constraint } {? + } } %}
   cumul_sort_poly_decl ::= @%{ {? {* @ident } {| %| | ; } } {* {? {| + | = | * } } @ident } {? + } {? %| {*, @sort_poly_constraint } {? + } } %}
   sort_poly_constraint ::= @universe_name {| < | = | <= } @universe_name
   | @sort_quality_var -> @sort_quality_var

(here, it doesn't know sort_quality_var). Any idea on how to fix this?

[mattam82]

For the grammar I think you need to follow the instructions on regenerating the files for the linting check between the .mlg's and the doc.
Relevant part of CONTRIBUTING.md:

- **Documented syntax is up-to-date**.  If you update the grammar, you
  should run `make doc_gram_rsts` to update the
  documented syntax.  You should then update the text describing the
  syntax in the documentation and commit the changes.  In some cases,
  the documented syntax is edited to make the documentation more
  readable.  In this case, you may have to edit
  `doc/tools/docgram/common.edit_mlg` to make `doc_gram_rsts` pass.
  See [doc_grammar's README][doc_gram] for details.

  Note that in the case where you added new commands or tactics, you
  will have to manually insert them in the documentation, the tool
  won't do that for you, although it should detect in most cases if you
  have forgotten to add documentation for your new command or tactic,
  or if the documentation is not consistent with the parser.

[SkySkimmer]

@coqbot run full ci

[mattam82]

I only have minor comments, I think we will need to play with this code and have a few iterations anyway to ensure its correctness. Just one thing, we don't touch the "broken" transitivity closure issue found by @tabareau here, right? If not I think this can be merged.

[mattam82]

The comment above the code becomes misleading if you don't change it. I think the solution is fine, but the comment should reflect it.

[mattam82]

Isn't this outdated? We have @{s;u} already in this branch no?

[SkySkimmer]

this is a note about the old syntax (which is still parsed)

[TDiazT]

Just one thing, we don't touch the "broken" transitivity closure issue found by @tabareau here, right?

I think it is being handled by the changes in RigidPaths, and checked in the test file test-suite/success/sort_poly_elim_rigid_paths.v.

[tabareau]

Just one thing, we don't touch the "broken" transitivity closure issue found by @tabareau here, right?

I think it is being handled by the changes in RigidPaths, and checked in the test file test-suite/success/sort_poly_elim_rigid_paths.v.

Yes, it has been fixed by Commit e28c9b8

[mattam82]

Great!

[mattam82]

@jrosain this needs a last rebase due to @ppedrot's PR on effects conflicting... I can help if you're busy, just tell me.

[jrosain]

Should be good now!

[mattam82]

@coqbot merge now

[coqbot-app]

@mattam82: You cannot merge this PR because:

• There is still a needs: fixing label.
• There is no kind: label.
• No milestone has been set.

[mattam82]

It's missing a changelog entry

[mattam82]

@jrosain ?

[jrosain]

Is this fine?

[mattam82]

Yes!

[mattam82]

@coqbot merge now

[coqbot-app]

@mattam82: You cannot merge this PR because:

• There is still a needs: changelog entry label.

[mattam82]

@coqbot merge now

[coqbot-app]

@mattam82: Please take care of the following overlays:

• 21195-jrosain-elimination-constraints.sh

[mattam82]

Overlay time!

[mattam82]

I pinged everyone

[ppedrot]

@fajb please merge the overlay on itauto, there is some backlog already.