Relation.TransGen vs. TC from Init.Core

Stream: mathlib4

[Malvin Gattinger]

I only just realised that there are two definitions of the transitive closure of relations: docs#TC in Init.Core and docs#Relation.TransGen in Mathlib.Logic.Relation. It seems the latter is what I should use if I want to also get Lemmas about it, ans relate it to ReflTransGen which as no equivalent in Init.Core?
I also noticed that TC is defined with a trans case that combines two TC steps, whereas TransGen is defined with a tail case that combines a TransGen step and a single r step.

But I feel like they should be equivalent? Did I miss the theorem that says so?

[Kim Morrison]

I'm away from my computer for a bit, but:

• A note near TransGen about TC would be helpful.
• A theorem relating them would be good.
• Investigating how TC is used in Lean would be helpful. Perhaps we can move it lower? Perhaps it is replaceable by upstreaming TransGen itself? This doesn't seem super high priority, but if someone wanted to look into it I'd be interested.

[Mario Carneiro]

IMO we should remove TC if possible

[Yury G. Kudryashov]

IMHO, TC is a hardly guessable name.

[Yury G. Kudryashov]

Both TransGen and TransClosure (if we want to have closure in the name) are better.

[Malvin Gattinger]

Here is a proof.

import Mathlib.Logic.Relation

theorem Relation.TransGen_iff_TC (r : α → α → Prop) : Relation.TransGen r a b ↔ TC r a b := by
  constructor
  · intro tgen
    induction tgen
    case single c a_c =>
      exact TC.base a c a_c
    case tail b c _ b_c IH =>
      exact TC.trans a b c IH (TC.base b c b_c)
  · intro tc
    induction tc
    case base a_b =>
      exact Relation.TransGen.single a_b
    case trans x y z _ _ IH_x_y IH_y_z =>
      exact Relation.transitive_transGen IH_x_y IH_y_z

[Johan Commelin]

The string TC (with word boundaries) only appears in comments in mathlib, and refers to TypeClass.

[Kim Morrison]

lean#4760

[Malvin Gattinger]

Ah, I understand this means the old TC will be gone, and Relation.TransGen will then be provided by Lean instead of Mathlib (once it has moved to a Lean version including this PR)? So any third project using Relation.TransGenshould just continue to work? Cool!

[Malvin Gattinger]

I think a small detail in the documentation needs to be adjusted for this change: https://github.com/leanprover/lean4/issues/6899 - I tried to make a PR to the lean repo, but it's my first time, hope I did it correctly.