{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-}
module Data.Type.Natural.Class.Order
(PeanoOrder(..), DiffNat(..), LeqView(..),
FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,
sLeqCongL, sLeqCongR, sLeqCong,
type (-.), (%-.), minPlusTruncMinus, truncMinusLeq,
module Data.Type.Natural.Singleton.Compat
) where
import Data.Type.Natural.Class.Arithmetic
import Data.Type.Natural.Singleton.Compat (type (<), type (<=), type (<=@#@$),
type (<=@#@$$), type (<=@#@$$$),
type (<@#@$), type (<@#@$$),
type (<@#@$$$), type (>), type (>=),
type (>=@#@$), type (>=@#@$$),
type (>=@#@$$$), type (>@#@$),
type (>@#@$$), type (>@#@$$$),
type Min, type Max, type Compare,
type MinSym0, type MinSym1, type MinSym2,
type MaxSym0, type MaxSym1, type MaxSym2,
type CompareSym0, type CompareSym1, type CompareSym2,
Sing (SLT, SEQ, SGT), SOrd(..), POrd(..),
LTSym0, GTSym0, EQSym0,
(%<), (%<=), (%>), (%>=))
import Data.Singletons.Prelude (Sing (SFalse, STrue), sing, withSingI)
import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ)
import Data.Singletons.TH (singletonsOnly)
import Data.Type.Equality ((:~:) (..))
import Data.Void (Void, absurd)
import Proof.Equational (because, coerce, start, sym, trans,
withRefl, (===), (=~=))
import Proof.Propositional (IsTrue (..), eliminate, withWitness)
data LeqView (n :: nat) (m :: nat) where
LeqZero :: Sing n -> LeqView (Zero nat) n
LeqSucc :: Sing n -> Sing m -> IsTrue (n <= m) -> LeqView (Succ n) (Succ m)
data DiffNat n m where
DiffNat :: Sing n -> Sing m -> DiffNat n (n + m)
newtype LeqWitPf n = LeqWitPf { leqWitPf :: forall m. Sing m -> IsTrue (n <= m) -> DiffNat n m }
newtype LeqStepPf n = LeqStepPf { leqStepPf :: forall m l. Sing m -> Sing l -> n + l :~: m -> IsTrue (n <= m) }
succDiffNat :: IsPeano nat
=> Sing n -> Sing m -> DiffNat (n :: nat) m -> DiffNat (Succ n) (Succ m)
succDiffNat _ _ (DiffNat n m) = coerce (plusSuccL n m) $ DiffNat (sSucc n) m
coerceLeqL :: forall (n :: nat) m l . IsPeano nat => n :~: m -> Sing l
-> IsTrue (n <= l) -> IsTrue (m <= l)
coerceLeqL Refl _ Witness = Witness
coerceLeqR :: forall (n :: nat) m l . IsPeano nat => Sing l -> n :~: m
-> IsTrue (l <= n) -> IsTrue (l <= m)
coerceLeqR _ Refl Witness = Witness
singletonsOnly [d|
flipOrdering :: Ordering -> Ordering
flipOrdering EQ = EQ
flipOrdering LT = GT
flipOrdering GT = LT
|]
congFlipOrdering :: a :~: b -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering Refl = Refl
compareCongR :: Sing (a :: k) -> b :~: c -> Compare a b :~: Compare a c
compareCongR _ Refl = Refl
sLeqCong :: a :~: b -> c :~: d -> (a <= c) :~: (b <= d)
sLeqCong Refl Refl = Refl
sLeqCongL :: a :~: b -> Sing c -> (a <= c) :~: (b <= c)
sLeqCongL Refl _ = Refl
sLeqCongR :: Sing a -> b :~: c -> (a <= b) :~: (a <= c)
sLeqCongR _ Refl = Refl
newtype LTSucc n = LTSucc { proofLTSucc :: Compare n (Succ n) :~: 'LT }
newtype CmpSuccStepR (n :: nat) =
CmpSuccStepR { proofCmpSuccStepR :: forall (m :: nat). Sing m
-> Compare n m :~: 'LT
-> Compare n (Succ m) :~: 'LT
}
newtype LeqViewRefl n = LeqViewRefl { proofLeqViewRefl :: LeqView n n }
class (SOrd nat, IsPeano nat) => PeanoOrder nat where
{-# MINIMAL ( succLeqToLT, cmpZero, leqRefl
| leqZero, leqSucc , viewLeq
| leqWitness, leqStep
),
eqlCmpEQ, ltToLeq, eqToRefl,
flipCompare, leqToCmp,
leqReversed, lneqSuccLeq, lneqReversed,
(leqToMin, geqToMin | minLeqL, minLeqR, minLargest),
(leqToMax, geqToMax | maxLeqL, maxLeqR, maxLeast) #-}
leqToCmp :: Sing (a :: nat) -> Sing b -> IsTrue (a <= b)
-> Either (a :~: b) (Compare a b :~: 'LT)
eqlCmpEQ :: Sing (a :: nat) -> Sing b -> a :~: b -> Compare a b :~: 'EQ
eqToRefl :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'EQ -> a :~: b
flipCompare :: Sing (a :: nat) -> Sing b
-> FlipOrdering (Compare a b) :~: Compare b a
ltToNeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT
-> a :~: b -> Void
ltToNeq a b aLTb aEQb = eliminate $
start SLT
=== sCompare a b `because` sym aLTb
=== SEQ `because` eqlCmpEQ a b aEQb
leqNeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (a <= b) -> (a :~: b -> Void) -> Compare a b :~: 'LT
leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb
succLeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: 'LT
succLeqToLT a b saLEQb =
case leqWitness (sSucc a) b saLEQb of
DiffNat _ k -> let aLEQb = leqStep a b (sSucc k) $
start (a %+ sSucc k)
=== sSucc (a %+ k) `because` plusSuccR a k
=== sSucc a %+ k `because` sym (plusSuccL a k)
=~= b
aNEQb aeqb = succNonCyclic k $ plusEqCancelL a (sSucc k) sZero $
start (a %+ sSucc k)
=== sSucc (a %+ k) `because` plusSuccR a k
=== sSucc a %+ k `because` sym (plusSuccL a k)
=~= b
=== a `because` sym aeqb
=== a %+ sZero `because` sym (plusZeroR a)
in leqNeqToLT a b aLEQb aNEQb
ltToLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT
-> IsTrue (a <= b)
gtToLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'GT
-> IsTrue (b <= a)
gtToLeq n m nGTm = ltToLeq m n $
start (sCompare m n) === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)
=== sFlipOrdering SGT `because` congFlipOrdering nGTm
=~= SLT
ltToSuccLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT
-> IsTrue (Succ a <= b)
ltToSuccLeq n m nLTm =
leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm)
cmpZero :: Sing a -> Compare (Zero nat) (Succ a) :~: 'LT
cmpZero sn = leqToLT sZero (sSucc sn) $ leqStep (sSucc sZero) (sSucc sn) sn $
start (sSucc sZero %+ sn)
=== sSucc (sZero %+ sn) `because` plusSuccL sZero sn
=== sSucc sn `because` succCong (plusZeroL sn)
leqToGT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ b <= a)
-> Compare a b :~: 'GT
leqToGT a b sbLEQa =
start (sCompare a b)
=== sFlipOrdering (sCompare b a) `because` sym (flipCompare b a)
=== sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa)
=~= SGT
cmpZero' :: Sing a -> Either (Compare (Zero nat) a :~: 'EQ) (Compare (Zero nat) a :~: 'LT)
cmpZero' n =
case zeroOrSucc n of
IsZero -> Left $ eqlCmpEQ sZero n Refl
IsSucc n' -> Right $ cmpZero n'
zeroNoLT :: Sing a -> Compare a (Zero nat) :~: 'LT -> Void
zeroNoLT n eql =
case cmpZero' n of
Left cmp0nEQ -> eliminate $
start SGT
=~= sFlipOrdering SLT
=== sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql)
=== sCompare sZero n `because` flipCompare n sZero
=== SEQ `because` cmp0nEQ
Right cmp0nLT -> eliminate $
start SGT
=~= sFlipOrdering SLT
=== sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql)
=== sCompare sZero n `because` flipCompare n sZero
=== SLT `because` cmp0nLT
ltRightPredSucc :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT -> b :~: Succ (Pred b)
ltRightPredSucc a b aLTb =
case zeroOrSucc b of
IsZero -> absurd $ zeroNoLT a aLTb
IsSucc b' -> sym $
start (sSucc (sPred b))
=~= sSucc (sPred (sSucc b'))
=== sSucc b' `because` succCong (predSucc b')
=~= b
cmpSucc :: Sing (n :: nat) -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)
cmpSucc n m =
case sCompare n m of
SEQ -> let nEQm = eqToRefl n m Refl
in sym $ eqlCmpEQ (sSucc n) (sSucc m) $ succCong nEQm
SLT -> case leqWitness (sSucc n) m $ ltToSuccLeq n m Refl of
DiffNat _ k ->
sym $ succLeqToLT (sSucc n) (sSucc m) $
leqStep (sSucc (sSucc n)) (sSucc m) k $
start (sSucc (sSucc n) %+ k)
=== sSucc (sSucc n %+ k) `because` plusSuccL (sSucc n) k
=~= sSucc m
SGT -> case leqWitness (sSucc m) n $ ltToSuccLeq m n (sym $ flipCompare n m) of
DiffNat _ k ->
let pf = (succLeqToLT (sSucc m) (sSucc n) $
leqStep (sSucc (sSucc m)) (sSucc n) k $
start (sSucc (sSucc m) %+ k)
=== sSucc (sSucc m %+ k) `because` plusSuccL (sSucc m) k
=~= sSucc n)
in start (sCompare n m)
=~= SGT
=~= sFlipOrdering SLT
=== sFlipOrdering (sCompare (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf)
=== sCompare (sSucc n) (sSucc m) `because` flipCompare (sSucc m) (sSucc n)
ltSucc :: Sing (a :: nat) -> Compare a (Succ a) :~: 'LT
ltSucc = proofLTSucc . induction base step
where
base :: LTSucc (Zero nat)
base = LTSucc $ cmpZero (sZero :: Sing (Zero nat))
step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n)
step n (LTSucc ih) = LTSucc $
start (sCompare (sSucc n) (sSucc (sSucc n)))
=== sCompare n (sSucc n) `because` sym (cmpSucc n (sSucc n))
=== SLT `because` ih
cmpSuccStepR :: Sing (n :: nat) -> Sing m -> Compare n m :~: 'LT
-> Compare n (Succ m) :~: 'LT
cmpSuccStepR = proofCmpSuccStepR . induction base step
where
base :: CmpSuccStepR (Zero nat)
base = CmpSuccStepR $ \m _ -> cmpZero m
step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n)
step n (CmpSuccStepR ih) = CmpSuccStepR $ \m snltm ->
case zeroOrSucc m of
IsZero -> absurd $ zeroNoLT (sSucc n) snltm
IsSucc m' ->
let nLTm' = trans (cmpSucc n m') snltm
in start (sCompare (sSucc n) (sSucc m))
=~= sCompare (sSucc n) (sSucc (sSucc m'))
=== sCompare n (sSucc m') `because` sym (cmpSucc n (sSucc m'))
=== SLT `because` ih m' nLTm'
ltSuccLToLT :: Sing (n :: nat) -> Sing m -> Compare (Succ n) m :~: 'LT
-> Compare n m :~: 'LT
ltSuccLToLT n m snLTm =
case zeroOrSucc m of
IsZero -> absurd $ zeroNoLT (sSucc n) snLTm
IsSucc m' ->
let nLTm = cmpSucc n m' `trans` snLTm
in start (sCompare n (sSucc m'))
=== SLT `because` cmpSuccStepR n m' nLTm
leqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ a <= b)
-> Compare a b :~: 'LT
leqToLT n m snLEQm =
case leqToCmp (sSucc n) m snLEQm of
Left eql -> withRefl eql $
start (sCompare n m)
=~= sCompare n (sSucc n)
=== SLT `because` ltSucc n
Right nLTm -> ltSuccLToLT n m nLTm
leqZero :: Sing n -> IsTrue (Zero nat <= n)
leqZero sn =
case zeroOrSucc sn of
IsZero -> leqRefl sn
IsSucc pn -> ltToLeq sZero sn $ cmpZero pn
leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m)
leqSucc n m nLEQm =
case leqToCmp n m nLEQm of
Left eql -> withRefl eql $ leqRefl (sSucc n)
Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm
fromLeqView :: LeqView (n :: nat) m -> IsTrue (n <= m)
fromLeqView (LeqZero n) = leqZero n
fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm
leqViewRefl :: Sing (n :: nat) -> LeqView n n
leqViewRefl = proofLeqViewRefl . induction base step
where
base :: LeqViewRefl (Zero nat)
base = LeqViewRefl $ LeqZero sZero
step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n)
step n (LeqViewRefl nLEQn) =
LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn)
viewLeq :: forall n m . Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> LeqView n m
viewLeq n m nLEQm =
case (zeroOrSucc n, leqToCmp n m nLEQm) of
(IsZero, _) -> LeqZero m
(_, Left Refl) -> leqViewRefl n
(IsSucc n', Right nLTm) ->
let sm'EQm = ltRightPredSucc n m nLTm
m' = sPred m
n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm
in coerce (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm'
leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> DiffNat n m
leqWitness = leqWitPf . induction base step
where
base :: LeqWitPf (Zero nat)
base = LeqWitPf $ \sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm
step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n)
step (n :: Sing n) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->
case viewLeq (sSucc n) m snLEQm of
LeqZero _ -> absurd $ succNonCyclic n Refl
LeqSucc (_ :: Sing n') pm nLEQpm ->
succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm
leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m -> IsTrue (n <= m)
leqStep = leqStepPf . induction base step
where
base :: LeqStepPf (Zero nat)
base = LeqStepPf $ \k _ _ -> leqZero k
step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n)
step n (LeqStepPf ih) =
LeqStepPf $ \k l snPlEqk ->
let kEQspk = start k
=== sSucc n %+ l `because` sym snPlEqk
=== sSucc (n %+ l) `because` plusSuccL n l
pk = n %+ l
in coerceLeqR (sSucc n) (sym kEQspk) $ leqSucc n pk $ ih pk l Refl
leqNeqToSuccLeq :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> (n :~: m -> Void) -> IsTrue (Succ n <= m)
leqNeqToSuccLeq n m nLEQm nNEQm =
case leqWitness n m nLEQm of
DiffNat _ k ->
case zeroOrSucc k of
IsZero -> absurd $ nNEQm $ sym $ plusZeroR n
IsSucc k' -> leqStep (sSucc n) m k' $
start (sSucc n %+ k')
=== sSucc (n %+ k') `because` plusSuccL n k'
=== n %+ sSucc k' `because` sym (plusSuccR n k')
=~= m
leqRefl :: Sing (n :: nat) -> IsTrue (n <= n)
leqRefl sn = leqStep sn sn sZero (plusZeroR sn)
leqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m)
leqSuccStepR n m nLEQm =
case leqWitness n m nLEQm of
DiffNat _ k -> leqStep n (sSucc m) (sSucc k) $
start (n %+ sSucc k) === sSucc (n %+ k) `because` plusSuccR n k =~= sSucc m
leqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m)
leqSuccStepL n m snLEQm =
leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm
leqReflexive :: Sing (n :: nat) -> Sing m -> n :~: m -> IsTrue (n <= m)
leqReflexive n _ Refl = leqRefl n
leqTrans :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l)
leqTrans n m k nLEm mLEk =
case leqWitness n m nLEm of
DiffNat _ mMn -> case leqWitness m k mLEk of
DiffNat _ kMn -> leqStep n k (mMn %+ kMn) (sym $ plusAssoc n mMn kMn)
leqAntisymm :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m
leqAntisymm n m nLEm mLEn =
case (leqWitness n m nLEm, leqWitness m n mLEn) of
(DiffNat _ mMn, DiffNat _ nMm) ->
let pEQ0 = plusEqCancelL n (mMn %+ nMm) sZero $
start (n %+ (mMn %+ nMm))
=== (n %+ mMn) %+ nMm
`because` sym (plusAssoc n mMn nMm)
=~= m %+ nMm
=~= n
=== n %+ sZero
`because` sym (plusZeroR n)
nMmEQ0 = plusEqZeroL mMn nMm pEQ0
in sym $ start m
=~= n %+ mMn
=== n %+ sZero `because` plusCongR n nMmEQ0
=== n `because` plusZeroR n
plusMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k
-> IsTrue (n <= m) -> IsTrue (l <= k)
-> IsTrue ((n + l) <= (m + k))
plusMonotone n m l k nLEm lLEk =
case (leqWitness n m nLEm, leqWitness l k lLEk) of
(DiffNat _ mMINn, DiffNat _ kMINl) ->
let r = mMINn %+ kMINl
in leqStep (n %+ l) (m %+ k) r $
start (n %+ l %+ r)
=== n %+ (l %+ r)
`because` plusAssoc n l r
=~= n %+ (l %+ (mMINn %+ kMINl))
=== n %+ (l %+ (kMINl %+ mMINn))
`because` plusCongR n (plusCongR l (plusComm mMINn kMINl))
=== n %+ ((l %+ kMINl) %+ mMINn)
`because` plusCongR n (sym $ plusAssoc l kMINl mMINn)
=~= n %+ (k %+ mMINn)
=== n %+ (mMINn %+ k)
`because` plusCongR n (plusComm k mMINn)
=== n %+ mMINn %+ k
`because` sym (plusAssoc n mMINn k)
=~= m %+ k
leqZeroElim :: Sing n -> IsTrue (n <= Zero nat) -> n :~: Zero nat
leqZeroElim n nLE0 =
case viewLeq n sZero nLE0 of
LeqZero _ -> Refl
LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl
plusMonotoneL :: Sing (n :: nat) -> Sing m -> Sing (l :: nat) -> IsTrue (n <= m)
-> IsTrue ((n + l) <= (m + l))
plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l)
plusMonotoneR :: Sing n -> Sing m -> Sing (l :: nat) -> IsTrue (m <= l)
-> IsTrue ((n + m) <= (n + l))
plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq
plusLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n <= (n + m))
plusLeqL n m = leqStep n (n %+ m) m Refl
plusLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m <= (n + m))
plusLeqR n m = leqStep m (n %+ m) n $ plusComm m n
plusCancelLeqR :: Sing (n :: nat) -> Sing m -> Sing l
-> IsTrue ((n + l) <= (m + l))
-> IsTrue (n <= m)
plusCancelLeqR n m l nlLEQml =
case leqWitness (n %+ l) (m %+ l) nlLEQml of
DiffNat _ k ->
let pf = plusEqCancelR (n %+ k) m l $
start ((n %+ k) %+ l)
=== n %+ (k %+ l) `because` plusAssoc n k l
=== n %+ (l %+ k) `because` plusCongR n (plusComm k l)
=== n %+ l %+ k `because` sym (plusAssoc n l k)
=~= m %+ l
in leqStep n m k pf
plusCancelLeqL :: Sing (n :: nat) -> Sing m -> Sing l
-> IsTrue ((n + m) <= (n + l))
-> IsTrue (m <= l)
plusCancelLeqL n m l nmLEQnl =
plusCancelLeqR m l n $
coerceLeqL (plusComm n m) (l %+ n) $
coerceLeqR (n %+ m) (plusComm n l) nmLEQnl
succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero nat) -> Void
succLeqZeroAbsurd n leq =
succNonCyclic n (leqZeroElim (sSucc n) leq)
succLeqZeroAbsurd' :: Sing n -> (S n <= Zero nat) :~: 'False
succLeqZeroAbsurd' n =
case sSucc n %<= sZero of
STrue -> absurd $ succLeqZeroAbsurd n Witness
SFalse -> Refl
succLeqAbsurd :: Sing (n :: nat) -> IsTrue (S n <= n) -> Void
succLeqAbsurd n snLEQn =
eliminate $
start SLT
=== sCompare n n `because` sym (succLeqToLT n n snLEQn)
=== SEQ `because` eqlCmpEQ n n Refl
succLeqAbsurd' :: Sing (n :: nat) -> (S n <= n) :~: 'False
succLeqAbsurd' n =
case sSucc n %<= n of
STrue -> absurd $ succLeqAbsurd n Witness
SFalse -> Refl
notLeqToLeq :: ((n <= m) ~ 'False) => Sing (n :: nat) -> Sing m -> IsTrue (m <= n)
notLeqToLeq n m =
case sCompare n m of
SLT -> eliminate $ ltToLeq n m Refl
SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl
SGT -> gtToLeq n m Refl
leqSucc' :: Sing (n :: nat) -> Sing m -> (n <= m) :~: (Succ n <= Succ m)
leqSucc' n m =
case n %<= m of
STrue -> withWitness (leqSucc n m Witness) Refl
SFalse ->
case sSucc n %<= sSucc m of
SFalse -> Refl
STrue ->
case viewLeq (sSucc n) (sSucc m) Witness of
LeqZero _ -> absurd $ succNonCyclic n Refl
LeqSucc n' m' Witness ->
eliminate $
start STrue
=~= (n' %<= m')
=== (n %<= m) `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl)
=~= SFalse
leqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> Min n m :~: n
leqToMin n m nLEQm =
leqAntisymm (sMin n m) n (minLeqL n m)
(minLargest n n m (leqRefl n) nLEQm)
geqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Min n m :~: m
geqToMin n m mLEQn =
leqAntisymm (sMin n m) m (minLeqR n m)
(minLargest m n m mLEQn (leqRefl m))
minComm :: Sing (n :: nat) -> Sing m -> Min n m :~: Min m n
minComm n m =
case n %<= m of
STrue -> start (sMin n m) === n `because` leqToMin n m Witness
=== sMin m n `because` sym (geqToMin m n Witness)
SFalse -> start (sMin n m) === m `because` geqToMin n m (notLeqToLeq n m)
=== sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m)
minLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m <= n)
minLeqL n m =
case n %<= m of
STrue -> leqReflexive (sMin n m) n $ leqToMin n m Witness
SFalse -> let mLEQn = notLeqToLeq n m
in leqTrans (sMin n m) m n
(leqReflexive (sMin n m) m (geqToMin n m mLEQn)) $
mLEQn
minLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m <= m)
minLeqR n m = leqTrans (sMin n m) (sMin m n) m
(leqReflexive (sMin n m) (sMin m n) $ minComm n m)
(minLeqL m n)
minLargest :: Sing (l :: nat) -> Sing n -> Sing m
-> IsTrue (l <= n) -> IsTrue (l <= m)
-> IsTrue (l <= Min n m)
minLargest l n m lLEQn lLEQm =
withSingI l $ withSingI n $ withSingI m $ withSingI (sMin n m) $
case n %<= m of
STrue -> leqTrans l n (sMin n m) lLEQn $
leqReflexive sing sing $ sym $ leqToMin n m Witness
SFalse ->
let mLEQn = notLeqToLeq n m
in leqTrans l m (sMin n m) lLEQm $
leqReflexive sing sing $ sym $ geqToMin n m mLEQn
leqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> Max n m :~: m
leqToMax n m nLEQm =
leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m)
geqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Max n m :~: n
geqToMax n m mLEQn =
leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m)
maxComm :: Sing (n :: nat) -> Sing m -> Max n m :~: Max m n
maxComm n m =
case n %<= m of
STrue -> start (sMax n m) === m `because` leqToMax n m Witness
=== sMax m n `because` sym (geqToMax m n Witness)
SFalse -> start (sMax n m) === n `because` geqToMax n m (notLeqToLeq n m)
=== sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m)
maxLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m <= Max n m)
maxLeqR n m =
case n %<= m of
STrue -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness
SFalse -> let mLEQn = notLeqToLeq n m
in leqTrans m n (sMax n m) mLEQn
(leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn))
maxLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n <= Max n m)
maxLeqL n m = leqTrans n (sMax m n) (sMax n m)
(maxLeqR m n)
(leqReflexive (sMax m n) (sMax n m) $ maxComm m n)
maxLeast :: Sing (l :: nat) -> Sing n -> Sing m
-> IsTrue (n <= l) -> IsTrue (m <= l)
-> IsTrue (Max n m <= l)
maxLeast l n m lLEQn lLEQm =
withSingI l $ withSingI n $ withSingI m $ withSingI (sMax n m) $
case n %<= m of
STrue -> leqTrans (sMax n m) m l
(leqReflexive sing sing $ leqToMax n m Witness)
lLEQm
SFalse ->
let mLEQn = notLeqToLeq n m
in leqTrans (sMax n m) n l
(leqReflexive sing sing $ geqToMax n m mLEQn)
lLEQn
leqReversed :: Sing (n :: nat) -> Sing m -> (n <= m) :~: (m >= n)
lneqSuccLeq :: Sing (n :: nat) -> Sing m -> (n < m) :~: (Succ n <= m)
lneqReversed :: Sing (n :: nat) -> Sing m -> (n < m) :~: (m > n)
lneqToLT :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n < m)
-> Compare n m :~: 'LT
lneqToLT n m nLNEm =
succLeqToLT n m $ coerce (lneqSuccLeq n m) nLNEm
ltToLneq :: Sing (n :: nat) -> Sing (m :: nat) -> Compare n m :~: 'LT
-> IsTrue (n < m)
ltToLneq n m nLTm =
coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm
lneqZero :: Sing (a :: nat) -> IsTrue (Zero nat < Succ a)
lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n
lneqSucc :: Sing (n :: nat) -> IsTrue (n < Succ n)
lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n
succLneqSucc :: Sing (n :: nat) -> Sing (m :: nat)
-> (n < m) :~: (Succ n < Succ m)
succLneqSucc n m =
start (n %< m)
=== (sSucc n %<= m) `because` lneqSuccLeq n m
=== (sSucc (sSucc n) %<= sSucc m) `because` leqSucc' (sSucc n) m
=== (sSucc n %< sSucc m) `because` sym (lneqSuccLeq (sSucc n) (sSucc m))
lneqRightPredSucc :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n < m)
-> m :~: Succ (Pred m)
lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm
lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m)
lneqSuccStepL n m snLNEQm =
coerce (sym $ lneqSuccLeq n m) $
leqSuccStepL (sSucc n) m $
coerce (lneqSuccLeq (sSucc n) m) snLNEQm
lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m)
lneqSuccStepR n m nLNEQm =
coerce (sym $ lneqSuccLeq n (sSucc m)) $
leqSuccStepR (sSucc n) m $
coerce (lneqSuccLeq n m) nLNEQm
plusStrictMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k
-> IsTrue (n < m) -> IsTrue (l < k)
-> IsTrue ((n + l) < (m + k))
plusStrictMonotone n m l k nLNm lLNk =
coerce (sym $ lneqSuccLeq (n %+ l) (m %+ k)) $
flip coerceLeqL (m %+ k) (plusSuccL n l) $
plusMonotone (sSucc n) m l k
(coerce (lneqSuccLeq n m) nLNm)
(leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $
coerce (lneqSuccLeq l k) lLNk)
maxZeroL :: Sing n -> Max (Zero nat) n :~: n
maxZeroL n = leqToMax sZero n (leqZero n)
maxZeroR :: Sing n -> Max n (Zero nat) :~: n
maxZeroR n = geqToMax n sZero (leqZero n)
minZeroL :: Sing n -> Min (Zero nat) n :~: Zero nat
minZeroL n = leqToMin sZero n (leqZero n)
minZeroR :: Sing n -> Min n (Zero nat) :~: Zero nat
minZeroR n = geqToMin n sZero (leqZero n)
minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Succ n - m :~: Succ (n - m)
minusSucc n m mLEQn =
case leqWitness m n mLEQn of
DiffNat _ k ->
start (sSucc n %- m)
=~= sSucc (m %+ k) %- m
=== (m %+ sSucc k) %- m `because` minusCongL (sym $ plusSuccR m k) m
=== (sSucc k %+ m) %- m `because` minusCongL (plusComm m (sSucc k)) m
=== sSucc k `because` plusMinus (sSucc k) m
=== sSucc (k %+ m %- m) `because` succCong (sym $ plusMinus k m)
=== sSucc (m %+ k %- m) `because` succCong (minusCongL (plusComm k m) m)
=~= sSucc (n %- m)
lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero nat) -> Void
lneqZeroAbsurd n leq =
succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq)
minusPlus :: forall (n :: nat) m .PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n)
-> n - m + m :~: n
minusPlus n m mLEQn =
case leqWitness m n mLEQn of
DiffNat _ k ->
start (n %- m %+ m)
=~= m %+ k %- m %+ m
=== k %+ m %- m %+ m `because` plusCongL (minusCongL (plusComm m k) m) m
=== k %+ m `because` plusCongL (plusMinus k m) m
=== m %+ k `because` plusComm k m
=~= n
type n -. m = Subt n m (m <= n)
type family Subt (n :: nat) (m :: nat) (b :: Bool) :: nat where
Subt n m 'True = n - m
Subt (n :: nat) m 'False = Zero nat
infixl 6 -.
(%-.) :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing (n -. m)
n %-. m =
case m %<= n of
STrue -> n %- m
SFalse -> sZero
minPlusTruncMinus :: (PeanoOrder nat) => Sing (n :: nat) -> Sing (m :: nat)
-> Min n m + (n -. m) :~: n
minPlusTruncMinus n m =
case m %<= n of
STrue ->
start (sMin n m %+ (n %-. m))
=== m %+ (n %-. m) `because` plusCongL (geqToMin n m Witness) (n %-. m)
=~= m %+ (n %- m)
=== (n %- m) %+ m `because` plusComm m (n %- m)
=== n `because` minusPlus n m Witness
SFalse ->
start (sMin n m %+ (n %-. m))
=~= sMin n m %+ sZero
=== sMin n m `because` plusZeroR (sMin n m)
=== n `because` leqToMin n m (notLeqToLeq m n)
truncMinusLeq :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue ((n -. m) <= n)
truncMinusLeq n m =
case m %<= n of
STrue -> leqStep (n %-. m) n m $ minusPlus n m Witness
SFalse -> leqZero n