{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
module Data.Type.Natural.Lemma.Order
( DiffNat (..),
LeqView (..),
type (<),
type (<?),
(%<?),
type (>),
type (>?),
(%>?),
type (>=),
type (>=?),
(%>=?),
FlipOrdering,
Min,
sMin,
Max,
sMax,
sFlipOrdering,
coerceLeqL,
coerceLeqR,
sLeqCongL,
sLeqCongR,
sLeqCong,
succDiffNat,
compareCongR,
leqToCmp,
eqlCmpEQ,
eqToRefl,
flipCmpNat,
ltToNeq,
leqNeqToLT,
succLeqToLT,
ltToLeq,
gtToLeq,
congFlipOrdering,
ltToSuccLeq,
cmpZero,
leqToGT,
cmpZero',
zeroNoLT,
ltRightPredSucc,
cmpSucc,
ltSucc,
cmpSuccStepR,
ltSuccLToLT,
leqToLT,
leqZero,
leqSucc,
fromLeqView,
leqViewRefl,
viewLeq,
leqWitness,
leqStep,
leqNeqToSuccLeq,
leqRefl,
leqSuccStepR,
leqSuccStepL,
leqReflexive,
leqTrans,
leqAntisymm,
plusMonotone,
leqZeroElim,
plusMonotoneL,
plusMonotoneR,
plusLeqL,
plusLeqR,
plusCancelLeqR,
plusCancelLeqL,
succLeqZeroAbsurd,
succLeqZeroAbsurd',
succLeqAbsurd,
succLeqAbsurd',
notLeqToLeq,
leqSucc',
leqToMin,
geqToMin,
minComm,
minLeqL,
minLeqR,
minLargest,
leqToMax,
geqToMax,
maxComm,
maxLeqR,
maxLeqL,
maxLeast,
lneqSuccLeq,
lneqReversed,
lneqToLT,
ltToLneq,
lneqZero,
lneqSucc,
succLneqSucc,
lneqRightPredSucc,
lneqSuccStepL,
lneqSuccStepR,
plusStrictMonotone,
maxZeroL,
maxZeroR,
minZeroL,
minZeroR,
minusSucc,
lneqZeroAbsurd,
minusPlus,
minPlusTruncMinus,
truncMinusLeq,
type (-.),
(%-.),
LeqWitness,
(:<:),
Leq (..),
leqRhs,
leqLhs,
propToBoolLeq,
boolToPropLeq,
propToBoolLt,
boolToPropLt,
)
where
import Data.Coerce (coerce)
import Data.Type.Equality (gcastWith, (:~:) (..))
import Data.Type.Natural.Core
import Data.Type.Natural.Lemma.Arithmetic
import Data.Void (Void, absurd)
import Numeric.Natural (Natural)
import Proof.Equational
( because,
start,
sym,
trans,
withRefl,
(===),
(=~=),
)
import Proof.Propositional (IsTrue (..), eliminate, withWitness)
data Leq n m where
ZeroLeq :: SNat m -> Leq 0 m
SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1)
type LeqWitness n m = IsTrue (n <=? m)
data a :<: b where
ZeroLtSucc :: 0 :<: (m + 1)
SuccLtSucc :: n :<: m -> (n + 1) :<: (m + 1)
deriving instance Show (a :<: b)
propToBoolLeq :: forall n m. Leq n m -> LeqWitness n m
propToBoolLeq :: Leq n m -> LeqWitness n m
propToBoolLeq (ZeroLeq SNat m
_) = LeqWitness n m
IsTrue 'True
Witness
propToBoolLeq (SuccLeqSucc Leq n m
leq) = IsTrue (n <=? m)
-> (((n <=? m) ~ 'True) => LeqWitness n m) -> LeqWitness n m
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness (Leq n m -> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat). Leq n m -> LeqWitness n m
propToBoolLeq Leq n m
leq) IsTrue 'True
((n <=? m) ~ 'True) => LeqWitness n m
Witness
{-# INLINE propToBoolLeq #-}
boolToPropLeq :: (n <= m) => SNat n -> SNat m -> Leq n m
boolToPropLeq :: SNat n -> SNat m -> Leq n m
boolToPropLeq SNat n
Zero SNat m
m = SNat m -> Leq 0 m
forall (m :: Nat). SNat m -> Leq 0 m
ZeroLeq SNat m
m
boolToPropLeq (Succ SNat n1
n) (Succ SNat n1
m) = Leq n1 n1 -> Leq (n1 + 1) (n1 + 1)
forall (n :: Nat) (m :: Nat). Leq n m -> Leq (n + 1) (m + 1)
SuccLeqSucc (Leq n1 n1 -> Leq (n1 + 1) (n1 + 1))
-> Leq n1 n1 -> Leq (n1 + 1) (n1 + 1)
forall a b. (a -> b) -> a -> b
$ SNat n1 -> SNat n1 -> Leq n1 n1
forall (n :: Nat) (m :: Nat).
(n <= m) =>
SNat n -> SNat m -> Leq n m
boolToPropLeq SNat n1
n SNat n1
m
boolToPropLeq (Succ SNat n1
n) SNat m
Zero = Void -> Leq n m
forall a. Void -> a
absurd (Void -> Leq n m) -> Void -> Leq n m
forall a b. (a -> b) -> a -> b
$ SNat n1 -> IsTrue (S n1 <=? 0) -> Void
forall (n :: Nat). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n1
n IsTrue (S n1 <=? 0)
IsTrue 'True
Witness
leqRhs :: Leq n m -> SNat m
leqRhs :: Leq n m -> SNat m
leqRhs (ZeroLeq SNat m
m) = SNat m
m
leqRhs (SuccLeqSucc Leq n m
leq) = SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m -> SNat (Succ m)) -> SNat m -> SNat (Succ m)
forall a b. (a -> b) -> a -> b
$ Leq n m -> SNat m
forall (n :: Nat) (m :: Nat). Leq n m -> SNat m
leqRhs Leq n m
leq
leqLhs :: Leq n m -> SNat n
leqLhs :: Leq n m -> SNat n
leqLhs (ZeroLeq SNat m
_) = SNat n
forall (n :: Nat). (n ~ 0) => SNat n
Zero
leqLhs (SuccLeqSucc Leq n m
leq) = SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)) -> SNat n -> SNat (Succ n)
forall a b. (a -> b) -> a -> b
$ Leq n m -> SNat n
forall (n :: Nat) (m :: Nat). Leq n m -> SNat n
leqLhs Leq n m
leq
propToBoolLt :: n :<: m -> IsTrue (n <? m)
propToBoolLt :: (n :<: m) -> IsTrue (n <? m)
propToBoolLt n :<: m
ZeroLtSucc = IsTrue (n <? m)
IsTrue 'True
Witness
propToBoolLt (SuccLtSucc n :<: m
lt) =
IsTrue (n <=? m)
-> (((n <=? m) ~ 'True) => IsTrue (n <? m)) -> IsTrue (n <? m)
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness ((n :<: m) -> IsTrue (n <? m)
forall (n :: Nat) (m :: Nat). (n :<: m) -> IsTrue (n <? m)
propToBoolLt n :<: m
lt) IsTrue 'True
((n <=? m) ~ 'True) => IsTrue (n <? m)
Witness
boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m
boolToPropLt :: SNat n -> SNat m -> n :<: m
boolToPropLt SNat n
Zero (Succ SNat n1
_) = n :<: m
forall (m :: Nat). 0 :<: (m + 1)
ZeroLtSucc
boolToPropLt (Succ SNat n1
_) SNat m
Zero = (0 :~: 1) -> n :<: m
forall a x. Empty a => a -> x
eliminate (0 :~: 1
forall k (a :: k). a :~: a
Refl :: 0 :~: 1)
boolToPropLt (Succ SNat n1
n) (Succ SNat n1
m) = (n1 :<: n1) -> (n1 + 1) :<: (n1 + 1)
forall (n :: Nat) (m :: Nat). (n :<: m) -> (n + 1) :<: (m + 1)
SuccLtSucc (SNat n1 -> SNat n1 -> n1 :<: n1
forall (n :: Nat) (m :: Nat).
(n < m) =>
SNat n -> SNat m -> n :<: m
boolToPropLt SNat n1
n SNat n1
m)
type Min n m = MinAux (n <=? m) n m
sMin :: SNat n -> SNat m -> SNat (Min n m)
sMin :: SNat n -> SNat m -> SNat (Min n m)
sMin = (Natural -> Natural -> Natural)
-> SNat n -> SNat m -> SNat (Min n m)
coerce ((Natural -> Natural -> Natural)
-> SNat n -> SNat m -> SNat (Min n m))
-> (Natural -> Natural -> Natural)
-> SNat n
-> SNat m
-> SNat (Min n m)
forall a b. (a -> b) -> a -> b
$ Ord Natural => Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
min @Natural
sMax :: SNat n -> SNat m -> SNat (Max n m)
sMax :: SNat n -> SNat m -> SNat (Max n m)
sMax = (Natural -> Natural -> Natural)
-> SNat n -> SNat m -> SNat (Max n m)
coerce ((Natural -> Natural -> Natural)
-> SNat n -> SNat m -> SNat (Max n m))
-> (Natural -> Natural -> Natural)
-> SNat n
-> SNat m
-> SNat (Max n m)
forall a b. (a -> b) -> a -> b
$ Ord Natural => Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
max @Natural
type family MinAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where
MinAux 'True n _ = n
MinAux 'False _ m = m
type Max n m = MaxAux (n >=? m) n m
type family MaxAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where
MaxAux 'True n _ = n
MaxAux 'False _ m = m
infix 4 <?, <, >=?, >=, >, >?
type n <? m = n + 1 <=? m
(%<?) :: SNat n -> SNat m -> SBool (n <? m)
%<? :: SNat n -> SNat m -> SBool (n <? m)
(%<?) = SNat (n + 1) -> SNat m -> SBool (n <? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
(%<=?) (SNat (n + 1) -> SNat m -> SBool (n <? m))
-> (SNat n -> SNat (n + 1)) -> SNat n -> SNat m -> SBool (n <? m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> SNat (n + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc
type n < m = (n <? m) ~ 'True
type n >=? m = m <=? n
(%>=?) :: SNat n -> SNat m -> SBool (n >=? m)
%>=? :: SNat n -> SNat m -> SBool (n >=? m)
(%>=?) = (SNat m -> SNat n -> SBool (n >=? m))
-> SNat n -> SNat m -> SBool (n >=? m)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SNat m -> SNat n -> SBool (n >=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
(%<=?)
type n >= m = (n >=? m) ~ 'True
type n >? m = m <? n
(%>?) :: SNat n -> SNat m -> SBool (n >? m)
%>? :: SNat n -> SNat m -> SBool (n >? m)
(%>?) = (SNat m -> SNat n -> SBool (n >? m))
-> SNat n -> SNat m -> SBool (n >? m)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SNat m -> SNat n -> SBool (n >? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
(%<?)
type n > m = (n >? m) ~ 'True
infix 4 %>?, %<?, %>=?
data LeqView n m where
LeqZero :: SNat n -> LeqView 0 n
LeqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)
data DiffNat n m where
DiffNat :: SNat n -> SNat m -> DiffNat n (n + m)
newtype LeqWitPf n = LeqWitPf {LeqWitPf n
-> forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitPf :: forall m. SNat m -> IsTrue (n <=? m) -> DiffNat n m}
newtype LeqStepPf n = LeqStepPf {LeqStepPf n
-> forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStepPf :: forall m l. SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)}
succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat SNat n
_ SNat m
_ (DiffNat SNat n
n SNat m
m) = ((Succ n + m) :~: Succ m)
-> (((Succ n + m) ~ Succ m) => DiffNat (Succ n) (Succ m))
-> DiffNat (Succ n) (Succ m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> (Succ n + m) :~: S (n + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat m
m) ((((Succ n + m) ~ Succ m) => DiffNat (Succ n) (Succ m))
-> DiffNat (Succ n) (Succ m))
-> (((Succ n + m) ~ Succ m) => DiffNat (Succ n) (Succ m))
-> DiffNat (Succ n) (Succ m)
forall a b. (a -> b) -> a -> b
$ SNat (Succ n) -> SNat m -> DiffNat (Succ n) (Succ n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> DiffNat n (n + m)
DiffNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m
coerceLeqL ::
forall n m l.
n :~: m ->
SNat l ->
IsTrue (n <=? l) ->
IsTrue (m <=? l)
coerceLeqL :: (n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL n :~: m
Refl SNat l
_ IsTrue (n <=? l)
Witness = IsTrue (m <=? l)
IsTrue 'True
Witness
coerceLeqR ::
forall n m l.
SNat l ->
n :~: m ->
IsTrue (l <=? n) ->
IsTrue (l <=? m)
coerceLeqR :: SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)
coerceLeqR SNat l
_ n :~: m
Refl IsTrue (l <=? n)
Witness = IsTrue (l <=? m)
IsTrue 'True
Witness
compareCongR :: SNat a -> b :~: c -> CmpNat a b :~: CmpNat a c
compareCongR :: SNat a -> (b :~: c) -> CmpNat a b :~: CmpNat a c
compareCongR SNat a
_ b :~: c
Refl = CmpNat a b :~: CmpNat a c
forall k (a :: k). a :~: a
Refl
sLeqCong :: a :~: b -> c :~: d -> (a <= c) :~: (b <= d)
sLeqCong :: (a :~: b) -> (c :~: d) -> (a <= c) :~: (b <= d)
sLeqCong a :~: b
Refl c :~: d
Refl = (a <= c) :~: (b <= d)
forall k (a :: k). a :~: a
Refl
sLeqCongL :: a :~: b -> SNat c -> (a <= c) :~: (b <= c)
sLeqCongL :: (a :~: b) -> SNat c -> (a <= c) :~: (b <= c)
sLeqCongL a :~: b
Refl SNat c
_ = (a <= c) :~: (b <= c)
forall k (a :: k). a :~: a
Refl
sLeqCongR :: SNat a -> b :~: c -> (a <= b) :~: (a <= c)
sLeqCongR :: SNat a -> (b :~: c) -> (a <= b) :~: (a <= c)
sLeqCongR SNat a
_ b :~: c
Refl = (a <= b) :~: (a <= c)
forall k (a :: k). a :~: a
Refl
newtype LTSucc n = LTSucc {LTSucc n -> CmpNat n (Succ n) :~: 'LT
proofLTSucc :: CmpNat n (Succ n) :~: 'LT}
newtype CmpSuccStepR n = CmpSuccStepR
{ CmpSuccStepR n
-> forall (m :: Nat).
SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
proofCmpSuccStepR ::
forall m.
SNat m ->
CmpNat n m :~: 'LT ->
CmpNat n (Succ m) :~: 'LT
}
newtype LeqViewRefl n = LeqViewRefl {LeqViewRefl n -> LeqView n n
proofLeqViewRefl :: LeqView n n}
leqToCmp ::
SNat a ->
SNat b ->
IsTrue (a <=? b) ->
Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp :: SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat a
n SNat b
m IsTrue (a <=? b)
Witness =
case SNat a
n SNat a -> SNat b -> Equality a b
forall (l :: Nat) (r :: Nat). SNat l -> SNat r -> Equality l r
%~ SNat b
m of
Equality a b
Equal -> (a :~: a) -> Either (a :~: a) ('EQ :~: 'LT)
forall a b. a -> Either a b
Left a :~: a
forall k (a :: k). a :~: a
Refl
Equality a b
NonEqual -> ('LT :~: 'LT) -> Either (a :~: b) ('LT :~: 'LT)
forall a b. b -> Either a b
Right 'LT :~: 'LT
forall k (a :: k). a :~: a
Refl
eqlCmpEQ :: SNat a -> SNat b -> a :~: b -> CmpNat a b :~: 'EQ
eqlCmpEQ :: SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat a
_ SNat b
_ a :~: b
Refl = CmpNat a b :~: 'EQ
forall k (a :: k). a :~: a
Refl
eqToRefl :: SNat a -> SNat b -> CmpNat a b :~: 'EQ -> a :~: b
eqToRefl :: SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b
eqToRefl SNat a
_ SNat b
_ CmpNat a b :~: 'EQ
Refl = a :~: b
forall k (a :: k). a :~: a
Refl
flipCmpNat ::
SNat a ->
SNat b ->
FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat :: SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat a
n SNat b
m = case SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat b
m of
SOrdering (CmpNat a b)
SGT -> FlipOrdering (CmpNat a b) :~: CmpNat b a
forall k (a :: k). a :~: a
Refl
SOrdering (CmpNat a b)
SLT -> FlipOrdering (CmpNat a b) :~: CmpNat b a
forall k (a :: k). a :~: a
Refl
SOrdering (CmpNat a b)
SEQ -> FlipOrdering (CmpNat a b) :~: CmpNat b a
forall k (a :: k). a :~: a
Refl
ltToNeq ::
SNat a ->
SNat b ->
CmpNat a b :~: 'LT ->
a :~: b ->
Void
ltToNeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void
ltToNeq SNat a
a SNat b
b CmpNat a b :~: 'LT
aLTb a :~: b
aEQb =
('LT :~: 'EQ) -> Void
forall a x. Empty a => a -> x
eliminate (('LT :~: 'EQ) -> Void) -> ('LT :~: 'EQ) -> Void
forall a b. (a -> b) -> a -> b
$
SOrdering 'LT -> 'LT :~: 'LT
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SOrdering 'LT
SLT
('LT :~: 'LT)
-> Reason (:~:) 'LT (CmpNat a b) -> 'LT :~: CmpNat a b
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
a SNat b
b SOrdering (CmpNat a b)
-> ('LT :~: CmpNat a b) -> Reason (:~:) 'LT (CmpNat a b)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (CmpNat a b :~: 'LT) -> 'LT :~: CmpNat a b
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym CmpNat a b :~: 'LT
aLTb
('LT :~: CmpNat a b)
-> Reason (:~:) (CmpNat a b) 'EQ -> 'LT :~: 'EQ
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'EQ
SEQ SOrdering 'EQ
-> (CmpNat a b :~: 'EQ) -> Reason (:~:) (CmpNat a b) 'EQ
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat a
a SNat b
b a :~: b
aEQb
leqNeqToLT :: SNat a -> SNat b -> IsTrue (a <=? b) -> (a :~: b -> Void) -> CmpNat a b :~: 'LT
leqNeqToLT :: SNat a
-> SNat b
-> IsTrue (a <=? b)
-> ((a :~: b) -> Void)
-> CmpNat a b :~: 'LT
leqNeqToLT SNat a
a SNat b
b IsTrue (a <=? b)
aLEQb (a :~: b) -> Void
aNEQb = ((a :~: b) -> CmpNat a b :~: 'LT)
-> ((CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
-> CmpNat a b :~: 'LT
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Void -> CmpNat a b :~: 'LT
forall a. Void -> a
absurd (Void -> CmpNat a b :~: 'LT)
-> ((a :~: b) -> Void) -> (a :~: b) -> CmpNat a b :~: 'LT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a :~: b) -> Void
aNEQb) (CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT
forall a. a -> a
id (Either (a :~: b) (CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT)
-> Either (a :~: b) (CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
forall (a :: Nat) (b :: Nat).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat a
a SNat b
b IsTrue (a <=? b)
aLEQb
succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT SNat a
a SNat b
b IsTrue (S a <=? b)
saLEQb =
case SNat (S a) -> SNat b -> IsTrue (S a <=? b) -> DiffNat (S a) b
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness (SNat a -> SNat (S a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
a) SNat b
b IsTrue (S a <=? b)
saLEQb of
DiffNat SNat (S a)
_ SNat m
k ->
let aLEQb :: IsTrue (a <=? b)
aLEQb =
SNat a
-> SNat b
-> SNat (m + 1)
-> ((a + (m + 1)) :~: b)
-> IsTrue (a <=? b)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat a
a SNat b
b (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) (((a + (m + 1)) :~: b) -> IsTrue (a <=? b))
-> ((a + (m + 1)) :~: b) -> IsTrue (a <=? b)
forall a b. (a -> b) -> a -> b
$
SNat (a + (m + 1)) -> (a + (m + 1)) :~: (a + (m + 1))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat a
a SNat a -> SNat (m + 1) -> SNat (a + (m + 1))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k)
((a + (m + 1)) :~: (a + (m + 1)))
-> Reason (:~:) (a + (m + 1)) ((a + m) + 1)
-> (a + (m + 1)) :~: ((a + m) + 1)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat (a + m) -> SNat ((a + m) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat a
a SNat a -> SNat m -> SNat (a + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat ((a + m) + 1)
-> ((a + (m + 1)) :~: ((a + m) + 1))
-> Reason (:~:) (a + (m + 1)) ((a + m) + 1)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> SNat m -> (a + (m + 1)) :~: ((a + m) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat a
a SNat m
k
((a + (m + 1)) :~: ((a + m) + 1))
-> Reason (:~:) ((a + m) + 1) b -> (a + (m + 1)) :~: b
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat a -> SNat (S a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
a SNat (S a) -> SNat m -> SNat (S a + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat b -> (((a + m) + 1) :~: b) -> Reason (:~:) ((a + m) + 1) b
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (b :~: ((a + m) + 1)) -> ((a + m) + 1) :~: b
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat a -> SNat m -> (S a + m) :~: ((a + m) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat a
a SNat m
k)
((a + (m + 1)) :~: b) -> SNat b -> (a + (m + 1)) :~: b
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat b
b
aNEQb :: (a :~: b) -> Void
aNEQb a :~: b
aeqb =
SNat m -> ((m + 1) :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat m
k (((m + 1) :~: 0) -> Void) -> ((m + 1) :~: 0) -> Void
forall a b. (a -> b) -> a -> b
$
SNat a
-> SNat (m + 1)
-> SNat 0
-> ((a + (m + 1)) :~: (a + 0))
-> (m + 1) :~: 0
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) :~: (n + l)) -> m :~: l
plusEqCancelL SNat a
a (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) SNat 0
sZero (((a + (m + 1)) :~: (a + 0)) -> (m + 1) :~: 0)
-> ((a + (m + 1)) :~: (a + 0)) -> (m + 1) :~: 0
forall a b. (a -> b) -> a -> b
$
SNat (a + (m + 1)) -> (a + (m + 1)) :~: (a + (m + 1))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat a
a SNat a -> SNat (m + 1) -> SNat (a + (m + 1))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k)
((a + (m + 1)) :~: (a + (m + 1)))
-> Reason (:~:) (a + (m + 1)) ((a + m) + 1)
-> (a + (m + 1)) :~: ((a + m) + 1)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat (a + m) -> SNat ((a + m) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat a
a SNat a -> SNat m -> SNat (a + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat ((a + m) + 1)
-> ((a + (m + 1)) :~: ((a + m) + 1))
-> Reason (:~:) (a + (m + 1)) ((a + m) + 1)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> SNat m -> (a + (m + 1)) :~: ((a + m) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat a
a SNat m
k
((a + (m + 1)) :~: ((a + m) + 1))
-> Reason (:~:) ((a + m) + 1) b -> (a + (m + 1)) :~: b
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat a -> SNat (S a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
a SNat (S a) -> SNat m -> SNat (S a + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat b -> (((a + m) + 1) :~: b) -> Reason (:~:) ((a + m) + 1) b
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (b :~: ((a + m) + 1)) -> ((a + m) + 1) :~: b
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat a -> SNat m -> (S a + m) :~: ((a + m) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat a
a SNat m
k)
((a + (m + 1)) :~: b) -> SNat b -> (a + (m + 1)) :~: b
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat b
b
((a + (m + 1)) :~: b) -> Reason (:~:) b a -> (a + (m + 1)) :~: a
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat a
a SNat a -> (b :~: a) -> Reason (:~:) b a
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (a :~: b) -> b :~: a
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym a :~: b
aeqb
((a + (m + 1)) :~: a) -> Reason (:~:) a a -> (a + (m + 1)) :~: a
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat a
a SNat a -> SNat 0 -> SNat (a + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero SNat a -> (a :~: a) -> Reason (:~:) a a
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (a :~: a) -> a :~: a
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat a -> (a + 0) :~: a
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat a
a)
in SNat a
-> SNat b
-> IsTrue (a <=? b)
-> ((a :~: b) -> Void)
-> CmpNat a b :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> ((a :~: b) -> Void)
-> CmpNat a b :~: 'LT
leqNeqToLT SNat a
a SNat b
b IsTrue (a <=? b)
aLEQb (a :~: b) -> Void
aNEQb
ltToLeq ::
SNat a ->
SNat b ->
CmpNat a b :~: 'LT ->
IsTrue (a <=? b)
ltToLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat a
_ SNat b
_ CmpNat a b :~: 'LT
Refl = IsTrue (a <=? b)
IsTrue 'True
Witness
gtToLeq ::
SNat a ->
SNat b ->
CmpNat a b :~: 'GT ->
IsTrue (b <=? a)
gtToLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a)
gtToLeq SNat a
n SNat b
m CmpNat a b :~: 'GT
nGTm =
SNat b -> SNat a -> (CmpNat b a :~: 'LT) -> IsTrue (b <=? a)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat b
m SNat a
n ((CmpNat b a :~: 'LT) -> IsTrue (b <=? a))
-> (CmpNat b a :~: 'LT) -> IsTrue (b <=? a)
forall a b. (a -> b) -> a -> b
$
SOrdering (CmpNat b a) -> CmpNat b a :~: CmpNat b a
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat b -> SNat a -> SOrdering (CmpNat b a)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat b
m SNat a
n) (CmpNat b a :~: CmpNat b a)
-> Reason (:~:) (CmpNat b a) (FlipOrdering (CmpNat a b))
-> CmpNat b a :~: FlipOrdering (CmpNat a b)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering (CmpNat a b) -> SOrdering (FlipOrdering (CmpNat a b))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat b
m) SOrdering (FlipOrdering (CmpNat a b))
-> (CmpNat b a :~: FlipOrdering (CmpNat a b))
-> Reason (:~:) (CmpNat b a) (FlipOrdering (CmpNat a b))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (FlipOrdering (CmpNat a b) :~: CmpNat b a)
-> CmpNat b a :~: FlipOrdering (CmpNat a b)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat a
n SNat b
m)
(CmpNat b a :~: FlipOrdering (CmpNat a b))
-> Reason (:~:) (FlipOrdering (CmpNat a b)) 'LT
-> CmpNat b a :~: 'LT
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'GT -> SOrdering (FlipOrdering 'GT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'GT
SGT SOrdering 'LT
-> (FlipOrdering (CmpNat a b) :~: 'LT)
-> Reason (:~:) (FlipOrdering (CmpNat a b)) 'LT
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (CmpNat a b :~: 'GT)
-> FlipOrdering (CmpNat a b) :~: FlipOrdering 'GT
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering CmpNat a b :~: 'GT
nGTm
(CmpNat b a :~: 'LT) -> SOrdering 'LT -> CmpNat b a :~: 'LT
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'LT
SLT
congFlipOrdering ::
a :~: b -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering :: (a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering a :~: b
Refl = FlipOrdering a :~: FlipOrdering b
forall k (a :: k). a :~: a
Refl
ltToSuccLeq ::
SNat a ->
SNat b ->
CmpNat a b :~: 'LT ->
IsTrue (Succ a <=? b)
ltToSuccLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat a
n SNat b
m CmpNat a b :~: 'LT
nLTm =
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> ((a :~: b) -> Void)
-> IsTrue (Succ a <=? b)
forall (n :: Nat) (m :: Nat).
SNat n
-> SNat m
-> IsTrue (n <=? m)
-> ((n :~: m) -> Void)
-> IsTrue (Succ n <=? m)
leqNeqToSuccLeq SNat a
n SNat b
m (SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat a
n SNat b
m CmpNat a b :~: 'LT
nLTm) (SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void
ltToNeq SNat a
n SNat b
m CmpNat a b :~: 'LT
nLTm)
cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat a
sn =
SNat 0
-> SNat (Succ a)
-> IsTrue (Succ 0 <=? Succ a)
-> CmpNat 0 (Succ a) :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
leqToLT SNat 0
sZero (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
sn) (IsTrue (Succ 0 <=? Succ a) -> CmpNat 0 (Succ a) :~: 'LT)
-> IsTrue (Succ 0 <=? Succ a) -> CmpNat 0 (Succ a) :~: 'LT
forall a b. (a -> b) -> a -> b
$
SNat 1
-> SNat (Succ a)
-> SNat a
-> ((1 + a) :~: Succ a)
-> IsTrue (1 <=? Succ a)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat 0 -> SNat (Succ 0)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat 0
sZero) (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
sn) SNat a
sn (((1 + a) :~: Succ a) -> IsTrue (1 <=? Succ a))
-> ((1 + a) :~: Succ a) -> IsTrue (1 <=? Succ a)
forall a b. (a -> b) -> a -> b
$
SNat (1 + a) -> (1 + a) :~: (1 + a)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat 0 -> SNat (Succ 0)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat 0
sZero SNat 1 -> SNat a -> SNat (1 + a)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat a
sn)
((1 + a) :~: (1 + a))
-> Reason (:~:) (1 + a) (Succ a) -> (1 + a) :~: Succ a
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat 0
sZero SNat 0 -> SNat a -> SNat (0 + a)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat a
sn) SNat (Succ a)
-> ((1 + a) :~: Succ a) -> Reason (:~:) (1 + a) (Succ a)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat 0 -> SNat a -> (Succ 0 + a) :~: S (0 + a)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat 0
sZero SNat a
sn
((1 + a) :~: Succ a)
-> Reason (:~:) (Succ a) (Succ a) -> (1 + a) :~: Succ a
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
sn SNat (Succ a)
-> (Succ a :~: Succ a) -> Reason (:~:) (Succ a) (Succ a)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (a :~: a) -> Succ a :~: Succ a
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong (SNat a -> (0 + a) :~: a
forall (n :: Nat). SNat n -> (0 + n) :~: n
plusZeroL SNat a
sn)
leqToGT ::
SNat a ->
SNat b ->
IsTrue (Succ b <=? a) ->
CmpNat a b :~: 'GT
leqToGT :: SNat a -> SNat b -> IsTrue (Succ b <=? a) -> CmpNat a b :~: 'GT
leqToGT SNat a
a SNat b
b IsTrue (Succ b <=? a)
sbLEQa =
SOrdering (CmpNat a b) -> CmpNat a b :~: CmpNat a b
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
a SNat b
b)
(CmpNat a b :~: CmpNat a b)
-> Reason (:~:) (CmpNat a b) (FlipOrdering (CmpNat b a))
-> CmpNat a b :~: FlipOrdering (CmpNat b a)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering (CmpNat b a) -> SOrdering (FlipOrdering (CmpNat b a))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat b -> SNat a -> SOrdering (CmpNat b a)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat b
b SNat a
a) SOrdering (FlipOrdering (CmpNat b a))
-> (CmpNat a b :~: FlipOrdering (CmpNat b a))
-> Reason (:~:) (CmpNat a b) (FlipOrdering (CmpNat b a))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (FlipOrdering (CmpNat b a) :~: CmpNat a b)
-> CmpNat a b :~: FlipOrdering (CmpNat b a)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat b -> SNat a -> FlipOrdering (CmpNat b a) :~: CmpNat a b
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat b
b SNat a
a)
(CmpNat a b :~: FlipOrdering (CmpNat b a))
-> Reason (:~:) (FlipOrdering (CmpNat b a)) 'GT
-> CmpNat a b :~: 'GT
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'LT -> SOrdering (FlipOrdering 'LT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'LT
SLT SOrdering 'GT
-> (FlipOrdering (CmpNat b a) :~: 'GT)
-> Reason (:~:) (FlipOrdering (CmpNat b a)) 'GT
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (CmpNat b a :~: 'LT)
-> FlipOrdering (CmpNat b a) :~: FlipOrdering 'LT
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering (SNat b -> SNat a -> IsTrue (Succ b <=? a) -> CmpNat b a :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
leqToLT SNat b
b SNat a
a IsTrue (Succ b <=? a)
sbLEQa)
(CmpNat a b :~: 'GT) -> SOrdering 'GT -> CmpNat a b :~: 'GT
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'GT
SGT
cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' SNat a
n =
case SNat a -> ZeroOrSucc a
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat a
n of
ZeroOrSucc a
IsZero -> ('EQ :~: 'EQ) -> Either ('EQ :~: 'EQ) ('EQ :~: 'LT)
forall a b. a -> Either a b
Left (('EQ :~: 'EQ) -> Either ('EQ :~: 'EQ) ('EQ :~: 'LT))
-> ('EQ :~: 'EQ) -> Either ('EQ :~: 'EQ) ('EQ :~: 'LT)
forall a b. (a -> b) -> a -> b
$ SNat 0 -> SNat a -> (0 :~: a) -> CmpNat 0 a :~: 'EQ
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat 0
sZero SNat a
n 0 :~: a
forall k (a :: k). a :~: a
Refl
IsSucc SNat n
n' -> (CmpNat 0 a :~: 'LT)
-> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
forall a b. b -> Either a b
Right ((CmpNat 0 a :~: 'LT)
-> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT))
-> (CmpNat 0 a :~: 'LT)
-> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
forall a b. (a -> b) -> a -> b
$ SNat n -> CmpNat 0 (Succ n) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat n
n'
zeroNoLT :: SNat a -> CmpNat a 0 :~: 'LT -> Void
zeroNoLT :: SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT SNat a
n CmpNat a 0 :~: 'LT
eql =
case SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
forall (a :: Nat).
SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' SNat a
n of
Left CmpNat 0 a :~: 'EQ
cmp0nEQ ->
('GT :~: 'EQ) -> Void
forall a x. Empty a => a -> x
eliminate (('GT :~: 'EQ) -> Void) -> ('GT :~: 'EQ) -> Void
forall a b. (a -> b) -> a -> b
$
SOrdering 'GT -> 'GT :~: 'GT
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SOrdering 'GT
SGT
('GT :~: 'GT) -> SOrdering 'GT -> 'GT :~: 'GT
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'LT -> SOrdering (FlipOrdering 'LT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'LT
SLT
('GT :~: 'GT)
-> Reason (:~:) 'GT (FlipOrdering (CmpNat a 0))
-> 'GT :~: FlipOrdering (CmpNat a 0)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering (CmpNat a 0) -> SOrdering (FlipOrdering (CmpNat a 0))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat a -> SNat 0 -> SOrdering (CmpNat a 0)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat 0
sZero) SOrdering (FlipOrdering (CmpNat a 0))
-> ('GT :~: FlipOrdering (CmpNat a 0))
-> Reason (:~:) 'GT (FlipOrdering (CmpNat a 0))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ('LT :~: CmpNat a 0)
-> FlipOrdering 'LT :~: FlipOrdering (CmpNat a 0)
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering ((CmpNat a 0 :~: 'LT) -> 'LT :~: CmpNat a 0
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym CmpNat a 0 :~: 'LT
eql)
('GT :~: FlipOrdering (CmpNat a 0))
-> Reason (:~:) (FlipOrdering (CmpNat a 0)) (CmpNat 0 a)
-> 'GT :~: CmpNat 0 a
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat 0 -> SNat a -> SOrdering (CmpNat 0 a)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat 0
sZero SNat a
n SOrdering (CmpNat 0 a)
-> (FlipOrdering (CmpNat a 0) :~: CmpNat 0 a)
-> Reason (:~:) (FlipOrdering (CmpNat a 0)) (CmpNat 0 a)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> SNat 0 -> FlipOrdering (CmpNat a 0) :~: CmpNat 0 a
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat a
n SNat 0
sZero
('GT :~: CmpNat 0 a)
-> Reason (:~:) (CmpNat 0 a) 'EQ -> 'GT :~: 'EQ
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'EQ
SEQ SOrdering 'EQ
-> (CmpNat 0 a :~: 'EQ) -> Reason (:~:) (CmpNat 0 a) 'EQ
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` CmpNat 0 a :~: 'EQ
cmp0nEQ
Right CmpNat 0 a :~: 'LT
cmp0nLT ->
('GT :~: 'LT) -> Void
forall a x. Empty a => a -> x
eliminate (('GT :~: 'LT) -> Void) -> ('GT :~: 'LT) -> Void
forall a b. (a -> b) -> a -> b
$
SOrdering 'GT -> 'GT :~: 'GT
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SOrdering 'GT
SGT
('GT :~: 'GT) -> SOrdering 'GT -> 'GT :~: 'GT
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'LT -> SOrdering (FlipOrdering 'LT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'LT
SLT
('GT :~: 'GT)
-> Reason (:~:) 'GT (FlipOrdering (CmpNat a 0))
-> 'GT :~: FlipOrdering (CmpNat a 0)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering (CmpNat a 0) -> SOrdering (FlipOrdering (CmpNat a 0))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat a -> SNat 0 -> SOrdering (CmpNat a 0)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat 0
sZero) SOrdering (FlipOrdering (CmpNat a 0))
-> ('GT :~: FlipOrdering (CmpNat a 0))
-> Reason (:~:) 'GT (FlipOrdering (CmpNat a 0))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ('LT :~: CmpNat a 0)
-> FlipOrdering 'LT :~: FlipOrdering (CmpNat a 0)
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering ((CmpNat a 0 :~: 'LT) -> 'LT :~: CmpNat a 0
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym CmpNat a 0 :~: 'LT
eql)
('GT :~: FlipOrdering (CmpNat a 0))
-> Reason (:~:) (FlipOrdering (CmpNat a 0)) (CmpNat 0 a)
-> 'GT :~: CmpNat 0 a
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat 0 -> SNat a -> SOrdering (CmpNat 0 a)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat 0
sZero SNat a
n SOrdering (CmpNat 0 a)
-> (FlipOrdering (CmpNat a 0) :~: CmpNat 0 a)
-> Reason (:~:) (FlipOrdering (CmpNat a 0)) (CmpNat 0 a)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> SNat 0 -> FlipOrdering (CmpNat a 0) :~: CmpNat 0 a
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat a
n SNat 0
sZero
('GT :~: CmpNat 0 a)
-> Reason (:~:) (CmpNat 0 a) 'LT -> 'GT :~: 'LT
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'LT
SLT SOrdering 'LT
-> (CmpNat 0 a :~: 'LT) -> Reason (:~:) (CmpNat 0 a) 'LT
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` CmpNat 0 a :~: 'LT
cmp0nLT
ltRightPredSucc :: SNat a -> SNat b -> CmpNat a b :~: 'LT -> b :~: Succ (Pred b)
ltRightPredSucc :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
ltRightPredSucc SNat a
a SNat b
b CmpNat a b :~: 'LT
aLTb =
case SNat b -> ZeroOrSucc b
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat b
b of
ZeroOrSucc b
IsZero -> Void -> 0 :~: ((0 - 1) + 1)
forall a. Void -> a
absurd (Void -> 0 :~: ((0 - 1) + 1)) -> Void -> 0 :~: ((0 - 1) + 1)
forall a b. (a -> b) -> a -> b
$ SNat a -> (CmpNat a 0 :~: 'LT) -> Void
forall (a :: Nat). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT SNat a
a CmpNat a b :~: 'LT
CmpNat a 0 :~: 'LT
aLTb
IsSucc SNat n
b' ->
(Succ (Pred b) :~: b) -> b :~: Succ (Pred b)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((Succ (Pred b) :~: b) -> b :~: Succ (Pred b))
-> (Succ (Pred b) :~: b) -> b :~: Succ (Pred b)
forall a b. (a -> b) -> a -> b
$
SNat (Succ (Pred b)) -> Succ (Pred b) :~: Succ (Pred b)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Pred b) -> SNat (Succ (Pred b))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat b -> SNat (Pred b)
forall (n :: Nat). SNat n -> SNat (Pred n)
sPred SNat b
b))
(Succ (Pred b) :~: Succ (Pred b))
-> SNat (Succ (Pred b)) -> Succ (Pred b) :~: Succ (Pred b)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat (Pred b) -> SNat (Succ (Pred b))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat b -> SNat (Pred b)
forall (n :: Nat). SNat n -> SNat (Pred n)
sPred (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
b'))
(Succ (Pred b) :~: Succ (Pred b))
-> Reason (:~:) (Succ (Pred b)) b -> Succ (Pred b) :~: b
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
b' SNat b -> (Succ (Pred b) :~: b) -> Reason (:~:) (Succ (Pred b)) b
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (Pred b :~: n) -> Succ (Pred b) :~: Succ n
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong (SNat n -> Pred (Succ n) :~: n
forall (n :: Nat). SNat n -> Pred (Succ n) :~: n
predSucc SNat n
b')
(Succ (Pred b) :~: b) -> SNat b -> Succ (Pred b) :~: b
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat b
b
cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n SNat m
m =
case SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m of
SOrdering (CmpNat n m)
SEQ ->
let nEQm :: n :~: m
nEQm = SNat n -> SNat m -> (CmpNat n m :~: 'EQ) -> n :~: m
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b
eqToRefl SNat n
n SNat m
m CmpNat n m :~: 'EQ
forall k (a :: k). a :~: a
Refl
in (CmpNat (Succ n) (Succ m) :~: 'EQ)
-> 'EQ :~: CmpNat (Succ n) (Succ m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((CmpNat (Succ n) (Succ m) :~: 'EQ)
-> 'EQ :~: CmpNat (Succ n) (Succ m))
-> (CmpNat (Succ n) (Succ m) :~: 'EQ)
-> 'EQ :~: CmpNat (Succ n) (Succ m)
forall a b. (a -> b) -> a -> b
$ SNat (Succ n)
-> SNat (Succ m)
-> (Succ n :~: Succ m)
-> CmpNat (Succ n) (Succ m) :~: 'EQ
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) ((Succ n :~: Succ m) -> CmpNat (Succ n) (Succ m) :~: 'EQ)
-> (Succ n :~: Succ m) -> CmpNat (Succ n) (Succ m) :~: 'EQ
forall a b. (a -> b) -> a -> b
$ (n :~: m) -> Succ n :~: Succ m
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong n :~: m
nEQm
SOrdering (CmpNat n m)
SLT -> case SNat (Succ n)
-> SNat m -> IsTrue (Succ n <=? m) -> DiffNat (Succ n) m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (IsTrue (Succ n <=? m) -> DiffNat (Succ n) m)
-> IsTrue (Succ n <=? m) -> DiffNat (Succ n) m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (Succ n <=? m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat n
n SNat m
m CmpNat n m :~: 'LT
forall k (a :: k). a :~: a
Refl of
DiffNat SNat (Succ n)
_ SNat m
k ->
(CmpNat (Succ n) (Succ m) :~: 'LT)
-> 'LT :~: CmpNat (Succ n) (Succ m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((CmpNat (Succ n) (Succ m) :~: 'LT)
-> 'LT :~: CmpNat (Succ n) (Succ m))
-> (CmpNat (Succ n) (Succ m) :~: 'LT)
-> 'LT :~: CmpNat (Succ n) (Succ m)
forall a b. (a -> b) -> a -> b
$
SNat (Succ n)
-> SNat (Succ m)
-> IsTrue (S (Succ n) <=? Succ m)
-> CmpNat (Succ n) (Succ m) :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (IsTrue (S (Succ n) <=? Succ m)
-> CmpNat (Succ n) (Succ m) :~: 'LT)
-> IsTrue (S (Succ n) <=? Succ m)
-> CmpNat (Succ n) (Succ m) :~: 'LT
forall a b. (a -> b) -> a -> b
$
SNat (S (Succ n))
-> SNat (Succ m)
-> SNat m
-> ((S (Succ n) + m) :~: Succ m)
-> IsTrue (S (Succ n) <=? Succ m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat (Succ n) -> SNat (S (Succ n))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SNat m
k (((S (Succ n) + m) :~: Succ m) -> IsTrue (S (Succ n) <=? Succ m))
-> ((S (Succ n) + m) :~: Succ m) -> IsTrue (S (Succ n) <=? Succ m)
forall a b. (a -> b) -> a -> b
$
SNat (S (Succ n) + m) -> (S (Succ n) + m) :~: (S (Succ n) + m)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Succ n) -> SNat (S (Succ n))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat (S (Succ n)) -> SNat m -> SNat (S (Succ n) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k)
((S (Succ n) + m) :~: (S (Succ n) + m))
-> Reason (:~:) (S (Succ n) + m) (Succ m)
-> (S (Succ n) + m) :~: Succ m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat m -> SNat (Succ n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ m)
-> ((S (Succ n) + m) :~: Succ m)
-> Reason (:~:) (S (Succ n) + m) (Succ m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat (Succ n) -> SNat m -> (S (Succ n) + m) :~: S (Succ n + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
k
((S (Succ n) + m) :~: Succ m)
-> SNat (Succ m) -> (S (Succ n) + m) :~: Succ m
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m
SOrdering (CmpNat n m)
SGT -> case SNat (Succ m)
-> SNat n -> IsTrue (Succ m <=? n) -> DiffNat (Succ m) n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SNat n
n (IsTrue (Succ m <=? n) -> DiffNat (Succ m) n)
-> IsTrue (Succ m <=? n) -> DiffNat (Succ m) n
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat n -> (CmpNat m n :~: 'LT) -> IsTrue (Succ m <=? n)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat m
m SNat n
n (('LT :~: CmpNat m n) -> CmpNat m n :~: 'LT
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (('LT :~: CmpNat m n) -> CmpNat m n :~: 'LT)
-> ('LT :~: CmpNat m n) -> CmpNat m n :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> FlipOrdering (CmpNat n m) :~: CmpNat m n
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat n
n SNat m
m) of
DiffNat SNat (Succ m)
_ SNat m
k ->
let pf :: CmpNat (Succ m) (Succ n) :~: 'LT
pf =
( SNat (Succ m)
-> SNat (Succ n)
-> IsTrue (S (Succ m) <=? Succ n)
-> CmpNat (Succ m) (Succ n) :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (IsTrue (S (Succ m) <=? Succ n)
-> CmpNat (Succ m) (Succ n) :~: 'LT)
-> IsTrue (S (Succ m) <=? Succ n)
-> CmpNat (Succ m) (Succ n) :~: 'LT
forall a b. (a -> b) -> a -> b
$
SNat (S (Succ m))
-> SNat (Succ n)
-> SNat m
-> ((S (Succ m) + m) :~: Succ n)
-> IsTrue (S (Succ m) <=? Succ n)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat (Succ m) -> SNat (S (Succ m))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m)) (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
k (((S (Succ m) + m) :~: Succ n) -> IsTrue (S (Succ m) <=? Succ n))
-> ((S (Succ m) + m) :~: Succ n) -> IsTrue (S (Succ m) <=? Succ n)
forall a b. (a -> b) -> a -> b
$
SNat (S (Succ m) + m) -> (S (Succ m) + m) :~: (S (Succ m) + m)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Succ m) -> SNat (S (Succ m))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SNat (S (Succ m)) -> SNat m -> SNat (S (Succ m) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k)
((S (Succ m) + m) :~: (S (Succ m) + m))
-> Reason (:~:) (S (Succ m) + m) (Succ n)
-> (S (Succ m) + m) :~: Succ n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m SNat (Succ m) -> SNat m -> SNat (Succ m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ n)
-> ((S (Succ m) + m) :~: Succ n)
-> Reason (:~:) (S (Succ m) + m) (Succ n)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat (Succ m) -> SNat m -> (S (Succ m) + m) :~: S (Succ m + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SNat m
k
((S (Succ m) + m) :~: Succ n)
-> SNat (Succ n) -> (S (Succ m) + m) :~: Succ n
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n
)
in SOrdering 'GT -> 'GT :~: 'GT
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m)
('GT :~: 'GT) -> SOrdering 'GT -> 'GT :~: 'GT
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'GT
SGT
('GT :~: 'GT) -> SOrdering 'GT -> 'GT :~: 'GT
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'LT -> SOrdering (FlipOrdering 'LT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'LT
SLT
('GT :~: 'GT)
-> Reason (:~:) 'GT (FlipOrdering (CmpNat (Succ m) (Succ n)))
-> 'GT :~: FlipOrdering (CmpNat (Succ m) (Succ n))
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering (CmpNat (Succ m) (Succ n))
-> SOrdering (FlipOrdering (CmpNat (Succ m) (Succ n)))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat (Succ m)
-> SNat (Succ n) -> SOrdering (CmpNat (Succ m) (Succ n))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)) SOrdering (FlipOrdering (CmpNat (Succ m) (Succ n)))
-> ('GT :~: FlipOrdering (CmpNat (Succ m) (Succ n)))
-> Reason (:~:) 'GT (FlipOrdering (CmpNat (Succ m) (Succ n)))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ('LT :~: CmpNat (Succ m) (Succ n))
-> FlipOrdering 'LT :~: FlipOrdering (CmpNat (Succ m) (Succ n))
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering ((CmpNat (Succ m) (Succ n) :~: 'LT)
-> 'LT :~: CmpNat (Succ m) (Succ n)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym CmpNat (Succ m) (Succ n) :~: 'LT
pf)
('GT :~: FlipOrdering (CmpNat (Succ m) (Succ n)))
-> Reason
(:~:)
(FlipOrdering (CmpNat (Succ m) (Succ n)))
(CmpNat (Succ n) (Succ m))
-> 'GT :~: CmpNat (Succ n) (Succ m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat (Succ n)
-> SNat (Succ m) -> SOrdering (CmpNat (Succ n) (Succ m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SOrdering (CmpNat (Succ n) (Succ m))
-> (FlipOrdering (CmpNat (Succ m) (Succ n))
:~: CmpNat (Succ n) (Succ m))
-> Reason
(:~:)
(FlipOrdering (CmpNat (Succ m) (Succ n)))
(CmpNat (Succ n) (Succ m))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat (Succ m)
-> SNat (Succ n)
-> FlipOrdering (CmpNat (Succ m) (Succ n))
:~: CmpNat (Succ n) (Succ m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)
ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc = LTSucc a -> CmpNat a (Succ a) :~: 'LT
forall (n :: Nat). LTSucc n -> CmpNat n (Succ n) :~: 'LT
proofLTSucc (LTSucc a -> CmpNat a (Succ a) :~: 'LT)
-> (SNat a -> LTSucc a) -> SNat a -> CmpNat a (Succ a) :~: 'LT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LTSucc 0
-> (forall (n :: Nat). SNat n -> LTSucc n -> LTSucc (S n))
-> SNat a
-> LTSucc a
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction LTSucc 0
base forall (n :: Nat). SNat n -> LTSucc n -> LTSucc (S n)
step
where
base :: LTSucc 0
base :: LTSucc 0
base = (CmpNat 0 (Succ 0) :~: 'LT) -> LTSucc 0
forall (n :: Nat). (CmpNat n (Succ n) :~: 'LT) -> LTSucc n
LTSucc ((CmpNat 0 (Succ 0) :~: 'LT) -> LTSucc 0)
-> (CmpNat 0 (Succ 0) :~: 'LT) -> LTSucc 0
forall a b. (a -> b) -> a -> b
$ SNat 0 -> CmpNat 0 (Succ 0) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero (SNat 0
sZero :: SNat 0)
step :: SNat n -> LTSucc n -> LTSucc (Succ n)
step :: SNat n -> LTSucc n -> LTSucc (Succ n)
step SNat n
n (LTSucc CmpNat n (Succ n) :~: 'LT
ih) =
(CmpNat (Succ n) (Succ (Succ n)) :~: 'LT) -> LTSucc (Succ n)
forall (n :: Nat). (CmpNat n (Succ n) :~: 'LT) -> LTSucc n
LTSucc ((CmpNat (Succ n) (Succ (Succ n)) :~: 'LT) -> LTSucc (Succ n))
-> (CmpNat (Succ n) (Succ (Succ n)) :~: 'LT) -> LTSucc (Succ n)
forall a b. (a -> b) -> a -> b
$
SOrdering (CmpNat (Succ n) (Succ (Succ n)))
-> CmpNat (Succ n) (Succ (Succ n))
:~: CmpNat (Succ n) (Succ (Succ n))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Succ n)
-> SNat (Succ (Succ n))
-> SOrdering (CmpNat (Succ n) (Succ (Succ n)))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat (Succ n) -> SNat (Succ (Succ n))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)))
(CmpNat (Succ n) (Succ (Succ n))
:~: CmpNat (Succ n) (Succ (Succ n)))
-> Reason
(:~:) (CmpNat (Succ n) (Succ (Succ n))) (CmpNat n (Succ n))
-> CmpNat (Succ n) (Succ (Succ n)) :~: CmpNat n (Succ n)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat (Succ n) -> SOrdering (CmpNat n (Succ n))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SOrdering (CmpNat n (Succ n))
-> (CmpNat (Succ n) (Succ (Succ n)) :~: CmpNat n (Succ n))
-> Reason
(:~:) (CmpNat (Succ n) (Succ (Succ n))) (CmpNat n (Succ n))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (CmpNat n (Succ n) :~: CmpNat (Succ n) (Succ (Succ n)))
-> CmpNat (Succ n) (Succ (Succ n)) :~: CmpNat n (Succ n)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n
-> SNat (Succ n)
-> CmpNat n (Succ n) :~: CmpNat (Succ n) (Succ (Succ n))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n))
(CmpNat (Succ n) (Succ (Succ n)) :~: CmpNat n (Succ n))
-> Reason (:~:) (CmpNat n (Succ n)) 'LT
-> CmpNat (Succ n) (Succ (Succ n)) :~: 'LT
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'LT
SLT SOrdering 'LT
-> (CmpNat n (Succ n) :~: 'LT)
-> Reason (:~:) (CmpNat n (Succ n)) 'LT
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` CmpNat n (Succ n) :~: 'LT
ih
cmpSuccStepR ::
forall n m.
SNat n ->
SNat m ->
CmpNat n m :~: 'LT ->
CmpNat n (Succ m) :~: 'LT
cmpSuccStepR :: SNat n
-> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
cmpSuccStepR = \SNat n
sn -> CmpSuccStepR n
-> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
forall (n :: Nat).
CmpSuccStepR n
-> forall (m :: Nat).
SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
proofCmpSuccStepR (CmpSuccStepR 0
-> (forall (n :: Nat).
SNat n -> CmpSuccStepR n -> CmpSuccStepR (S n))
-> SNat n
-> CmpSuccStepR n
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction CmpSuccStepR 0
base forall (n :: Nat). SNat n -> CmpSuccStepR n -> CmpSuccStepR (S n)
step SNat n
sn) @m
where
base :: CmpSuccStepR 0
base :: CmpSuccStepR 0
base = (forall (m :: Nat).
SNat m -> (CmpNat 0 m :~: 'LT) -> CmpNat 0 (Succ m) :~: 'LT)
-> CmpSuccStepR 0
forall (n :: Nat).
(forall (m :: Nat).
SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT)
-> CmpSuccStepR n
CmpSuccStepR ((forall (m :: Nat).
SNat m -> (CmpNat 0 m :~: 'LT) -> CmpNat 0 (Succ m) :~: 'LT)
-> CmpSuccStepR 0)
-> (forall (m :: Nat).
SNat m -> (CmpNat 0 m :~: 'LT) -> CmpNat 0 (Succ m) :~: 'LT)
-> CmpSuccStepR 0
forall a b. (a -> b) -> a -> b
$ \SNat m
m CmpNat 0 m :~: 'LT
_ -> SNat m -> CmpNat 0 (Succ m) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat m
m
step :: SNat x -> CmpSuccStepR x -> CmpSuccStepR (Succ x)
step :: SNat x -> CmpSuccStepR x -> CmpSuccStepR (Succ x)
step SNat x
n (CmpSuccStepR forall (m :: Nat).
SNat m -> (CmpNat x m :~: 'LT) -> CmpNat x (Succ m) :~: 'LT
ih) = (forall (m :: Nat).
SNat m
-> (CmpNat (Succ x) m :~: 'LT) -> CmpNat (Succ x) (Succ m) :~: 'LT)
-> CmpSuccStepR (Succ x)
forall (n :: Nat).
(forall (m :: Nat).
SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT)
-> CmpSuccStepR n
CmpSuccStepR ((forall (m :: Nat).
SNat m
-> (CmpNat (Succ x) m :~: 'LT) -> CmpNat (Succ x) (Succ m) :~: 'LT)
-> CmpSuccStepR (Succ x))
-> (forall (m :: Nat).
SNat m
-> (CmpNat (Succ x) m :~: 'LT) -> CmpNat (Succ x) (Succ m) :~: 'LT)
-> CmpSuccStepR (Succ x)
forall a b. (a -> b) -> a -> b
$ \SNat m
m CmpNat (Succ x) m :~: 'LT
snltm ->
case SNat m -> ZeroOrSucc m
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat m
m of
ZeroOrSucc m
IsZero -> Void -> CmpNat (Succ x) 1 :~: 'LT
forall a. Void -> a
absurd (Void -> CmpNat (Succ x) 1 :~: 'LT)
-> Void -> CmpNat (Succ x) 1 :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat (Succ x) -> (CmpNat (Succ x) 0 :~: 'LT) -> Void
forall (a :: Nat). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT (SNat x -> SNat (Succ x)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat x
n) CmpNat (Succ x) m :~: 'LT
CmpNat (Succ x) 0 :~: 'LT
snltm
IsSucc SNat n
m' ->
let nLTm' :: CmpNat x n :~: 'LT
nLTm' = (CmpNat x n :~: CmpNat (Succ x) m)
-> (CmpNat (Succ x) m :~: 'LT) -> CmpNat x n :~: 'LT
forall k (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
trans (SNat x -> SNat n -> CmpNat x n :~: CmpNat (Succ x) (Succ n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat x
n SNat n
m') CmpNat (Succ x) m :~: 'LT
snltm
in SOrdering (CmpNat (Succ x) (Succ m))
-> CmpNat (Succ x) (Succ m) :~: CmpNat (Succ x) (Succ m)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Succ x)
-> SNat (Succ m) -> SOrdering (CmpNat (Succ x) (Succ m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat x -> SNat (Succ x)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat x
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m))
(CmpNat (Succ x) (Succ m) :~: CmpNat (Succ x) (Succ m))
-> SOrdering (CmpNat (Succ x) (Succ m))
-> CmpNat (Succ x) (Succ m) :~: CmpNat (Succ x) (Succ m)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat (Succ x)
-> SNat (Succ m) -> SOrdering (CmpNat (Succ x) (Succ m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat x -> SNat (Succ x)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat x
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
m'))
(CmpNat (Succ x) (Succ m) :~: CmpNat (Succ x) (Succ m))
-> Reason (:~:) (CmpNat (Succ x) (Succ m)) (CmpNat x m)
-> CmpNat (Succ x) (Succ m) :~: CmpNat x m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat x -> SNat m -> SOrdering (CmpNat x m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat x
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
m') SOrdering (CmpNat x m)
-> (CmpNat (Succ x) (Succ m) :~: CmpNat x m)
-> Reason (:~:) (CmpNat (Succ x) (Succ m)) (CmpNat x m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (CmpNat x m :~: CmpNat (Succ x) (Succ m))
-> CmpNat (Succ x) (Succ m) :~: CmpNat x m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat x -> SNat m -> CmpNat x m :~: CmpNat (Succ x) (Succ m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat x
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
m'))
(CmpNat (Succ x) (Succ m) :~: CmpNat x m)
-> Reason (:~:) (CmpNat x m) 'LT
-> CmpNat (Succ x) (Succ m) :~: 'LT
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'LT
SLT SOrdering 'LT
-> (CmpNat x m :~: 'LT) -> Reason (:~:) (CmpNat x m) 'LT
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> (CmpNat x n :~: 'LT) -> CmpNat x (Succ n) :~: 'LT
forall (m :: Nat).
SNat m -> (CmpNat x m :~: 'LT) -> CmpNat x (Succ m) :~: 'LT
ih SNat n
m' CmpNat x n :~: 'LT
nLTm'
ltSuccLToLT ::
SNat n ->
SNat m ->
CmpNat (Succ n) m :~: 'LT ->
CmpNat n m :~: 'LT
ltSuccLToLT :: SNat n
-> SNat m -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n m :~: 'LT
ltSuccLToLT SNat n
n SNat m
m CmpNat (Succ n) m :~: 'LT
snLTm =
case SNat m -> ZeroOrSucc m
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat m
m of
ZeroOrSucc m
IsZero -> Void -> CmpNat n 0 :~: 'LT
forall a. Void -> a
absurd (Void -> CmpNat n 0 :~: 'LT) -> Void -> CmpNat n 0 :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat (Succ n) -> (CmpNat (Succ n) 0 :~: 'LT) -> Void
forall (a :: Nat). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) CmpNat (Succ n) m :~: 'LT
CmpNat (Succ n) 0 :~: 'LT
snLTm
IsSucc SNat n
m' ->
let nLTm :: CmpNat n n :~: 'LT
nLTm = SNat n -> SNat n -> CmpNat n n :~: CmpNat (Succ n) (Succ n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n SNat n
m' (CmpNat n n :~: CmpNat (Succ n) m)
-> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n n :~: 'LT
forall k (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
`trans` CmpNat (Succ n) m :~: 'LT
snLTm
in SOrdering (CmpNat n m) -> CmpNat n m :~: CmpNat n m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
m'))
(CmpNat n m :~: CmpNat n m)
-> Reason (:~:) (CmpNat n m) 'LT -> CmpNat n m :~: 'LT
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'LT
SLT SOrdering 'LT
-> (CmpNat n m :~: 'LT) -> Reason (:~:) (CmpNat n m) 'LT
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n
-> SNat n -> (CmpNat n n :~: 'LT) -> CmpNat n (Succ n) :~: 'LT
forall (n :: Nat) (m :: Nat).
SNat n
-> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
cmpSuccStepR SNat n
n SNat n
m' CmpNat n n :~: 'LT
nLTm
leqToLT ::
SNat a ->
SNat b ->
IsTrue (Succ a <=? b) ->
CmpNat a b :~: 'LT
leqToLT :: SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
leqToLT SNat a
n SNat b
m IsTrue (Succ a <=? b)
snLEQm =
case SNat (Succ a)
-> SNat b
-> IsTrue (Succ a <=? b)
-> Either (Succ a :~: b) (CmpNat (Succ a) b :~: 'LT)
forall (a :: Nat) (b :: Nat).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
n) SNat b
m IsTrue (Succ a <=? b)
snLEQm of
Left Succ a :~: b
eql ->
(Succ a :~: b)
-> ((Succ a ~ b) => CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
withRefl Succ a :~: b
eql (((Succ a ~ b) => CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT)
-> ((Succ a ~ b) => CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT
forall a b. (a -> b) -> a -> b
$
SOrdering (CmpNat a b) -> CmpNat a b :~: CmpNat a b
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat b
m)
(CmpNat a b :~: CmpNat a b)
-> SOrdering (CmpNat a b) -> CmpNat a b :~: CmpNat a b
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
n)
(CmpNat a b :~: CmpNat a b)
-> Reason (:~:) (CmpNat a b) 'LT -> CmpNat a b :~: 'LT
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'LT
SLT SOrdering 'LT
-> (CmpNat a b :~: 'LT) -> Reason (:~:) (CmpNat a b) 'LT
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> CmpNat a (Succ a) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc SNat a
n
Right CmpNat (Succ a) b :~: 'LT
nLTm -> SNat a
-> SNat b -> (CmpNat (Succ a) b :~: 'LT) -> CmpNat a b :~: 'LT
forall (n :: Nat) (m :: Nat).
SNat n
-> SNat m -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n m :~: 'LT
ltSuccLToLT SNat a
n SNat b
m CmpNat (Succ a) b :~: 'LT
nLTm
leqZero :: SNat n -> IsTrue (0 <=? n)
leqZero :: SNat n -> IsTrue (0 <=? n)
leqZero SNat n
_ = IsTrue (0 <=? n)
IsTrue 'True
Witness
leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc SNat n
_ SNat m
_ IsTrue (n <=? m)
Witness = IsTrue (Succ n <=? Succ m)
IsTrue 'True
Witness
fromLeqView :: LeqView n m -> IsTrue (n <=? m)
fromLeqView :: LeqView n m -> IsTrue (n <=? m)
fromLeqView (LeqZero SNat m
n) = SNat m -> IsTrue (0 <=? m)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat m
n
fromLeqView (LeqSucc SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm) = SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm
leqViewRefl :: SNat n -> LeqView n n
leqViewRefl :: SNat n -> LeqView n n
leqViewRefl = LeqViewRefl n -> LeqView n n
forall (n :: Nat). LeqViewRefl n -> LeqView n n
proofLeqViewRefl (LeqViewRefl n -> LeqView n n)
-> (SNat n -> LeqViewRefl n) -> SNat n -> LeqView n n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeqViewRefl 0
-> (forall (n :: Nat).
SNat n -> LeqViewRefl n -> LeqViewRefl (S n))
-> SNat n
-> LeqViewRefl n
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction LeqViewRefl 0
base forall (n :: Nat). SNat n -> LeqViewRefl n -> LeqViewRefl (S n)
step
where
base :: LeqViewRefl 0
base :: LeqViewRefl 0
base = LeqView 0 0 -> LeqViewRefl 0
forall (n :: Nat). LeqView n n -> LeqViewRefl n
LeqViewRefl (LeqView 0 0 -> LeqViewRefl 0) -> LeqView 0 0 -> LeqViewRefl 0
forall a b. (a -> b) -> a -> b
$ SNat 0 -> LeqView 0 0
forall (n :: Nat). SNat n -> LeqView 0 n
LeqZero SNat 0
sZero
step :: SNat n -> LeqViewRefl n -> LeqViewRefl (Succ n)
step :: SNat n -> LeqViewRefl n -> LeqViewRefl (Succ n)
step SNat n
n (LeqViewRefl LeqView n n
nLEQn) =
LeqView (Succ n) (Succ n) -> LeqViewRefl (Succ n)
forall (n :: Nat). LeqView n n -> LeqViewRefl n
LeqViewRefl (LeqView (Succ n) (Succ n) -> LeqViewRefl (Succ n))
-> LeqView (Succ n) (Succ n) -> LeqViewRefl (Succ n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat n -> IsTrue (n <=? n) -> LeqView (Succ n) (Succ n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)
LeqSucc SNat n
n SNat n
n (LeqView n n -> IsTrue (n <=? n)
forall (n :: Nat) (m :: Nat). LeqView n m -> IsTrue (n <=? m)
fromLeqView LeqView n n
nLEQn)
viewLeq :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm =
case (SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat n
n, SNat n
-> SNat m
-> IsTrue (n <=? m)
-> Either (n :~: m) (CmpNat n m :~: 'LT)
forall (a :: Nat) (b :: Nat).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm) of
(ZeroOrSucc n
IsZero, Either (n :~: m) (CmpNat n m :~: 'LT)
_) -> SNat m -> LeqView 0 m
forall (n :: Nat). SNat n -> LeqView 0 n
LeqZero SNat m
m
(ZeroOrSucc n
_, Left n :~: m
Refl) -> SNat n -> LeqView n n
forall (n :: Nat). SNat n -> LeqView n n
leqViewRefl SNat n
n
(IsSucc SNat n
n', Right CmpNat n m :~: 'LT
nLTm) ->
let sm'EQm :: m :~: Succ (Pred m)
sm'EQm = SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> m :~: Succ (Pred m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
ltRightPredSucc SNat n
n SNat m
m CmpNat n m :~: 'LT
nLTm
m' :: SNat (Pred m)
m' = SNat m -> SNat (Pred m)
forall (n :: Nat). SNat n -> SNat (Pred n)
sPred SNat m
m
n'LTm' :: CmpNat n (Pred m) :~: 'LT
n'LTm' = SNat n
-> SNat (Pred m)
-> CmpNat n (Pred m) :~: CmpNat (Succ n) (Succ (Pred m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n' SNat (Pred m)
m' (CmpNat n (Pred m) :~: CmpNat n (Succ (Pred m)))
-> (CmpNat n (Succ (Pred m)) :~: CmpNat n m)
-> CmpNat n (Pred m) :~: CmpNat n m
forall k (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
`trans` SNat n
-> (Succ (Pred m) :~: m) -> CmpNat n (Succ (Pred m)) :~: CmpNat n m
forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> (b :~: c) -> CmpNat a b :~: CmpNat a c
compareCongR SNat n
n ((m :~: Succ (Pred m)) -> Succ (Pred m) :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym m :~: Succ (Pred m)
sm'EQm) (CmpNat n (Pred m) :~: CmpNat n m)
-> (CmpNat n m :~: 'LT) -> CmpNat n (Pred m) :~: 'LT
forall k (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
`trans` CmpNat n m :~: 'LT
nLTm
in (Succ (Pred m) :~: m)
-> ((Succ (Pred m) ~ m) => LeqView n m) -> LeqView n m
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((m :~: Succ (Pred m)) -> Succ (Pred m) :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym m :~: Succ (Pred m)
sm'EQm) (((Succ (Pred m) ~ m) => LeqView n m) -> LeqView n m)
-> ((Succ (Pred m) ~ m) => LeqView n m) -> LeqView n m
forall a b. (a -> b) -> a -> b
$ SNat n
-> SNat (Pred m)
-> IsTrue (n <=? Pred m)
-> LeqView (Succ n) (Succ (Pred m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)
LeqSucc SNat n
n' SNat (Pred m)
m' (IsTrue (n <=? Pred m) -> LeqView (Succ n) (Succ (Pred m)))
-> IsTrue (n <=? Pred m) -> LeqView (Succ n) (Succ (Pred m))
forall a b. (a -> b) -> a -> b
$ SNat n
-> SNat (Pred m)
-> (CmpNat n (Pred m) :~: 'LT)
-> IsTrue (n <=? Pred m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat n
n' SNat (Pred m)
m' CmpNat n (Pred m) :~: 'LT
n'LTm'
leqWitness :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness :: SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness = \SNat n
sn -> LeqWitPf n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat).
LeqWitPf n
-> forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitPf (LeqWitPf 0
-> (forall (n :: Nat). SNat n -> LeqWitPf n -> LeqWitPf (S n))
-> SNat n
-> LeqWitPf n
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction LeqWitPf 0
base forall (n :: Nat). SNat n -> LeqWitPf n -> LeqWitPf (S n)
step SNat n
sn) @m
where
base :: LeqWitPf 0
base :: LeqWitPf 0
base = (forall (m :: Nat). SNat m -> IsTrue (0 <=? m) -> DiffNat 0 m)
-> LeqWitPf 0
forall (n :: Nat).
(forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m)
-> LeqWitPf n
LeqWitPf ((forall (m :: Nat). SNat m -> IsTrue (0 <=? m) -> DiffNat 0 m)
-> LeqWitPf 0)
-> (forall (m :: Nat). SNat m -> IsTrue (0 <=? m) -> DiffNat 0 m)
-> LeqWitPf 0
forall a b. (a -> b) -> a -> b
$ \SNat m
sm IsTrue (0 <=? m)
_ -> (m :~: m) -> ((m ~ m) => DiffNat 0 m) -> DiffNat 0 m
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat m -> (0 + m) :~: m
forall (n :: Nat). SNat n -> (0 + n) :~: n
plusZeroL SNat m
sm) (((m ~ m) => DiffNat 0 m) -> DiffNat 0 m)
-> ((m ~ m) => DiffNat 0 m) -> DiffNat 0 m
forall a b. (a -> b) -> a -> b
$ SNat 0 -> SNat m -> DiffNat 0 (0 + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> DiffNat n (n + m)
DiffNat SNat 0
sZero SNat m
sm
step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)
step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)
step (SNat x
n :: SNat x) (LeqWitPf forall (m :: Nat). SNat m -> IsTrue (x <=? m) -> DiffNat x m
ih) = (forall (m :: Nat).
SNat m -> IsTrue (Succ x <=? m) -> DiffNat (Succ x) m)
-> LeqWitPf (Succ x)
forall (n :: Nat).
(forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m)
-> LeqWitPf n
LeqWitPf ((forall (m :: Nat).
SNat m -> IsTrue (Succ x <=? m) -> DiffNat (Succ x) m)
-> LeqWitPf (Succ x))
-> (forall (m :: Nat).
SNat m -> IsTrue (Succ x <=? m) -> DiffNat (Succ x) m)
-> LeqWitPf (Succ x)
forall a b. (a -> b) -> a -> b
$ \SNat m
m IsTrue (Succ x <=? m)
snLEQm ->
case SNat (Succ x)
-> SNat m -> IsTrue (Succ x <=? m) -> LeqView (Succ x) m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq (SNat x -> SNat (Succ x)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat x
n) SNat m
m IsTrue (Succ x <=? m)
snLEQm of
LeqZero SNat m
_ -> Void -> DiffNat (Succ x) m
forall a. Void -> a
absurd (Void -> DiffNat (Succ x) m) -> Void -> DiffNat (Succ x) m
forall a b. (a -> b) -> a -> b
$ SNat x -> (Succ x :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat x
n Succ x :~: 0
forall k (a :: k). a :~: a
Refl
LeqSucc (SNat n
_ :: SNat n') SNat m
pm IsTrue (n <=? m)
nLEQpm ->
SNat x -> SNat m -> DiffNat x m -> DiffNat (Succ x) (Succ m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat SNat x
n SNat m
pm (DiffNat x m -> DiffNat (Succ x) (Succ m))
-> DiffNat x m -> DiffNat (Succ x) (Succ m)
forall a b. (a -> b) -> a -> b
$ SNat m -> IsTrue (x <=? m) -> DiffNat x m
forall (m :: Nat). SNat m -> IsTrue (x <=? m) -> DiffNat x m
ih SNat m
pm (IsTrue (x <=? m) -> DiffNat x m)
-> IsTrue (x <=? m) -> DiffNat x m
forall a b. (a -> b) -> a -> b
$ (n :~: x) -> SNat m -> IsTrue (n <=? m) -> IsTrue (x <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL ((Succ n :~: Succ x) -> n :~: x
forall (n :: Nat) (m :: Nat). (Succ n :~: Succ m) -> n :~: m
succInj Succ n :~: Succ x
forall k (a :: k). a :~: a
Refl :: n' :~: x) SNat m
pm IsTrue (n <=? m)
nLEQpm
leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)
leqStep :: SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
sn = LeqStepPf n
-> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
forall (n :: Nat).
LeqStepPf n
-> forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStepPf (LeqStepPf 0
-> (forall (n :: Nat). SNat n -> LeqStepPf n -> LeqStepPf (S n))
-> SNat n
-> LeqStepPf n
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction LeqStepPf 0
base forall (n :: Nat). SNat n -> LeqStepPf n -> LeqStepPf (S n)
step SNat n
sn) @m @l
where
base :: LeqStepPf 0
base :: LeqStepPf 0
base = (forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((0 + l) :~: m) -> IsTrue (0 <=? m))
-> LeqStepPf 0
forall (n :: Nat).
(forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m))
-> LeqStepPf n
LeqStepPf ((forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((0 + l) :~: m) -> IsTrue (0 <=? m))
-> LeqStepPf 0)
-> (forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((0 + l) :~: m) -> IsTrue (0 <=? m))
-> LeqStepPf 0
forall a b. (a -> b) -> a -> b
$ \SNat m
k SNat l
_ (0 + l) :~: m
_ -> SNat m -> IsTrue (0 <=? m)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat m
k
step :: forall k. SNat k -> LeqStepPf k -> LeqStepPf (Succ k)
step :: SNat k -> LeqStepPf k -> LeqStepPf (Succ k)
step SNat k
n (LeqStepPf forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((k + l) :~: m) -> IsTrue (k <=? m)
ih) =
(forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((Succ k + l) :~: m) -> IsTrue (Succ k <=? m))
-> LeqStepPf (Succ k)
forall (n :: Nat).
(forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m))
-> LeqStepPf n
LeqStepPf ((forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((Succ k + l) :~: m) -> IsTrue (Succ k <=? m))
-> LeqStepPf (Succ k))
-> (forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((Succ k + l) :~: m) -> IsTrue (Succ k <=? m))
-> LeqStepPf (Succ k)
forall a b. (a -> b) -> a -> b
$ \SNat m
k SNat l
l (Succ k + l) :~: m
snPlEqk ->
let kEQspk :: m :~: ((k + l) + 1)
kEQspk =
SNat m -> m :~: m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SNat m
k
(m :~: m) -> Reason (:~:) m (Succ k + l) -> m :~: (Succ k + l)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat k -> SNat (Succ k)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat k
n SNat (Succ k) -> SNat l -> SNat (Succ k + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l SNat (Succ k + l)
-> (m :~: (Succ k + l)) -> Reason (:~:) m (Succ k + l)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ((Succ k + l) :~: m) -> m :~: (Succ k + l)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (Succ k + l) :~: m
snPlEqk
(m :~: (Succ k + l))
-> Reason (:~:) (Succ k + l) ((k + l) + 1) -> m :~: ((k + l) + 1)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat (k + l) -> SNat ((k + l) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat k
n SNat k -> SNat l -> SNat (k + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) SNat ((k + l) + 1)
-> ((Succ k + l) :~: ((k + l) + 1))
-> Reason (:~:) (Succ k + l) ((k + l) + 1)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat k -> SNat l -> (Succ k + l) :~: ((k + l) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat k
n SNat l
l
pk :: SNat (k + l)
pk = SNat k
n SNat k -> SNat l -> SNat (k + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l
in SNat (Succ k)
-> (((k + l) + 1) :~: m)
-> IsTrue (Succ k <=? ((k + l) + 1))
-> IsTrue (Succ k <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)
coerceLeqR (SNat k -> SNat (Succ k)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat k
n) ((m :~: ((k + l) + 1)) -> ((k + l) + 1) :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym m :~: ((k + l) + 1)
kEQspk) (IsTrue (Succ k <=? ((k + l) + 1)) -> IsTrue (Succ k <=? m))
-> IsTrue (Succ k <=? ((k + l) + 1)) -> IsTrue (Succ k <=? m)
forall a b. (a -> b) -> a -> b
$ SNat k
-> SNat (k + l)
-> IsTrue (k <=? (k + l))
-> IsTrue (Succ k <=? ((k + l) + 1))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc SNat k
n SNat (k + l)
pk (IsTrue (k <=? (k + l)) -> IsTrue (Succ k <=? ((k + l) + 1)))
-> IsTrue (k <=? (k + l)) -> IsTrue (Succ k <=? ((k + l) + 1))
forall a b. (a -> b) -> a -> b
$ SNat (k + l)
-> SNat l -> ((k + l) :~: (k + l)) -> IsTrue (k <=? (k + l))
forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((k + l) :~: m) -> IsTrue (k <=? m)
ih SNat (k + l)
pk SNat l
l (k + l) :~: (k + l)
forall k (a :: k). a :~: a
Refl
leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> (n :~: m -> Void) -> IsTrue (Succ n <=? m)
leqNeqToSuccLeq :: SNat n
-> SNat m
-> IsTrue (n <=? m)
-> ((n :~: m) -> Void)
-> IsTrue (Succ n <=? m)
leqNeqToSuccLeq SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm (n :~: m) -> Void
nNEQm =
case SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm of
DiffNat SNat n
_ SNat m
k ->
case SNat m -> ZeroOrSucc m
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat m
k of
ZeroOrSucc m
IsZero -> Void -> IsTrue (Succ n <=? n)
forall a. Void -> a
absurd (Void -> IsTrue (Succ n <=? n)) -> Void -> IsTrue (Succ n <=? n)
forall a b. (a -> b) -> a -> b
$ (n :~: m) -> Void
nNEQm ((n :~: m) -> Void) -> (n :~: m) -> Void
forall a b. (a -> b) -> a -> b
$ (m :~: n) -> n :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((m :~: n) -> n :~: m) -> (m :~: n) -> n :~: m
forall a b. (a -> b) -> a -> b
$ SNat n -> (n + 0) :~: n
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat n
n
IsSucc SNat n
k' ->
SNat (Succ n)
-> SNat m
-> SNat n
-> ((Succ n + n) :~: m)
-> IsTrue (Succ n <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m SNat n
k' (((Succ n + n) :~: m) -> IsTrue (Succ n <=? m))
-> ((Succ n + n) :~: m) -> IsTrue (Succ n <=? m)
forall a b. (a -> b) -> a -> b
$
SNat (Succ n + n) -> (Succ n + n) :~: (Succ n + n)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat n -> SNat (Succ n + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
k')
((Succ n + n) :~: (Succ n + n))
-> Reason (:~:) (Succ n + n) ((n + n) + 1)
-> (Succ n + n) :~: ((n + n) + 1)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat (n + n) -> SNat ((n + n) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat n -> SNat (n + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
k') SNat ((n + n) + 1)
-> ((Succ n + n) :~: ((n + n) + 1))
-> Reason (:~:) (Succ n + n) ((n + n) + 1)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat n -> (Succ n + n) :~: ((n + n) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat n
k'
((Succ n + n) :~: ((n + n) + 1))
-> Reason (:~:) ((n + n) + 1) m -> (Succ n + n) :~: m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
k' SNat m -> (((n + n) + 1) :~: m) -> Reason (:~:) ((n + n) + 1) m
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (m :~: ((n + n) + 1)) -> ((n + n) + 1) :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat n -> (n + Succ n) :~: ((n + n) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat n
n SNat n
k')
((Succ n + n) :~: m) -> SNat m -> (Succ n + n) :~: m
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m
leqRefl :: SNat n -> IsTrue (n <=? n)
leqRefl :: SNat n -> IsTrue (n <=? n)
leqRefl SNat n
sn = SNat n -> SNat n -> SNat 0 -> ((n + 0) :~: n) -> IsTrue (n <=? n)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
sn SNat n
sn SNat 0
sZero (SNat n -> (n + 0) :~: n
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat n
sn)
leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm =
case SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm of
DiffNat SNat n
_ SNat m
k ->
SNat n
-> SNat (Succ m)
-> SNat (m + 1)
-> ((n + (m + 1)) :~: Succ m)
-> IsTrue (n <=? Succ m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
n (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) (((n + (m + 1)) :~: Succ m) -> IsTrue (n <=? Succ m))
-> ((n + (m + 1)) :~: Succ m) -> IsTrue (n <=? Succ m)
forall a b. (a -> b) -> a -> b
$
SNat (n + (m + 1)) -> (n + (m + 1)) :~: (n + (m + 1))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n
n SNat n -> SNat (m + 1) -> SNat (n + (m + 1))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) ((n + (m + 1)) :~: (n + (m + 1)))
-> Reason (:~:) (n + (m + 1)) (Succ m) -> (n + (m + 1)) :~: Succ m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ m)
-> ((n + (m + 1)) :~: Succ m)
-> Reason (:~:) (n + (m + 1)) (Succ m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> (n + (m + 1)) :~: S (n + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat n
n SNat m
k ((n + (m + 1)) :~: Succ m)
-> SNat (Succ m) -> (n + (m + 1)) :~: Succ m
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m
leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL SNat n
n SNat m
m IsTrue (Succ n <=? m)
snLEQm =
SNat n
-> SNat (Succ n)
-> SNat m
-> IsTrue (n <=? Succ n)
-> IsTrue (Succ n <=? m)
-> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (SNat n -> SNat n -> IsTrue (n <=? n) -> IsTrue (n <=? Succ n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR SNat n
n SNat n
n (IsTrue (n <=? n) -> IsTrue (n <=? Succ n))
-> IsTrue (n <=? n) -> IsTrue (n <=? Succ n)
forall a b. (a -> b) -> a -> b
$ SNat n -> IsTrue (n <=? n)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
n) IsTrue (Succ n <=? m)
snLEQm
leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m)
leqReflexive :: SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat n
n SNat m
_ n :~: m
Refl = SNat n -> IsTrue (n <=? n)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
n
leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)
leqTrans :: SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans SNat n
n SNat m
m SNat l
k IsTrue (n <=? m)
nLEm IsTrue (m <=? l)
mLEk =
case SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEm of
DiffNat SNat n
_ SNat m
mMn -> case SNat m -> SNat l -> IsTrue (m <=? l) -> DiffNat m l
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat m
m SNat l
k IsTrue (m <=? l)
mLEk of
DiffNat SNat m
_ SNat m
kMn -> SNat n
-> SNat l
-> SNat (m + m)
-> ((n + (m + m)) :~: l)
-> IsTrue (n <=? l)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
n SNat l
k (SNat m
mMn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
kMn) ((l :~: (n + (m + m))) -> (n + (m + m)) :~: l
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((l :~: (n + (m + m))) -> (n + (m + m)) :~: l)
-> (l :~: (n + (m + m))) -> (n + (m + m)) :~: l
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> SNat m -> ((n + m) + m) :~: (n + (m + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat m
mMn SNat m
kMn)
leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm SNat n
n SNat m
m IsTrue (n <=? m)
nLEm IsTrue (m <=? n)
mLEn =
case (SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEm, SNat m -> SNat n -> IsTrue (m <=? n) -> DiffNat m n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat m
m SNat n
n IsTrue (m <=? n)
mLEn) of
(DiffNat SNat n
_ SNat m
mMn, DiffNat SNat m
_ SNat m
nMm) ->
let pEQ0 :: (m + m) :~: 0
pEQ0 =
SNat n
-> SNat (m + m)
-> SNat 0
-> ((n + (m + m)) :~: (n + 0))
-> (m + m) :~: 0
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) :~: (n + l)) -> m :~: l
plusEqCancelL SNat n
n (SNat m
mMn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
nMm) SNat 0
sZero (((n + (m + m)) :~: (n + 0)) -> (m + m) :~: 0)
-> ((n + (m + m)) :~: (n + 0)) -> (m + m) :~: 0
forall a b. (a -> b) -> a -> b
$
SNat (n + (m + m)) -> (n + (m + m)) :~: (n + (m + m))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n
n SNat n -> SNat (m + m) -> SNat (n + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
mMn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
nMm))
((n + (m + m)) :~: (n + (m + m)))
-> Reason (:~:) (n + (m + m)) n -> (n + (m + m)) :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMn) SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
nMm
SNat n -> ((n + (m + m)) :~: n) -> Reason (:~:) (n + (m + m)) n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (n :~: (n + (m + m))) -> (n + (m + m)) :~: n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat m -> SNat m -> ((n + m) + m) :~: (n + (m + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat m
mMn SNat m
nMm)
((n + (m + m)) :~: n) -> SNat n -> (n + (m + m)) :~: n
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
nMm
((n + (m + m)) :~: n) -> SNat n -> (n + (m + m)) :~: n
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n
n
((n + (m + m)) :~: n) -> Reason (:~:) n n -> (n + (m + m)) :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat 0 -> SNat (n + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero
SNat n -> (n :~: n) -> Reason (:~:) n n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (n :~: n) -> n :~: n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> (n + 0) :~: n
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat n
n)
nMmEQ0 :: m :~: 0
nMmEQ0 = SNat m -> SNat m -> ((m + m) :~: 0) -> m :~: 0
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> ((n + m) :~: 0) -> n :~: 0
plusEqZeroL SNat m
mMn SNat m
nMm (m + m) :~: 0
pEQ0
in (m :~: n) -> n :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((m :~: n) -> n :~: m) -> (m :~: n) -> n :~: m
forall a b. (a -> b) -> a -> b
$
SNat m -> m :~: m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SNat m
m
(m :~: m) -> SNat m -> m :~: m
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMn
(m :~: m) -> Reason (:~:) m n -> m :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat 0 -> SNat (n + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero SNat n -> (m :~: n) -> Reason (:~:) m n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> (m :~: 0) -> (n + m) :~: (n + 0)
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n m :~: 0
nMmEQ0
(m :~: n) -> Reason (:~:) n n -> m :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> (n :~: n) -> Reason (:~:) n n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> (n + 0) :~: n
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat n
n
plusMonotone ::
SNat n ->
SNat m ->
SNat l ->
SNat k ->
IsTrue (n <=? m) ->
IsTrue (l <=? k) ->
IsTrue ((n + l) <=? (m + k))
plusMonotone :: SNat n
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <=? m)
-> IsTrue (l <=? k)
-> IsTrue ((n + l) <=? (m + k))
plusMonotone SNat n
n SNat m
m SNat l
l SNat k
k IsTrue (n <=? m)
nLEm IsTrue (l <=? k)
lLEk =
case (SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEm, SNat l -> SNat k -> IsTrue (l <=? k) -> DiffNat l k
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat l
l SNat k
k IsTrue (l <=? k)
lLEk) of
(DiffNat SNat n
_ SNat m
mMINn, DiffNat SNat l
_ SNat m
kMINl) ->
let r :: SNat (m + m)
r = SNat m
mMINn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
kMINl
in SNat (n + l)
-> SNat (m + k)
-> SNat (m + m)
-> (((n + l) + (m + m)) :~: (m + k))
-> IsTrue ((n + l) <=? (m + k))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) (SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k) SNat (m + m)
r ((((n + l) + (m + m)) :~: (m + k)) -> IsTrue ((n + l) <=? (m + k)))
-> (((n + l) + (m + m)) :~: (m + k))
-> IsTrue ((n + l) <=? (m + k))
forall a b. (a -> b) -> a -> b
$
SNat ((n + l) + (m + m))
-> ((n + l) + (m + m)) :~: ((n + l) + (m + m))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l SNat (n + l) -> SNat (m + m) -> SNat ((n + l) + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat (m + m)
r)
(((n + l) + (m + m)) :~: ((n + l) + (m + m)))
-> Reason (:~:) ((n + l) + (m + m)) (n + (l + (m + m)))
-> ((n + l) + (m + m)) :~: (n + (l + (m + m)))
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat (l + (m + m)) -> SNat (n + (l + (m + m)))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat l
l SNat l -> SNat (m + m) -> SNat (l + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat (m + m)
r)
SNat (n + (l + (m + m)))
-> (((n + l) + (m + m)) :~: (n + (l + (m + m))))
-> Reason (:~:) ((n + l) + (m + m)) (n + (l + (m + m)))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n
-> SNat l
-> SNat (m + m)
-> ((n + l) + (m + m)) :~: (n + (l + (m + m)))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat l
l SNat (m + m)
r
(((n + l) + (m + m)) :~: (n + (l + (m + m))))
-> SNat (n + (l + (m + m)))
-> ((n + l) + (m + m)) :~: (n + (l + (m + m)))
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n
n SNat n -> SNat (l + (m + m)) -> SNat (n + (l + (m + m)))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat l
l SNat l -> SNat (m + m) -> SNat (l + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
mMINn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
kMINl))
(((n + l) + (m + m)) :~: (n + (l + (m + m))))
-> Reason (:~:) (n + (l + (m + m))) (n + (l + (m + m)))
-> ((n + l) + (m + m)) :~: (n + (l + (m + m)))
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat (l + (m + m)) -> SNat (n + (l + (m + m)))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat l
l SNat l -> SNat (m + m) -> SNat (l + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
kMINl SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMINn))
SNat (n + (l + (m + m)))
-> ((n + (l + (m + m))) :~: (n + (l + (m + m))))
-> Reason (:~:) (n + (l + (m + m))) (n + (l + (m + m)))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n
-> ((l + (m + m)) :~: (l + (m + m)))
-> (n + (l + (m + m))) :~: (n + (l + (m + m)))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n (SNat l -> ((m + m) :~: (m + m)) -> (l + (m + m)) :~: (l + (m + m))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat l
l (SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
mMINn SNat m
kMINl))
(((n + l) + (m + m)) :~: (n + (l + (m + m))))
-> Reason (:~:) (n + (l + (m + m))) (n + (k + m))
-> ((n + l) + (m + m)) :~: (n + (k + m))
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat (k + m) -> SNat (n + (k + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ ((SNat l
l SNat l -> SNat m -> SNat (l + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
kMINl) SNat k -> SNat m -> SNat (k + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMINn)
SNat (n + (k + m))
-> ((n + (l + (m + m))) :~: (n + (k + m)))
-> Reason (:~:) (n + (l + (m + m))) (n + (k + m))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n
-> ((l + (m + m)) :~: (k + m))
-> (n + (l + (m + m))) :~: (n + (k + m))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n (((k + m) :~: (l + (m + m))) -> (l + (m + m)) :~: (k + m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((k + m) :~: (l + (m + m))) -> (l + (m + m)) :~: (k + m))
-> ((k + m) :~: (l + (m + m))) -> (l + (m + m)) :~: (k + m)
forall a b. (a -> b) -> a -> b
$ SNat l -> SNat m -> SNat m -> ((l + m) + m) :~: (l + (m + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat l
l SNat m
kMINl SNat m
mMINn)
(((n + l) + (m + m)) :~: (n + (k + m)))
-> SNat (n + (k + m)) -> ((n + l) + (m + m)) :~: (n + (k + m))
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n
n SNat n -> SNat (k + m) -> SNat (n + (k + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat k
k SNat k -> SNat m -> SNat (k + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMINn)
(((n + l) + (m + m)) :~: (n + (k + m)))
-> Reason (:~:) (n + (k + m)) (n + (m + k))
-> ((n + l) + (m + m)) :~: (n + (m + k))
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat (m + k) -> SNat (n + (m + k))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
mMINn SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k)
SNat (n + (m + k))
-> ((n + (k + m)) :~: (n + (m + k)))
-> Reason (:~:) (n + (k + m)) (n + (m + k))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> ((k + m) :~: (m + k)) -> (n + (k + m)) :~: (n + (m + k))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n (SNat k -> SNat m -> (k + m) :~: (m + k)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat k
k SNat m
mMINn)
(((n + l) + (m + m)) :~: (n + (m + k)))
-> Reason (:~:) (n + (m + k)) (m + k)
-> ((n + l) + (m + m)) :~: (m + k)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMINn SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k
SNat (m + k)
-> ((n + (m + k)) :~: (m + k))
-> Reason (:~:) (n + (m + k)) (m + k)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ((m + k) :~: (n + (m + k))) -> (n + (m + k)) :~: (m + k)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat m -> SNat k -> ((n + m) + k) :~: (n + (m + k))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat m
mMINn SNat k
k)
(((n + l) + (m + m)) :~: (m + k))
-> SNat (m + k) -> ((n + l) + (m + m)) :~: (m + k)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k
leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim SNat n
n IsTrue (n <=? 0)
nLE0 =
case SNat n -> SNat 0 -> IsTrue (n <=? 0) -> LeqView n 0
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq SNat n
n SNat 0
sZero IsTrue (n <=? 0)
nLE0 of
LeqZero SNat 0
_ -> n :~: 0
forall k (a :: k). a :~: a
Refl
LeqSucc SNat n
_ SNat m
pZ IsTrue (n <=? m)
_ -> Void -> n :~: 0
forall a. Void -> a
absurd (Void -> n :~: 0) -> Void -> n :~: 0
forall a b. (a -> b) -> a -> b
$ SNat m -> (Succ m :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat m
pZ Succ m :~: 0
forall k (a :: k). a :~: a
Refl
plusMonotoneL ::
SNat n ->
SNat m ->
SNat l ->
IsTrue (n <=? m) ->
IsTrue ((n + l) <=? (m + l))
plusMonotoneL :: SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue ((n + l) <=? (m + l))
plusMonotoneL SNat n
n SNat m
m SNat l
l IsTrue (n <=? m)
leq = SNat n
-> SNat m
-> SNat l
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (l <=? l)
-> IsTrue ((n + l) <=? (m + l))
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))
plusMonotone SNat n
n SNat m
m SNat l
l SNat l
l IsTrue (n <=? m)
leq (SNat l -> IsTrue (l <=? l)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat l
l)
plusMonotoneR ::
SNat n ->
SNat m ->
SNat l ->
IsTrue (m <=? l) ->
IsTrue ((n + m) <=? (n + l))
plusMonotoneR :: SNat n
-> SNat m
-> SNat l
-> IsTrue (m <=? l)
-> IsTrue ((n + m) <=? (n + l))
plusMonotoneR SNat n
n SNat m
m SNat l
l IsTrue (m <=? l)
leq = SNat n
-> SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? n)
-> IsTrue (m <=? l)
-> IsTrue ((n + m) <=? (n + l))
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))
plusMonotone SNat n
n SNat n
n SNat m
m SNat l
l (SNat n -> IsTrue (n <=? n)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
n) IsTrue (m <=? l)
leq
plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqL SNat n
n SNat m
m = SNat n
-> SNat (n + m)
-> SNat m
-> ((n + m) :~: (n + m))
-> IsTrue (n <=? (n + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
n (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) SNat m
m (n + m) :~: (n + m)
forall k (a :: k). a :~: a
Refl
plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))
plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))
plusLeqR SNat n
n SNat m
m = SNat m
-> SNat (n + m)
-> SNat n
-> ((m + n) :~: (n + m))
-> IsTrue (m <=? (n + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat m
m (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) SNat n
n (((m + n) :~: (n + m)) -> IsTrue (m <=? (n + m)))
-> ((m + n) :~: (n + m)) -> IsTrue (m <=? (n + m))
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat n -> (m + n) :~: (n + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m SNat n
n
plusCancelLeqR ::
SNat n ->
SNat m ->
SNat l ->
IsTrue ((n + l) <=? (m + l)) ->
IsTrue (n <=? m)
plusCancelLeqR :: SNat n
-> SNat m
-> SNat l
-> IsTrue ((n + l) <=? (m + l))
-> IsTrue (n <=? m)
plusCancelLeqR SNat n
n SNat m
m SNat l
l IsTrue ((n + l) <=? (m + l))
nlLEQml =
case SNat (n + l)
-> SNat (m + l)
-> IsTrue ((n + l) <=? (m + l))
-> DiffNat (n + l) (m + l)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) (SNat m
m SNat m -> SNat l -> SNat (m + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) IsTrue ((n + l) <=? (m + l))
nlLEQml of
DiffNat SNat (n + l)
_ SNat m
k ->
let pf :: (n + m) :~: m
pf =
SNat (n + m)
-> SNat m -> SNat l -> (((n + m) + l) :~: (m + l)) -> (n + m) :~: m
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: (m + l)) -> n :~: m
plusEqCancelR (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat m
m SNat l
l ((((n + m) + l) :~: (m + l)) -> (n + m) :~: m)
-> (((n + m) + l) :~: (m + l)) -> (n + m) :~: m
forall a b. (a -> b) -> a -> b
$
SNat ((n + m) + l) -> ((n + m) + l) :~: ((n + m) + l)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start ((SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (n + m) -> SNat l -> SNat ((n + m) + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l)
(((n + m) + l) :~: ((n + m) + l))
-> Reason (:~:) ((n + m) + l) (n + (m + l))
-> ((n + m) + l) :~: (n + (m + l))
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat (m + l) -> SNat (n + (m + l))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
k SNat m -> SNat l -> SNat (m + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) SNat (n + (m + l))
-> (((n + m) + l) :~: (n + (m + l)))
-> Reason (:~:) ((n + m) + l) (n + (m + l))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat m
k SNat l
l
(((n + m) + l) :~: (n + (m + l)))
-> Reason (:~:) (n + (m + l)) (n + (l + m))
-> ((n + m) + l) :~: (n + (l + m))
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat (l + m) -> SNat (n + (l + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat l
l SNat l -> SNat m -> SNat (l + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (n + (l + m))
-> ((n + (m + l)) :~: (n + (l + m)))
-> Reason (:~:) (n + (m + l)) (n + (l + m))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> ((m + l) :~: (l + m)) -> (n + (m + l)) :~: (n + (l + m))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n (SNat m -> SNat l -> (m + l) :~: (l + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
k SNat l
l)
(((n + m) + l) :~: (n + (l + m)))
-> Reason (:~:) (n + (l + m)) ((n + l) + m)
-> ((n + m) + l) :~: ((n + l) + m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l SNat (n + l) -> SNat m -> SNat ((n + l) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat ((n + l) + m)
-> ((n + (l + m)) :~: ((n + l) + m))
-> Reason (:~:) (n + (l + m)) ((n + l) + m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (((n + l) + m) :~: (n + (l + m)))
-> (n + (l + m)) :~: ((n + l) + m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat l -> SNat m -> ((n + l) + m) :~: (n + (l + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat l
l SNat m
k)
(((n + m) + l) :~: ((n + l) + m))
-> SNat ((n + l) + m) -> ((n + m) + l) :~: ((n + l) + m)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m SNat m -> SNat l -> SNat (m + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l
in SNat n -> SNat m -> SNat m -> ((n + m) :~: m) -> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
n SNat m
m SNat m
k (n + m) :~: m
pf
plusCancelLeqL ::
SNat n ->
SNat m ->
SNat l ->
IsTrue ((n + m) <=? (n + l)) ->
IsTrue (m <=? l)
plusCancelLeqL :: SNat n
-> SNat m
-> SNat l
-> IsTrue ((n + m) <=? (n + l))
-> IsTrue (m <=? l)
plusCancelLeqL SNat n
n SNat m
m SNat l
l IsTrue ((n + m) <=? (n + l))
nmLEQnl =
SNat m
-> SNat l
-> SNat n
-> IsTrue ((m + n) <=? (l + n))
-> IsTrue (m <=? l)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue ((n + l) <=? (m + l))
-> IsTrue (n <=? m)
plusCancelLeqR SNat m
m SNat l
l SNat n
n (IsTrue ((m + n) <=? (l + n)) -> IsTrue (m <=? l))
-> IsTrue ((m + n) <=? (l + n)) -> IsTrue (m <=? l)
forall a b. (a -> b) -> a -> b
$
((n + m) :~: (m + n))
-> SNat (l + n)
-> IsTrue ((n + m) <=? (l + n))
-> IsTrue ((m + n) <=? (l + n))
forall (n :: Nat) (m :: Nat) (l :: Nat).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL (SNat n -> SNat m -> (n + m) :~: (m + n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat n
n SNat m
m) (SNat l
l SNat l -> SNat n -> SNat (l + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
n) (IsTrue ((n + m) <=? (l + n)) -> IsTrue ((m + n) <=? (l + n)))
-> IsTrue ((n + m) <=? (l + n)) -> IsTrue ((m + n) <=? (l + n))
forall a b. (a -> b) -> a -> b
$
SNat (n + m)
-> ((n + l) :~: (l + n))
-> IsTrue ((n + m) <=? (n + l))
-> IsTrue ((n + m) <=? (l + n))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)
coerceLeqR (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) (SNat n -> SNat l -> (n + l) :~: (l + n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat n
n SNat l
l) IsTrue ((n + m) <=? (n + l))
nmLEQnl
succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n
n IsTrue (S n <=? 0)
leq =
SNat n -> (S n :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat n
n (SNat (S n) -> IsTrue (S n <=? 0) -> S n :~: 0
forall (n :: Nat). SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim (SNat n -> SNat (S n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) IsTrue (S n <=? 0)
leq)
succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False
succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False
succLeqZeroAbsurd' SNat n
n =
case SNat n -> SNat (S n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (S n) -> SNat 0 -> SBool (S n <=? 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat 0
sZero of
SBool (S n <=? 0)
STrue -> Void -> 'True :~: 'False
forall a. Void -> a
absurd (Void -> 'True :~: 'False) -> Void -> 'True :~: 'False
forall a b. (a -> b) -> a -> b
$ SNat n -> IsTrue (S n <=? 0) -> Void
forall (n :: Nat). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n
n IsTrue (S n <=? 0)
IsTrue 'True
Witness
SBool (S n <=? 0)
SFalse -> (S n <=? 0) :~: 'False
forall k (a :: k). a :~: a
Refl
succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd SNat n
n IsTrue (S n <=? n)
snLEQn =
('LT :~: 'EQ) -> Void
forall a x. Empty a => a -> x
eliminate (('LT :~: 'EQ) -> Void) -> ('LT :~: 'EQ) -> Void
forall a b. (a -> b) -> a -> b
$
SOrdering 'LT -> 'LT :~: 'LT
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SOrdering 'LT
SLT
('LT :~: 'LT) -> Reason (:~:) 'LT 'EQ -> 'LT :~: 'EQ
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat n -> SOrdering (CmpNat n n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat n
n SOrdering 'EQ -> ('LT :~: 'EQ) -> Reason (:~:) 'LT 'EQ
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ('EQ :~: 'LT) -> 'LT :~: 'EQ
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat n -> IsTrue (S n <=? n) -> CmpNat n n :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT SNat n
n SNat n
n IsTrue (S n <=? n)
snLEQn)
('LT :~: 'EQ) -> Reason (:~:) 'EQ 'EQ -> 'LT :~: 'EQ
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'EQ
SEQ SOrdering 'EQ -> ('EQ :~: 'EQ) -> Reason (:~:) 'EQ 'EQ
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat n -> (n :~: n) -> CmpNat n n :~: 'EQ
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat n
n SNat n
n n :~: n
forall k (a :: k). a :~: a
Refl
succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False
succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False
succLeqAbsurd' SNat n
n =
case SNat n -> SNat (S n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (S n) -> SNat n -> SBool (S n <=? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
SBool (S n <=? n)
STrue -> Void -> 'True :~: 'False
forall a. Void -> a
absurd (Void -> 'True :~: 'False) -> Void -> 'True :~: 'False
forall a b. (a -> b) -> a -> b
$ SNat n -> IsTrue (S n <=? n) -> Void
forall (n :: Nat). SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd SNat n
n IsTrue (S n <=? n)
IsTrue 'True
Witness
SBool (S n <=? n)
SFalse -> (S n <=? n) :~: 'False
forall k (a :: k). a :~: a
Refl
notLeqToLeq :: ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq :: SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m =
case SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m of
SOrdering (CmpNat n m)
SLT -> IsTrue 'False -> IsTrue (m <=? n)
forall a x. Empty a => a -> x
eliminate (IsTrue 'False -> IsTrue (m <=? n))
-> IsTrue 'False -> IsTrue (m <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <=? m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat n
n SNat m
m CmpNat n m :~: 'LT
forall k (a :: k). a :~: a
Refl
SOrdering (CmpNat n m)
SEQ -> IsTrue 'False -> IsTrue (m <=? n)
forall a x. Empty a => a -> x
eliminate (IsTrue 'False -> IsTrue (m <=? n))
-> IsTrue 'False -> IsTrue (m <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat n
n SNat m
m ((n :~: m) -> IsTrue (n <=? m)) -> (n :~: m) -> IsTrue (n <=? m)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (CmpNat n m :~: 'EQ) -> n :~: m
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b
eqToRefl SNat n
n SNat m
m CmpNat n m :~: 'EQ
forall k (a :: k). a :~: a
Refl
SOrdering (CmpNat n m)
SGT -> SNat n -> SNat m -> (CmpNat n m :~: 'GT) -> IsTrue (m <=? n)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a)
gtToLeq SNat n
n SNat m
m CmpNat n m :~: 'GT
forall k (a :: k). a :~: a
Refl
leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
leqSucc' SNat n
_ SNat m
_ = (n <=? m) :~: (Succ n <=? Succ m)
forall k (a :: k). a :~: a
Refl
leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
_ SNat m
_ IsTrue (n <=? m)
Witness = Min n m :~: n
forall k (a :: k). a :~: a
Refl
geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m IsTrue (m <=? n)
Witness =
case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
SBool (n <=? m)
SFalse -> Min n m :~: m
forall k (a :: k). a :~: a
Refl
SBool (n <=? m)
STrue -> Min n m :~: m
forall k (a :: k). a :~: a
Refl
minComm :: SNat n -> SNat m -> Min n m :~: Min m n
minComm :: SNat n -> SNat m -> Min n m :~: Min m n
minComm SNat n
n SNat m
m =
case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
SBool (n <=? m)
STrue ->
SNat n -> n :~: n
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (n :~: n) -> Reason (:~:) n n -> n :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> (n :~: n) -> Reason (:~:) n n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
(n :~: n) -> Reason (:~:) n (Min m n) -> n :~: Min m n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat n -> SNat (Min m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n SNat (Min m n) -> (n :~: Min m n) -> Reason (:~:) n (Min m n)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (Min m n :~: n) -> n :~: Min m n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (n <=? m) -> Min m n :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat m
m SNat n
n IsTrue (n <=? m)
IsTrue 'True
Witness)
SBool (n <=? m)
SFalse ->
SNat m -> m :~: m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (m :~: m) -> Reason (:~:) m m -> m :~: m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m -> (m :~: m) -> Reason (:~:) m m
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m (SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)
(m :~: m) -> Reason (:~:) m (Min m n) -> m :~: Min m n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat n -> SNat (Min m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n SNat (Min m n) -> (m :~: Min m n) -> Reason (:~:) m (Min m n)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (Min m n :~: m) -> m :~: Min m n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (m <=? n) -> Min m n :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat m
m SNat n
n (IsTrue (m <=? n) -> Min m n :~: m)
-> IsTrue (m <=? n) -> Min m n :~: m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)
minLeqL :: SNat n -> SNat m -> IsTrue (Min n m <=? n)
minLeqL :: SNat n -> SNat m -> IsTrue (Min n m <=? n)
minLeqL SNat n
n SNat m
m =
case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
SBool (n <=? m)
STrue -> SNat n -> SNat n -> (n :~: n) -> IsTrue (n <=? n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) SNat n
n ((n :~: n) -> IsTrue (n <=? n)) -> (n :~: n) -> IsTrue (n <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
SBool (n <=? m)
SFalse ->
let mLEQn :: IsTrue (m <=? n)
mLEQn = SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m
in SNat m
-> SNat m
-> SNat n
-> IsTrue (m <=? m)
-> IsTrue (m <=? n)
-> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
(SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
SNat m
m
SNat n
n
(SNat m -> SNat m -> (m :~: m) -> IsTrue (m <=? m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) SNat m
m (SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn))
(IsTrue (m <=? n) -> IsTrue (m <=? n))
-> IsTrue (m <=? n) -> IsTrue (m <=? n)
forall a b. (a -> b) -> a -> b
$ IsTrue (m <=? n)
mLEQn
minLeqR :: SNat n -> SNat m -> IsTrue (Min n m <=? m)
minLeqR :: SNat n -> SNat m -> IsTrue (Min n m <=? m)
minLeqR SNat n
n SNat m
m =
SNat (Min n m)
-> SNat (MinAux (m <=? n) m n)
-> SNat m
-> IsTrue (Min n m <=? MinAux (m <=? n) m n)
-> IsTrue (MinAux (m <=? n) m n <=? m)
-> IsTrue (Min n m <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
(SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
(SNat m -> SNat n -> SNat (MinAux (m <=? n) m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n)
SNat m
m
(SNat (Min n m)
-> SNat (MinAux (m <=? n) m n)
-> (Min n m :~: MinAux (m <=? n) m n)
-> IsTrue (Min n m <=? MinAux (m <=? n) m n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (SNat m -> SNat n -> SNat (MinAux (m <=? n) m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n) ((Min n m :~: MinAux (m <=? n) m n)
-> IsTrue (Min n m <=? MinAux (m <=? n) m n))
-> (Min n m :~: MinAux (m <=? n) m n)
-> IsTrue (Min n m <=? MinAux (m <=? n) m n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> Min n m :~: MinAux (m <=? n) m n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Min n m :~: Min m n
minComm SNat n
n SNat m
m)
(SNat m -> SNat n -> IsTrue (MinAux (m <=? n) m n <=? m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (Min n m <=? n)
minLeqL SNat m
m SNat n
n)
minLargest ::
SNat l ->
SNat n ->
SNat m ->
IsTrue (l <=? n) ->
IsTrue (l <=? m) ->
IsTrue (l <=? Min n m)
minLargest :: SNat l
-> SNat n
-> SNat m
-> IsTrue (l <=? n)
-> IsTrue (l <=? m)
-> IsTrue (l <=? Min n m)
minLargest SNat l
l SNat n
n SNat m
m IsTrue (l <=? n)
lLEQn IsTrue (l <=? m)
lLEQm =
SNat l
-> (KnownNat l => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat l
l ((KnownNat l => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m))
-> (KnownNat l => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall a b. (a -> b) -> a -> b
$
SNat n
-> (KnownNat n => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m))
-> (KnownNat n => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall a b. (a -> b) -> a -> b
$
SNat m
-> (KnownNat m => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat m
m ((KnownNat m => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m))
-> (KnownNat m => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall a b. (a -> b) -> a -> b
$
SNat (Min n m)
-> (KnownNat (Min n m) => IsTrue (l <=? Min n m))
-> IsTrue (l <=? Min n m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) ((KnownNat (Min n m) => IsTrue (l <=? Min n m))
-> IsTrue (l <=? Min n m))
-> (KnownNat (Min n m) => IsTrue (l <=? Min n m))
-> IsTrue (l <=? Min n m)
forall a b. (a -> b) -> a -> b
$
case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
SBool (n <=? m)
STrue -> IsTrue (l <=? n)
IsTrue (l <=? Min n m)
lLEQn
SBool (n <=? m)
SFalse -> IsTrue (l <=? m)
IsTrue (l <=? Min n m)
lLEQm
leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm =
SNat (Max n m)
-> SNat m
-> IsTrue (Max n m <=? m)
-> IsTrue (m <=? Max n m)
-> Max n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) SNat m
m (SNat m
-> SNat n
-> SNat m
-> IsTrue (n <=? m)
-> IsTrue (m <=? m)
-> IsTrue (Max n m <=? m)
forall (l :: Nat) (n :: Nat) (m :: Nat).
SNat l
-> SNat n
-> SNat m
-> IsTrue (n <=? l)
-> IsTrue (m <=? l)
-> IsTrue (Max n m <=? l)
maxLeast SNat m
m SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm (SNat m -> IsTrue (m <=? m)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat m
m)) (SNat n -> SNat m -> IsTrue (m <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR SNat n
n SNat m
m)
geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn =
SNat (Max n m)
-> SNat n
-> IsTrue (Max n m <=? n)
-> IsTrue (n <=? Max n m)
-> Max n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) SNat n
n (SNat n
-> SNat n
-> SNat m
-> IsTrue (n <=? n)
-> IsTrue (m <=? n)
-> IsTrue (Max n m <=? n)
forall (l :: Nat) (n :: Nat) (m :: Nat).
SNat l
-> SNat n
-> SNat m
-> IsTrue (n <=? l)
-> IsTrue (m <=? l)
-> IsTrue (Max n m <=? l)
maxLeast SNat n
n SNat n
n SNat m
m (SNat n -> IsTrue (n <=? n)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
n) IsTrue (m <=? n)
mLEQn) (SNat n -> SNat m -> IsTrue (n <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? Max n m)
maxLeqL SNat n
n SNat m
m)
maxComm :: SNat n -> SNat m -> Max n m :~: Max m n
maxComm :: SNat n -> SNat m -> Max n m :~: Max m n
maxComm SNat n
n SNat m
m =
case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
SBool (n <=? m)
STrue ->
SNat (Max n m) -> Max n m :~: Max n m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) (Max n m :~: Max n m) -> Reason (:~:) (Max n m) m -> Max n m :~: m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m -> (Max n m :~: m) -> Reason (:~:) (Max n m) m
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
(Max n m :~: m) -> Reason (:~:) m m -> Max n m :~: m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat n -> SNat (Max m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n SNat m -> (m :~: m) -> Reason (:~:) m m
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (m :~: m) -> m :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (n <=? m) -> Max m n :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat m
m SNat n
n IsTrue (n <=? m)
IsTrue 'True
Witness)
SBool (n <=? m)
SFalse ->
SNat (Max n m) -> Max n m :~: Max n m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) (Max n m :~: Max n m) -> Reason (:~:) (Max n m) n -> Max n m :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> (Max n m :~: n) -> Reason (:~:) (Max n m) n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat m
m (SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)
(Max n m :~: n) -> Reason (:~:) n n -> Max n m :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat n -> SNat (Max m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n SNat n -> (n :~: n) -> Reason (:~:) n n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (n :~: n) -> n :~: n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (m <=? n) -> Max m n :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat m
m SNat n
n (IsTrue (m <=? n) -> Max m n :~: n)
-> IsTrue (m <=? n) -> Max m n :~: n
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)
maxLeqR :: SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR :: SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR SNat n
n SNat m
m =
case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
SBool (n <=? m)
STrue -> SNat m
-> SNat (Max n m) -> (m :~: Max n m) -> IsTrue (m <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat m
m (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((m :~: Max n m) -> IsTrue (m <=? Max n m))
-> (m :~: Max n m) -> IsTrue (m <=? Max n m)
forall a b. (a -> b) -> a -> b
$ (Max n m :~: m) -> m :~: Max n m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((Max n m :~: m) -> m :~: Max n m)
-> (Max n m :~: m) -> m :~: Max n m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
SBool (n <=? m)
SFalse ->
let mLEQn :: IsTrue (m <=? n)
mLEQn = SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m
in SNat m
-> SNat n
-> SNat (Max n m)
-> IsTrue (m <=? n)
-> IsTrue (n <=? Max n m)
-> IsTrue (m <=? Max n m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
SNat m
m
SNat n
n
(SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m)
IsTrue (m <=? n)
mLEQn
(SNat n
-> SNat (Max n m) -> (n :~: Max n m) -> IsTrue (n <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat n
n (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((Max n m :~: n) -> n :~: Max n m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((Max n m :~: n) -> n :~: Max n m)
-> (Max n m :~: n) -> n :~: Max n m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn))
maxLeqL :: SNat n -> SNat m -> IsTrue (n <=? Max n m)
maxLeqL :: SNat n -> SNat m -> IsTrue (n <=? Max n m)
maxLeqL SNat n
n SNat m
m =
SNat n
-> SNat (MaxAux (n <=? m) m n)
-> SNat (Max n m)
-> IsTrue (n <=? MaxAux (n <=? m) m n)
-> IsTrue (MaxAux (n <=? m) m n <=? Max n m)
-> IsTrue (n <=? Max n m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
SNat n
n
(SNat m -> SNat n -> SNat (MaxAux (n <=? m) m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n)
(SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m)
(SNat m -> SNat n -> IsTrue (n <=? MaxAux (n <=? m) m n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR SNat m
m SNat n
n)
(SNat (MaxAux (n <=? m) m n)
-> SNat (Max n m)
-> (MaxAux (n <=? m) m n :~: Max n m)
-> IsTrue (MaxAux (n <=? m) m n <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat m -> SNat n -> SNat (MaxAux (n <=? m) m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n) (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((MaxAux (n <=? m) m n :~: Max n m)
-> IsTrue (MaxAux (n <=? m) m n <=? Max n m))
-> (MaxAux (n <=? m) m n :~: Max n m)
-> IsTrue (MaxAux (n <=? m) m n <=? Max n m)
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat n -> MaxAux (n <=? m) m n :~: Max n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Max n m :~: Max m n
maxComm SNat m
m SNat n
n)
maxLeast ::
SNat l ->
SNat n ->
SNat m ->
IsTrue (n <=? l) ->
IsTrue (m <=? l) ->
IsTrue (Max n m <=? l)
maxLeast :: SNat l
-> SNat n
-> SNat m
-> IsTrue (n <=? l)
-> IsTrue (m <=? l)
-> IsTrue (Max n m <=? l)
maxLeast SNat l
l SNat n
n SNat m
m IsTrue (n <=? l)
lLEQn IsTrue (m <=? l)
lLEQm =
SNat l
-> (KnownNat l => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat l
l ((KnownNat l => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l))
-> (KnownNat l => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall a b. (a -> b) -> a -> b
$
SNat n
-> (KnownNat n => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l))
-> (KnownNat n => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall a b. (a -> b) -> a -> b
$
SNat m
-> (KnownNat m => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat m
m ((KnownNat m => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l))
-> (KnownNat m => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall a b. (a -> b) -> a -> b
$
SNat (Max n m)
-> (KnownNat (Max n m) => IsTrue (Max n m <=? l))
-> IsTrue (Max n m <=? l)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((KnownNat (Max n m) => IsTrue (Max n m <=? l))
-> IsTrue (Max n m <=? l))
-> (KnownNat (Max n m) => IsTrue (Max n m <=? l))
-> IsTrue (Max n m <=? l)
forall a b. (a -> b) -> a -> b
$
case SNat n
n SNat n -> SNat m -> SBool (n >=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >=? m)
%>=? SNat m
m of
SBool (n >=? m)
STrue -> IsTrue (n <=? l)
IsTrue (Max n m <=? l)
lLEQn
SBool (n >=? m)
SFalse -> IsTrue (m <=? l)
IsTrue (Max n m <=? l)
lLEQm
lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (Succ n <= m)
lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
_ SNat m
_ = (n < m) :~: (n < m)
forall k (a :: k). a :~: a
Refl
lneqReversed :: SNat n -> SNat m -> (n < m) :~: (m > n)
lneqReversed :: SNat n -> SNat m -> (n < m) :~: (n < m)
lneqReversed SNat n
_ SNat m
_ = (n < m) :~: (n < m)
forall k (a :: k). a :~: a
Refl
lneqToLT ::
SNat n ->
SNat m ->
IsTrue (n <? m) ->
CmpNat n m :~: 'LT
lneqToLT :: SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
lneqToLT SNat n
n SNat m
m IsTrue (n <? m)
nLNEm =
SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT SNat n
n SNat m
m (IsTrue (n <? m) -> CmpNat n m :~: 'LT)
-> IsTrue (n <? m) -> CmpNat n m :~: 'LT
forall a b. (a -> b) -> a -> b
$ (((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) IsTrue (n <? m)
(((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m)
nLNEm
ltToLneq ::
SNat n ->
SNat m ->
CmpNat n m :~: 'LT ->
IsTrue (n <? m)
ltToLneq :: SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
ltToLneq SNat n
n SNat m
m CmpNat n m :~: 'LT
nLTm =
(((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> (((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) (((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat n
n SNat m
m CmpNat n m :~: 'LT
nLTm
lneqZero :: SNat a -> IsTrue (0 <? Succ a)
lneqZero :: SNat a -> IsTrue (0 <? Succ a)
lneqZero SNat a
n = SNat 0
-> SNat (Succ a)
-> (CmpNat 0 (Succ a) :~: 'LT)
-> IsTrue (0 <? Succ a)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToLneq SNat 0
sZero (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
n) ((CmpNat 0 (Succ a) :~: 'LT) -> IsTrue (0 <? Succ a))
-> (CmpNat 0 (Succ a) :~: 'LT) -> IsTrue (0 <? Succ a)
forall a b. (a -> b) -> a -> b
$ SNat a -> CmpNat 0 (Succ a) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat a
n
lneqSucc :: SNat n -> IsTrue (n <? Succ n)
lneqSucc :: SNat n -> IsTrue (n <? Succ n)
lneqSucc SNat n
n = SNat n
-> SNat (Succ n)
-> (CmpNat n (Succ n) :~: 'LT)
-> IsTrue (n <? Succ n)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToLneq SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) ((CmpNat n (Succ n) :~: 'LT) -> IsTrue (n <? Succ n))
-> (CmpNat n (Succ n) :~: 'LT) -> IsTrue (n <? Succ n)
forall a b. (a -> b) -> a -> b
$ SNat n -> CmpNat n (Succ n) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc SNat n
n
succLneqSucc ::
SNat n ->
SNat m ->
(n <? m) :~: (Succ n <? Succ m)
succLneqSucc :: SNat n -> SNat m -> (n <? m) :~: (Succ n <? Succ m)
succLneqSucc SNat n
_ SNat m
_ = (n <? m) :~: (Succ n <? Succ m)
forall k (a :: k). a :~: a
Refl
lneqRightPredSucc ::
SNat n ->
SNat m ->
IsTrue (n <? m) ->
m :~: Succ (Pred m)
lneqRightPredSucc :: SNat n -> SNat m -> IsTrue (n <? m) -> m :~: Succ (Pred m)
lneqRightPredSucc SNat n
n SNat m
m IsTrue (n <? m)
nLNEQm = SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> m :~: Succ (Pred m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
ltRightPredSucc SNat n
n SNat m
m ((CmpNat n m :~: 'LT) -> m :~: Succ (Pred m))
-> (CmpNat n m :~: 'LT) -> m :~: Succ (Pred m)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
lneqToLT SNat n
n SNat m
m IsTrue (n <? m)
nLNEQm
lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
lneqSuccStepL SNat n
n SNat m
m IsTrue (Succ n <? m)
snLNEQm =
(((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> (((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) (((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall a b. (a -> b) -> a -> b
$
SNat (Succ n) -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (IsTrue (Succ n <? m) -> IsTrue (n <? m))
-> IsTrue (Succ n <? m) -> IsTrue (n <? m)
forall a b. (a -> b) -> a -> b
$
(((Succ n <? m) ~ 'True) :~: ((Succ n <? m) ~ 'True))
-> ((((Succ n <? m) ~ 'True) ~ ((Succ n <? m) ~ 'True)) =>
IsTrue (Succ n <? m))
-> IsTrue (Succ n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat (Succ n)
-> SNat m -> ((Succ n <? m) ~ 'True) :~: ((Succ n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m) IsTrue (Succ n <? m)
(((Succ n <? m) ~ 'True) ~ ((Succ n <? m) ~ 'True)) =>
IsTrue (Succ n <? m)
snLNEQm
lneqSuccStepR :: SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)
lneqSuccStepR :: SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)
lneqSuccStepR SNat n
n SNat m
m IsTrue (n <? m)
nLNEQm =
(((n <? Succ m) ~ 'True) :~: ((n <? Succ m) ~ 'True))
-> ((((n <? Succ m) ~ 'True) ~ ((n <? Succ m) ~ 'True)) =>
IsTrue (n <? Succ m))
-> IsTrue (n <? Succ m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((((n <? Succ m) ~ 'True) :~: ((n <? Succ m) ~ 'True))
-> ((n <? Succ m) ~ 'True) :~: ((n <? Succ m) ~ 'True)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((n <? Succ m) ~ 'True) :~: ((n <? Succ m) ~ 'True))
-> ((n <? Succ m) ~ 'True) :~: ((n <? Succ m) ~ 'True))
-> (((n <? Succ m) ~ 'True) :~: ((n <? Succ m) ~ 'True))
-> ((n <? Succ m) ~ 'True) :~: ((n <? Succ m) ~ 'True)
forall a b. (a -> b) -> a -> b
$ SNat n
-> SNat (Succ m)
-> ((n <? Succ m) ~ 'True) :~: ((n <? Succ m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m)) (((((n <? Succ m) ~ 'True) ~ ((n <? Succ m) ~ 'True)) =>
IsTrue (n <? Succ m))
-> IsTrue (n <? Succ m))
-> ((((n <? Succ m) ~ 'True) ~ ((n <? Succ m) ~ 'True)) =>
IsTrue (n <? Succ m))
-> IsTrue (n <? Succ m)
forall a b. (a -> b) -> a -> b
$
SNat (n + 1) -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR (SNat n -> SNat (n + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (IsTrue (n <? m) -> IsTrue (n <? Succ m))
-> IsTrue (n <? m) -> IsTrue (n <? Succ m)
forall a b. (a -> b) -> a -> b
$
(((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) IsTrue (n <? m)
(((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m)
nLNEQm
plusStrictMonotone ::
SNat n ->
SNat m ->
SNat l ->
SNat k ->
IsTrue (n <? m) ->
IsTrue (l <? k) ->
IsTrue ((n + l) <? (m + k))
plusStrictMonotone :: SNat n
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <? m)
-> IsTrue (l <? k)
-> IsTrue ((n + l) <? (m + k))
plusStrictMonotone SNat n
n SNat m
m SNat l
l SNat k
k IsTrue (n <? m)
nLNm IsTrue (l <? k)
lLNk =
((((n + l) <? (m + k)) ~ 'True) :~: (((n + l) <? (m + k)) ~ 'True))
-> (((((n + l) <? (m + k)) ~ 'True)
~ (((n + l) <? (m + k)) ~ 'True)) =>
IsTrue ((n + l) <? (m + k)))
-> IsTrue ((n + l) <? (m + k))
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (((((n + l) <? (m + k)) ~ 'True) :~: (((n + l) <? (m + k)) ~ 'True))
-> (((n + l) <? (m + k)) ~ 'True)
:~: (((n + l) <? (m + k)) ~ 'True)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((((n + l) <? (m + k)) ~ 'True)
:~: (((n + l) <? (m + k)) ~ 'True))
-> (((n + l) <? (m + k)) ~ 'True)
:~: (((n + l) <? (m + k)) ~ 'True))
-> ((((n + l) <? (m + k)) ~ 'True)
:~: (((n + l) <? (m + k)) ~ 'True))
-> (((n + l) <? (m + k)) ~ 'True)
:~: (((n + l) <? (m + k)) ~ 'True)
forall a b. (a -> b) -> a -> b
$ SNat (n + l)
-> SNat (m + k)
-> (((n + l) <? (m + k)) ~ 'True)
:~: (((n + l) <? (m + k)) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) (SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k)) ((((((n + l) <? (m + k)) ~ 'True)
~ (((n + l) <? (m + k)) ~ 'True)) =>
IsTrue ((n + l) <? (m + k)))
-> IsTrue ((n + l) <? (m + k)))
-> (((((n + l) <? (m + k)) ~ 'True)
~ (((n + l) <? (m + k)) ~ 'True)) =>
IsTrue ((n + l) <? (m + k)))
-> IsTrue ((n + l) <? (m + k))
forall a b. (a -> b) -> a -> b
$
((((n + 1) + l) :~: ((n + l) + 1))
-> SNat (m + k)
-> IsTrue (((n + 1) + l) <=? (m + k))
-> IsTrue ((n + l) <? (m + k)))
-> SNat (m + k)
-> (((n + 1) + l) :~: ((n + l) + 1))
-> IsTrue (((n + 1) + l) <=? (m + k))
-> IsTrue ((n + l) <? (m + k))
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((n + 1) + l) :~: ((n + l) + 1))
-> SNat (m + k)
-> IsTrue (((n + 1) + l) <=? (m + k))
-> IsTrue ((n + l) <? (m + k))
forall (n :: Nat) (m :: Nat) (l :: Nat).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL (SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k) (SNat n -> SNat l -> ((n + 1) + l) :~: ((n + l) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat l
l) (IsTrue (((n + 1) + l) <=? (m + k)) -> IsTrue ((n + l) <? (m + k)))
-> IsTrue (((n + 1) + l) <=? (m + k))
-> IsTrue ((n + l) <? (m + k))
forall a b. (a -> b) -> a -> b
$
SNat (n + 1)
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <? m)
-> IsTrue (l <=? k)
-> IsTrue (((n + 1) + l) <=? (m + k))
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))
plusMonotone
(SNat n -> SNat (n + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)
SNat m
m
SNat l
l
SNat k
k
((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) IsTrue (n <? m)
(((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m)
nLNm)
( SNat l
-> SNat (l + 1)
-> SNat k
-> IsTrue (l <=? (l + 1))
-> IsTrue (l <? k)
-> IsTrue (l <=? k)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans SNat l
l (SNat l -> SNat (l + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat l
l) SNat k
k (SNat l -> SNat l -> IsTrue (l <=? l) -> IsTrue (l <=? (l + 1))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR SNat l
l SNat l
l (SNat l -> IsTrue (l <=? l)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat l
l)) (IsTrue (l <? k) -> IsTrue (l <=? k))
-> IsTrue (l <? k) -> IsTrue (l <=? k)
forall a b. (a -> b) -> a -> b
$
(((l <? k) ~ 'True) :~: ((l <? k) ~ 'True))
-> ((((l <? k) ~ 'True) ~ ((l <? k) ~ 'True)) => IsTrue (l <? k))
-> IsTrue (l <? k)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat l -> SNat k -> ((l <? k) ~ 'True) :~: ((l <? k) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat l
l SNat k
k) IsTrue (l <? k)
(((l <? k) ~ 'True) ~ ((l <? k) ~ 'True)) => IsTrue (l <? k)
lLNk
)
maxZeroL :: SNat n -> Max 0 n :~: n
maxZeroL :: SNat n -> Max 0 n :~: n
maxZeroL SNat n
n = SNat 0 -> SNat n -> IsTrue (0 <=? n) -> Max 0 n :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat 0
sZero SNat n
n (SNat n -> IsTrue (0 <=? n)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)
maxZeroR :: SNat n -> Max n 0 :~: n
maxZeroR :: SNat n -> Max n 0 :~: n
maxZeroR SNat n
n = SNat n -> SNat 0 -> IsTrue (0 <=? n) -> Max n 0 :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat 0
sZero (SNat n -> IsTrue (0 <=? n)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)
minZeroL :: SNat n -> Min 0 n :~: 0
minZeroL :: SNat n -> Min 0 n :~: 0
minZeroL SNat n
n = SNat 0 -> SNat n -> IsTrue (0 <=? n) -> Min 0 n :~: 0
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat 0
sZero SNat n
n (SNat n -> IsTrue (0 <=? n)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)
minZeroR :: SNat n -> Min n 0 :~: 0
minZeroR :: SNat n -> Min n 0 :~: 0
minZeroR SNat n
n = SNat n -> SNat 0 -> IsTrue (0 <=? n) -> Min n 0 :~: 0
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat 0
sZero (SNat n -> IsTrue (0 <=? n)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)
minusSucc :: SNat n -> SNat m -> IsTrue (m <=? n) -> Succ n - m :~: Succ (n - m)
minusSucc :: SNat n
-> SNat m -> IsTrue (m <=? n) -> (Succ n - m) :~: Succ (n - m)
minusSucc SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn =
case SNat m -> SNat n -> IsTrue (m <=? n) -> DiffNat m n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat m
m SNat n
n IsTrue (m <=? n)
mLEQn of
DiffNat SNat m
_ SNat m
k ->
SNat (Succ n - m) -> (Succ n - m) :~: (Succ n - m)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat m -> SNat (Succ n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
((Succ n - m) :~: (Succ n - m))
-> SNat (Succ n - m) -> (Succ n - m) :~: (Succ n - m)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ n) -> SNat m -> SNat (Succ n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m
((Succ n - m) :~: (Succ n - m))
-> Reason (:~:) (Succ n - m) ((m + (m + 1)) - m)
-> (Succ n - m) :~: ((m + (m + 1)) - m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== (SNat m
m SNat m -> SNat (m + 1) -> SNat (m + (m + 1))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) SNat (m + (m + 1)) -> SNat m -> SNat ((m + (m + 1)) - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat ((m + (m + 1)) - m)
-> ((Succ n - m) :~: ((m + (m + 1)) - m))
-> Reason (:~:) (Succ n - m) ((m + (m + 1)) - m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (Succ n :~: (m + (m + 1)))
-> SNat m -> (Succ n - m) :~: ((m + (m + 1)) - m)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (((m + (m + 1)) :~: Succ n) -> Succ n :~: (m + (m + 1))
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((m + (m + 1)) :~: Succ n) -> Succ n :~: (m + (m + 1)))
-> ((m + (m + 1)) :~: Succ n) -> Succ n :~: (m + (m + 1))
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat m -> (m + (m + 1)) :~: S (m + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat m
m SNat m
k) SNat m
m
((Succ n - m) :~: ((m + (m + 1)) - m))
-> Reason (:~:) ((m + (m + 1)) - m) (((m + 1) + m) - m)
-> (Succ n - m) :~: (((m + 1) + m) - m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k SNat (m + 1) -> SNat m -> SNat ((m + 1) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) SNat ((m + 1) + m) -> SNat m -> SNat (((m + 1) + m) - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (((m + 1) + m) - m)
-> (((m + (m + 1)) - m) :~: (((m + 1) + m) - m))
-> Reason (:~:) ((m + (m + 1)) - m) (((m + 1) + m) - m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ((m + (m + 1)) :~: ((m + 1) + m))
-> SNat m -> ((m + (m + 1)) - m) :~: (((m + 1) + m) - m)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat (m + 1) -> (m + (m + 1)) :~: ((m + 1) + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k)) SNat m
m
((Succ n - m) :~: (((m + 1) + m) - m))
-> Reason (:~:) (((m + 1) + m) - m) (m + 1)
-> (Succ n - m) :~: (m + 1)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k SNat (m + 1)
-> ((((m + 1) + m) - m) :~: (m + 1))
-> Reason (:~:) (((m + 1) + m) - m) (m + 1)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat (m + 1) -> SNat m -> (((m + 1) + m) - m) :~: (m + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) SNat m
m
((Succ n - m) :~: (m + 1))
-> Reason (:~:) (m + 1) (((m + m) - m) + 1)
-> (Succ n - m) :~: (((m + m) - m) + 1)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat ((m + m) - m) -> SNat (((m + m) - m) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m
k SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (m + m) -> SNat m -> SNat ((m + m) - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m) SNat (((m + m) - m) + 1)
-> ((m + 1) :~: (((m + m) - m) + 1))
-> Reason (:~:) (m + 1) (((m + m) - m) + 1)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (m :~: ((m + m) - m)) -> (m + 1) :~: (((m + m) - m) + 1)
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong ((((m + m) - m) :~: m) -> m :~: ((m + m) - m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((m + m) - m) :~: m) -> m :~: ((m + m) - m))
-> (((m + m) - m) :~: m) -> m :~: ((m + m) - m)
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat m -> ((m + m) - m) :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus SNat m
k SNat m
m)
((Succ n - m) :~: (((m + m) - m) + 1))
-> Reason (:~:) (((m + m) - m) + 1) (Succ (n - m))
-> (Succ n - m) :~: Succ (n - m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat (n - m) -> SNat (Succ (n - m))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m) SNat (Succ (n - m))
-> ((((m + m) - m) + 1) :~: Succ (n - m))
-> Reason (:~:) (((m + m) - m) + 1) (Succ (n - m))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (((m + m) - m) :~: (n - m)) -> (((m + m) - m) + 1) :~: Succ (n - m)
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong (((m + m) :~: n) -> SNat m -> ((m + m) - m) :~: (n - m)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
k SNat m
m) SNat m
m)
((Succ n - m) :~: Succ (n - m))
-> SNat (Succ (n - m)) -> (Succ n - m) :~: Succ (n - m)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat (n - m) -> SNat (Succ (n - m))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
lneqZeroAbsurd :: SNat n -> IsTrue (n <? 0) -> Void
lneqZeroAbsurd :: SNat n -> IsTrue (n <? 0) -> Void
lneqZeroAbsurd SNat n
n IsTrue (n <? 0)
leq =
SNat n -> IsTrue (n <? 0) -> Void
forall (n :: Nat). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n
n ((((n <? 0) ~ 'True) :~: ((n <? 0) ~ 'True))
-> ((((n <? 0) ~ 'True) ~ ((n <? 0) ~ 'True)) => IsTrue (n <? 0))
-> IsTrue (n <? 0)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat 0 -> ((n <? 0) ~ 'True) :~: ((n <? 0) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat 0
sZero) IsTrue (n <? 0)
(((n <? 0) ~ 'True) ~ ((n <? 0) ~ 'True)) => IsTrue (n <? 0)
leq)
minusPlus ::
forall n m.
SNat n ->
SNat m ->
IsTrue (m <=? n) ->
n - m + m :~: n
minusPlus :: SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn =
case SNat m -> SNat n -> IsTrue (m <=? n) -> DiffNat m n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat m
m SNat n
n IsTrue (m <=? n)
mLEQn of
DiffNat SNat m
_ SNat m
k ->
SNat ((n - m) + m) -> ((n - m) + m) :~: ((n - m) + m)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m)
(((n - m) + m) :~: ((n - m) + m))
-> SNat ((n - m) + m) -> ((n - m) + m) :~: ((n - m) + m)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m
(((n - m) + m) :~: ((n - m) + m))
-> Reason (:~:) ((n - m) + m) (((m + m) - m) + m)
-> ((n - m) + m) :~: (((m + m) - m) + m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
k SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (m + m) -> SNat m -> SNat ((m + m) - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat ((m + m) - m) -> SNat m -> SNat (((m + m) - m) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (((m + m) - m) + m)
-> (((n - m) + m) :~: (((m + m) - m) + m))
-> Reason (:~:) ((n - m) + m) (((m + m) - m) + m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ((n - m) :~: ((m + m) - m))
-> SNat m -> ((n - m) + m) :~: (((m + m) - m) + m)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL ((n :~: (m + m)) -> SNat m -> (n - m) :~: ((m + m) - m)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m SNat m
k) SNat m
m) SNat m
m
(((n - m) + m) :~: (((m + m) - m) + m))
-> Reason (:~:) (((m + m) - m) + m) (m + m)
-> ((n - m) + m) :~: (m + m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
k SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (m + m)
-> ((((m + m) - m) + m) :~: (m + m))
-> Reason (:~:) (((m + m) - m) + m) (m + m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (((m + m) - m) :~: m) -> SNat m -> (((m + m) - m) + m) :~: (m + m)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL (SNat m -> SNat m -> ((m + m) - m) :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus SNat m
k SNat m
m) SNat m
m
(((n - m) + m) :~: (m + m))
-> Reason (:~:) (m + m) n -> ((n - m) + m) :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat n -> ((m + m) :~: n) -> Reason (:~:) (m + m) n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
k SNat m
m
(((n - m) + m) :~: n) -> SNat n -> ((n - m) + m) :~: n
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n
n
type n -. m = Subt n m (m <=? n)
type family Subt n m (b :: Bool) where
Subt n m 'True = n - m
Subt n m 'False = 0
infixl 6 -.
(%-.) :: SNat n -> SNat m -> SNat (n -. m)
SNat n
n %-. :: SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m =
case SNat m
m SNat m -> SNat n -> SBool (m <=? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
SBool (m <=? n)
STrue -> SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m
SBool (m <=? n)
SFalse -> SNat 0
SNat (n -. m)
sZero
minPlusTruncMinus ::
SNat n ->
SNat m ->
Min n m + (n -. m) :~: n
minPlusTruncMinus :: SNat n -> SNat m -> (Min n m + (n -. m)) :~: n
minPlusTruncMinus SNat n
n SNat m
m =
case SNat m
m SNat m -> SNat n -> SBool (m <=? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
SBool (m <=? n)
STrue ->
SNat (Min n m + (n - m))
-> (Min n m + (n - m)) :~: (Min n m + (n - m))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (Min n m) -> SNat (n - m) -> SNat (Min n m + (n - m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m))
((Min n m + (n - m)) :~: (Min n m + (n - m)))
-> Reason (:~:) (Min n m + (n - m)) (m + (n - m))
-> (Min n m + (n - m)) :~: (m + (n - m))
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m -> SNat (n - m) -> SNat (m + (n - m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m) SNat (m + (n - m))
-> ((Min n m + (n - m)) :~: (m + (n - m)))
-> Reason (:~:) (Min n m + (n - m)) (m + (n - m))
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (Min n m :~: m)
-> SNat (n - m) -> (Min n m + (n - m)) :~: (m + (n - m))
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL (SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m IsTrue (m <=? n)
IsTrue 'True
Witness) (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m)
((Min n m + (n - m)) :~: (m + (n - m)))
-> SNat (m + (n - m)) -> (Min n m + (n - m)) :~: (m + (n - m))
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m SNat m -> SNat (n - m) -> SNat (m + (n - m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
((Min n m + (n - m)) :~: (m + (n - m)))
-> Reason (:~:) (m + (n - m)) ((n - m) + m)
-> (Min n m + (n - m)) :~: ((n - m) + m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m) SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat ((n - m) + m)
-> ((m + (n - m)) :~: ((n - m) + m))
-> Reason (:~:) (m + (n - m)) ((n - m) + m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat m -> SNat (n - m) -> (m + (n - m)) :~: ((n - m) + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
((Min n m + (n - m)) :~: ((n - m) + m))
-> Reason (:~:) ((n - m) + m) n -> (Min n m + (n - m)) :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> (((n - m) + m) :~: n) -> Reason (:~:) ((n - m) + m) n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue (m <=? n)
IsTrue 'True
Witness
SBool (m <=? n)
SFalse ->
SNat (Min n m) -> Min n m :~: Min n m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (Min n m) -> SNat 0 -> SNat (Min n m + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m))
(Min n m :~: Min n m) -> SNat (Min n m) -> Min n m :~: Min n m
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
(proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (Min n m) -> SNat 0 -> SNat (Min n m + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero
(Min n m :~: Min n m)
-> Reason (:~:) (Min n m) (Min n m) -> Min n m :~: Min n m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (Min n m)
-> (Min n m :~: Min n m) -> Reason (:~:) (Min n m) (Min n m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat (Min n m) -> (Min n m + 0) :~: Min n m
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
(Min n m :~: Min n m) -> Reason (:~:) (Min n m) n -> Min n m :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> (Min n m :~: n) -> Reason (:~:) (Min n m) n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
(eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m (SNat m -> SNat n -> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat m
m SNat n
n)
truncMinusLeq :: SNat n -> SNat m -> IsTrue ((n -. m) <=? n)
truncMinusLeq :: SNat n -> SNat m -> IsTrue ((n -. m) <=? n)
truncMinusLeq SNat n
n SNat m
m =
case SNat m
m SNat m -> SNat n -> SBool (m <=? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
SBool (m <=? n)
STrue -> SNat (n - m)
-> SNat n
-> SNat m
-> (((n - m) + m) :~: n)
-> IsTrue ((n - m) <=? n)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m) SNat n
n SNat m
m ((((n - m) + m) :~: n) -> IsTrue ((n - m) <=? n))
-> (((n - m) + m) :~: n) -> IsTrue ((n - m) <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue (m <=? n)
IsTrue 'True
Witness
SBool (m <=? n)
SFalse -> SNat n -> IsTrue (0 <=? n)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n