Confusing error in Mathematics in Lean 7.3

Stream: general

[Jan Cristina]

First of all I wanted to say thank to the lean prover community for creating such excellent tools as well as the instructional materials. It's been really nice to explore formal mathematics in Mathematics in Lean. Is "general" the right place for help requests?

I'm now working on § 7.3
and have stumbled on what I think is a bit of a confusing error. I'm trying to prove the definition

def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M  where

and I had what I thought was a promising approach

def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M  where
  r := fun x y ↦ ∃ w ∈ N, ∃ z ∈ N, x*w = y*z
  iseqv := {
    refl := fun x ↦ ⟨1, N.one_mem, 1, N.one_mem, rfl⟩
    symm := fun ⟨w, hw, z, hz, h⟩ ↦ ⟨z, hz, w, hw, h.symm⟩
    trans := by
      rintro x y z ⟨u, hu, v, hv, huv⟩
      rintro ⟨v', hv', w, hw, hvw⟩
      have h := CommMonoid.mul_comm v v'
      exact ⟨ u * v', N.mul_mem hu hv', w * v, N.mul_mem hw hv, (by
        rw [<-mul_assoc, huv, <-mul_assoc, <-hvw, mul_assoc, mul_assoc]
        simp
        have h := CommMonoid.mul_comm v v'
        exact h
      )⟩
    }

but this yields a somewhat confusing error

▶ 106:9-106:16: error:
type mismatch
  h
has type
  v * v' = v' * v : Prop
but is expected to have type
  v * v' = v' * v : Prop

If I skip the indirection and just try

    ...
        exact CommMonoid.mul_comm v v'

The error becomes somewhat clearer:

▶ 105:9-105:39: error:
type mismatch
  CommMonoid.mul_comm v v'
has type
  @HMul.hMul M M M (@instHMul M (@Semigroup.toMul M (@Monoid.toSemigroup M CommMonoid.toMonoid))) v v' = v' * v : Prop
but is expected to have type
  @HMul.hMul M M M (@instHMul M (@Semigroup.toMul M (@Monoid.toSemigroup M DivInvMonoid.toMonoid))) v v' = v' * v : Prop

I haven't fully groked how implicit resolution works here, but that DivInvMonoid seems suspicious
I compared with the solution where it seams that the idea is commute with the y and v ( b and z in the solution proof):

      rintro a b c ⟨w, hw, z, hz, h⟩ ⟨w', hw', z', hz', h'⟩
      refine ⟨w*w', N.mul_mem hw hw', z*z', N.mul_mem hz hz', ?_⟩
      rw [← mul_assoc, h, mul_comm b, mul_assoc, h', ← mul_assoc, mul_comm z, mul_assoc]

Is there a way to make this work by commuting the two divisor elements?

[Kevin Buzzard]

Not at a computer right now but CommMonoid.mul_comm looks like a code smell -- what happens if you just use mul_comm? The user isn't supposed to have to worry about implementation details such as DivInvMonoid.

[Jan Cristina]

I changed the proof a little:

      rw [<-mul_assoc, huv, <-mul_assoc, <-hvw, mul_assoc, mul_assoc]
      exact mul_comm v v'

and it still looks like the same error

▶ 105:9-105:39: error:
type mismatch
  CommMonoid.mul_comm v v'
has type
  @HMul.hMul M M M (@instHMul M (@Semigroup.toMul M (@Monoid.toSemigroup M CommMonoid.toMonoid))) v v' = v' * v : Prop
but is expected to have type
  @HMul.hMul M M M (@instHMul M (@Semigroup.toMul M (@Monoid.toSemigroup M DivInvMonoid.toMonoid))) v v' = v' * v : Prop

[Ruben Van de Velde]

Sounds like you may have two multiplications defined

[Jan Cristina]

I originally tried a rw [mul_comm], rw [mul_comm v], and rw [mul_comm v'] but it couldn't find matchin patterns (also tried adding reverse arrows)

[Ruben Van de Velde]

Try putting #where before def Submonoid.Setoid [CommMonoid M]

[Jan Cristina]

I forgot I do have some variables in scope that could be messing with it. I got the following from the #where

variable (M: Type) (gm : Group M) (sbgm : Subgroup₁ M) ...

I deleted those variables and now it works! Thanks!

[Kevin Buzzard]

That's why you should post full #mwe s.

[Ruben Van de Velde]

It's probably the Group M, then

[Eric Wieser]

Should MIL be suggesting for this exercise that you use docs#Con instead of Setoid?

[Patrick Massot]

This is a very special context where everything is basically redone from scratch. So indeed one must be careful not to mix hand-rolled classes with Mathlib ones.

[Emilie (Shad Amethyst)]

I really do believe this is a scenario that could greatly benefit from having better error printing. The error "v * v' = v' * v is expected to have type v * v' = v' * v" is not usable, since the actually-differring bit (which instance of Mul is used here) is hidden. I've encountered it more than once and it can be quite frustrating.
I don't know how hard it would be to detect cases like this, but even just having a diff of the fully-expanded expressions would help in that scenario.

[Eric Wieser]

@Patrick Massot, I think in this example you are telling the reader to use the mathlib versions, right?

def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M  where

Maybe this is a mistake and you meant to write Submonoid₁ if you intended the from-scratch version?

[Kyle Miller]

Emilie (Shad Amethyst) said:

I don't know how hard it would be to detect cases like this, but even just having a diff of the fully-expanded expressions would help in that scenario.

Having the type mismatch error figure out how to pretty print the expressions to highlight a difference is something that's at least on my own radar, and I think it would be nice to have. It's a bit subtle to do in general, since the system needs to be able to turn off notation pretty printing here and there to be able to reveal where the difference is. A basic version that can't handle notations, but which can reveal implicit arguments to functions, shouldn't be so hard to implement.

Side note: ignoring pretty printing issues, there's the general problem of coming up with an explanation for why two expressions are not definitionally equal, which to do for some value of 'right' would involve a version of isDefEq that takes the execution trace and can synthesize a reason why expressions aren't defeq. That seems like a lot of work, and it's not clear that these synthesized reasons would be understandable as error messages, so coming up with some ad hoc syntax-based heuristics for why some expressions might not be defeq seems like a better approach. Computing a diff is a heuristic because, for example, Function.const 1 2 is not defeq to Function.const 3 4, but that's because 1 and 3 aren't defeq, and it has nothing to do with 2 and 4.

[Patrick Massot]

Eric Wieser said:

Patrick Massot, I think in this example you are telling the reader to use the mathlib versions, right?

Sorry, I wrote my message without checking this specific example and it was indeed misleading. This exercise is indeed using Mathlib's classes.