open import 1Lab.Prelude

open import Data.Wellfounded.Base
open import Data.Nat.Order
open import Data.Nat.Base
module Data.Wellfounded.Properties where

It was mentioned in the definition of Acc that being accessible is a proposition, but this has not yet been established. We can do so using, as usual, induction:

private variable
  β„“ β„“r β„“s : Level
  A B : Type β„“
  R S : A β†’ A β†’ Type β„“
Acc-is-prop : βˆ€ x β†’ is-prop (Acc R x)
Acc-is-prop x (acc s) (acc t) =
  ap acc (ext Ξ» y y<x β†’ Acc-is-prop y (s y y<x) (t y y<x))

Wf-is-prop : is-prop (Wf R)
Wf-is-prop = Ξ -is-hlevel 1 Acc-is-prop

InstancesπŸ”—

The usual induction principle for the natural numbers is equivalent to saying that the relation is well-founded. Additionally, the relation on the natural numbers is well-founded.

suc-wf : Wf (Ξ» x y β†’ y ≑ suc x)
suc-wf = Induction-wf (Ξ» x y β†’ y ≑ suc x) Ξ» P m β†’
  Nat-elim P
    (m 0 λ y 0=suc → absurd (zero≠suc 0=suc))
    Ξ» {n} Pn β†’ m (suc n) (Ξ» y s β†’ subst P (suc-inj s) Pn)

<-wf : Wf _<_
<-wf x = go x x ≀-refl where
  go : (x y : Nat) β†’ .(y ≀ x) β†’ Acc _<_ y
  go x zero w = acc Ξ» _ ()
  go (suc x) (suc y) w = acc k' where
    k' : βˆ€ x β†’ x < suc y β†’ Acc _<_ x
    k' x' w' = go x x' (≀-trans (≀-peel w') (≀-peel w))

Let and be a pair of types equipped with relations, and be a map that satisfies

If is a well-founded relation on then must also be well-founded.

reflect-wf
  : Wf S
  β†’ (f : A β†’ B)
  β†’ (βˆ€ {x y} β†’ R x y β†’ S (f x) (f y))
  β†’ Wf R

The idea here is to use the fact that every in the image of must be accessible. Let such that and is accessible via To show that is accessible via we must show that is accessible for every However, monotonicity of means that and which means that must be accessible via We can then recurse to show that is accessible.

reflect-wf {B = B} {S = S} {A = A} {R = R} S-wf f f-mono a = im-acc (f a) a refl (S-wf (f a)) where
  im-acc : (b : B) (a : A) β†’ f a ≑ b β†’ Acc S b β†’ Acc R a
  im-acc b a fa=b (acc rec) = acc Ξ» a' R[a',a] β†’
    im-acc (f a') a' refl (rec (f a') (subst (S (f a')) fa=b (f-mono R[a',a])))

As a corollary, we can pull back accessibility along arbitrary functions.

pullback-wf
  : (f : A β†’ B)
  β†’ Wf R
  β†’ Wf (Ξ» x y β†’ R (f x) (f y))
pullback-wf f R-wf = reflect-wf R-wf f id