Safe Haskell	None
Language	Haskell2010

Data.Type.Natural.Lemma.Order

Contents

Lemmas
Various witnesses for orderings
- conversions between lax orders
- conversions between strict orders

Synopsis

data DiffNat (n :: Natural) (m :: Natural) where
- DiffNat :: forall (n :: Natural) (m1 :: Natural). SNat n -> SNat m1 -> DiffNat n (n + m1)
data LeqView (n :: Natural) (m :: Nat) where
- LeqZero :: forall (m :: Nat). SNat m -> LeqView 0 m
- LeqSucc :: forall (n1 :: Natural) (m1 :: Natural). SNat n1 -> SNat m1 -> IsTrue (n1 <=? m1) -> LeqView (n1 + 1) (m1 + 1)
type (<) (n :: Nat) (m :: Nat) = n < m
type (<?) (n :: Nat) (m :: Nat) = n <? m
(%<?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
type (>) (n :: Nat) (m :: Nat) = n > m
type (>?) (n :: Nat) (m :: Nat) = n >? m
(%>?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >? m)
type (>=) (n :: Nat) (m :: Nat) = n >= m
type (>=?) (n :: Nat) (m :: Nat) = n >=? m
(%>=?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >=? m)
type family FlipOrdering (ord :: Ordering) :: Ordering where ...
type Min (m :: Nat) (n :: Nat) = Min m n
sMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
type Max (m :: Nat) (n :: Nat) = Max m n
sMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
type family OrdCond (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where ...
sOrdCond :: forall {k} (o :: Ordering) f (lt :: k) (eq :: k) (gt :: k). SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
ordCondDistrib :: forall {k1} {k2} proxy (f :: k1 -> k2) (o :: Ordering) p (l :: k1) p' (e :: k1) p'' (g :: k1). proxy f -> SOrdering o -> p l -> p' e -> p'' g -> OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)
leqOrdCond :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <=? m) :~: OrdCond (CmpNat n m) 'True 'True 'False
sFlipOrdering :: forall (ord :: Ordering). SOrdering ord -> SOrdering (FlipOrdering ord)
coerceLeqL :: forall (n :: Nat) (m :: Nat) (l :: Nat). (n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqR :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)
sLeqCongL :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a :~: b) -> SNat c -> (a <= c) :~: (b <= c)
sLeqCongR :: forall (a :: Nat) (b :: Nat) (c :: Nat). SNat a -> (b :~: c) -> (a <= b) :~: (a <= c)
sLeqCong :: forall {t} (a :: t) (b :: t) (c :: t) (d :: t). (a :~: b) -> (c :~: d) -> (a <= c) :~: (b <= d)
succDiffNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
compareCongR :: forall (a :: Nat) (b :: Natural) (c :: Natural). SNat a -> (b :~: c) -> CmpNat a b :~: CmpNat a c
leqToCmp :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (a <=? b) -> Either (a :~: b) (CmpNat a b :~: 'LT)
eqlCmpEQ :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqToRefl :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b
flipCmpNat :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
ltToNeq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void
leqNeqToLT :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (a <=? b) -> ((a :~: b) -> Void) -> CmpNat a b :~: 'LT
succLeqToLT :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
ltToLeq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
gtToLeq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a)
congFlipOrdering :: forall (a :: Ordering) (b :: Ordering). (a :~: b) -> FlipOrdering a :~: FlipOrdering b
ltToSuccLeq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
cmpZero :: forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpSuccZeroGT :: forall (a :: Nat). SNat a -> CmpNat (Succ a) 0 :~: 'GT
leqToGT :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (Succ b <=? a) -> CmpNat a b :~: 'GT
cmpZero' :: forall (a :: Nat). SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
zeroNoLT :: forall (a :: Nat). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
ltRightPredSucc :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
cmpSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
ltSucc :: forall (a :: Nat). SNat a -> CmpNat a (Succ a) :~: 'LT
cmpSuccStepR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
ltSuccLToLT :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n m :~: 'LT
leqToLT :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
leqZero :: forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
fromLeqView :: forall (n :: Natural) (m :: Nat). LeqView n m -> IsTrue (n <=? m)
leqViewRefl :: forall (n :: Nat). SNat n -> LeqView n n
viewLeq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
leqWitness :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqStep :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqNeqToSuccLeq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <=? m)
leqRefl :: forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqSuccStepR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqReflexive :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqTrans :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)
leqAntisymm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
plusMonotone :: forall (n :: Nat) (m :: Nat) (l :: Nat) (k :: Nat). SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <=? m) -> IsTrue (l <=? k) -> IsTrue ((n + l) <=? (m + k))
leqZeroElim :: forall (n :: Nat). SNat n -> IsTrue (n <=? 0) -> n :~: 0
plusMonotoneL :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue ((n + l) <=? (m + l))
plusMonotoneR :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue (m <=? l) -> IsTrue ((n + m) <=? (n + l))
plusLeqL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? (n + m))
plusCancelLeqR :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue ((n + l) <=? (m + l)) -> IsTrue (n <=? m)
plusCancelLeqL :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue ((n + m) <=? (n + l)) -> IsTrue (m <=? l)
succLeqZeroAbsurd :: forall (n :: Nat). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd' :: forall (n :: Nat). SNat n -> (S n <=? 0) :~: 'False
succLeqAbsurd :: forall (n :: Nat). SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd' :: forall (n :: Nat). SNat n -> (S n <=? n) :~: 'False
notLeqToLeq :: forall (n :: Nat) (m :: Nat). (n <=? m) ~ 'False => SNat n -> SNat m -> IsTrue (m <=? n)
leqSucc' :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
leqToMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
geqToMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
minComm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Min n m :~: Min m n
minLeqL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (Min n m <=? n)
minLeqR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (Min n m <=? m)
minLargest :: forall (l :: Nat) (n :: Nat) (m :: Nat). SNat l -> SNat n -> SNat m -> IsTrue (l <=? n) -> IsTrue (l <=? m) -> IsTrue (l <=? Min n m)
leqToMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
geqToMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
maxComm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Max n m :~: Max m n
maxLeqR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? Max n m)
maxLeast :: forall (l :: Nat) (n :: Nat) (m :: Nat). SNat l -> SNat n -> SNat m -> IsTrue (n <=? l) -> IsTrue (m <=? l) -> IsTrue (Max n m <=? l)
lneqSuccLeq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqReversed :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <? m) :~: (m >? n)
lneqToLT :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
ltToLneq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
lneqZero :: forall (a :: Nat). SNat a -> IsTrue (0 <? Succ a)
lneqSucc :: forall (n :: Nat). SNat n -> IsTrue (n <? Succ n)
succLneqSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <? m) :~: (Succ n <? Succ m)
lneqRightPredSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <? m) -> m :~: Succ (Pred m)
lneqSuccStepL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
lneqSuccStepR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)
plusStrictMonotone :: forall (n :: Nat) (m :: Nat) (l :: Nat) (k :: Nat). SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <? m) -> IsTrue (l <? k) -> IsTrue ((n + l) <? (m + k))
minCase :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m)
maxCase :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n)
maxZeroL :: forall (n :: Nat). SNat n -> Max 0 n :~: n
maxZeroR :: forall (n :: Nat). SNat n -> Max n 0 :~: n
minZeroL :: forall (n :: Nat). SNat n -> Min 0 n :~: 0
minZeroR :: forall (n :: Nat). SNat n -> Min n 0 :~: 0
minusSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? n) -> (Succ n - m) :~: Succ (n - m)
lneqZeroAbsurd :: forall (n :: Nat). SNat n -> IsTrue (n <? 0) -> Void
minusPlus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minPlusTruncMinus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (Min n m + (n -. m)) :~: n
truncMinusLeq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue ((n -. m) <=? n)
type (-.) (n :: Natural) (m :: Natural) = Subt n m (m <=? n)
(%-.) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
type LeqWitness (n :: k) (m :: k) = IsTrue (n <=? m)
data (a :: Natural) :<: (b :: Natural)
data Leq (n :: Natural) (m :: Nat) where
- ZeroLeq :: forall (m :: Nat). SNat m -> Leq 0 m
- SuccLeqSucc :: forall (n1 :: Natural) (m1 :: Natural). Leq n1 m1 -> Leq (n1 + 1) (m1 + 1)
leqRhs :: forall (n :: Natural) (m :: Nat). Leq n m -> SNat m
leqLhs :: forall (n :: Natural) (m :: Nat). Leq n m -> SNat n
propToBoolLeq :: forall (n :: Natural) (m :: Nat). Leq n m -> LeqWitness n m
boolToPropLeq :: forall (n :: Nat) (m :: Nat). n <= m => SNat n -> SNat m -> Leq n m
propToBoolLt :: forall (n :: Natural) (m :: Natural). (n :<: m) -> IsTrue (n <? m)
boolToPropLt :: forall (n :: Nat) (m :: Nat). n < m => SNat n -> SNat m -> n :<: m

