Adapt with respect to rocq-prover/rocq#21371

[tabareau]

This time the change should be backward compatible with 8.19.

[jdchristensen]

@tabareau It looks like our CI is happy, except for dev versions (because the new Rocq PR is not applied in our CI). Feel free to remove references to the internal lemma if that helps make this work.

And if I'm reading this PR correctly, it's just a single-line change, which is very reasonable.

[jdchristensen]

Here's a link to the Rocq fix that makes things backwards compatible, which is now merged: rocq-prover/rocq#21371

I've restarted the failed jobs to see if our CI will pull in the merged changes.

[tabareau]

Indeed, I managed to make it a single line change in the end.

However, we can't remove the references to the internal lemma as it would probably not be backward compatible.

[jdchristensen]

Ok, the dev jobs were successful. @tabareau Thanks for making the Rocq changes backwards compatible!

The failing jobs are probably because I only restarted the failed jobs, so I think this is good to merge.

[jdchristensen]

However, we can't remove the references to the internal lemma as it would probably not be backward compatible.

I'm pretty sure we don't use these anywhere. In any case, we'll be sure to revamp this code when 9.2 is our lowest supported version. In fact, I should add a comment to this PR saying this. Let me do that in a couple of hours, and then I'll merge.

[tabareau]

Indeed, it seems you don't use it, do you want me to update the PR so that it is removed ?

[jdchristensen]

I'd like to keep the code involving internal wrappers for now, until we officially bump our minimum version high enough. But I would like to update the comment near where they are generated in Overture.v. It currently says:

(** TODO: Since Coq 8.20 has PR#18299, once that is our minimum version we can instead register wrappers for [transport] to be used for rewriting.  See the comment by Dan Christensen in that PR for how to do this.  Then the tactics [internal_paths_rew_to_transport] and [rewrite_to_transport] can be removed from ../Tactics.v. *)

rocq-prover/rocq#18299 introduced being able to register what is used for rewrite. Can you explain to me what rocq-prover/rocq#21098 adds in addition to the earlier PR, so I can update this comment in a sensible way? I plan to also reference the reverted Coq-HoTT PR #2331 to illustrate how this mechanism works.

[tabareau]

It adds a general mechanism using typeclasses instead of predefined registered names, and it allows to use elimination for other sorts than Prop and Type in a sort polymorphic setting. Maybe not yet relevant in your case.

[jdchristensen]

@tabareau Thanks, that's a good summary. Has the registration method been removed? If so, then it will be hard to for us to be compatible with both 9.1 and 9.2 if we want to be able to provide our own terms to be used for rewriting...

[tabareau]

No it is still there, but now used more consistently (before, discriminate was not using it for instance)

[tabareau]

I have a PR doing on your code and probably backward compatible as well, do you want me to test it (I can remove it if it breaks on 8.19) ?

[jdchristensen]

I have a PR doing on your code and probably backward compatible as well, do you want me to test it (I can remove it if it breaks on 8.19) ?

I thought the registration didn't become available until 8.20? But feel free to try.

[jdchristensen]

@tabareau I don't understand what your last commit is trying to achieve. Testing it with Rocq 9.1, it's still the case that when you use rewrite in a proof, it uses an internally generated lemma in the proof. For example, this term defined in Overture.v uses the internal lemma internal_paths_rew_r:

define_internal_paths_rew_r@{u u0} =
fun (A : Type) (x y : A) (P : A -> Type) (u : P y) (H : x = y) =>
internal_paths_rew_r A x y (fun x0 : A => P x0) u H
     : forall (A : Type) (x y : A) (P : A -> Type), P y -> x = y -> P x

What the TODO wants to achieve is that when rewrite is used in a proof, the term that is produced uses transport, or at least something that unfolds to it. This is because we have many lemmas about the behaviour of transport, and we would like to be able to use them when reasoning about such proofs. The tactics provided are intended to make it possible to reason about such terms, so we would still want to have them in place if the term isn't literally transport. What I'm hoping is that the registration process that is available starting with 8.20 (or maybe the new process using typeclasses) can allow us to make rewrite use the terms we prefer. Also, the test you removed was there to ensure that the generated lemmas didn't have extra universe variables. That happens if they are generated within a Section with a Universe variable, for example.

Here is what I plan to do once 8.20 is the minimum: rocq-prover/rocq#18299 (comment)

In summary, as long as those internal lemmas are being generated and used by rewrite, we want both the tactic and the test that they are not overly polymorphic.

Could you force push and remove the last commit from the history? Then I'll update the TODO comment and will merge.

[tabareau]

The PR is doing what you say on Rocq master only (and thus for 9.2)

Local Lemma define_internal_paths_rew A x y P (u : P x) (H : x = y :> A) : P y.
Proof. rewrite <- H. exact u. Defined.

Print define_internal_paths_rew.
(*define_internal_paths_rew@{u u0} =
fun (A : Type) (x y : A) (P : A -> Type) (u : P x) (H : x = y) =>
paths_rec x (fun y0 : A => P y0) u y H
	 : forall (A : Type) (x y : A) (P : A -> Type), P x -> x = y -> P y*)

[tabareau]

It can now be achieved either by Register (backward compatible as just ignored for version <9.2) or using typeclasses (not backward compatible).

On master, as internal_rew_* constants do not exists anymore, the universe checking tests have to be removed otherwise they fail.

[tabareau]

So in my opinion the last commit is strictly better, but I can remove it no problem

[jdchristensen]

Ok, I didn't realize that you were trying to achieve something whose behaviour was so different across versions. But I still think it's better to wait until we support the appropriate version. (Also, what you did didn't seem to achieve the goal of producing a term which unfolds to transport. But I think that could be fixed.)

I'm still confused by your description, and maybe you can clarify for future reference. I thought that with 8.20 and newer, one could use Register to say which lemmas would be used by rewrite. But you wrote that using Register is ignored for < 9.2. Is that because the names that need to be registered have changed? If so, can we Register the names that work with 8.20 to 9.1 as well as the names that work with 9.2 to achieve what I want across multiple versions?

[tabareau]

In 8.20, I think only "core.eq.*" is handled properly, but it should be usable in your case. To make systematic use of transport, you have to define paths_rec using transport instead, as transport cannot be registered directly as it doesn't its arguments in the expected order. If you want, you can get back to me when you are ready to move to "8.20 and later" and I can do a PR for using transport systematically.

[jdchristensen]

In 8.20, I think only "core.eq.*" is handled properly, but it should be usable in your case. To make systematic use of transport, you have to define paths_rec using transport instead, as transport cannot be registered directly as it doesn't its arguments in the expected order.

Yes, this corresponds to what I did in rocq-prover/rocq#18299 (comment)

If you want, you can get back to me when you are ready to move to "8.20 and later" and I can do a PR for using transport systematically.

That would be great! Thanks!