Control.WellFounded


   0 | ||| Defines well-founded induction and recursion.
   1 | |||
   2 | ||| Induction is way to consume elements of recursive types where each step of
   3 | ||| the computation has access to the previous steps.
   4 | ||| Normally, induction is structural: the previous steps are the children of
   5 | ||| the current element.
   6 | ||| Well-founded induction generalises this as follows: each step has access to
   7 | ||| any value that is less than the current element, based on a relation.
   8 | |||
   9 | ||| Well-founded induction is implemented in terms of accessibility: an element
  10 | ||| is accessible (with respect to a given relation) if every element less than
  11 | ||| it is also accessible. This can only terminate at minimum elements.
  12 | |||
  13 | ||| This corresponds to the idea that for a computation to terminate, there
  14 | ||| must be a finite path to an element from which there is no way to recurse.
  15 | |||
  16 | ||| Many instances of well-founded induction are actually induction over
  17 | ||| natural numbers that are derived from the elements being inducted over. For
  18 | ||| this purpose, the `Sized` interface and related functions are provided.
  19 | module Control.WellFounded
  20 | 
  21 | import Control.Relation
  22 | import Data.Nat
  23 | 
  24 | %default total
  25 | 
  26 | ||| A value is accessible if everything smaller than it is also accessible.
  27 | public export
  28 | data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where
  29 |   Access : (rec : (y : a) -> rel y x -> Accessible rel y) ->
  30 |            Accessible rel x
  31 | 
  32 | ||| A relation is well-founded if every element is accessible.
  33 | public export
  34 | interface WellFounded a rel where
  35 |   wellFounded : (x : a) -> Accessible rel x
  36 | 
  37 | ||| Simply-typed recursion based on accessibility.
  38 | |||
  39 | ||| The recursive step for an element has access to all elements smaller than
  40 | ||| it. The recursion will therefore halt when it reaches a minimum element.
  41 | |||
  42 | ||| This may sometimes improve type-inference, compared to `accInd`.
  43 | export
  44 | accRec : {0 rel : (arg1 : a) -> (arg2 : a) -> Type} ->
  45 |          (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
  46 |          (z : a) -> (0 acc : Accessible rel z) -> b
  47 | accRec step z (Access f) =
  48 |   step z $ \yarg, lt => accRec step yarg (f yarg lt)
  49 | 
  50 | ||| Dependently-typed induction based on accessibility.
  51 | |||
  52 | ||| The recursive step for an element has access to all elements smaller than
  53 | ||| it. The recursion will therefore halt when it reaches a minimum element.
  54 | export
  55 | accInd : {0 rel : a -> a -> Type} -> {0 P : a -> Type} ->
  56 |          (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
  57 |          (z : a) -> (0 acc : Accessible rel z) -> P z
  58 | accInd step z (Access f) =
  59 |   step z $ \y, lt => accInd step y (f y lt)
  60 | 
  61 | ||| Depedently-typed induction for creating extrinsic proofs on results of `accInd`.
  62 | export
  63 | accIndProp : {0 P : a -> Type} ->
  64 |             (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
  65 |             {0 RP : (x : a) -> P x -> Type} ->
  66 |             (ih : (x : a) ->
  67 |                   (f : (y : a) -> rel y x -> P y) ->
  68 |                   ((y : a) -> (isRel : rel y x) -> RP y (f y isRel)) ->
  69 |                   RP x (step x f)) ->
  70 |             (z : a) -> (0 acc : Accessible rel z) -> RP z (accInd step z acc)
  71 | accIndProp step ih z (Access rec) =
  72 |   ih z (\y, lt => accInd step y (rec y lt))
  73 |        (\y, lt => accIndProp {RP} step ih y (rec y lt))
  74 | 
  75 | ||| Simply-typed recursion based on well-founded-ness.
  76 | |||
  77 | ||| This is `accRec` applied to accessibility derived from a `WellFounded`
  78 | ||| instance.
  79 | export
  80 | wfRec : (0 _ : WellFounded a rel) =>
  81 |         (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
  82 |         a -> b
  83 | wfRec step x = accRec step x (wellFounded {rel} x)
  84 | 
  85 | ||| Depedently-typed induction based on well-founded-ness.
  86 | |||
  87 | ||| This is `accInd` applied to accessibility derived from a `WellFounded`
  88 | ||| instance.
  89 | export
  90 | wfInd : (0 _ : WellFounded a rel) => {0 P : a -> Type} ->
  91 |         (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
  92 |         (myz : a) -> P myz
  93 | wfInd step myz = accInd step myz (wellFounded {rel} myz)
  94 | 
  95 | ||| Depedently-typed induction for creating extrinsic proofs on results of `wfInd`.
  96 | export
  97 | wfIndProp : (0 _ : WellFounded a rel) =>
  98 |             {0 P : a -> Type} ->
  99 |             (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
 100 |             {0 RP : (x : a) -> P x -> Type} ->
 101 |             (ih : (x : a) ->
 102 |                   (f : (y : a) -> rel y x -> P y) ->
 103 |                   ((y : a) -> (isRel : rel y x) -> RP y (f y isRel)) ->
 104 |                   RP x (step x f)) ->
 105 |             (myz : a) -> RP myz (wfInd step myz)
 106 | wfIndProp step ih myz = accIndProp {RP} step ih myz (wellFounded {rel} myz)
 107 | 
 108 | ||| Types that have a concept of size. The size must be a natural number.
 109 | public export
 110 | interface Sized a where
 111 |   constructor MkSized
 112 |   total size : a -> Nat
 113 | 
 114 | ||| A relation based on the size of the values.
 115 | public export
 116 | Smaller : Sized a => a -> a -> Type
 117 | Smaller = \x, y => size x `LT` size y
 118 | 
 119 | ||| Values that are accessible based on their size.
 120 | public export
 121 | SizeAccessible : Sized a => a -> Type
 122 | SizeAccessible = Accessible Smaller
 123 | 
 124 | ||| Any value of a sized type is accessible, since naturals are well-founded.
 125 | export
 126 | sizeAccessible : Sized a => (x : a) -> SizeAccessible x
 127 | sizeAccessible x = Access (acc $ size x)
 128 |   where
 129 |     acc : (sizeX : Nat) -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
 130 |     acc (S x') y (LTESucc yLEx')
 131 |         = Access $ \z, zLTy => acc x' z $ transitive zLTy yLEx'
 132 | 
 133 | ||| Depedently-typed induction based on the size of values.
 134 | |||
 135 | ||| This is `accInd` applied to accessibility derived from size.
 136 | export
 137 | sizeInd : Sized a => {0 P : a -> Type} ->
 138 |           (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x) ->
 139 |           (z : a) ->
 140 |           P z
 141 | sizeInd step z = accInd step z (sizeAccessible z)
 142 | 
 143 | ||| Simply-typed recursion based on the size of values.
 144 | |||
 145 | ||| This is `recInd` applied to accessibility derived from size.
 146 | export
 147 | sizeRec : Sized a =>
 148 |           (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b) ->
 149 |           (z : a) -> b
 150 | sizeRec step z = accRec step z (sizeAccessible z)
 151 | 
 152 | export
 153 | Sized Nat where
 154 |   size = id
 155 | 
 156 | export
 157 | WellFounded Nat LT where
 158 |   wellFounded = sizeAccessible
 159 | 
 160 | export
 161 | Sized (List a) where
 162 |   size = length
 163 | 
 164 | export
 165 | (Sized a, Sized b) => Sized (Pair a b) where
 166 |   size (x,y) = size x + size y
 167 |