Documentation

data DiffNat (n :: Natural) (m :: Natural) where Source #

Constructors

DiffNat :: forall (n :: Natural) (m1 :: Natural). SNat n -> SNat m1 -> DiffNat n (n + m1)

data LeqView (n :: Natural) (m :: Nat) where Source #

Constructors

LeqZero :: forall (m :: Nat). SNat m -> LeqView 0 m
LeqSucc :: forall (n1 :: Natural) (m1 :: Natural). SNat n1 -> SNat m1 -> IsTrue (n1 <=? m1) -> LeqView (n1 + 1) (m1 + 1)

type (<) (n :: Nat) (m :: Nat) = n < m infix 4 Source #

type (<?) (n :: Nat) (m :: Nat) = n <? m infix 4 Source #

(%<?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m) infix 4 Source #

type (>) (n :: Nat) (m :: Nat) = n > m infix 4 Source #

type (>?) (n :: Nat) (m :: Nat) = n >? m infix 4 Source #

(%>?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >? m) infix 4 Source #

type (>=) (n :: Nat) (m :: Nat) = n >= m infix 4 Source #

type (>=?) (n :: Nat) (m :: Nat) = n >=? m infix 4 Source #

(%>=?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >=? m) infix 4 Source #

type family FlipOrdering (ord :: Ordering) :: Ordering where ... Source #

