fix: use `getRel` in `@[trans]` attribute

[digama0]

Incl. minor formatting of Trans.lean.

fixes #1222

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch batteries-pr-testing-1223 build failed against this PR. (2025-05-04 16:34:56) View Log
• 💥 Mathlib branch batteries-pr-testing-1223 build failed against this PR. (2025-05-05 00:24:57) View Log

[fgdorais]

I added a MWE test for the Mathlib build failures but I haven't investigated the issue.

[fgdorais]

The remaining Mathlib error seems to be a term depth issue:

error: /home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean:263:2: @[trans] attribute only applies to lemmas proving
        x ∼ y → y ∼ z → x ∼ z, got 
  {k : Type u_1} →
    {P₁ : Type u_2} →
      {P₂ : Type u_3} →
        {P₃ : Type u_4} →
          {V₁ : Type u_6} →
            {V₂ : Type u_7} →
              {V₃ : Type u_8} →
                [inst : Ring k] →
                  [inst_1 : AddCommGroup V₁] →
                    [inst_2 : AddCommGroup V₂] →
                      [inst_3 : AddCommGroup V₃] →
                        [inst_4 : Module k V₁] →
                          [inst_5 : Module k V₂] →
                            [inst_6 : Module k V₃] →
                              [inst_7 : AffineSpace V₁ P₁] →
                                [inst_8 : AffineSpace V₂ P₂] →
                                  [inst_9 : AffineSpace V₃ P₃] →
                                    (P₁ ≃ᵃ[k] P₂) → (P₂ ≃ᵃ[k] P₃) → P₁ ≃ᵃ[k] P₃ with target 
  P₁ ≃ᵃ[k] P₃

[digama0]

I don't think it's term depth, unless it's a problem of inferring the Trans instance. Could you make a MWE version of this example?

[fgdorais]

Added MWE test case. Looks like it's about an unusual ordering of parameters.

[fgdorais]

I did a bit of digging, the issue with the MWE is that mkAppOptM' in RelKind.mkRel can't infer the M k V instances while adding the trans instance. Changing the order to

def MT.rel {V₁ V₂} (k P₁ P₂) [M k V₁] [M k V₂] [T V₁ P₁] [T V₂ P₂] := Unit

fixes that but mkRel still has issues in the trans tactic.

[staroperator]

I did a bit of digging, the issue with the MWE is that mkAppOptM' in RelKind.mkRel can't infer the M k V instances while adding the trans instance. Changing the order to

def MT.rel {V₁ V₂} (k P₁ P₂) [M k V₁] [M k V₂] [T V₁ P₁] [T V₂ P₂] := Unit

fixes that but mkRel still has issues in the trans tactic.

I feel the problem is that mkAppOptM' tries to synthesize the instances but we want to make them mvars as more as possible. A smaller MWE for your new version is

class C (k α : Type)
def C.rel (k : Type) (α β : Type) [C k α] [C k β] := Unit
@[trans] def C.trans {k α β γ : Type} [C k α] [C k β] [C k γ] : rel k α β → rel k β γ → rel k α γ := sorry

def aaa {k α β γ : Type} [C k α] [C k β] [C k γ] : C.rel k α β → C.rel k β γ → C.rel k α γ := by
  intro h₁ h₂
  trans β
  · exact h₁
  · exact h₂

The C.trans is registered as decl C.trans, key #[C.rel, _uniq.3342], kind global but key #[C.rel] is expected. I guess this is because getExplicitRelArg succeeds at C.rel k but fails at C.rel _ due to instance synthesis.

[staroperator]

I feel the problem is that mkAppOptM' tries to synthesize the instances but we want to make them mvars as more as possible. A smaller MWE for your new version is

class C (k α : Type)
def C.rel (k : Type) (α β : Type) [C k α] [C k β] := Unit
@[trans] def C.trans {k α β γ : Type} [C k α] [C k β] [C k γ] : rel k α β → rel k β γ → rel k α γ := sorry

def aaa {k α β γ : Type} [C k α] [C k β] [C k γ] : C.rel k α β → C.rel k β γ → C.rel k α γ := by
  intro h₁ h₂
  trans β
  · exact h₁
  · exact h₂

The C.trans is registered as decl C.trans, key #[C.rel, _uniq.3342], kind global but key #[C.rel] is expected. I guess this is because getExplicitRelArg succeeds at C.rel k but fails at C.rel _ due to instance synthesis.

And an amazing fact: you can complete aaa with

def aaa {k α β γ : Type} [C k α] [C k β] [C k γ] : C.rel k α β → C.rel k β γ → C.rel k α γ := by
  intro h₁ h₂
  trans β
  · exact h₁

#print aaa

It gives

def aaa : {k α β γ : Type} →
  [inst : C k α] → [inst_1 : C k β] → [inst_2 : C k γ] → C.rel k α β → C.rel k β γ → C.rel k α γ :=
fun {k α β γ} [C k α] [C k β] [C k γ] h₁ h₂ => h₁

which should not type check. Is this a soundness bug?