{-|
Description : Type level natural number representation at runtime
Copyright   : (c) Galois, Inc 2014-2019
Maintainer  : Joe Hendrix <jhendrix@galois.com>

This defines a type 'NatRepr' for representing a type-level natural
at runtime.  This can be used to branch on a type-level value.  For
each @n@, @NatRepr n@ contains a single value containing the value
@n@.  This can be used to help use type-level variables on code
with data dependendent types.

The @TestEquality@ and @DecidableEq@ instances for 'NatRepr'
are implemented using 'unsafeCoerce', as is the `isZeroNat` function. This
should be typesafe because we maintain the invariant that the integer value
contained in a NatRepr value matches its static type.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
#if __GLASGOW_HASKELL__ >= 805
{-# LANGUAGE NoStarIsType #-}
#endif
module Data.Parameterized.NatRepr
  ( NatRepr
  , natValue
  , intValue
  , knownNat
  , withKnownNat
  , IsZeroNat(..)
  , isZeroNat
  , isZeroOrGT1
  , NatComparison(..)
  , compareNat
  , decNat
  , predNat
  , incNat
  , addNat
  , subNat
  , divNat
  , halfNat
  , withDivModNat
  , natMultiply
  , someNat
  , mkNatRepr
  , maxNat
  , natRec
  , natRecStrong
  , natRecBounded
  , natRecStrictlyBounded
  , natForEach
  , natFromZero
  , NatCases(..)
  , testNatCases
    -- * Strict order
  , lessThanIrreflexive
  , lessThanAsymmetric
    -- * Bitvector utilities
  , widthVal
  , minUnsigned
  , maxUnsigned
  , minSigned
  , maxSigned
  , toUnsigned
  , toSigned
  , unsignedClamp
  , signedClamp
    -- * LeqProof
  , LeqProof(..)
  , decideLeq
  , testLeq
  , testStrictLeq
  , leqRefl
  , leqSucc
  , leqTrans
  , leqZero
  , leqAdd2
  , leqSub2
  , leqMulCongr
    -- * LeqProof combinators
  , leqProof
  , withLeqProof
  , isPosNat
  , leqAdd
  , leqSub
  , leqMulPos
  , leqAddPos
  , addIsLeq
  , withAddLeq
  , addPrefixIsLeq
  , withAddPrefixLeq
  , addIsLeqLeft1
  , dblPosIsPos
  , leqMulMono
    -- * Arithmetic proof
  , plusComm
  , plusAssoc
  , mulComm
  , plusMinusCancel
  , minusPlusCancel
  , addMulDistribRight
  , withAddMulDistribRight
  , withSubMulDistribRight
  , mulCancelR
  , mul2Plus
  , lemmaMul
    -- * Re-exports typelists basics
--  , NatK
  , type (+)
  , type (-)
  , type (*)
  , type (<=)
  , Equality.TestEquality(..)
  , (Equality.:~:)(..)
  , Data.Parameterized.Some.Some
  ) where

import Data.Bits ((.&.), bit)
import Data.Data
import Data.Type.Equality as Equality
import Data.Void as Void
import Numeric.Natural
import GHC.TypeNats as TypeNats
import Unsafe.Coerce

import Data.Parameterized.Axiom
import Data.Parameterized.NatRepr.Internal
import Data.Parameterized.Some

maxInt :: Natural
maxInt :: Natural
maxInt = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Int)

intValue :: NatRepr n -> Integer
intValue :: forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr n
n = forall a. Integral a => a -> Integer
toInteger (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
n)
{-# INLINE intValue #-}

-- | Return the value of the nat representation.
widthVal :: NatRepr n -> Int
widthVal :: forall (n :: Natural). NatRepr n -> Int
widthVal (NatRepr Natural
i) | Natural
i forall a. Ord a => a -> a -> Bool
<= Natural
maxInt = forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i
                     | Bool
otherwise   = forall a. HasCallStack => [Char] -> a
error ([Char]
"Width is too large: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Natural
i)

withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat :: forall (n :: Natural) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (NatRepr Natural
nVal) KnownNat n => r
v =
  case Natural -> SomeNat
someNatVal Natural
nVal of
    SomeNat (Proxy n
Proxy :: Proxy n') ->
      case forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: n :~: n' of
        n :~: n
Refl -> KnownNat n => r
v

data IsZeroNat n where
  ZeroNat    :: IsZeroNat 0
  NonZeroNat :: IsZeroNat (n+1)

isZeroNat :: NatRepr n -> IsZeroNat n
isZeroNat :: forall (n :: Natural). NatRepr n -> IsZeroNat n
isZeroNat (NatRepr Natural
0) = forall a b. a -> b
unsafeCoerce IsZeroNat 0
ZeroNat
isZeroNat (NatRepr Natural
_) = forall a b. a -> b
unsafeCoerce forall (n :: Natural). IsZeroNat (n + 1)
NonZeroNat

-- | Every nat is either zero or >= 1.
isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 :: forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr n
n =
  case forall (n :: Natural). NatRepr n -> IsZeroNat n
isZeroNat NatRepr n
n of
    IsZeroNat n
ZeroNat    -> forall a b. a -> Either a b
Left forall {k} (a :: k). a :~: a
Refl
    IsZeroNat n
NonZeroNat -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
      -- We have n = m + 1 for some m.
      let
        -- | x <= x + 1
        leqPlus :: forall f x y. ((x + 1) ~ y) => f x ->  LeqProof 1 y
        leqPlus :: forall (f :: Natural -> Type) (x :: Natural) (y :: Natural).
((x + 1) ~ y) =>
f x -> LeqProof 1 y
leqPlus f x
fx =
          case (forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm f x
fx (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) :: x + 1 :~: 1 + x)    of { (x + 1) :~: (1 + x)
Refl ->
          case (forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) f x
fx :: 1+x-x :~: 1) of { ((1 + x) - x) :~: 1
Refl ->
          case (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof (x+1) y)                    of { LeqProof (x + 1) y
LeqProof ->
          case (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof (1+x-x) (y-x))              of { LeqProof ((1 + x) - x) (y - x)
LeqProof ->
            forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 (y-x))
                     (forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
leqSub (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof y y)
                             (forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (forall (f :: Natural -> Type) (z :: Natural).
f z -> LeqProof z (z + 1)
leqSucc (forall {k} (t :: k). Proxy t
Proxy :: Proxy x))
                                       (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof) :: LeqProof x y) :: LeqProof (y - x) y)
          }}}}
      in forall (f :: Natural -> Type) (x :: Natural) (y :: Natural).
((x + 1) ~ y) =>
f x -> LeqProof 1 y
leqPlus (forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
predNat NatRepr n
n)

-- | Decrement a @NatRepr@
decNat :: (1 <= n) => NatRepr n -> NatRepr (n-1)
decNat :: forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat (NatRepr Natural
i) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (Natural
iforall a. Num a => a -> a -> a
-Natural
1)

-- | Get the predecessor of a nat
predNat :: NatRepr (n+1) -> NatRepr n
predNat :: forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
predNat (NatRepr Natural
i) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (Natural
iforall a. Num a => a -> a -> a
-Natural
1)

-- | Increment a @NatRepr@
incNat :: NatRepr n -> NatRepr (n+1)
incNat :: forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat (NatRepr Natural
x) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (Natural
xforall a. Num a => a -> a -> a
+Natural
1)

halfNat :: NatRepr (n+n) -> NatRepr n
halfNat :: forall (n :: Natural). NatRepr (n + n) -> NatRepr n
halfNat (NatRepr Natural
x) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (Natural
x forall a. Integral a => a -> a -> a
`div` Natural
2)

addNat :: NatRepr m -> NatRepr n -> NatRepr (m+n)
addNat :: forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (NatRepr Natural
m) (NatRepr Natural
n) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (Natural
mforall a. Num a => a -> a -> a
+Natural
n)

subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m-n)
subNat :: forall (n :: Natural) (m :: Natural).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
subNat (NatRepr Natural
m) (NatRepr Natural
n) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (Natural
mforall a. Num a => a -> a -> a
-Natural
n)

divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m
divNat :: forall (n :: Natural) (m :: Natural).
(1 <= n) =>
NatRepr (m * n) -> NatRepr n -> NatRepr m
divNat (NatRepr Natural
x) (NatRepr Natural
y) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (forall a. Integral a => a -> a -> a
div Natural
x Natural
y)

withDivModNat :: forall n m a.
                 NatRepr n
              -> NatRepr m
              -> (forall div mod. (n ~ ((div * m) + mod)) =>
                  NatRepr div -> NatRepr mod -> a)
              -> a
withDivModNat :: forall (n :: Natural) (m :: Natural) a.
NatRepr n
-> NatRepr m
-> (forall (div :: Natural) (mod :: Natural).
    (n ~ ((div * m) + mod)) =>
    NatRepr div -> NatRepr mod -> a)
-> a
withDivModNat NatRepr n
n NatRepr m
m forall (div :: Natural) (mod :: Natural).
(n ~ ((div * m) + mod)) =>
NatRepr div -> NatRepr mod -> a
f =
  case ( forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (n :: Natural). Natural -> NatRepr n
NatRepr Natural
divPart), forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (n :: Natural). Natural -> NatRepr n
NatRepr Natural
modPart)) of
     ( Some (NatRepr x
divn :: NatRepr div), Some (NatRepr x
modn :: NatRepr mod) )
       -> case forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom of
            (n :~: ((x * m) + x)
Refl :: (n :~: ((div * m) + mod))) -> forall (div :: Natural) (mod :: Natural).
(n ~ ((div * m) + mod)) =>
NatRepr div -> NatRepr mod -> a
f NatRepr x
divn NatRepr x
modn
  where
    (Natural
divPart, Natural
modPart) = forall a. Integral a => a -> a -> (a, a)
divMod (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
n) (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr m
m)

natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply :: forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply (NatRepr Natural
n) (NatRepr Natural
m) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (Natural
n forall a. Num a => a -> a -> a
* Natural
m)

------------------------------------------------------------------------
-- Operations for using NatRepr as a bitwidth.

-- | Return minimum unsigned value for bitvector with given width (always 0).
minUnsigned :: NatRepr w -> Integer
minUnsigned :: forall (n :: Natural). NatRepr n -> Integer
minUnsigned NatRepr w
_ = Integer
0

-- | Return maximum unsigned value for bitvector with given width.
maxUnsigned :: NatRepr w -> Integer
maxUnsigned :: forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr w
w = forall a. Bits a => Int -> a
bit (forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr w
w) forall a. Num a => a -> a -> a
- Integer
1