Equations

FlipOrdering 'LT = 'GT
FlipOrdering 'GT = 'LT
FlipOrdering 'EQ = 'EQ

type Min (m :: Nat) (n :: Nat) = Min m n Source #

sMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m) Source #

type Max (m :: Nat) (n :: Nat) = Max m n Source #

sMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m) Source #

type family OrdCond (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where ... #

A case statement on Ordering.

OrdCond c l e g is l when c ~ LT, e when c ~ EQ, and g when c ~ GT.

Since: base-4.16.0.0

Equations

OrdCond 'LT (lt :: k) (eq :: k) (gt :: k) = lt
OrdCond 'EQ (lt :: k) (eq :: k) (gt :: k) = eq
OrdCond 'GT (lt :: k) (eq :: k) (gt :: k) = gt

sOrdCond :: forall {k} (o :: Ordering) f (lt :: k) (eq :: k) (gt :: k). SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt) Source #

Lemmas

ordCondDistrib :: forall {k1} {k2} proxy (f :: k1 -> k2) (o :: Ordering) p (l :: k1) p' (e :: k1) p'' (g :: k1). proxy f -> SOrdering o -> p l -> p' e -> p'' g -> OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g) Source #

leqOrdCond :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <=? m) :~: OrdCond (CmpNat n m) 'True 'True 'False Source #

sFlipOrdering :: forall (ord :: Ordering). SOrdering ord -> SOrdering (FlipOrdering ord) Source #

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

Since 1.0.0.0 (type changed)

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

Since 1.0.0.0 (type changed)

sLeqCongL :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a :~: b) -> SNat c -> (a <= c) :~: (b <= c) Source #

sLeqCongR :: forall (a :: Nat) (b :: Nat) (c :: Nat). SNat a -> (b :~: c) -> (a <= b) :~: (a <= c) Source #

sLeqCong :: forall {t} (a :: t) (b :: t) (c :: t) (d :: t). (a :~: b) -> (c :~: d) -> (a <= c) :~: (b <= d) Source #

succDiffNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m) Source #

compareCongR :: forall (a :: Nat) (b :: Natural) (c :: Natural). SNat a -> (b :~: c) -> CmpNat a b :~: CmpNat a c Source #

leqToCmp :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (a <=? b) -> Either (a :~: b) (CmpNat a b :~: 'LT) Source #

eqlCmpEQ :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ Source #

eqToRefl :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b Source #

flipCmpNat :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a Source #

ltToNeq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void Source #

leqNeqToLT :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (a <=? b) -> ((a :~: b) -> Void) -> CmpNat a b :~: 'LT Source #

succLeqToLT :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT Source #

ltToLeq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b) Source #

gtToLeq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a) Source #

congFlipOrdering :: forall (a :: Ordering) (b :: Ordering). (a :~: b) -> FlipOrdering a :~: FlipOrdering b Source #

ltToSuccLeq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b) Source #

cmpZero :: forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT Source #

cmpSuccZeroGT :: forall (a :: Nat). SNat a -> CmpNat (Succ a) 0 :~: 'GT Source #

leqToGT :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (Succ b <=? a) -> CmpNat a b :~: 'GT Source #

cmpZero' :: forall (a :: Nat). SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT) Source #

zeroNoLT :: forall (a :: Nat). SNat a -> (CmpNat a 0 :~: 'LT) -> Void Source #

ltRightPredSucc :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b) Source #

cmpSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m) Source #

ltSucc :: forall (a :: Nat). SNat a -> CmpNat a (Succ a) :~: 'LT Source #

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

ltSuccLToLT :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n m :~: 'LT Source #

leqToLT :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT Source #

leqZero :: forall (n :: Nat). SNat n -> IsTrue (0 <=? n) Source #

leqSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m) Source #

fromLeqView :: forall (n :: Natural) (m :: Nat). LeqView n m -> IsTrue (n <=? m) Source #

leqViewRefl :: forall (n :: Nat). SNat n -> LeqView n n Source #

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

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

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

leqNeqToSuccLeq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <=? m) Source #

leqRefl :: forall (n :: Nat). SNat n -> IsTrue (n <=? n) Source #

leqSuccStepR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m) Source #

leqSuccStepL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m) Source #

leqReflexive :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m) Source #

leqTrans :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l) Source #

leqAntisymm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m Source #

plusMonotone :: forall (n :: Nat) (m :: Nat) (l :: Nat) (k :: Nat). SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <=? m) -> IsTrue (l <=? k) -> IsTrue ((n + l) <=? (m + k)) Source #

leqZeroElim :: forall (n :: Nat). SNat n -> IsTrue (n <=? 0) -> n :~: 0 Source #

plusMonotoneL :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue ((n + l) <=? (m + l)) Source #

plusMonotoneR :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue (m <=? l) -> IsTrue ((n + m) <=? (n + l)) Source #

plusLeqL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? (n + m)) Source #

plusLeqR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? (n + m)) Source #

plusCancelLeqR :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue ((n + l) <=? (m + l)) -> IsTrue (n <=? m) Source #

plusCancelLeqL :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> SNat m -> SNat l -> IsTrue ((n + m) <=? (n + l)) -> IsTrue (m <=? l) Source #

succLeqZeroAbsurd :: forall (n :: Nat). SNat n -> IsTrue (S n <=? 0) -> Void Source #

succLeqZeroAbsurd' :: forall (n :: Nat). SNat n -> (S n <=? 0) :~: 'False Source #

succLeqAbsurd :: forall (n :: Nat). SNat n -> IsTrue (S n <=? n) -> Void Source #

succLeqAbsurd' :: forall (n :: Nat). SNat n -> (S n <=? n) :~: 'False Source #

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

leqSucc' :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m) Source #

leqToMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n Source #

geqToMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m Source #

minComm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Min n m :~: Min m n Source #

minLeqL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (Min n m <=? n) Source #

minLeqR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (Min n m <=? m) Source #

