Regression: rewrite no longer works with JMeq in Rocq 9.2+rc1 (even with Scheme Rewriting for JMeq)

[davidnowak]

In Rocq 9.1.0 with stdlib 9.0.0, rewriting with a hypothesis of type JMeq x y works out of the box. However, in Rocq 9.2+rc1 with the current master branch of stdlib, the same code fails, even after explicitly enabling rewriting for JMeq. This appears to be a regression, but it is unclear whether the issue lies in Rocq itself or in stdlib.

Working behavior (Rocq 9.1.0 + stdlib 9.0.0):

From Stdlib Require Export JMeq.

Goal forall A (x y : A), JMeq x y -> x = y.
intros A x y H.
rewrite H.
(* Goal becomes: y = y *)

Failing behavior (Rocq 9.2+rc1 + stdlib master):

From Stdlib Require Export JMeq.

Scheme Rewriting for JMeq.

Goal forall A (x y : A), JMeq x y -> x = y.
intros A x y H.
Fail rewrite H.

Despite the Scheme Rewriting for JMeq command, rewrite H is rejected.

Is this behavior change expected while stdlib is being adapted to Rocq 9.2,
or should rewriting with JMeq continue to work in this situation?

[SkySkimmer]

It seems the new instance based rewriting doesn't work:

Inductive JMeq [A] (x : A) : forall [B], B -> Prop :=  JMeq_refl : JMeq x x.

(* in stdlib this is a consequence of axiom in Eqdep *)
Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.

Polymorphic Lemma JMeq_ind_r@{s;+} : forall (A:Type) (x:A) (P:A -> Type@{s;_}),
   P x -> forall y, JMeq y x -> P y.
Proof.
intros A x P H y H'. destruct (JMeq_eq _ _ _ H'). assumption.
Qed.

(* also doesn't work if we use jmeq directly *)
Definition JMeq' [A] x y := @JMeq A x A y.

Polymorphic Definition JMeq_leibniz_r@{s;+} : Has_Leibniz_r@{Type Prop s;_ _ _} JMeq' := JMeq_ind_r.

Hint Resolve JMeq_leibniz_r : rewrite_instances.

Goal forall A (x y : A), JMeq' x y -> x = y.
intros A x y H.
rewrite H. (* fails *)

but the code which handled jmeq is gone.

cc @tabareau

[tabareau]

rocq-prover/rocq#21601 should fix this