-- | Return minimum value for bitvector in two's complement with given width.
minSigned :: (1 <= w) => NatRepr w -> Integer
minSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w = forall a. Num a => a -> a
negate (forall a. Bits a => Int -> a
bit (forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr w
w forall a. Num a => a -> a -> a
- Int
1))

-- | Return maximum value for bitvector in two's complement with given width.
maxSigned :: (1 <= w) => NatRepr w -> Integer
maxSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w = forall a. Bits a => Int -> a
bit (forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr w
w forall a. Num a => a -> a -> a
- Int
1) forall a. Num a => a -> a -> a
- Integer
1

-- | @toUnsigned w i@ maps @i@ to a @i `mod` 2^w@.
toUnsigned :: NatRepr w -> Integer -> Integer
toUnsigned :: forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr w
w Integer
i = forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr w
w forall a. Bits a => a -> a -> a
.&. Integer
i

-- | @toSigned w i@ interprets the least-significant @w@ bits in @i@ as a
-- signed number in two's complement notation and returns that value.
toSigned :: (1 <= w) => NatRepr w -> Integer -> Integer
toSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
i0
    | Integer
i forall a. Ord a => a -> a -> Bool
> forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w = Integer
i forall a. Num a => a -> a -> a
- forall a. Bits a => Int -> a
bit (forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr w
w)
    | Bool
otherwise       = Integer
i
  where i :: Integer
i = Integer
i0 forall a. Bits a => a -> a -> a
.&. forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr w
w

-- | @unsignedClamp w i@ rounds @i@ to the nearest value between
-- @0@ and @2^w-1@ (inclusive).
unsignedClamp :: NatRepr w -> Integer -> Integer
unsignedClamp :: forall (w :: Natural). NatRepr w -> Integer -> Integer
unsignedClamp NatRepr w
w Integer
i
  | Integer
i forall a. Ord a => a -> a -> Bool
< forall (n :: Natural). NatRepr n -> Integer
minUnsigned NatRepr w
w = forall (n :: Natural). NatRepr n -> Integer
minUnsigned NatRepr w
w
  | Integer
i forall a. Ord a => a -> a -> Bool
> forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr w
w = forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr w
w
  | Bool
otherwise         = Integer
i

-- | @signedClamp w i@ rounds @i@ to the nearest value between
-- @-2^(w-1)@ and @2^(w-1)-1@ (inclusive).
signedClamp :: (1 <= w) => NatRepr w -> Integer -> Integer
signedClamp :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
signedClamp NatRepr w
w Integer
i
  | Integer
i forall a. Ord a => a -> a -> Bool
< forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w = forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w
  | Integer
i forall a. Ord a => a -> a -> Bool
> forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w = forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w
  | Bool
otherwise       = Integer
i

------------------------------------------------------------------------
-- Some NatRepr

-- | Turn an @Integral@ value into a @NatRepr@.  Returns @Nothing@
--   if the given value is negative.
someNat :: Integral a => a -> Maybe (Some NatRepr)
someNat :: forall a. Integral a => a -> Maybe (Some NatRepr)
someNat a
x | a
x forall a. Ord a => a -> a -> Bool
>= a
0 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Natural). Natural -> NatRepr n
NatRepr forall a b. (a -> b) -> a -> b
$! forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x
someNat a
_ = forall a. Maybe a
Nothing

-- | Turn a @Natural@ into the corresponding @NatRepr@
mkNatRepr :: Natural -> Some NatRepr
mkNatRepr :: Natural -> Some NatRepr
mkNatRepr Natural
n = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (n :: Natural). Natural -> NatRepr n
NatRepr Natural
n)

-- | Return the maximum of two nat representations.
maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
maxNat :: forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Some NatRepr
maxNat NatRepr m
x NatRepr n
y
  | forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr m
x forall a. Ord a => a -> a -> Bool
>= forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
y = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some NatRepr m
x
  | Bool
otherwise = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some NatRepr n
y

------------------------------------------------------------------------
-- Arithmetic

-- | Produce evidence that @+@ is commutative.
plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m
plusComm :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm f m
_ g n
_ = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom

-- | Produce evidence that @+@ is associative.
plusAssoc :: forall f m g n h o . f m -> g n -> h o -> m+(n+o) :~: (m+n)+o
plusAssoc :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural) (h :: Natural -> Type) (o :: Natural).
f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)
plusAssoc f m
_ g n
_ h o
_ = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom

-- | Produce evidence that @*@ is commutative.
mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)
mulComm :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> (m * n) :~: (n * m)
mulComm f m
_ g n
_ = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom

mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)
mul2Plus :: forall (f :: Natural -> Type) (n :: Natural).
f n -> (n + n) :~: (2 * n)
mul2Plus f n
n = case forall (n :: Natural) (m :: Natural) (p :: Natural)
       (f :: Natural -> Type) (g :: Natural -> Type)
       (h :: Natural -> Type).
f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
addMulDistribRight (forall {k} (t :: k). Proxy t
Proxy @1) (forall {k} (t :: k). Proxy t
Proxy @1) f n
n of
               ((1 * n) + (1 * n)) :~: ((1 + 1) * n)
Refl -> forall {k} (a :: k). a :~: a
Refl

