Why are there two transitive closures?

Stream: Is there code for X?

[Junyan Xu]

docs#tc (in core) and docs#relation.trans_gen (in mathlib. Notice the second parts of the inductive definitions are slightly different, so proof is required that relation.trans_gen is transitive. Implicit arguments in constructors also differ. There doesn't seem to be a lemma showing both definitions are equivalent.

[Scott Morrison]

Likely because no one noticed and/or for a long time changing core was impossible. If there's the possibility of discarding the presumably barely used tc, that would probably be good, but I haven't looked at all. Otherwise, if you feel like PR'ing either a note explaining the existence of both, or some glue, those would be fine too.

[Yaël Dillies]

I know tc exists but I have yet to see someone use it.

[Junyan Xu]

(deleted)

[Junyan Xu]

docs#tc.wf is among a bunch of basic facts about well-foundedness in core and that's why I discovered it ... I think it's best to rename it to wf.tc for dot notation, but as I learned above it's rarely used so probably no one cares, and I don't know how hard it is now to change the core ... is the only difference to PR at the leanprover-community/lean repo instead of mathlib, and CI would still work as usual?

[Junyan Xu]

I only found one actual usage of tc in the Lean repo so it's probably removable.

[Kyle Miller]

@Junyan Xu Here's a PR to remove tc: lean#713

I think it makes sense to port over the transitive closure of a well-founded relation (see this) to order/well_founded in mathlib using relation.trans_gen, if you want to do that.

[Yaël Dillies]

@Violeta Hernández has this result.

[Kyle Miller]

@Yaël Dillies Ok, is it somewhere? Right now the result is also in Lean and it's a matter of changing tc to relation.trans_gen and fixing the tc.rec_on.

[Yaël Dillies]

I believe it is in some PR, but Violeta knows best.

[Kyle Miller]

Here's the code that should, in some form, make it to mathlib to complete lean#713:

namespace relation.trans_gen
section
  parameters {α : Type*} {r : α → α → Prop}

  lemma accessible {z : α} (ac : acc r z) : acc (relation.trans_gen r) z :=
  acc.rec_on ac (λ x acx ih,
    acc.intro x (λ y rel,
      relation.trans_gen.rec_on rel
        (λ a hya z ih, ih _ hya)
        (λ a c hya hac ih₁ z ih₂, acc.inv (ih₂ _ hac) hya)
        acx ih))

  lemma wf (h : well_founded r) : well_founded (relation.trans_gen r) :=
  ⟨λ a, accessible (h.apply a)⟩
end
end relation.trans_gen

[Violeta Hernández]

docs#relation.well_founded.trans_gen

[Violeta Hernández]

Got merged about two weeks ago

[Yaël Dillies]

Should probably be called well_founded.trans_gen for dot notation.

[Junyan Xu]

I'm currently using tc in my combinatorial game work, because I only needed tc.wf and it's short to write; I only found out the existence of trans_gen by reading pgame.lean. Once docs#relation.well_founded.trans_gen is renamed to enable dot notation, I would have no objection to switch over.

[Kyle Miller]

Regarding the relationship between tc and relation.trans_gen, it's basically docs#relation.trans_gen.trans_induction_on.

If for some reason we still wanted something like tc, we could have this:

inductive relation.trans_gen' {α : Type*} (r : α → α → Prop) : α → α → Prop
| base  : ∀ a b, r a b → relation.trans_gen' a b
| trans : ∀ a b c, relation.trans_gen' a b → relation.trans_gen' b c → relation.trans_gen' a c

lemma relation.trans_gen'_eq {α : Type*} {r : α → α → Prop} :
  relation.trans_gen' r = relation.trans_gen r :=
begin
  ext x y,
  split,
  { intro h,
    induction h with a b hab a b c hab hbc ih₁ ih₂,
    { exact relation.trans_gen.single hab, },
    { exact relation.trans_gen.trans ih₁ ih₂, } },
  { intro h,
    apply h.trans_induction_on,
    { exact relation.trans_gen'.base, },
    { intros,
      apply relation.trans_gen'.trans; assumption, } },
end

[Kyle Miller]

@Junyan Xu @Violeta Hernández @Yaël Dillies Would any of you like to be responsible for renaming relation.well_founded.trans_gen to well_founded.trans_gen?

[Violeta Hernández]

I'll do it

[Violeta Hernández]

#14016

[Violeta Hernández]

I can't see any reason we'd need this alternate trans_gen'. If you can somehow show its induction hypothesis, then you can also immediately show the induction hypothesis from trans_gen, and I can't think of a situation in which the former wouldn't be strictly simpler.