# Strange failure of general rewriting

**URL:** <https://discourse.rocq-prover.org/t/strange-failure-of-general-rewriting/2302>\
**Category:** Using Rocq\
**Created:** [May 24, 2024, 6:13pm UTC](https://discourse.rocq-prover.org/t/strange-failure-of-general-rewriting/2302 "2024-05-24T18:13:50Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![Ailrun](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ailrun/32/975_2.png) [@Ailrun](https://discourse.rocq-prover.org/u/Ailrun)\
**Post date:** [May 24, 2024, 6:13pm UTC](https://discourse.rocq-prover.org/t/strange-failure-of-general-rewriting/2302/1 "2024-05-24T18:13:50Z")

</div>

While using the general rewriting for some complex statement, I realized that the following (distilled version) does not work:

```coq
From Coq Require Import Morphisms Morphisms_Relations Relation_Definitions RelationClasses.

Inductive my_ty : Set :=
| my_ty_cons : my_ty
.

Notation "R <~> R'" := (@relation_equivalence my_ty R R') (at level 90, no associativity).

Inductive my_rel : relation my_ty :=
| my_rel_cons : my_rel my_ty_cons my_ty_cons
.

Set Debug "tactic-unification".

Goal forall a b Rgen (x : nat),
  Rgen x <~> my_rel ->
  Rgen x a b ->
  my_rel a b.
Proof.
  Search relation_equivalence.
  intros * H H0.
  Fail setoid_rewrite H in H0.
  change (Rgen x) with (fun a b => Rgen x a b) in H0.
  Fail setoid_rewrite H in H0.
Abort.

Context (pr : subrelation relation_equivalence (pointwise_relation my_ty (pointwise_relation my_ty iff))).

Goal forall a b Rgen (x : nat),
  Rgen x <~> my_rel ->
  Rgen x a b ->
  my_rel a b.
Proof.
  Search relation_equivalence.
  intros * H H0.
  change (Rgen x) with (fun a b => Rgen x a b) in H0.
  setoid_rewrite H in H0.
Abort.

```

In the first goal, both rewriting fails, specifically the first one fails because of unification failure. Why does it unify `Rgen x` (the left side of `<~>`) only with `Rgen x a b`, `Rgen`, `x`, `a`, `b`, but never with `Rgen x`?

This works once I use `change (Rgen x) with (fun a b => Rgen x a b) in H0.` (so that `(fun a b => Rgen x a b)` becomes a head by itself), but then the problem is about that `subrelation` I put as a `Context`. Why does this rewriting requires that? Isn’t the `Proper` instance for `relation_equivalence` not enough?