symm attribute failure

Stream: mathlib4

[Winston Yin]

Is this is a bug in the symm attribute?

import Mathlib.Algebra.Hom.Group
import Mathlib.Logic.Equiv.Basic

def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M) (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : N →ₙ* M where
  toFun := g
  map_mul' x y :=
    calc
      g (x * y) = g (f (g x) * f (g y)) := by rw [h₂ x, h₂ y]
      _ = g (f (g x * g y)) := by rw [f.map_mul]
      _ = g x * g y := h₁ _

structure MulEquiv (M N : Type _) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

infixl:25 " ≃* " => MulEquiv

@[symm]
-- @[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got {M : Type u_1} →
--  {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
def foo_symm {M N : Type _} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M :=
  { h.toEquiv.symm with map_mul' := (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv).map_mul }

[Kevin Buzzard]

The fact that it's a def not a lemma seems not to be relevant -- for example docs4#CategoryTheory.Iso.symm is a def tagged @[symm] which looks very much like what you are doing (not that we can tell it's tagged @[symm] from the docs any more, unfortunately :-( ). It looks like a bug to me!

[Winston Yin]

Submitted issue mathlib4#855

[Winston Yin]

trans has a similar problem too

[Siddhartha Gadgil]

I'll take a look (I implemented symm).

[Siddhartha Gadgil]

@Winston Yin
I managed to narrow this and made a WIP PR mathlib4#857, which fixes the issue but it is not clear if in a correct way.
Somebody with more expertise will have to be called in to make some decisions on changing the implementation.

[Winston Yin]

Thank you, Siddhartha! I guess the question is, why did this work in mathlib3 but not mathlib4?

[Siddhartha Gadgil]

The implementation in mathlib4 was from scratch, not a port. I guess I made too restrictive assumptions and built a method based on these. The code should be rewritten (using mkAppM') to allow types to be inferred when flipping.

Will try in a day or two if nobody else has fixed it (have a bit of a deadline for now).

[Kyle Miller]

The Lean 3 implementation didn't really check much: https://github.com/leanprover-community/lean/blob/master/src/library/relation_manager.cpp#L147

It just checks that it takes at least one argument and returns a function application with a constant head.

The symmetry tactic itself doesn't do anything more than apply whatever's registered as the symm lemma for the given constant. https://github.com/leanprover-community/lean/blob/master/library/init/meta/relation_tactics.lean#L24

[Kyle Miller]

trans lemmas check a bit more, but still it just examines that the last couple arguments are function applications with a constant head: https://github.com/leanprover-community/lean/blob/master/src/library/relation_manager.cpp#L132

That's because every trans lemma gets registered in a table recording triples of constants ("given this relation and that relation, transitively we can produce such-and-such relation"). This was important for Lean 3's calc implementation.

[Scott Morrison]

@Siddhartha Gadgil, just letting you know that there is a refactor of symm in https://github.com/leanprover-community/mathlib4/pull/856. It looks like it is orthogonal to your mathlib4#857, but I wanted to give you a heads up.

[Siddhartha Gadgil]

@Kyle Miller @Scott Morrison Thanks.

So I will clean up the PR to drop the check in a couple of hours (when I get to my desktop which has the local branch) - it is clearly incorrectly blocking the label in some cases, and not needed anywhere.

[Siddhartha Gadgil]

@Winston Yin The PR mathlib4#857 fixes your issue (and includes it in a test) by removing the incorrect tests I had introduced during the labelling.