rewrite claims to succeed, but goal doesn't change

[kim-em]

I have an example where rewrite claims to succeed (and I think that it should), but the goal does not apparently change. I've also checked the goals with set_option pp.all true

I'm trying to rewrite along

FunctorComposition_associativity :
  ∀ (f : Functor ?M_1 ?M_2) (g : Functor ?M_2 ?M_3) (h : Functor ?M_3 ?M_4),
    FunctorComposition (FunctorComposition f g) h = FunctorComposition f (FunctorComposition g h)

and the goal state is

C : MonoidalCategory,
D : MonoidalCategory,
E : MonoidalCategory,
F : MonoidalFunctor C D,
G : MonoidalFunctor D E
⊢ ⇑(FunctorCategory
     ({Obj := C^.Obj,
       Hom := C^.Hom,
       identity := C^.identity,
       compose := C^.compose,
       left_identity := C^.left_identity,
       right_identity := C^.right_identity,
       associativity := C^.associativity} × {Obj := C^.Obj,
       Hom := C^.Hom,
       identity := C^.identity,
       compose := C^.compose,
       left_identity := C^.left_identity,
       right_identity := C^.right_identity,
       associativity := C^.associativity})
     ↑E)
    (FunctorComposition (C^.tensor) (FunctorComposition ↑F ↑G))
    (FunctorComposition (FunctorComposition ↑F ↑G × FunctorComposition ↑F ↑G) (E^.tensor))

Using rewrite FunctorComposition_associativity the goal seems to not change at all, but rewrite doesn't fail. If I turn on set_option pp.all true, the goal is much longer, but again doesn't change following the rewrite.

Curiously, if I try the force tactic suggested to me by Sebastian Ullrich, it agrees that the goals have changed.

I'm pretty certain the goal is not actually changing. One good piece of evidence for this is that you can apply the rewrite very many times, and it never fails.

This issue can be seen in monoidal_categories/monoidal_functor.lean, at line 47, in the following commit:

git clone https://github.com/semorrison/lean-category-theory
cd lean-category-theory
git reset --hard a921a46c864c5fae8cf0cd962036233a15b72e0c
lean --make

[leodemoura]

Attached commit to wrong issue: 36c7d46

[kim-em]

Using

set_option trace.rewrite true
set_option trace.kabstract true

I get some debugging messages on each rewrite, confirming that it is rewriting what I expect it to.

[rewrite] before kabstract
[kabstract] found target:
FunctorComposition (C^.tensor) (FunctorComposition ↑F ↑G)

If I wrap the rewrite tactic in a repeat, it prints the same message 250 times, and then reports an ever growing number of skipped messages.

[kim-em]

With set_option pp.all true, the target that is reported changes from the first occasion to the second, and then stabilises. I'll try to understand that change as a start. In any case, after the rewrite the goal doesn't appear to have changed at all, even though the left and right sides of the equation we're rewriting along are distinctly different.

[kim-em]

This one is still mysterious to me. The debugging messages report that the rewrite is happening exactly where I expect it to (in the explicit arguments), but after the rewrite the reported target is still there.

In any case, the problem no longer occurs after my big refactor, so I'm happy for this to be closed. Nevertheless I'll leave that for someone else to do, in case it seems worth investigating this apparent bad behaviour by rewrite.

[leodemoura]

We need self contained (small as possible) reproducible examples.