{-# 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 TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

module Data.Type.Natural.Lemma.Arithmetic
  ( Zero,
    One,
    S,
    sZero,
    sOne,
    ZeroOrSucc (..),
    plusCong,
    plusCongR,
    plusCongL,
    predCong,
    Succ,
    sS,
    sSucc,
    Pred,
    sPred,
    sPred',
    succCong,
    multCong,
    multCongL,
    multCongR,
    minusCong,
    minusCongL,
    minusCongR,
    succOneCong,
    succInj,
    succInj',
    succNonCyclic,
    induction,
    plusMinus,
    plusMinus',
    plusZeroL,
    plusSuccL,
    plusZeroR,
    plusSuccR,
    plusComm,
    plusAssoc,
    multZeroL,
    multSuccL,
    multSuccL',
    multZeroR,
    multSuccR,
    multComm,
    multOneR,
    multOneL,
    plusMultDistrib,
    multPlusDistrib,
    minusNilpotent,
    multAssoc,
    plusEqCancelL,
    plusEqCancelR,
    succAndPlusOneL,
    succAndPlusOneR,
    predSucc,
    viewNat,
    zeroOrSucc,
    plusEqZeroL,
    plusEqZeroR,
    predUnique,
    multEqSuccElimL,
    multEqSuccElimR,
    minusZero,
    multEqCancelR,
    succPred,
    multEqCancelL,
    pattern Zero,
    pattern Succ,
  )
where

import Data.Type.Equality
  ( gcastWith,
    (:~:) (..),
  )
import Data.Type.Natural.Core
import Data.Type.Natural.Lemma.Presburger
  ( plusEqZeroL,
    plusEqZeroR,
    succNonCyclic,
  )
import Data.Void (Void, absurd)
import Proof.Equational (because, start, sym, trans, (===))

predCong :: n :~: m -> Pred n :~: Pred m
predCong :: (n :~: m) -> Pred n :~: Pred m
predCong n :~: m
Refl = Pred n :~: Pred m
forall k (a :: k). a :~: a
Refl

plusCong :: n :~: m -> n' :~: m' -> n + n' :~: m + m'
plusCong :: (n :~: m) -> (n' :~: m') -> (n + n') :~: (m + m')
plusCong n :~: m
Refl n' :~: m'
Refl = (n + n') :~: (m + m')
forall k (a :: k). a :~: a
Refl

plusCongL :: n :~: m -> SNat k -> n + k :~: m + k
plusCongL :: (n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL n :~: m
Refl SNat k
_ = (n + k) :~: (m + k)
forall k (a :: k). a :~: a
Refl

plusCongR :: SNat k -> n :~: m -> k + n :~: k + m
plusCongR :: SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat k
_ n :~: m
Refl = (k + n) :~: (k + m)
forall k (a :: k). a :~: a
Refl

succCong :: n :~: m -> S n :~: S m
succCong :: (n :~: m) -> S n :~: S m
succCong n :~: m
Refl = S n :~: S m
forall k (a :: k). a :~: a
Refl

multCong :: n :~: m -> l :~: k -> n * l :~: m * k
multCong :: (n :~: m) -> (l :~: k) -> (n * l) :~: (m * k)
multCong n :~: m
Refl l :~: k
Refl = (n * l) :~: (m * k)
forall k (a :: k). a :~: a
Refl

multCongL :: n :~: m -> SNat k -> n * k :~: m * k
multCongL :: (n :~: m) -> SNat k -> (n * k) :~: (m * k)
multCongL n :~: m
Refl SNat k
_ = (n * k) :~: (m * k)
forall k (a :: k). a :~: a
Refl

multCongR :: SNat k -> n :~: m -> k * n :~: k * m
multCongR :: SNat k -> (n :~: m) -> (k * n) :~: (k * m)
multCongR SNat k
_ n :~: m
Refl = (k * n) :~: (k * m)
forall k (a :: k). a :~: a
Refl

minusCong :: n :~: m -> l :~: k -> n - l :~: m - k
minusCong :: (n :~: m) -> (l :~: k) -> (n - l) :~: (m - k)
minusCong n :~: m
Refl l :~: k
Refl = (n - l) :~: (m - k)
forall k (a :: k). a :~: a
Refl

minusCongL :: n :~: m -> SNat k -> n - k :~: m - k
minusCongL :: (n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL n :~: m
Refl SNat k
_ = (n - k) :~: (m - k)
forall k (a :: k). a :~: a
Refl

minusCongR :: SNat k -> n :~: m -> k - n :~: k - m
minusCongR :: SNat k -> (n :~: m) -> (k - n) :~: (k - m)
minusCongR SNat k
_ n :~: m
Refl = (k - n) :~: (k - m)
forall k (a :: k). a :~: a
Refl

succOneCong :: Succ 0 :~: 1
succOneCong :: Succ 0 :~: 1
succOneCong = Succ 0 :~: 1
forall k (a :: k). a :~: a
Refl

succInj :: Succ n :~: Succ m -> n :~: m
succInj :: (Succ n :~: Succ m) -> n :~: m
succInj Succ n :~: Succ m
Refl = n :~: m
forall k (a :: k). a :~: a
Refl

succInj' :: proxy n -> proxy' m -> Succ n :~: Succ m -> n :~: m
succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ m) -> n :~: m
succInj' proxy n
_ proxy' m
_ = (Succ n :~: Succ m) -> n :~: m
forall (n :: Nat) (m :: Nat). (Succ n :~: Succ m) -> n :~: m
succInj

induction :: forall p k. p 0 -> (forall n. SNat n -> p n -> p (S n)) -> SNat k -> p k
induction :: p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction p 0
base forall (n :: Nat). SNat n -> p n -> p (S n)
step = SNat k -> p k
forall (m :: Nat). SNat m -> p m
go
  where
    go :: SNat m -> p m
    go :: SNat m -> p m
go SNat m
sn = case SNat m -> ZeroOrSucc m
forall (n :: Nat). SNat n -> ZeroOrSucc n
viewNat SNat m
sn of
      ZeroOrSucc m
IsZero -> p m
p 0
base
      IsSucc SNat n
n -> SNat n -> (KnownNat n => p m) -> p m
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => p m) -> p m) -> (KnownNat n => p m) -> p m
forall a b. (a -> b) -> a -> b
$ SNat n -> p n -> p (S n)
forall (n :: Nat). SNat n -> p n -> p (S n)
step SNat n
n (SNat n -> p n
forall (m :: Nat). SNat m -> p m
go SNat n
n)

