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)
```