Add new tactic "ensatz" for proving polynomial equalities with existential quantifier

[lyonel2017]

This PR introduce the ensatz tactic that can prove automatically goals of the form:

$$\begin{array}{l} \forall X_1, \ldots, X_n \in A, \\\ P_1(X_1, \ldots, X_n) = Q_1(X_1, \ldots, X_n), \ldots, P_s(X_1, \ldots, X_n) = Q_s(X_1, \ldots, X_n) \\\ \vdash \exists Y_1, \ldots, Y_m \in A, P(X_1, \ldots, X_n) = Y_1 * Q'_1(X_1, \ldots, X_n) + \dots + Y_m * Q'_m(X_1, \ldots, X_n) \end{array}$$

Tests have be added to the test-suite in file test-suite/success/ENsatz.v.

• Added / updated documentation:

An entry to the sphinx documentation of Rocq is available here and ready for a PR.

• Added changelog.

[andres-erbsen]

This is an exciting feature. Would it be feasible to add this without another copy of the nsatz Ltac and especially the reification procedure? (Is this tactic intended to also prove all goals the previous one proves?)

[andres-erbsen]

Reading https://www.cl.cam.ac.uk/~jrh13/papers/divisibility.pdf theorem 5 i understand how to solve goals where Y_1..Y_m appear as linear-combination coefficients. Is the algorithm in this PR more general, or should Q(...) above be restricted more?

[lyonel2017]

Would it be feasible to add this without another copy of the nsatz Ltac and especially the reification procedure? (Is this tactic intended to also prove all goals the previous one proves?)

The ensatz tactic is not intended to replace the nsatz tactic. The ensatz tactic cannot solve goals without existential quantifier. Maybe there's a way to unify the two, but I can't see it at the moment. Especially, the part concerning the reifiction are quite different. But maybe I missed something.

[lyonel2017]

Reading https://www.cl.cam.ac.uk/~jrh13/papers/divisibility.pdf theorem 5 i understand how to solve goals where Y_1..Y_m appear as linear-combination coefficients. Is the algorithm in this PR more general, or should Q(...) above be restricted more?

You are right, Q(...) is restricted to the cases where Y_1 ... Y_m appear as linear-combination coefficients.

[SkySkimmer]

the entry point for reification is a typeclass Hint Extern, but the reification is ltac not typeclass based AFAIK

[lyonel2017]

I removed the line which was a left over from copying/pasting the NsatzTactic.v file.

[andres-erbsen]

I think there's a good chance a bunch of code could be shared. Whether it's worth it or not is for us to determine. But for example the hol-light implementation does seem to share code (examples).

[andres-erbsen]

I think it will be good having a tactic like this in stdlib. And I'd like to use it myself, both in stdlib and otherwise. At the same time, the proposed implementation provoked a number of initial responses and questions from me. This initial review is not complete and not everything here is requirement for merging, but I would like to hear your thoughts on these points and overall plan/goals.

Additionally, are you looking to keep using this tactic yourself, and where?

Edit: an important part of my context here is that I am a heavy user of nsatz and have spent a substantial amount of time fighting its implementation issues, including maintaining a part-reimplementation (in fiat-crypto). From this, my overall impression is that nsatz .v-file code is not something to be imitated, and every bit of this kind of in the repo is a liability (it is obviously also an asset). And not-thought-through implementation behaviors do tend to acquire rigid users, making them much harder to change later. rocq-prover/rocq#18325 is an example, #155 (comment) (WIP) is another.

[andres-erbsen]

Please check add the documentation and link to it here.

[lyonel2017]

I'm not sure I understand the remark. Is the changelog entry incomplete in terms of references to the new tactic's documentation? If so, I don't know how to proceed, since the documentation page for nsatz is in the Rocq project and not Stdlib. I wrote documentation for ensatz in my fork of Rocq.

[andres-erbsen]

My apologies for the broken sentence. Yes, I meant that it would be nice to have a documentation link in the changelog (and have it committed, somewhere). Example.

Where to actually put the documentation is indeed an interesting question. There are actually three plausible places: rocq refman, stdlib refman, and stdlib html+coqdoc documentation. And I'm not sure what the high-level plan is for documentation or ml-supported tactics in the rocq-stdlib split. But documenting next to nsatz (and making a linked PR) seems fine.

[andres-erbsen]

More tests would significantly increase my expectations of success for trying to use this tactic. E.g. the hol-light examples that are proven by INTEGER_TAC or INTEGER_RULE should be appropriate. If some of them don't work for a well-understood reason, documenting that is especially important.

[lyonel2017]

I've added a first batch of additional examples. Maybe I'll add a few more.

[andres-erbsen]

This procedure interleaves generalization of the goal over effective variables (from the perspective of ensatz) and the reification of it. For troubleshooting failing invocations, it is useful to be able to run the generalization phase without reification. (This also enables faster and more predictable reification methods.) Existing stdlib tactics do do something similar to the code here, and I am not going to hold this contribution to a hypocritically high standard, but I do genuinely believe it would be more useful if these steps were factored out.