-- | Cancel an add followed by a subtract
plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m
plusMinusCancel :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel f m
_ g n
_ = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom

minusPlusCancel :: forall f m g n . (n <= m) => f m -> g n -> (m - n) + n :~: m
minusPlusCancel :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel f m
_ g n
_ = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom

addMulDistribRight :: forall n m p f g h. f n -> g m -> h p
                    -> ((n * p) + (m * p)) :~: ((n + m) * p)
addMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural)
       (f :: Natural -> Type) (g :: Natural -> Type)
       (h :: Natural -> Type).
f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
addMulDistribRight f n
_n g m
_m h p
_p = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom



withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p
                    -> ( (((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a
withAddMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural)
       (f :: Natural -> Type) (g :: Natural -> Type)
       (h :: Natural -> Type) a.
f n
-> g m -> h p -> ((((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a
withAddMulDistribRight f n
n g m
m h p
p (((n * p) + (m * p)) ~ ((n + m) * p)) => a
f =
  case forall (n :: Natural) (m :: Natural) (p :: Natural)
       (f :: Natural -> Type) (g :: Natural -> Type)
       (h :: Natural -> Type).
f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
addMulDistribRight f n
n g m
m h p
p of
    ((n * p) + (m * p)) :~: ((n + m) * p)
Refl -> (((n * p) + (m * p)) ~ ((n + m) * p)) => a
f

withSubMulDistribRight :: forall n m p f g h a. (m <= n) => f n -> g m -> h p
                    -> ( (((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a
withSubMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural)
       (f :: Natural -> Type) (g :: Natural -> Type)
       (h :: Natural -> Type) a.
(m <= n) =>
f n
-> g m -> h p -> ((((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a
withSubMulDistribRight f n
_n g m
_m h p
_p (((n * p) - (m * p)) ~ ((n - m) * p)) => a
f =
  case forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom of
    (((n * p) - (m * p)) :~: ((n - m) * p)
Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> (((n * p) - (m * p)) ~ ((n - m) * p)) => a
f

------------------------------------------------------------------------
-- LeqProof

-- | @LeqProof m n@ is a type whose values are only inhabited when @m@
-- is less than or equal to @n@.
data LeqProof (m :: Nat) (n :: Nat) where
  LeqProof :: (m <= n) => LeqProof m n

-- | (<=) is a decidable relation on nats.
decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) ((LeqProof a b) -> Void)
decideLeq :: forall (a :: Natural) (b :: Natural).
NatRepr a
-> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)
decideLeq (NatRepr Natural
m) (NatRepr Natural
n)
  | Natural
m forall a. Ord a => a -> a -> Bool
<= Natural
n    = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0)
  | Bool
otherwise = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
      \LeqProof a b
x -> seq :: forall a b. a -> b -> b
seq LeqProof a b
x forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible [decidable <= on NatRepr]"

testStrictLeq :: forall m n
               . (m <= n)
              => NatRepr m
              -> NatRepr n
              -> Either (LeqProof (m+1) n) (m :~: n)
testStrictLeq :: forall (m :: Natural) (n :: Natural).
(m <= n) =>
NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
testStrictLeq (NatRepr Natural
m) (NatRepr Natural
n)
  | Natural
m forall a. Ord a => a -> a -> Bool
< Natural
n = forall a b. a -> Either a b
Left (forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0))
  | Bool
otherwise = forall a b. b -> Either a b
Right forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom
{-# NOINLINE testStrictLeq #-}

-- As for NatComparison above, but works with LeqProof
data NatCases m n where
  -- First number is less than second.
  NatCaseLT :: LeqProof (m+1) n -> NatCases m n
  NatCaseEQ :: NatCases m m
  -- First number is greater than second.
  NatCaseGT :: LeqProof (n+1) m -> NatCases m n

testNatCases ::  forall m n
              . NatRepr m
             -> NatRepr n
             -> NatCases m n
testNatCases :: forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr m
m NatRepr n
n =
  case forall a. Ord a => a -> a -> Ordering
compare (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr m
m) (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
n) of
    Ordering
LT -> forall (m :: Natural) (n :: Natural).
LeqProof (m + 1) n -> NatCases m n
NatCaseLT (forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0))
    Ordering
EQ -> forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ (forall (m :: Natural). NatCases m m
NatCaseEQ :: NatCases m m)
    Ordering
GT -> forall (n :: Natural) (m :: Natural).
LeqProof (n + 1) m -> NatCases m n
NatCaseGT (forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0))
{-# NOINLINE testNatCases #-}

-- | The strict order (\<), defined by n \< m \<-> n + 1 \<= m, is irreflexive.
lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void
lessThanIrreflexive :: forall (f :: Natural -> Type) (a :: Natural).
f a -> LeqProof (1 + a) a -> Void
lessThanIrreflexive f a
a LeqProof (1 + a) a
prf =
  let prf1 :: LeqProof (1 + a - a) (a - a)
      prf1 :: LeqProof ((1 + a) - a) (a - a)
prf1 = forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
leqSub2 LeqProof (1 + a) a
prf (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof a a)
      prf2 :: 1 + a - a :~: 1
      prf2 :: ((1 + a) - a) :~: 1
prf2 = forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) f a
a
      prf3 :: a - a :~: 0
      prf3 :: (a - a) :~: 0
prf3 = forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0) f a
a
      prf4 :: LeqProof 1 0
      prf4 :: LeqProof 1 0
prf4 = case ((1 + a) - a) :~: 1
prf2 of ((1 + a) - a) :~: 1
Refl -> case (a - a) :~: 0
prf3 of { (a - a) :~: 0
Refl -> LeqProof ((1 + a) - a) (a - a)
prf1 }
  in case LeqProof 1 0
prf4 of {}

-- | The strict order on the naturals is asymmetric
lessThanAsymmetric :: forall m f n
                    . LeqProof (n+1) m
                   -> LeqProof (m+1) n
                   -> f n
                   -> Void
lessThanAsymmetric :: forall (m :: Natural) (f :: Natural -> Type) (n :: Natural).
LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void
lessThanAsymmetric LeqProof (n + 1) m
nLTm LeqProof (m + 1) n
mLTn f n
n =
  case forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm f n
n (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) :: n + 1 :~: 1 + n of { (n + 1) :~: (1 + n)
Refl ->
  case forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof m m) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) :: LeqProof m (m+1) of
    LeqProof m (m + 1)
LeqProof -> forall (f :: Natural -> Type) (a :: Natural).
f a -> LeqProof (1 + a) a -> Void
lessThanIrreflexive f n
n forall a b. (a -> b) -> a -> b
$ forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans LeqProof (n + 1) m
nLTm forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof) LeqProof (m + 1) n
mLTn
  }

-- | @x `testLeq` y@ checks whether @x@ is less than or equal to @y@.
testLeq :: forall m n . NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq :: forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr Natural
m) (NatRepr Natural
n)
   | Natural
m forall a. Ord a => a -> a -> Bool
<= Natural
n    = forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0))
   | Bool
otherwise = forall a. Maybe a
Nothing
{-# NOINLINE testLeq #-}

-- | Apply reflexivity to LeqProof
leqRefl :: forall f n . f n -> LeqProof n n
leqRefl :: forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl f n
_ = forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof

leqSucc :: forall f z. f z -> LeqProof z (z + 1)
leqSucc :: forall (f :: Natural -> Type) (z :: Natural).
f z -> LeqProof z (z + 1)
leqSucc f z
fz = forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl f z
fz :: LeqProof z z) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)

-- | Apply transitivity to LeqProof
leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans :: forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans LeqProof m n
LeqProof LeqProof n p
LeqProof = forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0)
{-# NOINLINE leqTrans #-}

-- | Zero is less than or equal to any 'Nat'.
leqZero :: LeqProof 0 n
leqZero :: forall (n :: Natural). LeqProof 0 n
leqZero = forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0)

-- | Add both sides of two inequalities
leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 :: forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof x_l x_h
x LeqProof y_l y_h
y = seq :: forall a b. a -> b -> b
seq LeqProof x_l x_h
x forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq LeqProof y_l y_h
y forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0)
{-# NOINLINE leqAdd2 #-}

-- | Subtract sides of two inequalities.
leqSub2 :: LeqProof x_l x_h
        -> LeqProof y_l y_h
        -> LeqProof (x_l-y_h) (x_h-y_l)
leqSub2 :: forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
leqSub2 LeqProof x_l x_h
LeqProof LeqProof y_l y_h
LeqProof = forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0)
{-# NOINLINE leqSub2 #-}

------------------------------------------------------------------------
-- LeqProof combinators

-- | Create a leqProof using two proxies
leqProof :: (m <= n) => f m -> g n -> LeqProof m n
leqProof :: forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof f m
_ g n
_ = forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof

withLeqProof :: LeqProof m n -> ((m <= n) => a) -> a
withLeqProof :: forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof LeqProof m n
p (m <= n) => a
a =
  case LeqProof m n
p of
    LeqProof m n
LeqProof -> (m <= n) => a
a

-- | Test whether natural number is positive.
isPosNat :: NatRepr n -> Maybe (LeqProof 1 n)
isPosNat :: forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat = forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 1)

