IdrisDoc: Control.WellFounded

# Control.WellFounded

Well-founded recursion.

This is to let us implement some functions that don't have trivial
recursion patterns over datatypes, but instead are using some
other metric of size.

wfRec : WellFounded rel => (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) -> a -> b

Use well-foundedness of a relation to write terminating operations.

rel

a well-founded relation

wfInd : WellFounded rel => (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (x10 : a) -> P x10

Use well-foundedness of a relation to write proofs

rel

a well-founded relation

P

the motive for the induction

step

the induction step: take an element and its accessibility,
and give back a demonstration of P for that element,
potentially using accessibility

accRec : (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) -> (z : a) -> Accessible rel z -> b

A recursor over accessibility.

This allows us to recurse over the subset of some type that is
accessible according to some relation.

rel

the well-founded relation

step

how to take steps on reducing arguments

z

the starting point

accInd : (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (z : a) -> Accessible rel z -> P z

An induction principle for accessibility.

This allows us to recurse over the subset of some type that is
accessible according to some relation, producing a dependent type
as a result.

rel

the well-founded relation

step

how to take steps on reducing arguments

z

the starting point

interface WellFounded

A relation `rel` on `a` is well-founded if all elements of `a` are
acessible.

wellFounded : WellFounded rel => (x : a) -> Accessible rel x
data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type

Accessibility: some element `x` is accessible if all `y` such that
`rel y x` are themselves accessible.

a

the type of elements

rel

a relation on a

x

the acessible element

Access : (acc' : (y : a) -> rel y x -> Accessible rel y) -> Accessible rel x

Accessibility

x

the accessible element

acc'

a demonstration that all smaller elements are also accessible