module Data.Type.Natural.Class.Arithmetic
(Zero, One, S, sZero, sOne, ZeroOrSucc(..),
plusCong, plusCongR, plusCongL, succCong,
multCong, multCongL, multCongR,
minusCong, minusCongL, minusCongR,
IsPeano(..), pattern Zero, pattern Succ,
module Data.Type.Natural.Singleton.Compat
) where
import Data.Type.Natural.Singleton.Compat
(type (/=), type (==), type (+), type (*), type ()
,type (/=@#@$) ,type (/=@#@$$), type (/=@#@$$$)
,type (==@#@$) ,type (==@#@$$), type (==@#@$$$)
,type (+@#@$) ,type (+@#@$$), type (+@#@$$$)
,type (*@#@$) ,type (*@#@$$), type (*@#@$$$)
,type (-@#@$) ,type (-@#@$$), type (-@#@$$$)
,(%==), (%/=), (%+), (%*), (%-)
, FromInteger, FromIntegerSym0, FromIntegerSym1
,SNum(..), PNum(..)
)
import Data.Functor.Const (Const (..))
import Data.Singletons.Decide (SDecide (..))
import Data.Singletons.Prelude (Apply, SingI (..), SingKind (..),
SomeSing (..), Sing)
import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ, sPred, sSucc)
import Data.Type.Equality ((:~:) (..))
import Data.Void (Void, absurd)
import Numeric.Natural (Natural)
import Proof.Equational (because, coerce, start, sym, trans, (===))
type family Zero nat :: nat where
Zero nat = FromInteger 0
sZero :: (SNum nat) => Sing (Zero nat)
sZero = sFromInteger (sing :: Sing 0)
type family One nat :: nat where
One nat = FromInteger 1
sOne :: SNum nat => Sing (One nat)
sOne = sFromInteger (sing :: Sing 1)
type S n = Succ n
sS :: SEnum nat => Sing (n :: nat) -> Sing (S n)
sS = sSucc
predCong :: n :~: m -> Pred n :~: Pred m
predCong Refl = Refl
plusCong :: n :~: m -> n' :~: m' -> n + n' :~: m + m'
plusCong Refl Refl = Refl
plusCongL :: n :~: m -> Sing k -> n + k :~: m + k
plusCongL Refl _ = Refl
plusCongR :: Sing k -> n :~: m -> k + n :~: k + m
plusCongR _ Refl = Refl
succCong :: n :~: m -> S n :~: S m
succCong Refl = Refl
multCong :: n :~: m -> l :~: k -> n * l :~: m * k
multCong Refl Refl = Refl
multCongL :: n :~: m -> Sing k -> n * k :~: m * k
multCongL Refl _ = Refl
multCongR :: Sing k -> n :~: m -> k * n :~: k * m
multCongR _ Refl = Refl
minusCong :: n :~: m -> l :~: k -> n l :~: m k
minusCong Refl Refl = Refl
minusCongL :: n :~: m -> Sing k -> n k :~: m k
minusCongL Refl _ = Refl
minusCongR :: Sing k -> n :~: m -> k n :~: k m
minusCongR _ Refl = Refl
data ZeroOrSucc (n :: nat) where
IsZero :: ZeroOrSucc (Zero nat)
IsSucc :: Sing n -> ZeroOrSucc (Succ n)
newtype Assoc op n = Assoc { assocProof :: forall k l. Sing k -> Sing l ->
Apply (op (Apply (op n) k)) l :~:
Apply (op n) (Apply (op k) l)
}
newtype IdentityR op e (n :: nat) = IdentityR { idRProof :: Apply (op n) e :~: n }
newtype IdentityL op e (n :: nat) = IdentityL { idLProof :: Apply (op e) n :~: n }
type PlusZeroR (n :: nat) = IdentityR (+@#@$$) (Zero nat) n
newtype PlusSuccR (n :: nat) =
PlusSuccR { plusSuccRProof :: forall m. Sing m -> n + S m :~: S (n + m) }
type PlusZeroL (n :: nat) = IdentityL (+@#@$$) (Zero nat) n
newtype PlusSuccL (m :: nat) =
PlusSuccL { plusSuccLProof :: forall n. Sing n -> S n + m :~: S (n + m) }
newtype Comm op n = Comm { commProof :: forall m. Sing m -> Apply (op n) m :~: Apply (op m) n }
type PlusComm = Comm (+@#@$$)
newtype MultZeroL (n :: nat) = MultZeroL { multZeroLProof :: Zero nat * n :~: Zero nat }
newtype MultZeroR (n :: nat) =
MultZeroR { multZeroRProof :: n * Zero nat :~: Zero nat }
newtype MultSuccL (m :: nat) = MultSuccL { multSuccLProof :: forall n. Sing n -> S n * m :~: n * m + m }
newtype MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n * S m :~: n * m + n }
newtype PlusMultDistrib (n :: nat) =
PlusMultDistrib { plusMultDistribProof :: forall m l. Sing m -> Sing l
-> (n + m) * l :~: (n * l) + (m * l)
}
newtype PlusEqCancelL (n :: nat) =
PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l
-> n + m :~: n + l -> m :~: l }
newtype SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: Succ n :~: One nat + n }
newtype MultEqCancelR n =
MultEqCancelR { proofMultEqCancelR :: forall m l. Sing m -> Sing l
-> n * Succ l :~: m * Succ l
-> n :~: m
}
class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat)
=> IsPeano nat where
succOneCong :: Succ (Zero nat) :~: One nat
succInj :: Succ n :~: Succ (m :: nat) -> n :~: m
succInj' :: proxy n -> proxy' m -> Succ n :~: Succ (m :: nat) -> n :~: m
succInj' _ _ = succInj
succNonCyclic :: Sing n -> Succ n :~: Zero nat -> Void
induction :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k
plusMinus :: Sing (n :: nat) -> Sing m -> n + m m :~: n
plusMinus' :: Sing (n :: nat) -> Sing m -> n + m n :~: m
plusMinus' n m =
start (n %+ m %- n)
=== m %+ n %- n `because` minusCongL (plusComm n m) n
=== m `because` plusMinus m n
plusZeroL :: Sing n -> (Zero nat + n) :~: n
plusZeroL sn = idLProof (induction base step sn)
where
base :: PlusZeroL (Zero nat)
base = IdentityL (plusZeroR sZero)
step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n)
step sk (IdentityL ih) = IdentityL $
start (sZero %+ sS sk)
=== sS (sZero %+ sk) `because` plusSuccR sZero sk
=== sS sk `because` succCong ih
plusSuccL :: Sing n -> Sing m -> S n + m :~: S (n + m :: nat)
plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0
where
base :: PlusSuccL (Zero nat)
base = PlusSuccL $ \sn ->
start (sS sn %+ sZero)
=== sS sn `because` plusZeroR (sS sn)
=== sS (sn %+ sZero) `because` succCong (sym $ plusZeroR sn)
step :: Sing (n :: nat) -> PlusSuccL n -> PlusSuccL (S n)
step sm (PlusSuccL ih) = PlusSuccL $ \sn ->
start (sS sn %+ sS sm)
=== sS (sS sn %+ sm) `because` plusSuccR (sS sn) sm
=== sS (sS (sn %+ sm)) `because` succCong (ih sn)
=== sS (sn %+ sS sm) `because` succCong (sym $ plusSuccR sn sm)
plusZeroR :: Sing n -> (n + Zero nat) :~: n
plusZeroR sn = idRProof (induction base step sn)
where
base :: PlusZeroR (Zero nat)
base = IdentityR (plusZeroL sZero)
step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n)
step sk (IdentityR ih) = IdentityR $
start (sS sk %+ sZero)
=== sS (sk %+ sZero) `because` plusSuccL sk sZero
=== sS sk `because` succCong ih
plusSuccR :: Sing n -> Sing m -> n + S m :~: S (n + m :: nat)
plusSuccR sn0 = plusSuccRProof (induction base step sn0)
where
base :: PlusSuccR (Zero nat)
base = PlusSuccR $ \sk ->
start (sZero %+ sS sk)
=== sS sk `because` plusZeroL (sS sk)
=== sS (sZero %+ sk) `because` succCong (sym $ plusZeroL sk)
step :: Sing (n :: nat) -> PlusSuccR n -> PlusSuccR (S n)
step sn (PlusSuccR ih) = PlusSuccR $ \sk ->
start (sS sn %+ sS sk)
=== sS (sn %+ sS sk) `because` plusSuccL sn (sS sk)
=== sS (sS (sn %+ sk)) `because` succCong (ih sk)
=== sS (sS sn %+ sk) `because` succCong (sym $ plusSuccL sn sk)
plusComm :: Sing n -> Sing m -> n + m :~: (m :: nat) + n
plusComm sn0 = commProof (induction base step sn0)
where
base :: PlusComm (Zero nat)
base = Comm $ \sk ->
start (sZero %+ sk)
=== sk `because` plusZeroL sk
=== (sk %+ sZero) `because` sym (plusZeroR sk)
step :: Sing (n :: nat) -> PlusComm n -> PlusComm (S n)
step sn (Comm ih) = Comm $ \sk ->
start (sS sn %+ sk)
=== sS (sn %+ sk) `because` plusSuccL sn sk
=== sS (sk %+ sn) `because` succCong (ih sk)
=== sk %+ sS sn `because` sym (plusSuccR sk sn)
plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l
-> (n + m) + l :~: n + (m + l)
plusAssoc sn m l = assocProof (induction base step sn) m l
where
base :: Assoc (+@#@$$) (Zero nat)
base = Assoc $ \ sk sl ->
start ((sZero %+ sk) %+ sl)
=== sk %+ sl
`because` plusCongL (plusZeroL sk) sl
=== (sZero %+ (sk %+ sl))
`because` sym (plusZeroL (sk %+ sl))
step :: forall k . Sing (k :: nat) -> Assoc (+@#@$$) k -> Assoc (+@#@$$) (S k)
step sk (Assoc ih) = Assoc $ \ sl su ->
start ((sS sk %+ sl) %+ su)
=== (sS (sk %+ sl) %+ su) `because` plusCongL (plusSuccL sk sl) su
=== sS (sk %+ sl %+ su) `because` plusSuccL (sk %+ sl) su
=== sS (sk %+ (sl %+ su)) `because` succCong (ih sl su)
=== sS sk %+ (sl %+ su) `because` sym (plusSuccL sk (sl %+ su))
multZeroL :: Sing n -> Zero nat * n :~: Zero nat
multZeroL sn0 = multZeroLProof $ induction base step sn0
where
base :: MultZeroL (Zero nat)
base = MultZeroL (multZeroR sZero)
step :: Sing (k :: nat) -> MultZeroL k -> MultZeroL (S k)
step sk (MultZeroL ih) = MultZeroL $
start (sZero %* sS sk)
=== sZero %* sk %+ sZero `because` multSuccR sZero sk
=== sZero %* sk `because` plusZeroR (sZero %* sk)
=== sZero `because` ih
multSuccL :: Sing (n :: nat) -> Sing m -> S n * m :~: n * m + m
multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0
where
base :: MultSuccL (Zero nat)
base = MultSuccL $ \sk ->
start (sS sk %* sZero)
=== sZero `because` multZeroR (sS sk)
=== sk %* sZero `because` sym (multZeroR sk)
=== sk %* sZero %+ sZero `because` sym (plusZeroR (sk %* sZero))
step :: Sing (m :: nat) -> MultSuccL m -> MultSuccL (S m)
step sm (MultSuccL ih) = MultSuccL $ \sk ->
start (sS sk %* sS sm)
=== sS sk %* sm %+ sS sk
`because` multSuccR (sS sk) sm
=== (sk %* sm %+ sm) %+ sS sk
`because` plusCongL (ih sk) (sS sk)
=== sS ((sk %* sm %+ sm) %+ sk)
`because` plusSuccR (sk %* sm %+ sm) sk
=== sS (sk %* sm %+ (sm %+ sk))
`because` succCong (plusAssoc (sk %* sm) sm sk)
=== sS (sk %* sm %+ (sk %+ sm))
`because` succCong (plusCongR (sk %* sm) (plusComm sm sk))
=== sS ((sk %* sm %+ sk) %+ sm)
`because` succCong (sym $ plusAssoc (sk %* sm) sk sm)
=== sS ((sk %* sS sm) %+ sm)
`because` succCong (plusCongL (sym $ multSuccR sk sm) sm)
=== sk %* sS sm %+ sS sm `because` sym (plusSuccR (sk %* sS sm) sm)
multZeroR :: Sing n -> n * Zero nat :~: Zero nat
multZeroR sn0 = multZeroRProof $ induction base step sn0
where
base :: MultZeroR (Zero nat)
base = MultZeroR (multZeroR sZero)
step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k)
step sk (MultZeroR ih) = MultZeroR $
start (sS sk %* sZero)
=== sk %* sZero %+ sZero `because` multSuccL sk sZero
=== sk %* sZero `because` plusZeroR (sk %* sZero)
=== sZero `because` ih
multSuccR :: Sing n -> Sing m -> n * S m :~: n * m + (n :: nat)
multSuccR sn0 = multSuccRProof $ induction base step sn0
where
base :: MultSuccR (Zero nat)
base = MultSuccR $ \sk ->
start (sZero %* sS sk)
=== sZero
`because` multZeroL (sS sk)
=== sZero %* sk
`because` sym (multZeroL sk)
=== sZero %* sk %+ sZero
`because` sym (plusZeroR (sZero %* sk))
step :: Sing (n :: nat) -> MultSuccR n -> MultSuccR (S n)
step sn (MultSuccR ih) = MultSuccR $ \sk ->
start (sS sn %* sS sk)
=== sn %* sS sk %+ sS sk
`because` multSuccL sn (sS sk)
=== sS (sn %* sS sk %+ sk)
`because` plusSuccR (sn %* sS sk) sk
=== sS (sn %* sk %+ sn %+ sk)
`because` succCong (plusCongL (ih sk) sk)
=== sS (sn %* sk %+ (sn %+ sk))
`because` succCong (plusAssoc (sn %* sk) sn sk)
=== sS (sn %* sk %+ (sk %+ sn))
`because` succCong (plusCongR (sn %* sk) (plusComm sn sk))
=== sS (sn %* sk %+ sk %+ sn)
`because` succCong (sym $ plusAssoc (sn %* sk) sk sn)
=== sS (sS sn %* sk %+ sn)
`because` succCong (plusCongL (sym $ multSuccL sn sk) sn)
=== sS sn %* sk %+ sS sn
`because` sym (plusSuccR (sS sn %* sk) sn)
multComm :: Sing (n :: nat) -> Sing m -> n * m :~: m * n
multComm sn0 = commProof (induction base step sn0)
where
base :: Comm (*@#@$$) (Zero nat)
base = Comm $ \sk ->
start (sZero %* sk)
=== sZero `because` multZeroL sk
=== sk %* sZero `because` sym (multZeroR sk)
step :: Sing (n :: nat) -> Comm (*@#@$$) n -> Comm (*@#@$$) (S n)
step sn (Comm ih) = Comm $ \sk ->
start (sS sn %* sk)
=== sn %* sk %+ sk `because` multSuccL sn sk
=== sk %* sn %+ sk `because` plusCongL (ih sk) sk
=== sk %* sS sn `because` sym (multSuccR sk sn)
multOneR :: Sing n -> n * One nat :~: n
multOneR sn =
start (sn %* sOne)
=== sn %* sS sZero `because` multCongR sn (sym $ succOneCong)
=== sn %* sZero %+ sn `because` multSuccR sn sZero
=== sZero %+ sn `because` plusCongL (multZeroR sn) sn
=== sn `because` plusZeroL sn
multOneL :: Sing n -> One nat * n :~: n
multOneL sn =
start (sOne %* sn)
=== sn %* sOne `because` multComm sOne sn
=== sn `because` multOneR sn
plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l
-> (n + m) * l :~: (n * l) + (m * l)
plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0
where
base :: PlusMultDistrib (Zero nat)
base = PlusMultDistrib $ \sk sl ->
start ((sZero %+ sk) %* sl)
=== (sk %* sl)
`because` multCongL (plusZeroL sk) sl
=== sZero %+ (sk %* sl)
`because` sym (plusZeroL (sk %* sl))
=== sZero %* sl %+ sk %* sl
`because` plusCongL (sym $ multZeroL sl) (sk %* sl)
step :: Sing (n :: nat) -> PlusMultDistrib n -> PlusMultDistrib (S n)
step sn (PlusMultDistrib ih) = PlusMultDistrib $ \sk sl ->
start ((sS sn %+ sk) %* sl)
=== (sS (sn %+ sk) %* sl) `because` multCongL (plusSuccL sn sk) sl
=== (sn %+ sk) %* sl %+ sl `because` multSuccL (sn %+ sk) sl
=== ((sn %* sl) %+ (sk %* sl)) %+ sl `because` plusCongL (ih sk sl) sl
=== sn %* sl %+ (sk %* sl %+ sl) `because` plusAssoc (sn %* sl) (sk %* sl) sl
=== sn %* sl %+ (sl %+ (sk %* sl)) `because` plusCongR (sn %* sl) (plusComm (sk %* sl) sl)
=== (sn %* sl %+ sl) %+ (sk %* sl) `because` sym (plusAssoc (sn %* sl) sl (sk %* sl))
=== (sS sn %* sl) %+ (sk %* sl) `because` plusCongL (sym $ multSuccL sn sl) (sk %* sl)
multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l
-> n * (m + l) :~: (n * m) + (n * l)
multPlusDistrib n m l =
start (n %* (m %+ l))
=== (m %+ l) %* n `because` multComm n (m %+ l)
=== m %* n %+ l %* n `because` plusMultDistrib m l n
=== n %* m %+ n %* l `because` plusCong (multComm m n) (multComm l n)
minusNilpotent :: Sing n -> n n :~: Zero nat
minusNilpotent n =
start (n %- n)
=== (sZero %+ n) %- n `because` minusCongL (sym $ plusZeroL n) n
=== sZero `because` plusMinus sZero n
multAssoc :: Sing (n :: nat) -> Sing m -> Sing l
-> (n * m) * l :~: n * (m * l)
multAssoc sn0 = assocProof $ induction base step sn0
where
base :: Assoc (*@#@$$) (Zero nat)
base = Assoc $ \ m l ->
start (sZero %* m %* l)
=== sZero %* l `because` multCongL (multZeroL m) l
=== sZero `because` multZeroL l
=== sZero %* (m %* l) `because` sym (multZeroL (m %* l))
step :: Sing (n :: nat) -> Assoc (*@#@$$) n -> Assoc (*@#@$$) (S n)
step n _ = Assoc $ \ m l ->
start (sS n %* m %* l)
=== (n %* m %+ m) %* l `because` multCongL (multSuccL n m) l
=== n %* m %* l %+ m %* l `because` plusMultDistrib (n %* m) m l
=== n %* (m %* l) %+ m %* l `because` plusCongL (multAssoc n m l) (m %* l)
=== sS n %* (m %* l) `because` sym (multSuccL n (m %* l))
plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> n + m :~: n + l -> m :~: l
plusEqCancelL = plusEqCancelLProof . induction base step
where
base :: PlusEqCancelL (Zero nat)
base = PlusEqCancelL $ \l m nlnm ->
start l === sZero %+ l `because` sym (plusZeroL l)
=== sZero %+ m `because` nlnm
=== m `because` plusZeroL m
step :: Sing (n :: nat) -> PlusEqCancelL n -> PlusEqCancelL (Succ n)
step n (PlusEqCancelL ih) = PlusEqCancelL $ \l m snlsnm ->
succInj $ ih (sS l) (sS m) $
start (n %+ sS l)
=== sS (n %+ l) `because` plusSuccR n l
=== sS n %+ l `because` sym (plusSuccL n l)
=== sS n %+ m `because` snlsnm
=== sS (n %+ m) `because` plusSuccL n m
=== n %+ sS m `because` sym (plusSuccR n m)
plusEqCancelR :: forall n m l . Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m + l -> n :~: m
plusEqCancelR n m l nlml = plusEqCancelL l n m $
start (l %+ n)
=== (n %+ l) `because` plusComm l n
=== (m %+ l) `because` nlml
=== (l %+ m) `because` plusComm m l
succAndPlusOneL :: Sing n -> Succ n :~: One nat + n
succAndPlusOneL = proofSuccPlusL . induction base step
where
base :: SuccPlusL (Zero nat)
base = SuccPlusL $
start (sSucc sZero)
=== sOne `because` succOneCong
=== sOne %+ sZero `because` sym (plusZeroR sOne)
step :: Sing (n :: nat) -> SuccPlusL n -> SuccPlusL (Succ n)
step sn (SuccPlusL ih) = SuccPlusL $
start (sSucc (sSucc sn))
=== sSucc (sOne %+ sn) `because` succCong ih
=== sOne %+ sSucc sn `because` sym (plusSuccR sOne sn)
succAndPlusOneR :: Sing n -> Succ n :~: n + One nat
succAndPlusOneR n =
start (sSucc n)
=== sOne %+ n `because` succAndPlusOneL n
=== n %+ sOne `because` plusComm sOne n
predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat)
zeroOrSucc :: Sing (n :: nat) -> ZeroOrSucc n
zeroOrSucc = induction base step
where
base = IsZero
step sn _ = IsSucc sn
plusEqZeroL :: Sing n -> Sing m -> n + m :~: Zero nat -> n :~: Zero nat
plusEqZeroL n m Refl =
case zeroOrSucc n of
IsZero -> Refl
IsSucc pn -> absurd $ succNonCyclic (pn %+ m) (sym $ plusSuccL pn m)
plusEqZeroR :: Sing n -> Sing m -> n + m :~: Zero nat -> m :~: Zero nat
plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n)
predUnique :: Sing (n :: nat) -> Sing m -> Succ n :~: m -> n :~: Pred m
predUnique n m snEm =
start n === (sPred (sSucc n)) `because` sym (predSucc n)
=== sPred m `because` predCong snEm
multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> n :~: Succ (Pred n)
multEqSuccElimL n m l nmEsl =
case zeroOrSucc n of
IsZero -> absurd $ succNonCyclic l $ sym $
start sZero === sZero %* m `because` sym (multZeroL m)
=== sSucc l `because` nmEsl
IsSucc pn -> succCong (predUnique pn n Refl)
multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> m :~: Succ (Pred m)
multEqSuccElimR n m l nmEsl =
multEqSuccElimL m n l (multComm m n `trans` nmEsl)
minusZero :: Sing n -> n Zero nat :~: n
minusZero n =
start (n %- sZero)
=== (n %+ sZero) %- sZero
`because` minusCongL (sym $ plusZeroR n) sZero
=== n `because` plusMinus n sZero
multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n * Succ l :~: m * Succ l -> n :~: m
multEqCancelR = proofMultEqCancelR . induction base step
where
base :: MultEqCancelR (Zero nat)
base = MultEqCancelR $ \m l zslmsl ->
sym $ plusEqZeroR (m %* l) m $ sym $ start sZero
=== sZero %* l `because` sym (multZeroL l)
=== sZero %* l %+ sZero `because` sym (plusZeroR (sZero %* l))
=== sZero %* sSucc l `because` sym (multSuccR sZero l)
=== m %* sSucc l `because` zslmsl
=== m %* l %+ m `because` multSuccR m l
step :: Sing (n :: nat) -> MultEqCancelR n -> MultEqCancelR (Succ n)
step n (MultEqCancelR ih) = MultEqCancelR $ \m l snmssnl ->
let m' = sPred m
pf = start (m %* sSucc l)
=== sSucc n %* sSucc l `because` sym snmssnl
=== n %* sSucc l %+ sSucc l `because` multSuccL n (sSucc l)
=== sSucc (n %* sSucc l %+ l) `because` plusSuccR (n %* sSucc l) l
sm'Em = multEqSuccElimL m (sSucc l) (n %* sSucc l %+ l) pf
pf' = ih m' l $ plusEqCancelR (n %* sSucc l) (m' %* sSucc l) (sSucc l) $
start (n %* sSucc l %+ sSucc l)
=== sSucc (n %* sSucc l %+ l) `because` plusSuccR (n %* sSucc l) l
=== m %* sSucc l `because` sym pf
=== sSucc m' %* sSucc l `because` multCongL sm'Em (sSucc l)
=== (m' %* sSucc l %+ sSucc l) `because` multSuccL m' (sSucc l)
in succCong pf' `trans` sym sm'Em
succPred :: Sing n -> (n :~: Zero nat -> Void) -> Succ (Pred n) :~: n
succPred n nonZero =
case zeroOrSucc n of
IsZero -> absurd $ nonZero Refl
IsSucc n' -> sym $ succCong $ predUnique n' n Refl
multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> Succ n * m :~: Succ n * l -> m :~: l
multEqCancelL n m l snmEsnl =
multEqCancelR m l n $
multComm m (sSucc n) `trans` snmEsnl `trans` multComm (sSucc n) l
sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)
sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn)
toNatural :: Sing (n :: nat) -> Natural
toNatural = getConst . induction (Const 0) (\_ (Const k) -> (Const k + 1))
fromNatural :: Natural -> SomeSing nat
fromNatural 0 = SomeSing sZero
fromNatural n =
case fromNatural (n 1) of
SomeSing sn -> SomeSing (Succ sn)
pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n
pattern Zero <- (zeroOrSucc -> IsZero) where
Zero = sZero
pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n
pattern Succ n <- (zeroOrSucc -> IsSucc n) where
Succ n = sSucc n