-- | Congruence rule for multiplication
leqMulCongr :: LeqProof a x
            -> LeqProof b y
            -> LeqProof (a*b) (x*y)
leqMulCongr :: forall (a :: Natural) (x :: Natural) (b :: Natural) (y :: Natural).
LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
leqMulCongr LeqProof a x
LeqProof LeqProof b y
LeqProof = forall a b. a -> b
unsafeCoerce (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 1)
{-# NOINLINE leqMulCongr #-}

-- | Multiplying two positive numbers results in a positive number.
leqMulPos :: forall p q x y
          .  (1 <= x, 1 <= y)
          => p x
          -> q y
          -> LeqProof 1 (x*y)
leqMulPos :: forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
       (y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos p x
_ q y
_ = forall (a :: Natural) (x :: Natural) (b :: Natural) (y :: Natural).
LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
leqMulCongr (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 x) (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 y)

leqMulMono :: (1 <= x) => p x -> q y -> LeqProof y (x * y)
leqMulMono :: forall (x :: Natural) (p :: Natural -> Type) (q :: Natural -> Type)
       (y :: Natural).
(1 <= x) =>
p x -> q y -> LeqProof y (x * y)
leqMulMono p x
x q y
y = forall (a :: Natural) (x :: Natural) (b :: Natural) (y :: Natural).
LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
leqMulCongr (forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (forall {k} (t :: k). Proxy t
Proxy :: Proxy 1) p x
x) (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl q y
y)

-- | Produce proof that adding a value to the larger element in an LeqProof
-- is larger
leqAdd :: forall f m n p . LeqProof m n -> f p -> LeqProof m (n+p)
leqAdd :: forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof m n
x f p
_ = forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof m n
x (forall (n :: Natural). LeqProof 0 n
leqZero @p)

leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
leqAddPos :: forall (m :: Natural) (n :: Natural) (p :: Natural -> Type)
       (q :: Natural -> Type).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos p m
m q n
n = forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (forall {k} (t :: k). Proxy t
Proxy :: Proxy 1) p m
m) q n
n

-- | Produce proof that subtracting a value from the smaller element is smaller.
leqSub :: forall m n p . LeqProof m n -> LeqProof p m -> LeqProof (m-p) n
leqSub :: forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
leqSub LeqProof m n
x LeqProof p m
_ = forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
leqSub2 LeqProof m n
x (forall (n :: Natural). LeqProof 0 n
leqZero @p)

addIsLeq :: f n -> g m -> LeqProof n (n + m)
addIsLeq :: forall (f :: Natural -> Type) (n :: Natural) (g :: Natural -> Type)
       (m :: Natural).
f n -> g m -> LeqProof n (n + m)
addIsLeq f n
n g m
m = forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl f n
n) g m
m

addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)
addPrefixIsLeq :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> LeqProof n (m + n)
addPrefixIsLeq f m
m g n
n =
  case forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm g n
n f m
m of
    (n + m) :~: (m + n)
Refl -> forall (f :: Natural -> Type) (n :: Natural) (g :: Natural -> Type)
       (m :: Natural).
f n -> g m -> LeqProof n (n + m)
addIsLeq g n
n f m
m

dblPosIsPos :: forall n . LeqProof 1 n -> LeqProof 1 (n+n)
dblPosIsPos :: forall (n :: Natural). LeqProof 1 n -> LeqProof 1 (n + n)
dblPosIsPos LeqProof 1 n
x = forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 n
x forall {k} (t :: k). Proxy t
Proxy

addIsLeqLeft1 :: forall n n' m . LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 :: forall (n :: Natural) (n' :: Natural) (m :: Natural).
LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 LeqProof (n + n') m
p =
    case forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel Proxy n
n Proxy n'
n' of
      ((n + n') - n') :~: n
Refl -> forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
leqSub LeqProof (n + n') m
p LeqProof n' (n + n')
le
  where n :: Proxy n
        n :: Proxy n
n = forall {k} (t :: k). Proxy t
Proxy
        n' :: Proxy n'
        n' :: Proxy n'
n' = forall {k} (t :: k). Proxy t
Proxy
        le :: LeqProof n' (n + n')
        le :: LeqProof n' (n + n')
le = forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> LeqProof n (m + n)
addPrefixIsLeq Proxy n
n Proxy n'
n'

{-# INLINE withAddPrefixLeq #-}
withAddPrefixLeq :: NatRepr n -> NatRepr m -> ((m <= n + m) => a) -> a
withAddPrefixLeq :: forall (n :: Natural) (m :: Natural) a.
NatRepr n -> NatRepr m -> ((m <= (n + m)) => a) -> a
withAddPrefixLeq NatRepr n
n NatRepr m
m = forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> LeqProof n (m + n)
addPrefixIsLeq NatRepr n
n NatRepr m
m)

withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> ((n <= n + m) => NatRepr (n + m) -> a) -> a
withAddLeq :: forall (n :: Natural) (m :: Natural) a.
NatRepr n
-> NatRepr m -> ((n <= (n + m)) => NatRepr (n + m) -> a) -> a
withAddLeq NatRepr n
n NatRepr m
m (n <= (n + m)) => NatRepr (n + m) -> a
f = forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (forall (f :: Natural -> Type) (n :: Natural) (g :: Natural -> Type)
       (m :: Natural).
f n -> g m -> LeqProof n (n + m)
addIsLeq NatRepr n
n NatRepr m
m) ((n <= (n + m)) => NatRepr (n + m) -> a
f (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr n
n NatRepr m
m))

natForEach' :: forall l h a
            . NatRepr l
            -> NatRepr h
            -> (forall n. LeqProof l n -> LeqProof n h -> NatRepr n -> a)
            -> [a]
natForEach' :: forall (l :: Natural) (h :: Natural) a.
NatRepr l
-> NatRepr h
-> (forall (n :: Natural).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a)
-> [a]
natForEach' NatRepr l
l NatRepr h
h forall (n :: Natural).
LeqProof l n -> LeqProof n h -> NatRepr n -> a
f
  | Just LeqProof l h
LeqProof  <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq NatRepr l
l NatRepr h
h =
    let f' :: forall n. LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a
        f' :: forall (n :: Natural).
LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a
f' = \LeqProof (l + 1) n
lp LeqProof n h
hp -> forall (n :: Natural).
LeqProof l n -> LeqProof n h -> NatRepr n -> a
f (forall (n :: Natural) (n' :: Natural) (m :: Natural).
LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 LeqProof (l + 1) n
lp) LeqProof n h
hp
     in forall (n :: Natural).
LeqProof l n -> LeqProof n h -> NatRepr n -> a
f forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof NatRepr l
l forall a. a -> [a] -> [a]
: forall (l :: Natural) (h :: Natural) a.
NatRepr l
-> NatRepr h
-> (forall (n :: Natural).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a)
-> [a]
natForEach' (forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr l
l) NatRepr h
h forall (n :: Natural).
LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a
f'
  | Bool
