||| 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. module Control.WellFounded %default total ||| 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 data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where ||| Accessibility ||| ||| @ x the accessible element ||| @ acc' a demonstration that all smaller elements are also accessible Access : (acc' : (y : a) -> rel y x -> Accessible rel y) -> Accessible rel x ||| A relation `rel` on `a` is well-founded if all elements of `a` are ||| acessible. ||| ||| @ rel the well-founded relation class WellFounded (rel : a -> a -> Type) where wellFounded : (x : _) -> Accessible rel x ||| 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 accRec : {rel : a -> a -> Type} -> (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) -> (z : a) -> Accessible rel z -> b accRec step z (Access f) = step z \$ \y, lt => accRec step y (f y lt) ||| 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 accInd : {rel : a -> a -> Type} -> {P : a -> Type} -> (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (z : a) -> Accessible rel z -> P z accInd step z (Access f) = step z \$ \y, lt => accInd step y (f y lt) ||| Use well-foundedness of a relation to write terminating operations. ||| ||| @ rel a well-founded relation wfRec : WellFounded rel => (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) -> a -> b wfRec {rel} step x = accRec step x (wellFounded {rel} x) ||| 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 wfInd : WellFounded rel => {P : a -> Type} -> (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (x : a) -> P x wfInd {rel} step x = accInd step x (wellFounded {rel} x)