[andres-erbsen]

Now that we have two calls to this function, it would be really nice to have at least a basic comment describing what it should and should not do.

[andres-erbsen]

Does this vm_compute always succeed if there are no bugs in this tactic? If yes, consider vm_cast_no_check (eq_refl true)

[andres-erbsen]

Is the intent to perform unification of all subterms of the entire goal with c here? If not, pose and change.

[lyonel2017]

Yes, it is intentional.

[andres-erbsen]

Is this the plan? Currently, the PR adds new tactic ensatz, without adding support for existential quantifiers to nsatz.

[lyonel2017]

I change the entry message.

[lyonel2017]

I think it will be good having a tactic like this in stdlib. And I'd like to use it myself, both in stdlib and otherwise. At the same time, the proposed implementation provoked a number of initial responses and questions from me. This initial review is not complete and not everything here is requirement for merging, but I would like to hear your thoughts on these points and overall plan/goals.

Additionally, are you looking to keep using this tactic yourself, and where?

Edit: an important part of my context here is that I am a heavy user of nsatz and have spent a substantial amount of time fighting its implementation issues, including maintaining a part-reimplementation (in fiat-crypto). From this, my overall impression is that nsatz .v-file code is not something to be imitated, and every bit of this kind of in the repo is a liability (it is obviously also an asset). And not-thought-through implementation behaviors do tend to acquire rigid users, making them much harder to change later. rocq-prover/rocq#18325 is an example, #155 (comment) (WIP) is another.

My original plan was to use this tactic in Easycrypt. It is not certain that this will happen in the end. I will apply patches to answer the question as best I can. The ongoing re-implementation of nsatz is in conflict with ensatz and will require more time to patch.

[andres-erbsen]

The ongoing re-implementation of nsatz is in conflict with ensatz and will require more time to patch.

Just to be clear, I am not asking you to step in to resolve the situation with nsatz being duplicated in stdlib and fiat-crypto. And my plan there is to backport fixes from fiat-crypto in small minimally invasive changes, hopefully reaching a state where stdlib nsatz fits both use cases. The reason I am pointing out this duplication is to advocate for avoiding further duplication within stdlib: code shared between ensatz and nsatz will benefit from these backports, whereas dedicated ensatz code will not.

[lyonel2017]

I created a file ZENsatz.v to have ensatz for ZArith. The file is almost identical to ZNsatz.v. I have the impression that merging both files would be better.

[andres-erbsen]

Indeed, merging seems preferable to duplicating opaque-yet-relevant instances. Though, maybe ensatz just works (for Z) when ZNsatz is imported.

[andres-erbsen]

After reading the documentation, there's one more thing on my mind: the e prefix is generally used for tactics that instantiate create existential variables. I understand the code currently in this PR doesn't do that, but could it? E.g. Goal forall x : Z, { y : Z | y = x}. esplit. abstract ensatz. Defined.? IIUC the underlying algorithm does compute a witness, and the limitation is in the reification mechanism. I think the name is neat, and yet it would be inconsistent with current usage, unless we implemented this feature. exists_nsatz sounds much less fun.

[SkySkimmer]

there's one more thing on my mind: the e prefix is generally used for tactics that instantiate existential variables.

I wouldn't say so (other than refining the goal evar as all tactics do). For instance what evars does esplit in your example instantiate?
Rather the e prefix is used when the tactic creates new shelved evars. For instance apply -> new evars are all subgoals, eapply -> some of the new evars may be shelved.

[lyonel2017]

I have the impression that even if the ensatz tactic would supports examples such as Goal foall x:Z,{y:Z|y=x}, the name ensatz remains inconsistent with the current naming convention. One solution would be to merge nsatz and ensatz, i.e. add the capabilities of ensatz to nsatz, as the original name of this PR suggested.

[andres-erbsen]

Agreed. Overall, my intuition is that merging ensatz and nsatz would be great, both for user experience and (I hope) maintenance. Do you think it would be practical?

As for support for sig, I feel like building that specifically probably isn't worth it. I would welcome support for instantiating existing existential variables, primarily so I can call nstaz from/after scripts that leave behind evars without rewriting these scripts to work under existential quantifiers using setoid_rewrite.

[andres-erbsen]

On a third thought, isn't the difference between ensatz (with the proposed change to operate on evars) and nsatz pretty much the same as between eassumption and assumption? It' s possible that eassumption is an outlier though.

[lyonel2017]

Apparently, the auto and eauto tactics are another exception. Perhaps it's acceptable to have nsatz and ensatz?

I will give a try to add support for instantiating existential variables.

[lyonel2017]

I finally found the time to add the support for existential variables. I still have to refactor the code a bit and complete the documentation.

The source of the error in the CI is not clear to me.