otherwise             = []

-- | Apply a function to each element in a range; return the list of values
-- obtained.
natForEach :: forall l h a
            . NatRepr l
           -> NatRepr h
           -> (forall n. (l <= n, n <= h) => NatRepr n -> a)
           -> [a]
natForEach :: forall (l :: Natural) (h :: Natural) a.
NatRepr l
-> NatRepr h
-> (forall (n :: Natural). (l <= n, n <= h) => NatRepr n -> a)
-> [a]
natForEach NatRepr l
l NatRepr h
h forall (n :: Natural). (l <= n, n <= h) => NatRepr n -> a
f = forall (l :: Natural) (h :: Natural) a.
NatRepr l
-> NatRepr h
-> (forall (n :: Natural).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a)
-> [a]
natForEach' NatRepr l
l NatRepr h
h (\LeqProof l n
LeqProof LeqProof n h
LeqProof -> forall (n :: Natural). (l <= n, n <= h) => NatRepr n -> a
f)

-- | Apply a function to each element in a range starting at zero;
-- return the list of values obtained.
natFromZero :: forall h a
            . NatRepr h
           -> (forall n. (n <= h) => NatRepr n -> a)
           -> [a]
natFromZero :: forall (h :: Natural) a.
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> a) -> [a]
natFromZero NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> a
f = forall (l :: Natural) (h :: Natural) a.
NatRepr l
-> NatRepr h
-> (forall (n :: Natural). (l <= n, n <= h) => NatRepr n -> a)
-> [a]
natForEach (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0) NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> a
f

-- | Recursor for natural numbeers.
natRec :: forall p f
       .  NatRepr p
       -> f 0 {- ^ base case -}
       -> (forall n. NatRepr n -> f n -> f (n + 1))
       -> f p
natRec :: forall (p :: Natural) (f :: Natural -> Type).
NatRepr p
-> f 0
-> (forall (n :: Natural). NatRepr n -> f n -> f (n + 1))
-> f p
natRec NatRepr p
n f 0
base forall (n :: Natural). NatRepr n -> f n -> f (n + 1)
ind =
  case forall (n :: Natural). NatRepr n -> IsZeroNat n
isZeroNat NatRepr p
n of
    IsZeroNat p
ZeroNat    -> f 0
base
    IsZeroNat p
NonZeroNat -> let n' :: NatRepr n
n' = forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
predNat NatRepr p
n
                  in forall (n :: Natural). NatRepr n -> f n -> f (n + 1)
ind NatRepr n
n' (forall (p :: Natural) (f :: Natural -> Type).
NatRepr p
-> f 0
-> (forall (n :: Natural). NatRepr n -> f n -> f (n + 1))
-> f p
natRec NatRepr n
n' f 0
base forall (n :: Natural). NatRepr n -> f n -> f (n + 1)
ind)

-- | Strong induction variant of the recursor.
natRecStrong :: forall p f
             .  NatRepr p
             -> f 0 {- ^ base case -}
             -> (forall n.
                  NatRepr n ->
                  (forall m. (m <= n) => NatRepr m -> f m) ->
                  f (n + 1)) {- ^ inductive step -}
             -> f p
natRecStrong :: forall (p :: Natural) (f :: Natural -> Type).
NatRepr p
-> f 0
-> (forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f m)
    -> f (n + 1))
-> f p
natRecStrong NatRepr p
p f 0
base forall (n :: Natural).
NatRepr n
-> (forall (m :: Natural). (m <= n) => NatRepr m -> f m)
-> f (n + 1)
ind = forall (p' :: Natural) (f' :: Natural -> Type).
f' 0
-> (forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1))
-> NatRepr p'
-> f' p'
natRecStrong' f 0
base forall (n :: Natural).
NatRepr n
-> (forall (m :: Natural). (m <= n) => NatRepr m -> f m)
-> f (n + 1)
ind NatRepr p
p
  where -- We can't use use "flip" or some other basic combinator
        -- because type variables can't be instantiated to contain "forall"s.
        natRecStrong' :: forall p' f'
                      .  f' 0 {- ^ base case -}
                      -> (forall n.
                            NatRepr n ->
                            (forall m. (m <= n) => NatRepr m -> f' m) ->
                            f' (n + 1)) {- ^ inductive step -}
                      -> NatRepr p'
                      -> f' p'
        natRecStrong' :: forall (p' :: Natural) (f' :: Natural -> Type).
f' 0
-> (forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1))
-> NatRepr p'
-> f' p'
natRecStrong' f' 0
base' forall (n :: Natural).
NatRepr n
-> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
-> f' (n + 1)
ind' NatRepr p'
n =
          case forall (n :: Natural). NatRepr n -> IsZeroNat n
isZeroNat NatRepr p'
n of
            IsZeroNat p'
ZeroNat    -> f' 0
base'
            IsZeroNat p'
NonZeroNat -> forall (n :: Natural).
NatRepr n
-> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
-> f' (n + 1)
ind' (forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
predNat NatRepr p'
n) (forall (p' :: Natural) (f' :: Natural -> Type).
f' 0
-> (forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1))
-> NatRepr p'
-> f' p'
natRecStrong' f' 0
base' forall (n :: Natural).
NatRepr n
-> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
-> f' (n + 1)
ind')

