calc for group isos

Stream: mathlib4

[Kevin Buzzard]

I was rubbish at calc in Lean 3 for years and right now I feel the same about Lean 4 calc. Should this work?

import Mathlib.GroupTheory.QuotientGroup

example (A B C : Type) [Group A] [Group B] [Group C] (hAB : A ≃* B) (hBC : B ≃* C) : A ≃* C := by calc
  A ≃* B := hAB
  _ ≃* C := hBC

because right now I get two errors:

scratch3.lean:6:2
invalid 'calc' step, left-hand-side is
  Type ?u.1742 : Type (?u.1742 + 1)
previous right-hand-side is
  MulOneClass.toMul : Mul B

scratch3.lean:4:98
application type mismatch
  MulEquiv ?m.1744
argument
  ?m.1744
has type
  Mul B : Type
but is expected to have type
  Type ?u.1742 : Type (?u.1742 + 1)

[Eric Wieser]

This probably needs a Trans instance

[Eric Wieser]

docs4#MulEquiv

[Kevin Buzzard]

How do I insert [Mul A] into the Trans machinery?

[Eric Wieser]

I think it's getting confused, and the answer is you don't? Just insert MulEquiv into it

[Eric Wieser]

docs4#Trans

[Eric Wieser]

Uh oh, this looks impossible

[Eric Wieser]

Trans (@MulEquiv A B) (@MulEquiv B C) (@MulEquiv A C) maybe?

[Kevin Buzzard]

import Mathlib.GroupTheory.QuotientGroup

instance : Trans (@MulEquiv A B) (@MulEquiv B C) (@MulEquiv A C) where
  trans := MulEquiv.trans

example (A B C : Type) [Group A] [Group B] [Group C] (hAB : A ≃* B) (hBC : B ≃* C) : A ≃* C := by calc
  A ≃* B := hAB
  _ ≃* C := hBC

/-
scratch4.lean:8:2
invalid 'calc' step, left-hand-side is
  Type ?u.2425 : Type (?u.2425 + 1)
previous right-hand-side is
  MulOneClass.toMul : Mul B

scratch4.lean:6:98
application type mismatch
  MulEquiv ?m.2427
argument
  ?m.2427
has type
  Mul B : Type
but is expected to have type
  Type ?u.2425 : Type (?u.2425 + 1)
-/

It looks like a parsing error to me?

[Eric Wieser]

Can you turn on pp.explicit?

[Eric Wieser]

I think though this an indication that it's doomed after all

[Kevin Buzzard]

Well I only wanted it for that other thread and it looks like you've found a better solution anyway ;-)

invalid 'calc' step, left-hand-side is
  Type ?u.2425 : Type (?u.2425 + 1)
previous right-hand-side is
  @MulOneClass.toMul B (@Monoid.toMulOneClass B (@DivInvMonoid.toMonoid B (@Group.toDivInvMonoid B inst✝¹))) : Mul B

This is on _ ≃* C

[Kevin Buzzard]

I think it's parsing A ≃* B as (A) (≃) (* B) maybe?

[Eric Wieser]

I don't think that's it

[Kevin Buzzard]

It can't be because that doesn't even typecheck

[Eric Wieser]

I think it needs A and B to be the last arguments of the relation

[Eric Wieser]

But they're not, the Mul A and Mul B arguments are

[Eric Wieser]

This worked in lean 3, though possibly only the community version

[Eric Wieser]

Basically any typeclass that expects something of the form α → Sort* as an argument becomes useless when you have side conditions like "α is a group" or "equality on α is decidable"

[Eric Wieser]

(another example is not being able to use the monad typeclasses for computable finsets)

[Kevin Buzzard]

Yeah, one error goes away if I add instance : ∀ (G : Type _), Mul G := sorry, but this is probably not a good instance for mathlib...

[Eric Wieser]

Working with category theory isos should also solve the problem, as there the typeclass is bundled

[Eric Wieser]

But I think it would be better to fix calc...

[Kevin Buzzard]

I'll open an issue but I guess it's low-priority?

[Eric Wieser]

It might be worth checking if mathlib ever uses calc in this way, and that I'm not hallucinating that it used to work in lean 3

[Kevin Buzzard]

Huh,

type mismatch at application
  mul_equiv.trans
term
  A
has type
  Type : Type 1
but is expected to have type
  has_mul ?m_1 : Type ?

[Eric Wieser]

Lol, guess I imagined it

[Kevin Buzzard]

Works fine with regular equivs in lean 3 (and this is used)

[Kevin Buzzard]

I don't know how to search for a calc block with mul_equiv in (or indeed any equiv other than unadorned equiv)

[Kevin Buzzard]

calc.*≃ in regex mode is good enough to find examples though (with calc on the same line as the first iso) (and none are adorned)

[Eric Wieser]

Kevin Buzzard said:

Works fine with regular equivs in lean 3 (and this is used)

This works in lean 4 too

[Kevin Buzzard]

lean4#2217 . Thanks for the help.