`calc` for isomorphisms involving typeclasses

kbuzzard commented 1 year ago

Prerequisites

[x] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Reduced the issue to a self-contained, reproducible test case.

Description

I can't work out how to use calc for calculations involving isomorphisms between objects which have typeclasses attached to them.

Steps to Reproduce

structure MulEquiv (M N : Type _) [Mul M] [Mul N] where -- group isomorphism

infixl:25 " ≃* " => MulEquiv

def MulEquiv.trans [Mul A] [Mul B] [Mul C] (hAB : A ≃* B) (hBC : B ≃* C) : A ≃* C := sorry

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

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

/-
scratch4.lean:12:2
invalid 'calc' step, left-hand-side is
  Type : Type 1
previous right-hand-side is
  inst✝¹ : Mul B

scratch4.lean:10:92
application type mismatch
  MulEquiv ?m.8550
argument
  ?m.8550
has type
  Mul B : Type
but is expected to have type
  Type ?u.8548 : Type (?u.8548 + 1)
-/

Versions

Lean (version 4.0.0-nightly-2023-03-31, commit 742d053a97bd, Release)

Additional Information

The issue is that Lean wants Trans, which powers calc behind the scenes, wants to eat two types and return a type (in this case the type of group isomorphisms between the two types) but I can't figure out where to insert the group structure. Of course this can be worked around by just applying MulEquiv.trans directly so this is not blocking anything important, I just thought it was worth observing this potential limitation of calc (there is currently a push to introduce more calc blocks into mathlib and this came up there).

gebner commented 1 year ago

The problem is that calc expects the last two arguments of the relation to be the lhs/rhs resp.

urkud commented 1 year ago

In fact, I don't understand why the Trans instance works in this case. If I put trans := _, then the goal is

Expected type:
A : Type u_1
B : Type u_2
C : Type u_3
⊢ {a : Mul A} → {b : Mul B} → {c : Mul C} → A ≃* B → B ≃* C → A ≃* C

And this is strange. BTW, if I call this instance a, then #print a with set_opion pp.all true gives

def a.{u_1, u_2, u_3} : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      @Trans.{1, 1, 1, u_1 + 1, u_2 + 1, u_3 + 1} (Mul.{u_1} A) (Mul.{u_2} B) (Mul.{u_3} C) (@MulEquiv.{u_1, u_2} A B)
        (@MulEquiv.{u_2, u_3} B C) (@MulEquiv.{u_1, u_3} A C) :=
fun {A : Type u_1} {B : Type u_2} {C : Type u_3} ↦
  @Trans.mk.{1, 1, 1, u_1 + 1, u_2 + 1, u_3 + 1} (Mul.{u_1} A) (Mul.{u_2} B) (Mul.{u_3} C) (@MulEquiv.{u_1, u_2} A B)
    (@MulEquiv.{u_2, u_3} B C) (@MulEquiv.{u_1, u_3} A C) fun {a : Mul.{u_1} A} {b : Mul.{u_2} B} {c : Mul.{u_3} C} ↦
    @MulEquiv.trans.{u_1, u_2, u_3} A B C a b c

One solution I have in mind is to introduce

class HTrans (in1 : Sort _) (in2 : Sort _) (out : outParam (Sort _)) where
  trans : in1 → in2 → out

instance (r : α → β → Sort _) (s : β → γ → Sort _) (t : α → γ → Sort _) [Trans r s t] {x y z}
    : HTrans (r x y) (s y z) (t x z) where
  trans p1 p2 := Trans.trans p1 p2

Even if we make the example from the original post work by interpreting MulEquiv as an equivalence between Mul structures, this won't help with

structure RingEquiv (α β : Type _) [Mul α] [Add α] [Mul β] [Add β] where

eric-wieser commented 1 year ago

In https://github.com/leanprover-community/mathlib4/issues/6509 I was able to mostly get this working.

leanprover / lean4