Unifying the syntax of Definition, Theorem, Fixpoint and CoFixpoint (CEP #42)

[herbelin]

This PR is a first attempt at implementing rocq-prover/rfcs#42. It parses all of Definition/Theorem/Fixpoint/CoFixpoint using the same grammar, and, in particular, it supports:

Theorem foo : True := I.

or even:

Theorem f n {struct n} := match n with 0 => 0 | S n => S (f n) end .

The interpretation is still dispatched into a few commands:

• ComDefinition.do_definition_interactive
  • calling Declare.Proof.start_definition
• ComDefinition.do_definition which itself splits into:
  • Declare.Obls.add_definition (Program mode)
  • Declare.declare_definition (regular mode)
• ComFixpoint.do_mutually_recursive which itself splits into:
  • Declare.Proof.start_mutual_definitions (interactive)
  • Declare.Obls.add_mutual_definitions (Program mode)
  • Declare.declare_mutual_definitions (regular mode)

which could be merged further. For instance, the recursivity might just be a flag to a regular definition (as in let rec vs let in OCaml).

The vtmodifyprogram/vtopenproof dispatch is done in a rather heavy way which should be simplified.

The PR is complementary to #19029 which implements attributes sealed/unsealed.

A choice of default opacity for Theorem := is easy to do, it is in function ComDefinition.opacity_of_logical_kind.

• add tests for the different combinations
• add support for e.g. Coercion f n {struct n} := match n with 0 => 0 | S n => S (f n) end., or mutual coercions, or Instance f n {struct n} := match n with 0 => 0 | S n => S (f n) end.?
• documentation to update
• improve parsing of {measure ...}, {struct ...} and {wf ...} so that they can also be used as variable names

Incidentally fixes #19593.

Depends on:

• Move code for interactive definitions close to the one for non interactive definitions #19260
• Slightly rewording the documentation of Theorem, Definition and Fixpoint #19766

Synchronous overlays:

• Adapt to Coq PR #19301: unify the syntax of definition and theorem vsrocq#932
• Adapt to Coq PR #19301: unify the syntax of definition and theorem ejgallego/rocq-lsp#869
• Adapt to Coq PR #19301 which unifies the syntax of Theorem, Definition and Fixpoint uds-psl/autosubst-ocaml#21
• Adapt to Coq PR #19301 which unifies the syntax of Theorem, Definition and Fixpoint LPCIC/coq-elpi#703

[coqbot-app]

🔴 CI failure at commit 0aff711 without any failure in the test-suite

✔️ Corresponding job for the base commit aa08d5a succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-elpi_hb

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.