{-# 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