## Stream: new members

### Topic: Transitive closure of transitive

#### Andrew Souther (Nov 27 2020 at 02:21):

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 (Nov 27 2020 at 04:06):

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


Thank you!

#### Bryan Gin-ge Chen (Nov 27 2020 at 04:28):

This is probably worth PRing to mathlib.

#### Yakov Pechersky (Nov 27 2020 at 04:32):

#5129

Last updated: May 10 2021 at 19:16 UTC