Transitive closure of transitive

Stream: new members

[Andrew Souther]

Hello! Sorry if this question belongs in #Is there code for X?. I am still very new, so it feels right to ask here.
logic.relation has this lemma:

lemma refl_trans_gen_eq_self (refl : reflexive r) (trans : transitive r) :
  refl_trans_gen r = r :=

Is there a similar lemma for trans_gen which says that a transitive relation is its own transitive closure? I think that should be true, but I can't find it.

[Yakov Pechersky]

Pretty mechanical conversion by me, I'm probably missing something:

import logic.relation

open relation

namespace trans_gen

variables {α β : Type*} {r : α → α → Prop} {a b c : α}

lemma trans_gen_eq_self (trans : transitive r) :
  trans_gen r = r :=
funext $ λ a, funext $ λ b, propext $
⟨λ h, begin
  induction h,
  case trans_gen.single : c hc { exact hc },
  case trans_gen.tail : c d hac hcd hac { exact trans hac hcd }
end,
trans_gen.single⟩

@[trans]
lemma trans (hab : trans_gen r a b) (hbc : trans_gen r b c) : trans_gen r a c :=
begin
  induction hbc,
  case trans_gen.single : d hd { exact trans_gen.tail hab hd },
  case trans_gen.tail : c d hbc hcd hac { exact hac.tail hcd }
end

lemma transitive_trans_gen : transitive (trans_gen r) :=
assume a b c, trans

lemma trans_gen_idem :
  trans_gen (trans_gen r) = trans_gen r :=
trans_gen_eq_self transitive_trans_gen

lemma trans_gen_lift {p : β → β → Prop} {a b : α} (f : α → β)
  (h : ∀a b, r a b → p (f a) (f b)) (hab : trans_gen r a b) : trans_gen p (f a) (f b) :=
begin
  induction hab,
  case trans_gen.single : c hac { exact trans_gen.single (h a c hac) },
  case trans_gen.tail : c d hac hcd hac { exact trans_gen.tail hac (h c d hcd) }
end

lemma trans_gen_lift' {p : β → β → Prop} {a b : α} (f : α → β)
  (h : ∀ a b, r a b → trans_gen p (f a) (f b))
  (hab : trans_gen r a b) : trans_gen p (f a) (f b) :=
by simpa [trans_gen_idem] using trans_gen_lift f h hab

lemma trans_gen_closed {p : α → α → Prop} :
  (∀ a b, r a b → trans_gen p a b) → trans_gen r a b → trans_gen p a b :=
trans_gen_lift' id

end trans_gen

[Andrew Souther]

Thank you!

[Bryan Gin-ge Chen]

This is probably worth PRing to mathlib.

[Yakov Pechersky]

#5129