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