max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename TC to Relation.TransGen (#4760)

Browse source 
This is barely used in Lean, and this rename is both more readable, and
consistent with further developments downstream.

See
[zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Relation.2ETransGen.20vs.2E.20TC.20from.20Init.2ECore/near/448941824)
discussion.
This commit is contained in:
Kim Morrison 2024-07-16 12:06:49 -05:00 • committed by GitHub
parent b73fe04710
commit 1cf47bce5a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 26 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Core.lean
View file

@ -1089,15 +1089,18 @@ def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β
fun a₁ a₂ => r (f a₁) (f a₂)
/--
The transitive closure `r⁺` of a relation `r` is the smallest relation which is
transitive and contains `r`. `r⁺ a z` if and only if there exists a sequence
The transitive closure `TransGen r` of a relation `r` is the smallest relation which is
transitive and contains `r`. `TransGen r a z` if and only if there exists a sequence
`a r b r ... r z` of length at least 1 connecting `a` to `z`.
-/
inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop where
/-- If `r a b` then `r⁺ a b`. This is the base case of the transitive closure. -/
| base : ∀ a b, r a b → TC r a b
inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop
/-- If `r a b` then `TransGen r a b`. This is the base case of the transitive closure. -/
| single {a b} : r a b → TransGen r a b
/-- The transitive closure is transitive. -/
| trans : ∀ a b c, TC r a b → TC r b c → TC r a c
| tail {a b c} : TransGen r a b → r b c → TransGen r a c
/-- Deprecated synonym for `Relation.TransGen`. -/
@[deprecated Relation.TransGen (since := "2024-07-16")] abbrev TC := @Relation.TransGen
/-! # Subtype -/

30
src/Init/WF.lean
View file

@ -148,22 +148,26 @@ end InvImage
wf := InvImage.wf f h.wf
-- The transitive closure of a well-founded relation is well-founded
namespace TC
variable {α : Sort u} {r : α → α → Prop}
open Relation
theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
induction ac with
| intro x acx ih =>
apply Acc.intro x
intro y rel
induction rel with
| base a b rab => exact ih a rab
| trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
theorem Acc.transGen (h : Acc r a) : Acc (TransGen r) a := by
induction h with
| intro x _ H =>
refine Acc.intro x fun y hy ↦ ?_
cases hy with
| single hyx =>
exact H y hyx
| tail hyz hzx =>
exact (H _ hzx).inv hyz
theorem wf (h : WellFounded r) : WellFounded (TC r) :=
⟨fun a => accessible (apply h a)⟩
end TC
theorem acc_transGen_iff : Acc (TransGen r) a ↔ Acc r a :=
⟨Subrelation.accessible TransGen.single, Acc.transGen⟩
theorem WellFounded.transGen (h : WellFounded r) : WellFounded (TransGen r) :=
⟨fun a ↦ (h.apply a).transGen⟩
@[deprecated Acc.transGen (since := "2024-07-16")] abbrev TC.accessible := @Acc.transGen
@[deprecated WellFounded.transGen (since := "2024-07-16")] abbrev TC.wf := @WellFounded.transGen
namespace Nat
-- less-than is well-founded