-- | Bounded recursor for natural numbers.
--
-- If you can prove:
-- - Base case: f 0
-- - Inductive step: if n <= h and (f n) then (f (n + 1))
-- You can conclude: for all n <= h, (f (n + 1)).
natRecBounded :: forall m h f. (m <= h)
              => NatRepr m
              -> NatRepr h
              -> f 0
              -> (forall n. (n <= h) => NatRepr n -> f n -> f (n + 1))
              -> f (m + 1)
natRecBounded :: forall (m :: Natural) (h :: Natural) (f :: Natural -> Type).
(m <= h) =>
NatRepr m
-> NatRepr h
-> f 0
-> (forall (n :: Natural).
    (n <= h) =>
    NatRepr n -> f n -> f (n + 1))
-> f (m + 1)
natRecBounded NatRepr m
m NatRepr h
h f 0
base forall (n :: Natural). (n <= h) => NatRepr n -> f n -> f (n + 1)
indH =
  case forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr m
m of
    Left m :~: 0
Refl      -> forall (n :: Natural). (n <= h) => NatRepr n -> f n -> f (n + 1)
indH (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0) f 0
base
    Right LeqProof 1 m
LeqProof ->
      case forall (a :: Natural) (b :: Natural).
NatRepr a
-> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)
decideLeq NatRepr m
m NatRepr h
h of
        Left LeqProof m h
LeqProof {- :: m <= h -} ->
          let -- Since m is non-zero, it is n + 1 for some n.
              lemma :: LeqProof (m-1) h
              lemma :: LeqProof (m - 1) h
lemma = forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
leqSub (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof m h) (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 m)
          in forall (n :: Natural). (n <= h) => NatRepr n -> f n -> f (n + 1)
indH NatRepr m
m forall a b. (a -> b) -> a -> b
$
            case LeqProof (m - 1) h
lemma of { LeqProof (m - 1) h
LeqProof ->
            case forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr m
m (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) of { ((m - 1) + 1) :~: m
Refl ->
              forall (m :: Natural) (h :: Natural) (f :: Natural -> Type).
(m <= h) =>
NatRepr m
-> NatRepr h
-> f 0
-> (forall (n :: Natural).
    (n <= h) =>
    NatRepr n -> f n -> f (n + 1))
-> f (m + 1)
natRecBounded @(m - 1) @h @f (forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
predNat NatRepr m
m) NatRepr h
h f 0
base forall (n :: Natural). (n <= h) => NatRepr n -> f n -> f (n + 1)
indH
            }}
        Right LeqProof m h -> Void
f {- :: (m <= h) -> Void -} ->
          forall a. Void -> a
absurd forall a b. (a -> b) -> a -> b
$ LeqProof m h -> Void
f (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof m h)

-- | A version of 'natRecBounded' which doesn't require the type index of the
-- result to be greater than @0@ and provides a strict inequality constraint.
natRecStrictlyBounded ::
  forall m f.
  NatRepr m ->
  f 0 ->
  (forall n. (n + 1 <= m) => NatRepr n -> f n -> f (n + 1)) ->
  f m
natRecStrictlyBounded :: forall (m :: Natural) (f :: Natural -> Type).
NatRepr m
-> f 0
-> (forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> f n -> f (n + 1))
-> f m
natRecStrictlyBounded NatRepr m
m f 0
base forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> f n -> f (n + 1)
indH =
  case forall (n :: Natural). NatRepr n -> IsZeroNat n
isZeroNat NatRepr m
m of
    IsZeroNat m
ZeroNat -> f 0
base
    IsZeroNat m
NonZeroNat ->
      case forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
predNat NatRepr m
m of
        (NatRepr n
p :: NatRepr p) ->
          forall (m :: Natural) (h :: Natural) (f :: Natural -> Type).
(m <= h) =>
NatRepr m
-> NatRepr h
-> f 0
-> (forall (n :: Natural).
    (n <= h) =>
    NatRepr n -> f n -> f (n + 1))
-> f (m + 1)
natRecBounded
            NatRepr n
p
            NatRepr n
p
            f 0
base
            (\(NatRepr n
k :: NatRepr n) (f n
v :: f n) ->
              case forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof n p) (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 1) of
                LeqProof (n + 1) (n + 1)
LeqProof -> forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> f n -> f (n + 1)
indH NatRepr n
k f n
v)

mulCancelR ::
  (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
mulCancelR :: forall (c :: Natural) (n1 :: Natural) (n2 :: Natural)
       (f1 :: Natural -> Type) (f2 :: Natural -> Type)
       (f3 :: Natural -> Type).
(1 <= c, (n1 * c) ~ (n2 * c)) =>
f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2
mulCancelR f1 n1
_ f2 n2
_ f3 c
_ = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom

-- | Used in @Vector@
lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)
lemmaMul :: forall (n :: Natural) (p :: Natural -> Type) (w :: Natural)
       (q :: Natural -> Type).
(1 <= n) =>
p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)
lemmaMul p w
_ q n
_ = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom