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
  β„“ : Level
  A B : Type β„“
  R : 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))