Trans instances for Relation.ReflTransGen

Stream: mathlib4

[Chris Henson]

Should these instances (from a discussion with @Thomas Waring ) exist?

import Mathlib
open Relation Relation.ReflTransGen

variable {α : Type u} (R : α → α → Prop)

instance : Trans R R (ReflTransGen R) where
  trans hab hbc := head hab (single hbc)

instance : Trans R (ReflTransGen R) (ReflTransGen R) :=
  ⟨head⟩

instance : Trans (ReflTransGen R) R (ReflTransGen R) :=
  ⟨tail⟩

There are already some similar instances relating ReflTransGen and TransGen. This would have the benefit of allowing you to switch back and forth between single and multiple applications of the relation in a calc block.

[Jireh Loreaux]

That's a neat idea. I don't see anything immediately wrong with it.

Maybe, it could be nice to have some Trans instances for WCovby and CovBy and ≤ and < too, for the same reason.

[Eric Wieser]

These instances look like a good idea to me

[Chris Henson]

Adding these seems to break a few existing usages of calc and trans in Mathlib.Order.Lattice and Mathlib.Algebra.GCDMonoid.Basic. Specifically:

• docs#Monotone.forall_le_of_antitone
• docs#le_of_inf_le_sup_le
• docs#gcd_pow_right_dvd_pow_gcd
• docs#gcd_pow_left_dvd_pow_gcd
• docs#pow_dvd_of_mul_eq_pow

[Eric Wieser]

It's probably easier for you to make a draft PR so that people can play around with the failure themselves using an olean cache

[Chris Henson]

I have opened #27240. (This is my first Mathlib PR, so hopefully I did that correctly...).