IdrisDoc: Prelude.WellFounded

# Prelude.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

sizeRec : Sized a => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b) -> (z : a) -> b

Strong recursion principle for sized types.

sizeInd : Sized a => (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x) -> (z : a) -> P z

Strong induction principle for sized types.

sizeAccessible : Sized a => (x : a) -> SizeAccessible x

Proof of well-foundedness of `Smaller`.
Constructs accessibility for any given element of `a`, provided `Sized a`.

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
Smaller : Sized a => a -> a -> Type
interface Sized

Interface of types with sized values.
The size is used for proofs of termination via accessibility.

size : Sized a => a -> Nat
SizeAccessible : Sized a => a -> Type
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 : (rec : (y : a) -> rel y x -> Accessible rel y) -> Accessible rel x

Accessibility

x

the accessible element

rec

a demonstration that all smaller elements are also accessible