use Program less in stdlib

[andres-erbsen]

• replace all uses of Program mode with refine; abstract
• Import as little of Program as possible
• prefer non-program tactics when straightforward
• keep Require statements for compat (for now)

[andres-erbsen]

@coq/stdlib-maintainers This looks feasible, please review.

@coq-community/coq-dpdgraph CI contacts @Karmaki @ybertot: it seems that the coq-dpdgraph test suite compares stdlib definition graph to a golden reference stored outside stdlib, and that reference currently includes identifier names gensym-ed by Program. I could update the blessed reference, but is this level of coupling intentional and still desired for a coq-community-maintained project?

[silene]

I think that this pull request makes a good case for why Program is still meaningful nowadays. Sure, there were some places where Program was abusively used, e.g., PeanoNat.v, and they are worth a separate pull request that can be merged immediately. But all the places where you had to use a multi-tactic abstract tactic feel like a severe regression to me and show that Next Obligation is still worth its ugly syntax.

Also, keeping Next Obligation does not mean that we have to keep the implicit dependency on axiom K and the likes.

[ppedrot]

Maybe we can wait for the merge of #19023 to take advantage of the abstract selector.

[silene]

Good point. That would certainly make my objection moot. And it would actually be a good way to exercise the abstract selector.

[ppedrot]

I don't think we're in a hurry to get rid of Program, contrarily to the plugin whose name must not be uttered, that starts with fun and ends in ind. This command is used for several distinct reasons:

• Separating a computational skeleton (in Gallina) from its proof obligations (using tactics).
• In particular, proof obligations can be Qed-ed.
• Writing fancy dependently-typed recursive functions, i.e. the measure / wf and subset type features of Program.

The problematic stuff that is superseded by Equations is the third point. The two first points are legitimate even without the magic Program features. In particular, they are part of the short-term roadmap to reimplement the abstract tactical directly in the proof engine and would be subsumed by this.

As a result, I'd recommend waiting for the landing of the reimplemented abstract before touching anything Program-related in the stdlib.

[ybertot]

Concerning coq-dpdgraph, the differences that appear in the graph seem to have low significance. The normal way to proceed would be to accept the new version of the graph as the future reference. Normally, the coq-dpdgraph environment provides a way to do that in a few steps.

I don't remember why it was important to test coq-dpdgraph in conjunction with the Setoids machinery, but if the latter is in stdlib, then it makes sense that coq-dpdgraph depends on it. If it turns out to be a nuisance, we may need to come up with lower this nuisance in two ways:

• make the comparison ignore some aspects of the graph (any node outside a pre-defined set of identifiers, weight of arrows, numbering)
• remove this specific test altogether, but I think this should be the last resort.

[andres-erbsen]

I agree with the summary by @ppedrot, but there is a catch that makes me still lean towards ditching Program entirely asap: as far as I understand, it is not possible to use "Program just for separating computation from proof obligations"; it will translate your code and run globally-specified tactics even if you just wanted the code-structuring features. I agree having another mechanism for specifically the desired part would be nice (and I'm hoping for #[transparent] Definition with #[sealed] Lemma rather than abstract:{ ) but IMO that's still easier to migrate to after this PR than before it.

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

[proux01]

Stdlib is now in its own repo: https://github.com/coq/stdlib , if this PR is still current, please reopen it there.