Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: rename TC to Relation.TransGen #4760

Merged
merged 1 commit into from
Jul 16, 2024
Merged

chore: rename TC to Relation.TransGen #4760

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 9 additions & 6 deletions src/Init/Core.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 -/

Expand Down
36 changes: 20 additions & 16 deletions src/Init/WF.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}

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 wf (h : WellFounded r) : WellFounded (TC r) :=
⟨fun a => accessible (apply h a)⟩
end TC

open Relation

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 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
Expand Down
Loading