Transitive Closure of a Well-Founded Relation

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)