Control.WellFounded

Defines well-founded induction and recursion.

Induction is way to consume elements of recursive types where each step of
the computation has access to the previous steps.
Normally, induction is structural: the previous steps are the children of
the current element.
Well-founded induction generalises this as follows: each step has access to
any value that is less than the current element, based on a relation.

Well-founded induction is implemented in terms of accessibility: an element
is accessible (with respect to a given relation) if every element less than
it is also accessible. This can only terminate at minimum elements.

This corresponds to the idea that for a computation to terminate, there
must be a finite path to an element from which there is no way to recurse.

Many instances of well-founded induction are actually induction over
natural numbers that are derived from the elements being inducted over. For
this purpose, the `Sized` interface and related functions are provided.

Definitions

data Accessible : (a -> a -> Type) -> a -> Type

  A value is accessible if everything smaller than it is also accessible.

Totality: total
Visibility: public export
Constructor: 

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

interface WellFounded : (a : Type) -> (a -> a -> Type) -> Type

  A relation is well-founded if every element is accessible.

Parameters: a, rel
Methods:

wellFounded : (x : a) -> Accessible rel x

Implementation: 

WellFounded Nat LT

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

Totality: total
Visibility: public export

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

  Simply-typed recursion based on accessibility.
  
  The recursive step for an element has access to all elements smaller than
  it. The recursion will therefore halt when it reaches a minimum element.
  
  This may sometimes improve type-inference, compared to `accInd`.

Totality: total
Visibility: export

accInd : {0 P : a -> Type} -> ((x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (z : a) -> (0 _ : Accessible rel z) -> P z

  Dependently-typed induction based on accessibility.
  
  The recursive step for an element has access to all elements smaller than
  it. The recursion will therefore halt when it reaches a minimum element.

Totality: total
Visibility: export

accIndProp : {0 P : a -> Type} -> (step : ((x : a) -> ((y : a) -> rel y x -> P y) -> P x)) -> {0 RP : (x : a) -> P x -> Type} -> ((x : a) -> (f : ((y : a) -> rel y x -> P y)) -> ((y : a) -> (isRel : rel y x) -> RP y (f y isRel)) -> RP x (step x f)) -> (z : a) -> (0 acc : Accessible rel z) -> RP z (accInd step z acc)

  Depedently-typed induction for creating extrinsic proofs on results of `accInd`.

Totality: total
Visibility: export

wfRec : {auto 0 _ : WellFounded a rel} -> ((x : a) -> ((y : a) -> rel y x -> b) -> b) -> a -> b

  Simply-typed recursion based on well-founded-ness.
  
  This is `accRec` applied to accessibility derived from a `WellFounded`
  instance.

Totality: total
Visibility: export

wfInd : {auto 0 _ : WellFounded a rel} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (myz : a) -> P myz

  Depedently-typed induction based on well-founded-ness.
  
  This is `accInd` applied to accessibility derived from a `WellFounded`
  instance.

Totality: total
Visibility: export

wfIndProp : {auto 0 {conArg:1383} : WellFounded a rel} -> {0 P : a -> Type} -> (step : ((x : a) -> ((y : a) -> rel y x -> P y) -> P x)) -> {0 RP : (x : a) -> P x -> Type} -> ((x : a) -> (f : ((y : a) -> rel y x -> P y)) -> ((y : a) -> (isRel : rel y x) -> RP y (f y isRel)) -> RP x (step x f)) -> (myz : a) -> RP myz (wfInd step myz)

  Depedently-typed induction for creating extrinsic proofs on results of `wfInd`.

Totality: total
Visibility: export

interface Sized : Type -> Type

  Types that have a concept of size. The size must be a natural number.

Parameters: a
Constructor: 

MkSized

Methods:

size : a -> Nat

Implementations:

Sized Nat

Sized (List a)

(Sized a, Sized b) => Sized (a, b)

size : Sized a => a -> Nat

Totality: total
Visibility: public export

Smaller : Sized a => a -> a -> Type

  A relation based on the size of the values.

Totality: total
Visibility: public export

SizeAccessible : Sized a => a -> Type

  Values that are accessible based on their size.

Totality: total
Visibility: public export

sizeAccessible : {auto {conArg:1589} : Sized a} -> (x : a) -> SizeAccessible x

  Any value of a sized type is accessible, since naturals are well-founded.

Totality: total
Visibility: export

sizeInd : {auto {conArg:1654} : Sized a} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> Smaller y x -> P y) -> P x) -> (z : a) -> P z

  Depedently-typed induction based on the size of values.
  
  This is `accInd` applied to accessibility derived from size.

Totality: total
Visibility: export

sizeRec : {auto {conArg:1715} : Sized a} -> ((x : a) -> ((y : a) -> Smaller y x -> b) -> b) -> a -> b

  Simply-typed recursion based on the size of values.
  
  This is `recInd` applied to accessibility derived from size.

Totality: total
Visibility: export