plusMinus :: SNat n -> SNat m -> n + m - m :~: n
plusMinus :: SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus SNat n
_ SNat m
_ = ((n + m) - m) :~: n
forall k (a :: k). a :~: a
Refl

plusMinus' :: SNat n -> SNat m -> n + m - n :~: m
plusMinus' :: SNat n -> SNat m -> ((n + m) - n) :~: m
plusMinus' SNat n
n SNat m
m =
  SNat ((n + m) - n) -> ((n + m) - n) :~: ((n + m) - n)
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 n -> SNat ((n + m) - n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat n
n)
    (((n + m) - n) :~: ((n + m) - n))
-> Reason (:~:) ((n + m) - n) ((m + n) - n)
-> ((n + m) - n) :~: ((m + 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 m
m SNat m -> SNat n -> SNat (m + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
n SNat (m + n) -> SNat n -> SNat ((m + n) - n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat n
n SNat ((m + n) - n)
-> (((n + m) - n) :~: ((m + n) - n))
-> Reason (:~:) ((n + m) - n) ((m + 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 + m) :~: (m + n)) -> SNat n -> ((n + m) - n) :~: ((m + n) - n)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (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 n
n
    (((n + m) - n) :~: ((m + n) - n))
-> Reason (:~:) ((m + n) - n) m -> ((n + 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 -> (((m + n) - n) :~: m) -> Reason (:~:) ((m + n) - 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 m -> SNat n -> ((m + n) - n) :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus SNat m
m SNat n
n

plusZeroL :: SNat n -> (0 + n) :~: n
plusZeroL :: SNat n -> (0 + n) :~: n
plusZeroL SNat n
_ = (0 + n) :~: n
forall k (a :: k). a :~: a
Refl

plusSuccL :: SNat n -> SNat m -> S n + m :~: S (n + m)
plusSuccL :: SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
_ SNat m
_ = (S n + m) :~: S (n + m)
forall k (a :: k). a :~: a
Refl

plusZeroR :: SNat n -> (n + 0) :~: n
plusZeroR :: SNat n -> (n + 0) :~: n
plusZeroR SNat n
_ = (n + 0) :~: n
forall k (a :: k). a :~: a
Refl

plusSuccR :: SNat n -> SNat m -> n + S m :~: S (n + m)
plusSuccR :: SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat n
_ SNat m
_ = (n + S m) :~: S (n + m)
forall k (a :: k). a :~: a
Refl

plusComm :: SNat n -> SNat m -> n + m :~: m + n
plusComm :: SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat n
_ SNat m
_ = (n + m) :~: (m + n)
forall k (a :: k). a :~: a
Refl

plusAssoc ::
  forall n m l.
  SNat n ->
  SNat m ->
  SNat l ->
  (n + m) + l :~: n + (m + l)
plusAssoc :: SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
_ SNat m
_ SNat l
_ = ((n + m) + l) :~: (n + (m + l))
forall k (a :: k). a :~: a
Refl

multZeroL :: SNat n -> 0 * n :~: 0
multZeroL :: SNat n -> (0 * n) :~: 0
multZeroL SNat n
_ = (0 * n) :~: 0
forall k (a :: k). a :~: a
Refl

multSuccL :: SNat n -> SNat m -> S n * m :~: n * m + m
multSuccL :: SNat n -> SNat m -> (S n * m) :~: ((n * m) + m)
multSuccL SNat n
_ SNat m
_ = (S n * m) :~: ((n * m) + m)
forall k (a :: k). a :~: a
Refl

multSuccL' :: SNat n -> SNat m -> S n * m :~: n * m + 1 * m
multSuccL' :: SNat n -> SNat m -> (S n * m) :~: ((n * m) + (1 * m))
multSuccL' SNat n
_ SNat m
_ = (S n * m) :~: ((n * m) + (1 * m))
forall k (a :: k). a :~: a
Refl

multZeroR :: SNat n -> n * 0 :~: 0
multZeroR :: SNat n -> (n * 0) :~: 0
multZeroR SNat n
_ = (n * 0) :~: 0
forall k (a :: k). a :~: a
Refl

multSuccR :: SNat n -> SNat m -> n * S m :~: n * m + n
multSuccR :: SNat n -> SNat m -> (n * S m) :~: ((n * m) + n)
multSuccR SNat n
_ SNat m
_ = (n * S m) :~: ((n * m) + n)
forall k (a :: k). a :~: a
Refl

multComm :: SNat n -> SNat m -> n * m :~: m * n
multComm :: SNat n -> SNat m -> (n * m) :~: (m * n)
multComm SNat n
_ SNat m
_ = (n * m) :~: (m * n)
forall k (a :: k). a :~: a
Refl

multOneR :: SNat n -> n * 1 :~: n
multOneR :: SNat n -> (n * 1) :~: n
multOneR SNat n
_ = (n * 1) :~: n
forall k (a :: k). a :~: a
Refl

multOneL :: SNat n -> 1 * n :~: n
multOneL :: SNat n -> (1 * n) :~: n
multOneL SNat n
_ = (1 * n) :~: n
forall k (a :: k). a :~: a
Refl

plusMultDistrib ::
  SNat n ->
  SNat m ->
  SNat l ->
  (n + m) * l :~: (n * l) + (m * l)
plusMultDistrib :: SNat n -> SNat m -> SNat l -> ((n + m) * l) :~: ((n * l) + (m * l))
plusMultDistrib SNat n
_ SNat m
_ SNat l
_ = ((n + m) * l) :~: ((n * l) + (m * l))
forall k (a :: k). a :~: a
Refl

multPlusDistrib ::
  SNat n ->
  SNat m ->
  SNat l ->
  n * (m + l) :~: (n * m) + (n * l)
multPlusDistrib :: SNat n -> SNat m -> SNat l -> (n * (m + l)) :~: ((n * m) + (n * l))
multPlusDistrib SNat n
_ SNat m
_ SNat l
_ = (n * (m + l)) :~: ((n * m) + (n * l))
forall k (a :: k). a :~: a
Refl

minusNilpotent :: SNat n -> n - n :~: 0
minusNilpotent :: SNat n -> (n - n) :~: 0
minusNilpotent SNat n
_ = (n - n) :~: 0
forall k (a :: k). a :~: a
Refl

multAssoc ::
  SNat n ->
  SNat m ->
  SNat l ->
  (n * m) * l :~: n * (m * l)
multAssoc :: SNat n -> SNat m -> SNat l -> ((n * m) * l) :~: (n * (m * l))
multAssoc SNat n
_ SNat m
_ SNat l
_ = ((n * m) * l) :~: (n * (m * l))
forall k (a :: k). a :~: a
Refl

plusEqCancelL :: SNat n -> SNat m -> SNat l -> n + m :~: n + l -> m :~: l
plusEqCancelL :: SNat n -> SNat m -> SNat l -> ((n + m) :~: (n + l)) -> m :~: l
plusEqCancelL SNat n
_ SNat m
_ SNat l
_ (n + m) :~: (n + l)
Refl = m :~: l
forall k (a :: k). a :~: a
Refl

plusEqCancelR :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m + l -> n :~: m
plusEqCancelR :: SNat n -> SNat m -> SNat l -> ((n + l) :~: (m + l)) -> n :~: m
plusEqCancelR SNat n
n SNat m
m SNat l
l (n + l) :~: (m + l)
nlml =
  SNat l -> SNat n -> SNat m -> ((l + n) :~: (l + m)) -> n :~: m
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) :~: (n + l)) -> m :~: l
plusEqCancelL SNat l
l SNat n
n SNat m
m (((l + n) :~: (l + m)) -> n :~: m)
-> ((l + n) :~: (l + m)) -> n :~: m
forall a b. (a -> b) -> a -> b
$
    SNat (l + n) -> (l + n) :~: (l + n)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (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)
      ((l + n) :~: (l + n))
-> Reason (:~:) (l + n) (n + l) -> (l + n) :~: (n + 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 l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) SNat (n + l)
-> ((l + n) :~: (n + l)) -> Reason (:~:) (l + n) (n + 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 l -> SNat n -> (l + n) :~: (n + l)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat l
l SNat n
n
      ((l + n) :~: (n + l))
-> Reason (:~:) (n + l) (m + l) -> (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 m
m SNat m -> SNat l -> SNat (m + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) SNat (m + l)
-> ((n + l) :~: (m + l)) -> Reason (:~:) (n + l) (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` (n + l) :~: (m + l)
nlml
      ((l + n) :~: (m + l))
-> Reason (:~:) (m + l) (l + 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 l
l SNat l -> SNat m -> SNat (l + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) SNat (l + m)
-> ((m + l) :~: (l + m)) -> Reason (:~:) (m + l) (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 m -> SNat l -> (m + l) :~: (l + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m SNat l
l

succAndPlusOneL :: SNat n -> Succ n :~: 1 + n
succAndPlusOneL :: SNat n -> Succ n :~: (1 + n)
succAndPlusOneL SNat n
_ = Succ n :~: (1 + n)
forall k (a :: k). a :~: a
Refl

succAndPlusOneR :: SNat n -> Succ n :~: n + 1
succAndPlusOneR :: SNat n -> Succ n :~: Succ n
succAndPlusOneR SNat n
_ = Succ n :~: Succ n
forall k (a :: k). a :~: a
Refl

predSucc :: SNat n -> Pred (Succ n) :~: n
predSucc :: SNat n -> Pred (Succ n) :~: n
predSucc SNat n
_ = Pred (Succ n) :~: n
forall k (a :: k). a :~: a
Refl

zeroOrSucc :: SNat n -> ZeroOrSucc n
zeroOrSucc :: SNat n -> ZeroOrSucc n
zeroOrSucc = SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
viewNat

predUnique :: SNat n -> SNat m -> Succ n :~: m -> n :~: Pred m
predUnique :: SNat n -> SNat m -> (Succ n :~: m) -> n :~: Pred m
predUnique SNat n
_ SNat m
_ Succ n :~: m
Refl = n :~: Pred m
forall k (a :: k). a :~: a
Refl

minusZero :: SNat n -> n - 0 :~: n
minusZero :: SNat n -> (n - 0) :~: n
minusZero SNat n
_ = (n - 0) :~: n
forall k (a :: k). a :~: a
Refl

multEqCancelR :: forall n m l. SNat n -> SNat m -> SNat l -> n * Succ l :~: m * Succ l -> n :~: m
multEqCancelR :: SNat n
-> SNat m -> SNat l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m
multEqCancelR SNat n
_ SNat m
_ = SNat l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m
forall (k :: Nat).
SNat k -> ((n * Succ k) :~: (m * Succ k)) -> n :~: m
go
  where
    go :: forall k. SNat k -> n * Succ k :~: m * Succ k -> n :~: m
    go :: SNat k -> ((n * Succ k) :~: (m * Succ k)) -> n :~: m
go SNat k
Zero (n * Succ k) :~: (m * Succ k)
Refl = n :~: m
forall k (a :: k). a :~: a
Refl
    go (Succ SNat n1
n) (n * Succ k) :~: (m * Succ k)
Refl = (n :~: m) -> ((n ~ m) => n :~: m) -> n :~: m
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n1 -> ((n * Succ n1) :~: (m * Succ n1)) -> n :~: m
forall (k :: Nat).
SNat k -> ((n * Succ k) :~: (m * Succ k)) -> n :~: m
go SNat n1
n (n * Succ n1) :~: (m * Succ n1)
forall k (a :: k). a :~: a
Refl) (n ~ m) => n :~: m
forall k (a :: k). a :~: a
Refl

succPred :: SNat n -> (n :~: 0 -> Void) -> Succ (Pred n) :~: n
succPred :: SNat n -> ((n :~: 0) -> Void) -> Succ (Pred n) :~: n
succPred SNat n
n (n :~: 0) -> Void
nonZero =
  case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat n
n of
    ZeroOrSucc n
IsZero -> Void -> ((0 - 1) + 1) :~: 0
forall a. Void -> a
absurd (Void -> ((0 - 1) + 1) :~: 0) -> Void -> ((0 - 1) + 1) :~: 0
forall a b. (a -> b) -> a -> b
$ (n :~: 0) -> Void
nonZero n :~: 0
forall k (a :: k). a :~: a
Refl
    IsSucc SNat n
n' -> (n :~: Succ (Pred n)) -> Succ (Pred n) :~: n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((n :~: Succ (Pred n)) -> Succ (Pred n) :~: n)
-> (n :~: Succ (Pred n)) -> Succ (Pred n) :~: n
forall a b. (a -> b) -> a -> b
$ (n :~: Pred n) -> S n :~: Succ (Pred n)
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong ((n :~: Pred n) -> S n :~: Succ (Pred n))
-> (n :~: Pred n) -> S n :~: Succ (Pred n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat n -> (S n :~: n) -> n :~: Pred n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (Succ n :~: m) -> n :~: Pred m
predUnique SNat n
n' SNat n
n S n :~: n
forall k (a :: k). a :~: a
Refl

multEqCancelL :: SNat n -> SNat m -> SNat l -> Succ n * m :~: Succ n * l -> m :~: l
multEqCancelL :: SNat n
-> SNat m -> SNat l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l
multEqCancelL SNat n
n SNat m
m SNat l
l (Succ n * m) :~: (Succ n * l)
snmEsnl =
  SNat m
-> SNat l -> SNat n -> ((m * Succ n) :~: (l * Succ n)) -> m :~: l
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m -> SNat l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m
multEqCancelR SNat m
m SNat l
l SNat n
n (((m * Succ n) :~: (l * Succ n)) -> m :~: l)
-> ((m * Succ n) :~: (l * Succ n)) -> m :~: l
forall a b. (a -> b) -> a -> b
$
    SNat m -> SNat (Succ n) -> (m * Succ n) :~: (Succ n * m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n * m) :~: (m * n)
multComm SNat m
m (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) ((m * Succ n) :~: (Succ n * m))
-> ((Succ n * m) :~: (Succ n * l)) -> (m * Succ n) :~: (Succ n * l)
forall k (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
`trans` (Succ n * m) :~: (Succ n * l)
snmEsnl ((m * Succ n) :~: (Succ n * l))
-> ((Succ n * l) :~: (l * Succ n)) -> (m * Succ n) :~: (l * Succ n)
forall k (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
`trans` SNat (Succ n) -> SNat l -> (Succ n * l) :~: (l * Succ n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n * m) :~: (m * n)
multComm (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat l
l

sPred' :: proxy n -> SNat (Succ n) -> SNat n
sPred' :: proxy n -> SNat (Succ n) -> SNat n
sPred' proxy n
pxy SNat (Succ n)
sn = ((Succ n - 1) :~: n) -> (((Succ n - 1) ~ n) => SNat n) -> SNat n
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((Succ (Succ n - 1) :~: Succ n) -> (Succ n - 1) :~: n
forall (n :: Nat) (m :: Nat). (Succ n :~: Succ m) -> n :~: m
succInj ((Succ (Succ n - 1) :~: Succ n) -> (Succ n - 1) :~: n)
-> (Succ (Succ n - 1) :~: Succ n) -> (Succ n - 1) :~: n
forall a b. (a -> b) -> a -> b
$ ((Succ n - 1) :~: n) -> Succ (Succ n - 1) :~: Succ n
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong (((Succ n - 1) :~: n) -> Succ (Succ n - 1) :~: Succ n)
-> ((Succ n - 1) :~: n) -> Succ (Succ n - 1) :~: Succ n
forall a b. (a -> b) -> a -> b
$ SNat n -> (Succ n - 1) :~: n
forall (n :: Nat). SNat n -> Pred (Succ n) :~: n
predSucc (proxy n -> SNat (Succ n) -> SNat n
forall (proxy :: Nat -> Type) (n :: Nat).
proxy n -> SNat (Succ n) -> SNat n
sPred' proxy n
pxy SNat (Succ n)
sn)) (SNat (Succ n) -> SNat (Succ n - 1)
forall (n :: Nat). SNat n -> SNat (Pred n)
sPred SNat (Succ n)
sn)

multEqSuccElimL ::
  SNat n ->
  SNat m ->
  SNat l ->
  n * m :~: Succ l ->
  n :~: Succ (Pred n)
multEqSuccElimL :: SNat n
-> SNat m -> SNat l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n)
multEqSuccElimL SNat n
Zero SNat m
_ SNat l
l (n * m) :~: Succ l
Refl = 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 l -> (Succ l :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat l
l Succ l :~: 0
forall k (a :: k). a :~: a
Refl
multEqSuccElimL (Succ SNat n1
_) SNat m
_ SNat l
_ (n * m) :~: Succ l
Refl = n :~: Succ (Pred n)
forall k (a :: k). a :~: a
Refl

multEqSuccElimR :: SNat n -> SNat m -> SNat l -> n * m :~: Succ l -> m :~: Succ (Pred m)
multEqSuccElimR :: SNat n
-> SNat m -> SNat l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m)
multEqSuccElimR SNat n
_ SNat m
Zero SNat l
l (n * m) :~: Succ l
Refl = 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 l -> (Succ l :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat l
l Succ l :~: 0
forall k (a :: k). a :~: a
Refl
multEqSuccElimR SNat n
_ (Succ SNat n1
_) SNat l
_ (n * m) :~: Succ l
Refl = m :~: Succ (Pred m)
forall k (a :: k). a :~: a
Refl