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