Std.Trans

Stream: Is there code for X?

[Wrenna Robson]

Wrenna Robson said:

Still, the lack of a Std.Trans might trip/surprise some users.

I wanted to express again that I am somewhat Unsure about the lack of a Std.Trans in the same way that other properties of relations have standard properties. I'm not saying we should have Trans - but Trans can be used for heterogenous functions that give any Sort (for which I think the primary use is in calc?), and if nothing else writing Trans R R R (which is often how we use it as a typeclass hypothesis as far as I can tell) is a bit of a mouthful.

Essentially, just as Std.Symm is (effectively) doing all that Mathlib's IsSymm does, why can we not have a Std.Trans that does what Mathlib's IsTrans does?

I could absolutely see the need for something like:

class Symm (r : α → β → Sort u) (s : outParam (β → α → Sort v)) where
  /-- Use a symmetry, generalized over the relations involved. -/
  symm : r a b → s b a

Clearly that is a sensible general thing - one uses it when you have an r a b and you want to generate a s b a. But we don't have this - I'm not saying we need to add it. I am just saying that Trans feels to me like an odd design lacuna that I do not quite understand - and while it might be necessary under the hood for things like calc, I do question to what degree it is useful for it to be user-exposed. But this is deep core library design stuff - so I don't really feel like I can propose any kind of change. It's just that once again, I've been somewhat stalled by expecting Std.Trans to exist and then it not.

[Wrenna Robson]

It is possible though that nobody else is bothered about this. I would just like a world where instead of writing things like [Trans ( · < · : α → α → Prop) ( · < ·) ( · < ·)], we can instead write [Std.Trans ( · < · : α → α → Prop)]

[Snir Broshi]

I agree, though I'm not sure this is the correct channel for such proposals
btw #mathlib4 > Relation properties duplication is about deprecating IsSymm since Std.Symm exists, so no reason to add Std.Trans without deprecating IsTrans

[Wrenna Robson]

Yeah I wasn't sure what the right place was to suggest it!

[Wrenna Robson]

I agree that we should deprecate IsTrans if we add that