Data.Type.Natural.Lemma.Order

Documentation

data DiffNat n m where

Constructors

DiffNat :: SNat n -> SNat m -> DiffNat n (n + m)

data LeqView n m where

Constructors

LeqZero :: SNat n -> LeqView 0 n

LeqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)

type (<) n m = (n <? m) ~ 'True infix 4

type (<?) n m = (n + 1) <=? m infix 4

(%<?) :: SNat n -> SNat m -> SBool (n <? m) infix 4

type (>) n m = (n >? m) ~ 'True infix 4

type (>?) n m = m <? n infix 4

(%>?) :: SNat n -> SNat m -> SBool (n >? m) infix 4

type (>=) n m = (n >=? m) ~ 'True infix 4

type (>=?) n m = m <=? n infix 4

(%>=?) :: SNat n -> SNat m -> SBool (n >=? m) infix 4

type family FlipOrdering ord where ...

Equations

FlipOrdering 'LT = 'GT

FlipOrdering 'GT = 'LT

FlipOrdering 'EQ = 'EQ

type Min n m = MinAux (n <=? m) n m

sMin :: SNat n -> SNat m -> SNat (Min n m)

type Max n m = MaxAux (n >=? m) n m

sMax :: SNat n -> SNat m -> SNat (Max n m)

Lemmas

sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)

coerceLeqL :: forall n m l. (n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)

Since 1.0.0.0 (type changed)

coerceLeqR :: forall n m l. SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)

Since 1.0.0.0 (type changed)

sLeqCongL :: (a :~: b) -> SNat c -> (a <= c) :~: (b <= c)

sLeqCongR :: SNat a -> (b :~: c) -> (a <= b) :~: (a <= c)

sLeqCong :: (a :~: b) -> (c :~: d) -> (a <= c) :~: (b <= d)

succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)

compareCongR :: SNat a -> (b :~: c) -> CmpNat a b :~: CmpNat a c

leqToCmp :: SNat a -> SNat b -> IsTrue (a <=? b) -> Either (a :~: b) (CmpNat a b :~: 'LT)

eqlCmpEQ :: SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ

eqToRefl :: SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b

flipCmpNat :: SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a

ltToNeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void

leqNeqToLT :: SNat a -> SNat b -> IsTrue (a <=? b) -> ((a :~: b) -> Void) -> CmpNat a b :~: 'LT

succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT

ltToLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)

gtToLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a)

congFlipOrdering :: (a :~: b) -> FlipOrdering a :~: FlipOrdering b

ltToSuccLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)

cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT

leqToGT :: SNat a -> SNat b -> IsTrue (Succ b <=? a) -> CmpNat a b :~: 'GT

cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)

zeroNoLT :: SNat a -> (CmpNat a 0 :~: 'LT) -> Void

ltRightPredSucc :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)

cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)

ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT

cmpSuccStepR :: forall n m. SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT

ltSuccLToLT :: SNat n -> SNat m -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n m :~: 'LT

leqToLT :: SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT

leqZero :: SNat n -> IsTrue (0 <=? n)

leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)

fromLeqView :: LeqView n m -> IsTrue (n <=? m)

leqViewRefl :: SNat n -> LeqView n n

viewLeq :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m

leqWitness :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m

leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)

leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <=? m)

leqRefl :: SNat n -> IsTrue (n <=? n)

leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)

leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)

leqReflexive :: SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)

leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)

leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m

plusMonotone :: SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <=? m) -> IsTrue (l <=? k) -> IsTrue ((n + l) <=? (m + k))

leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0

plusMonotoneL :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue ((n + l) <=? (m + l))

plusMonotoneR :: SNat n -> SNat m -> SNat l -> IsTrue (m <=? l) -> IsTrue ((n + m) <=? (n + l))

plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))

plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))

plusCancelLeqR :: SNat n -> SNat m -> SNat l -> IsTrue ((n + l) <=? (m + l)) -> IsTrue (n <=? m)

plusCancelLeqL :: SNat n -> SNat m -> SNat l -> IsTrue ((n + m) <=? (n + l)) -> IsTrue (m <=? l)

succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void

succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False

succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void

succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False

notLeqToLeq :: forall n m. (n <=? m) ~ 'False => SNat n -> SNat m -> IsTrue (m <=? n)

leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)

leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n

geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m

minComm :: SNat n -> SNat m -> Min n m :~: Min m n

minLeqL :: SNat n -> SNat m -> IsTrue (Min n m <=? n)

minLeqR :: SNat n -> SNat m -> IsTrue (Min n m <=? m)

minLargest :: SNat l -> SNat n -> SNat m -> IsTrue (l <=? n) -> IsTrue (l <=? m) -> IsTrue (l <=? Min n m)

leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m

geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n

maxComm :: SNat n -> SNat m -> Max n m :~: Max m n

maxLeqR :: SNat n -> SNat m -> IsTrue (m <=? Max n m)

maxLeqL :: SNat n -> SNat m -> IsTrue (n <=? Max n m)

maxLeast :: SNat l -> SNat n -> SNat m -> IsTrue (n <=? l) -> IsTrue (m <=? l) -> IsTrue (Max n m <=? l)

lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (Succ n <= m)

lneqReversed :: SNat n -> SNat m -> (n < m) :~: (m > n)

lneqToLT :: SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT

ltToLneq :: SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)

lneqZero :: SNat a -> IsTrue (0 <? Succ a)

lneqSucc :: SNat n -> IsTrue (n <? Succ n)

succLneqSucc :: SNat n -> SNat m -> (n <? m) :~: (Succ n <? Succ m)

lneqRightPredSucc :: SNat n -> SNat m -> IsTrue (n <? m) -> m :~: Succ (Pred m)

lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)

lneqSuccStepR :: SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)

plusStrictMonotone :: SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <? m) -> IsTrue (l <? k) -> IsTrue ((n + l) <? (m + k))

maxZeroL :: SNat n -> Max 0 n :~: n

maxZeroR :: SNat n -> Max n 0 :~: n

minZeroL :: SNat n -> Min 0 n :~: 0

minZeroR :: SNat n -> Min n 0 :~: 0

minusSucc :: SNat n -> SNat m -> IsTrue (m <=? n) -> (Succ n - m) :~: Succ (n - m)

lneqZeroAbsurd :: SNat n -> IsTrue (n <? 0) -> Void

minusPlus :: forall n m. SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n

minPlusTruncMinus :: SNat n -> SNat m -> (Min n m + (n -. m)) :~: n

truncMinusLeq :: SNat n -> SNat m -> IsTrue ((n -. m) <=? n)

type (-.) n m = Subt n m (m <=? n) infixl 6

Natural subtraction, truncated to zero if m > n.

(%-.) :: SNat n -> SNat m -> SNat (n -. m)

Various witnesses for orderings

type LeqWitness n m = IsTrue (n <=? m)

data a :<: b

Instances

Show (a :<: b)

Defined in Data.Type.Natural.Lemma.Order

Methods

showsPrec :: Int -> (a :<: b) -> ShowS

show :: (a :<: b) -> String

showList :: [a :<: b] -> ShowS

data Leq n m where

Comparison via GADTs.

Constructors

ZeroLeq :: SNat m -> Leq 0 m

SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1)

leqRhs :: Leq n m -> SNat m

leqLhs :: Leq n m -> SNat n

conversions between lax orders

propToBoolLeq :: forall n m. Leq n m -> LeqWitness n m

boolToPropLeq :: n <= m => SNat n -> SNat m -> Leq n m

conversions between strict orders

propToBoolLt :: (n :<: m) -> IsTrue (n <? m)

boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m