module Data.Wellfounded.Base where
Well-founded relationsπ
Well-founded relations are, in essence, orders over which induction is acceptable. A relation is well-founded if all of its chains have bounded length, which we can summarize with the following inductive definition of accessibility:
data Acc (x : A) : Type (β β ββ²) where acc : (β y β y < x β Acc y) β Acc x
That is, an element is accessible if every element under it (by the relation ) is also accessible. Paraphrasing the HoTT book, it may seem like such a definition can never get started, but the βbase caseβ is when there are no elements β for example, taking to be the usual on the natural numbers, there are no numbers , so is accessible.
A relation is well-founded if every is accessible.
Wf : Type _ Wf = β x β Acc x
Being well-founded implies that we support induction, and conversely, any relation supporting induction is well-founded, by taking the motive to be the proposition β is accessibleβ.
Wf-induction : Wf β β {ββ²} (P : A β Type ββ²) β (β x β (β y β y < x β P y) β P x) β β x β P x Wf-induction wf P work x = go x (wf x) where go : β x β Acc x β P x go x (acc w) = work x (Ξ» y y<x β go y (w y y<x)) Induction-wf : (β {ββ²} (P : A β Type ββ²) β (β x β (β y β y < x β P y) β P x) β β x β P x) β Wf Induction-wf ind = ind Acc (Ξ» _ β acc)