# Transitive Closure of a Well-Founded Relation

Tue 07 March 2023 -

I recently encountered this issue when working with a well-founded relation R. I wanted to use well-founded induction to prove a proposition P, but I needed to use the fact that P holds for not just any y where R y x, but also any z where R z y and R y x-- in other words, I needed my inductive hypothesis to go more than just one step back. This is an issue because my relation is not transitive--in my case, R is a relation between game states, where R y x means that the move x -> y is a valid move. If x -> y and y -> z are valid moves, it does not necessarily follow that x -> z is a valid move.

The problem here is that our inductive hypothesis is not strong enough--we need the equivalent of strong induction on $\mathbb{N}$. To do so, let's instead define a new relation R' that is the transitive closure of R and then induct on R'. To use R', we need to show that it is also well-founded. That is what this short note is about.

Nothing here is novel--an equivalent proof is included in the Agda standard library, and while I couldn't find it in the Coq standard library, it's trivial to translate over.

module TransitiveClosure where

module _ {A : Set} where
module _ (_<_ : A → A → Set) where


The Acc predicate is defined with respect to a relation _<_. To prove that x is accessible, we need to show that if y < x, then y is accessible. Of course to show y is accessible, we would have to use the inductive definition again, so in order to prove anything is accessible, we must eventually arrive at some "least" element.

    data Acc (x : A) : Set where
acc-intro : ((y : A) → y < x → Acc y) → Acc x

-- Inversion lemma
acc-inv : (x : A) → Acc x → ((y : A) → y < x → Acc y)
acc-inv x (acc-intro H) = H


A relation is well-founded if every element is accessible.

    well-founded : Set
well-founded = (x : A) → Acc x


Now we define the transitive closure of _<_.

    data _<'_ : A → A → Set where
<-same : (x y : A) → x < y → x <' y
<-trans : (x y z : A) → x < y → y < z → x <' z


This is the main lemma: we show that if x is accessible under _<_, it is also accessible under _<'_. Suppose y <' x. We want to show that y is accessible under <'. We case on the two constructors:

• If y < x, then we can recursively call acc-trans.
• If y < z < x, then we know inductively that z is accessible under <'. Then since y < z, this follows from our acc-inv lemma.
  module _ (_<_ : A → A → Set) where
acc-trans : ((x : A) → Acc _<_ x → Acc (_<'_ _<_) x)
acc-trans x (acc-intro H) = acc-intro (λ {
y (<-same .y .x y<x) → acc-trans y (H y y<x);
y (<-trans .y z .x y<z z<x) →
acc-inv (_<'_ _<_) z (acc-trans z (H z z<x)) y (<-same y z y<z)
})


Finally we can show that the transitive closure of a well-founded relation is well-founded.

    wf-trans : well-founded _<_ → well-founded (_<'_ _<_)
wf-trans wf x = acc-trans x (wf x)