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 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 (funext Ξ» y β†’ funext Ξ» 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 R(x,y):=y=1+xR(x,y) := y = 1+x 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))