Finite trans-inverse image and trans-irreflexive implies wellfounded #
We prove some helper lemmas about Relation.TransGen and WellFounded.
The main result here is wf_of_finTransInvImage_of_transIrrefl
and to be used for termination of the tableauGame.
theorem
wf_of_trans_wf
{α : Type}
{r : α → α → Prop}
(trans_wf : WellFounded (Relation.TransGen r))
:
If the transitive closure of r is wellfounded, then r itself is wellfounded.
This was for example proven in https://www.cs.utexas.edu/~EWD/ewd12xx/EWD1241.PDF (page 2 aka 3)
(but here we prove it via WellFounded.wellFounded_iff_has_min instead.
theorem
Finite.wf_of_irrefl_trans
{α : Type}
(r : α → α → Prop)
[Finite α]
(trans_irrefl : IsIrrefl α (Relation.TransGen r))
:
theorem
TransGen_from_Subtype
{α : Type}
{r : α → α → Prop}
{P : α → Prop}
{x y : Subtype P}
(h : Relation.TransGen (fun (x y : Subtype P) => r ↑x ↑y) x y)
:
Relation.TransGen r ↑x ↑y
theorem
wf_of_finTransInvImage_of_transIrrefl
{α : Type}
(r : α → α → Prop)
(finTransInvImage : ∀ (p : α), Finite { q : α // Relation.TransGen r q p })
(trans_irrefl : IsIrrefl α (Relation.TransGen r))
:
Suppose for any p the inverse-image of p under the transitive closure of r is finite,
and suppose the transitive closure of r is irreflexive. Then r is wellfounded.