IsTrans

Stream: mathlib4

[Yury G. Kudryashov]

Should we migrate from IsTrans to Trans?

[Yury G. Kudryashov]

E.g., by using

abbreviation IsTrans α r := Trans r r r

[Yury G. Kudryashov]

Trans is used, e.g., by calc and tactic trans

[Yury G. Kudryashov]

With this definition Lean fails to extend IsTrans α r saying that it's not a class.

[Yury G. Kudryashov]

@Gabriel Ebner What should I do?

[Yury G. Kudryashov]

Make it class IsTrans α r extends Trans r r r and add a loop instance [IsTrans α r] : Trans r r r?

[Yury G. Kudryashov]

Or something else?

[Yury G. Kudryashov]

@Mario Carneiro @Gabriel Ebner :up:

[Gabriel Ebner]

I think there's class abbrev IsTrans α r := Trans r r r.

[Yury G. Kudryashov]

It seems that Trans is not in Prop.

[Yury G. Kudryashov]

So, I see 2 options.

• Add an instance [IsTrans α r] : Trans r r r and a linter that bans other Trans r r r instances.
• Add both instances [IsTrans α r] : Trans r r r and [Trans r r r] : IsTrans α r and hope that Lean 4 is good with instance loops.

[Gabriel Ebner]

Lean 4 is good with this kind of instance loop.

[Yury G. Kudryashov]

Related issue: since calc doesn't unfold Trans instances, an Equiv defined using calc uses Trans.trans, not Equiv.trans.

[Gabriel Ebner]

Ah, I don't think much thought has gone into non-Prop Trans instances.

[Yury G. Kudryashov]

While the results are defeq, simp doesn't work on the result.

[Yury G. Kudryashov]

Of course, we can drop Equiv.trans and use Trans.trans instead.

[Yury G. Kudryashov]

But this way we can't use dot notation.

[Yury G. Kudryashov]

One more question: can we unexport Trans.trans? In many cases, our _root_.trans is more useful.

[Yury G. Kudryashov]

I understand that Trans.trans is more general but in many cases it's not useful outside of calc. E.g., we can't write apply Trans.trans h and expect Lean to figure out the type of the second argument.

[Yury G. Kudryashov]

I added instances IsTrans α r → Trans r r r and Trans r r r → IsTrans α r, and now I have to add _root_ here and there.

[Yury G. Kudryashov]

These collisions are new because without these instances, one of two trans did not apply.

[Yury G. Kudryashov]

BTW, am I right that Lean 4 calc can't handle https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Hom/Equiv/Basic.html#MulEquiv.trans?

[Yury G. Kudryashov]

The only class-based solution that I can think of is

class Trans (α β : Sort _) (γ : outParam (Sort _)) where
  trans : α → β → γ

with instances like

instance [Preorder α] {a b c : α} : Trans (a ≤ b) (b ≤ c) (a ≤ c) :=
  ⟨le_trans⟩

instance [Mul M] [Mul N] [Mul P] : Trans (M ≃* N) (N ≃* P) (M ≃* P) :=
  ⟨MulEquiv.trans⟩

[Yury G. Kudryashov]

@Gabriel Ebner @Mario Carneiro Who is the right person to talk about calc support for MulEquiv etc?

[Mario Carneiro]

It's a core PR, but I don't think it has any special prerequisites

[Mario Carneiro]

but you should be aware that @Adrien Champion 's PR might affect how calc works because it needs the ability to add a refl step at the beginning

[Mario Carneiro]

(I wouldn't mind if we found another way to do it though)

[Mario Carneiro]

the issue is that the new syntax has an (optional) extra LHS term at the beginning which we have to fit into the inequality chain

[Yury G. Kudryashov]

I wanted to discuss what should be done before trying to do something.

[Yury G. Kudryashov]

Where can I read about the new syntax?

[Mario Carneiro]

Also, that more general instance will have problems with the Trans Eq R R and Trans R Eq R instances

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60calc.60.20indentation

[Yury G. Kudryashov]

We can have general instances Trans (a = b) (R b c) (R a b) and Trans (R a b) (b = c) (R a c). For MulEquivs etc, we can't have M = N → N ≃* P → M ≃* P anyway because the first equality says nothing about [Mul M] and [Mul N].