minLargest :: forall (l :: Nat) (n :: Nat) (m :: Nat). SNat l -> SNat n -> SNat m -> IsTrue (l <=? n) -> IsTrue (l <=? m) -> IsTrue (l <=? Min n m) Source #

leqToMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m Source #

geqToMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n Source #

maxComm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Max n m :~: Max m n Source #

maxLeqR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? Max n m) Source #

maxLeqL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <=? Max n m) Source #

maxLeast :: forall (l :: Nat) (n :: Nat) (m :: Nat). SNat l -> SNat n -> SNat m -> IsTrue (n <=? l) -> IsTrue (m <=? l) -> IsTrue (Max n m <=? l) Source #

lneqSuccLeq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m) Source #

Since 1.2.0.0 (type changed)

lneqReversed :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <? m) :~: (m >? n) Source #

Since 1.2.0.0 (type changed)

lneqToLT :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT Source #

ltToLneq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m) Source #

lneqZero :: forall (a :: Nat). SNat a -> IsTrue (0 <? Succ a) Source #

lneqSucc :: forall (n :: Nat). SNat n -> IsTrue (n <? Succ n) Source #

succLneqSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n <? m) :~: (Succ n <? Succ m) Source #

lneqRightPredSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <? m) -> m :~: Succ (Pred m) Source #

lneqSuccStepL :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m) Source #

lneqSuccStepR :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m) Source #

plusStrictMonotone :: forall (n :: Nat) (m :: Nat) (l :: Nat) (k :: Nat). SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <? m) -> IsTrue (l <? k) -> IsTrue ((n + l) <? (m + k)) Source #

minCase :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m) Source #

maxCase :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n) Source #

maxZeroL :: forall (n :: Nat). SNat n -> Max 0 n :~: n Source #

maxZeroR :: forall (n :: Nat). SNat n -> Max n 0 :~: n Source #

minZeroL :: forall (n :: Nat). SNat n -> Min 0 n :~: 0 Source #

minZeroR :: forall (n :: Nat). SNat n -> Min n 0 :~: 0 Source #

minusSucc :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue (m <=? n) -> (Succ n - m) :~: Succ (n - m) Source #

lneqZeroAbsurd :: forall (n :: Nat). SNat n -> IsTrue (n <? 0) -> Void Source #

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

minPlusTruncMinus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (Min n m + (n -. m)) :~: n Source #

truncMinusLeq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> IsTrue ((n -. m) <=? n) Source #

type (-.) (n :: Natural) (m :: Natural) = Subt n m (m <=? n) infixl 6 Source #

Natural subtraction, truncated to zero if m > n.

(%-.) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m) Source #

Various witnesses for orderings

type LeqWitness (n :: k) (m :: k) = IsTrue (n <=? m) Source #

data (a :: Natural) :<: (b :: Natural) Source #

Since 1.2.0 (argument changed)

Instances

Instances details

Show (a :<: b) Source #
Instance details Defined in Data.Type.Natural.Lemma.Order Methods showsPrec :: Int -> (a :<: b) -> ShowS # show :: (a :<: b) -> String # showList :: [a :<: b] -> ShowS #

data Leq (n :: Natural) (m :: Nat) where Source #

Comparison via GADTs.

Constructors

ZeroLeq :: forall (m :: Nat). SNat m -> Leq 0 m
SuccLeqSucc :: forall (n1 :: Natural) (m1 :: Natural). Leq n1 m1 -> Leq (n1 + 1) (m1 + 1)

leqRhs :: forall (n :: Natural) (m :: Nat). Leq n m -> SNat m Source #

leqLhs :: forall (n :: Natural) (m :: Nat). Leq n m -> SNat n Source #

conversions between lax orders

propToBoolLeq :: forall (n :: Natural) (m :: Nat). Leq n m -> LeqWitness n m Source #

boolToPropLeq :: forall (n :: Nat) (m :: Nat). n <= m => SNat n -> SNat m -> Leq n m Source #

conversions between strict orders

propToBoolLt :: forall (n :: Natural) (m :: Natural). (n :<: m) -> IsTrue (n <? m) Source #

boolToPropLt :: forall (n :: Nat) (m :: Nat). n < m => SNat n -> SNat m -> n :<: m Source #