Zulip Chat Archive

Stream: new members

Topic: Transitive closure of transitive


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Andrew Souther (Nov 27 2020 at 04:21):

Thank you!

view this post on Zulip Bryan Gin-ge Chen (Nov 27 2020 at 04:28):

This is probably worth PRing to mathlib.

view this post on Zulip Yakov Pechersky (Nov 27 2020 at 04:32):

#5129


Last updated: May 10 2021 at 19:16 UTC