SatisfyPairs.idr

%language ElabReflection

data SatisfyPairs : (a -> a -> Type) -> List a -> Type where
  SatEmpty : SatisfyPairs p []
  SatSingleton : SatisfyPairs p [x]
  SatPair : p x y -> SatisfyPairs p (y :: ys) -> SatisfyPairs p (x :: y :: ys)

MonotonicallyIncreasingNat : List Nat -> Type
MonotonicallyIncreasingNat = SatisfyPairs LTE

StrictlyIncreasingNat : List Nat -> Type
StrictlyIncreasingNat = SatisfyPairs LT

pf1 : StrictlyIncreasingNat [1..10]
pf1 = %runElab search

pf2 : MonotonicallyIncreasingNat [1,1,2,2,3,4,6,6,6]
pf2 = %runElab search

-- If we depend on the primitive boolean comparison operators:

OrdLT : Ord a => a -> a -> Type
OrdLT x y = (x < y) = True

OrdLTE : Ord a => a -> a -> Type
OrdLTE x y = (x <= y) = True

MonotonicallyIncreasing : Ord a => List a -> Type
MonotonicallyIncreasing = SatisfyPairs OrdLTE

StrictlyIncreasing : Ord a => List a -> Type
StrictlyIncreasing = SatisfyPairs OrdLT

pf3 : StrictlyIncreasing (the (List Int) [1,2,3])
pf3 = %runElab search

pf4 : MonotonicallyIncreasing (the (List Int) [1,1,2,2,3,4,6,6,6])
pf4 = %runElab search