{-|
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
  , 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
  , 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 = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: Int)

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

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

withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat :: 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 n :~: n
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom :: n :~: n' of
        n :~: n
Refl -> r
KnownNat n => r
v

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

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

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

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

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

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

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

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

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

divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m
divNat :: NatRepr (m * n) -> NatRepr n -> NatRepr m
divNat (NatRepr Natural
x) (NatRepr Natural
y) = Natural -> NatRepr m
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Natural -> Natural -> Natural
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 :: NatRepr n
-> NatRepr m
-> (forall (div :: Nat) (mod :: Nat).
    (n ~ ((div * m) + mod)) =>
    NatRepr div -> NatRepr mod -> a)
-> a
withDivModNat NatRepr n
n NatRepr m
m forall (div :: Nat) (mod :: Nat).
(n ~ ((div * m) + mod)) =>
NatRepr div -> NatRepr mod -> a
f =
  case ( NatRepr Any -> Some NatRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Natural -> NatRepr Any
forall (n :: Nat). Natural -> NatRepr n
NatRepr Natural
divPart), NatRepr Any -> Some NatRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Natural -> NatRepr Any
forall (n :: Nat). Natural -> NatRepr n
NatRepr Natural
modPart)) of
     ( Some (NatRepr x
divn :: NatRepr div), Some (NatRepr x
modn :: NatRepr mod) )
       -> case n :~: ((x * m) + x)
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom of
            (Refl :: (n :~: ((div * m) + mod))) -> NatRepr x -> NatRepr x -> a
forall (div :: Nat) (mod :: Nat).
(n ~ ((div * m) + mod)) =>
NatRepr div -> NatRepr mod -> a
f NatRepr x
divn NatRepr x
modn
  where
    (Natural
divPart, Natural
modPart) = Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
divMod (NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr n
n) (NatRepr m -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr m
m)

natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply (NatRepr Natural
n) (NatRepr Natural
m) = Natural -> NatRepr (n * m)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Natural
n Natural -> Natural -> Natural
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 :: NatRepr w -> Integer
minUnsigned NatRepr w
_ = Integer
0

-- | Return maximum unsigned value for bitvector with given width.
maxUnsigned :: NatRepr w -> Integer
maxUnsigned :: NatRepr w -> Integer
maxUnsigned NatRepr w
w = Int -> Integer
forall a. Bits a => Int -> a
bit (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w) Integer -> Integer -> Integer
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 :: NatRepr w -> Integer
minSigned NatRepr w
w = Integer -> Integer
forall a. Num a => a -> a
negate (Int -> Integer
forall a. Bits a => Int -> a
bit (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w Int -> Int -> Int
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 :: NatRepr w -> Integer
maxSigned NatRepr w
w = Int -> Integer
forall a. Bits a => Int -> a
bit (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
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 :: NatRepr w -> Integer -> Integer
toUnsigned NatRepr w
w Integer
i = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w Integer -> Integer -> Integer
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 :: NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
i0
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Int -> Integer
forall a. Bits a => Int -> a
bit (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w)
    | Bool
otherwise       = Integer
i
  where i :: Integer
i = Integer
i0 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> 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 :: NatRepr w -> Integer -> Integer
unsignedClamp NatRepr w
w Integer
i
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
minUnsigned NatRepr w
w = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
minUnsigned NatRepr w
w
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> 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 :: NatRepr w -> Integer -> Integer
signedClamp NatRepr w
w Integer
i
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w = NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w = NatRepr w -> Integer
forall (w :: Nat). (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 :: a -> Maybe (Some NatRepr)
someNat a
x | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 = Some NatRepr -> Maybe (Some NatRepr)
forall a. a -> Maybe a
Just (Some NatRepr -> Maybe (Some NatRepr))
-> (Natural -> Some NatRepr) -> Natural -> Maybe (Some NatRepr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr Any -> Some NatRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (NatRepr Any -> Some NatRepr)
-> (Natural -> NatRepr Any) -> Natural -> Some NatRepr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> NatRepr Any
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Natural -> Maybe (Some NatRepr))
-> Natural -> Maybe (Some NatRepr)
forall a b. (a -> b) -> a -> b
$! a -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x
someNat a
_ = Maybe (Some NatRepr)
forall a. Maybe a
Nothing

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

-- | Return the maximum of two nat representations.
maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
maxNat NatRepr m
x NatRepr n
y
  | NatRepr m -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr m
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr n
y = NatRepr m -> Some NatRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some NatRepr m
x
  | Bool
otherwise = NatRepr n -> Some NatRepr
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 :: f m -> g n -> (m + n) :~: (n + m)
plusComm f m
_ g n
_ = (m + n) :~: (n + m)
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 :: f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)
plusAssoc f m
_ g n
_ h o
_ = (m + (n + o)) :~: ((m + n) + 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 :: f m -> g n -> (m * n) :~: (n * m)
mulComm f m
_ g n
_ = (m * n) :~: (n * m)
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom

mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)
mul2Plus :: f n -> (n + n) :~: (2 * n)
mul2Plus f n
n = case Proxy 1 -> Proxy 1 -> f n -> ((1 * n) + (1 * n)) :~: ((1 + 1) * n)
forall (n :: Nat) (m :: Nat) (p :: Nat) (f :: Nat -> Type)
       (g :: Nat -> Type) (h :: Nat -> Type).
f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
addMulDistribRight (Proxy 1
forall k (t :: k). Proxy t
Proxy @1) (Proxy 1
forall k (t :: k). Proxy t
Proxy @1) f n
n of
               ((1 * n) + (1 * n)) :~: ((1 + 1) * n)
Refl -> (n + n) :~: (2 * n)
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 :: f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel f m
_ g n
_ = ((m + n) - n) :~: m
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 :: f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel f m
_ g n
_ = ((m - n) + n) :~: m
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 :: f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
addMulDistribRight f n
_n g m
_m h p
_p = ((n * p) + (m * p)) :~: ((n + m) * 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 :: 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 f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
forall (n :: Nat) (m :: Nat) (p :: Nat) (f :: Nat -> Type)
       (g :: Nat -> Type) (h :: Nat -> 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 -> a
(((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 :: 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 ((n * p) - (m * p)) :~: ((n - m) * p)
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom of
    (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> a
(((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 :: NatRepr a
-> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)
decideLeq (NatRepr Natural
m) (NatRepr Natural
n)
  | Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
n    = LeqProof a b -> Either (LeqProof a b) (LeqProof a b -> Void)
forall a b. a -> Either a b
Left (LeqProof a b -> Either (LeqProof a b) (LeqProof a b -> Void))
-> LeqProof a b -> Either (LeqProof a b) (LeqProof a b -> Void)
forall a b. (a -> b) -> a -> b
$ LeqProof 0 0 -> LeqProof a b
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0)
  | Bool
otherwise = (LeqProof a b -> Void)
-> Either (LeqProof a b) (LeqProof a b -> Void)
forall a b. b -> Either a b
Right ((LeqProof a b -> Void)
 -> Either (LeqProof a b) (LeqProof a b -> Void))
-> (LeqProof a b -> Void)
-> Either (LeqProof a b) (LeqProof a b -> Void)
forall a b. (a -> b) -> a -> b
$
      \LeqProof a b
x -> LeqProof a b -> Void -> Void
seq LeqProof a b
x (Void -> Void) -> Void -> Void
forall a b. (a -> b) -> a -> b
$ [Char] -> Void
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 :: NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
testStrictLeq (NatRepr Natural
m) (NatRepr Natural
n)
  | Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n = LeqProof (m + 1) n -> Either (LeqProof (m + 1) n) (m :~: n)
forall a b. a -> Either a b
Left (LeqProof 0 0 -> LeqProof (m + 1) n
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0))
  | Bool
otherwise = (m :~: n) -> Either (LeqProof (m + 1) n) (m :~: n)
forall a b. b -> Either a b
Right m :~: n
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 :: NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr m
m NatRepr n
n =
  case Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NatRepr m -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr m
m) (NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr n
n) of
    Ordering
LT -> LeqProof (m + 1) n -> NatCases m n
forall (m :: Nat) (n :: Nat). LeqProof (m + 1) n -> NatCases m n
NatCaseLT (LeqProof 0 0 -> LeqProof (m + 1) n
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0))
    Ordering
EQ -> NatCases m m -> NatCases m n
forall a b. a -> b
unsafeCoerce (NatCases m m -> NatCases m n) -> NatCases m m -> NatCases m n
forall a b. (a -> b) -> a -> b
$ (NatCases m m
forall (m :: Nat). NatCases m m
NatCaseEQ :: NatCases m m)
    Ordering
GT -> LeqProof (n + 1) m -> NatCases m n
forall (n :: Nat) (m :: Nat). LeqProof (n + 1) m -> NatCases m n
NatCaseGT (LeqProof 0 0 -> LeqProof (n + 1) m
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (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 :: 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 = LeqProof (1 + a) a
-> LeqProof a a -> LeqProof ((1 + a) - a) (a - a)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
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 (LeqProof a a
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof a a)
      prf2 :: 1 + a - a :~: 1
      prf2 :: ((1 + a) - a) :~: 1
prf2 = NatRepr 1 -> f a -> ((1 + a) - a) :~: 1
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) f a
a
      prf3 :: a - a :~: 0
      prf3 :: (a - a) :~: 0
prf3 = NatRepr 0 -> f a -> ((0 + a) - a) :~: 0
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel (KnownNat 0 => NatRepr 0
forall (n :: Nat). 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 0
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 :: 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 f n -> NatRepr 1 -> (n + 1) :~: (1 + n)
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
f m -> g n -> (m + n) :~: (n + m)
plusComm f n
n (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) :: n + 1 :~: 1 + n of { (n + 1) :~: (1 + n)
Refl ->
  case LeqProof m m -> NatRepr 1 -> LeqProof m (m + 1)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (LeqProof m m
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof m m) (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) :: LeqProof m (m+1) of
    LeqProof m (m + 1)
LeqProof -> f n -> LeqProof (1 + n) n -> Void
forall (f :: Nat -> Type) (a :: Nat).
f a -> LeqProof (1 + a) a -> Void
lessThanIrreflexive f n
n (LeqProof (1 + n) n -> Void) -> LeqProof (1 + n) n -> Void
forall a b. (a -> b) -> a -> b
$ LeqProof (n + 1) (m + 1)
-> LeqProof (m + 1) n -> LeqProof (n + 1) n
forall (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (LeqProof (n + 1) m
-> LeqProof m (m + 1) -> LeqProof (n + 1) (m + 1)
forall (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans LeqProof (n + 1) m
nLTm LeqProof m (m + 1)
forall (m :: Nat) (n :: Nat). (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 :: NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr Natural
m) (NatRepr Natural
n)
   | Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
n    = LeqProof m n -> Maybe (LeqProof m n)
forall a. a -> Maybe a
Just (LeqProof 0 0 -> LeqProof m n
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof 0 0))
   | Bool
otherwise = Maybe (LeqProof m n)
forall a. Maybe a
Nothing
{-# NOINLINE testLeq #-}

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

-- | Apply transitivity to LeqProof
leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans LeqProof m n
LeqProof LeqProof n p
LeqProof = LeqProof 0 0 -> LeqProof m p
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (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 :: LeqProof 0 n
leqZero = LeqProof 0 0 -> LeqProof 0 n
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (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 :: 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 = LeqProof x_l x_h
-> LeqProof (x_l + y_l) (x_h + y_h)
-> LeqProof (x_l + y_l) (x_h + y_h)
seq LeqProof x_l x_h
x (LeqProof (x_l + y_l) (x_h + y_h)
 -> LeqProof (x_l + y_l) (x_h + y_h))
-> LeqProof (x_l + y_l) (x_h + y_h)
-> LeqProof (x_l + y_l) (x_h + y_h)
forall a b. (a -> b) -> a -> b
$ LeqProof y_l y_h
-> LeqProof (x_l + y_l) (x_h + y_h)
-> LeqProof (x_l + y_l) (x_h + y_h)
seq LeqProof y_l y_h
y (LeqProof (x_l + y_l) (x_h + y_h)
 -> LeqProof (x_l + y_l) (x_h + y_h))
-> LeqProof (x_l + y_l) (x_h + y_h)
-> LeqProof (x_l + y_l) (x_h + y_h)
forall a b. (a -> b) -> a -> b
$ LeqProof 0 0 -> LeqProof (x_l + y_l) (x_h + y_h)
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (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 :: 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 = LeqProof 0 0 -> LeqProof (x_l - y_h) (x_h - y_l)
forall a b. a -> b
unsafeCoerce (LeqProof 0 0
forall (m :: Nat) (n :: Nat). (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 :: f m -> g n -> LeqProof m n
leqProof f m
_ g n
_ = LeqProof m n
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof

withLeqProof :: LeqProof m n -> ((m <= n) => a) -> a
withLeqProof :: 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 -> a
(m <= n) => a
a

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

-- | Congruence rule for multiplication
leqMulCongr :: LeqProof a x
            -> LeqProof b y
            -> LeqProof (a*b) (x*y)
leqMulCongr :: LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
leqMulCongr LeqProof a x
LeqProof LeqProof b y
LeqProof = LeqProof 1 1 -> LeqProof (a * b) (x * y)
forall a b. a -> b
unsafeCoerce (LeqProof 1 1
forall (m :: Nat) (n :: Nat). (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 :: p x -> q y -> LeqProof 1 (x * y)
leqMulPos p x
_ q y
_ = LeqProof 1 x -> LeqProof 1 y -> LeqProof (1 * 1) (x * y)
forall (a :: Nat) (x :: Nat) (b :: Nat) (y :: Nat).
LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
leqMulCongr (LeqProof 1 x
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 x) (LeqProof 1 y
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 y)

leqMulMono :: (1 <= x) => p x -> q y -> LeqProof y (x * y)
leqMulMono :: p x -> q y -> LeqProof y (x * y)
leqMulMono p x
x q y
y = LeqProof 1 x -> LeqProof y y -> LeqProof (1 * y) (x * y)
forall (a :: Nat) (x :: Nat) (b :: Nat) (y :: Nat).
LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
leqMulCongr (Proxy 1 -> p x -> LeqProof 1 x
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (Proxy 1
forall k (t :: k). Proxy t
Proxy :: Proxy 1) p x
x) (q y -> LeqProof y y
forall (f :: Nat -> Type) (n :: Nat). 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 :: LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof m n
x f p
_ = LeqProof m n -> LeqProof 0 p -> LeqProof (m + 0) (n + p)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof m n
x (LeqProof 0 p
forall (n :: Nat). LeqProof 0 n
leqZero @p)

leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
leqAddPos :: p m -> q n -> LeqProof 1 (m + n)
leqAddPos p m
m q n
n = LeqProof 1 m -> q n -> LeqProof 1 (m + n)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (Proxy 1 -> p m -> LeqProof 1 m
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (Proxy 1
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 :: LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
leqSub LeqProof m n
x LeqProof p m
_ = LeqProof m n -> LeqProof 0 p -> LeqProof (m - p) (n - 0)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
leqSub2 LeqProof m n
x (LeqProof 0 p
forall (n :: Nat). LeqProof 0 n
leqZero @p)

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

addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)
addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)
addPrefixIsLeq f m
m g n
n =
  case g n -> f m -> (n + m) :~: (m + n)
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
f m -> g n -> (m + n) :~: (n + m)
plusComm g n
n f m
m of
    (n + m) :~: (m + n)
Refl -> g n -> f m -> LeqProof n (n + m)
forall (f :: Nat -> Type) (n :: Nat) (g :: Nat -> Type) (m :: Nat).
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 :: LeqProof 1 n -> LeqProof 1 (n + n)
dblPosIsPos LeqProof 1 n
x = LeqProof 1 n -> Proxy n -> LeqProof 1 (n + n)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 n
x Proxy n
forall k (t :: k). Proxy t
Proxy

addIsLeqLeft1 :: forall n n' m . LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 :: LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 LeqProof (n + n') m
p =
    case Proxy n -> Proxy n' -> ((n + n') - n') :~: n
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel Proxy n
n Proxy n'
n' of
      ((n + n') - n') :~: n
Refl -> LeqProof (n + n') m
-> LeqProof n' (n + n') -> LeqProof ((n + n') - n') m
forall (m :: Nat) (n :: Nat) (p :: Nat).
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 = Proxy n
forall k (t :: k). Proxy t
Proxy
        n' :: Proxy n'
        n' :: Proxy n'
n' = Proxy n'
forall k (t :: k). Proxy t
Proxy
        le :: LeqProof n' (n + n')
        le :: LeqProof n' (n + n')
le = Proxy n -> Proxy n' -> LeqProof n' (n + n')
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
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 :: NatRepr n -> NatRepr m -> ((m <= (n + m)) => a) -> a
withAddPrefixLeq NatRepr n
n NatRepr m
m = LeqProof m (n + m) -> ((m <= (n + m)) => a) -> a
forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr n -> NatRepr m -> LeqProof m (n + m)
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
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 :: 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 = LeqProof n (n + m) -> ((n <= (n + m)) => a) -> a
forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr n -> NatRepr m -> LeqProof n (n + m)
forall (f :: Nat -> Type) (n :: Nat) (g :: Nat -> Type) (m :: Nat).
f n -> g m -> LeqProof n (n + m)
addIsLeq NatRepr n
n NatRepr m
m) ((n <= (n + m)) => NatRepr (n + m) -> a
NatRepr (n + m) -> a
f (NatRepr n -> NatRepr m -> NatRepr (n + m)
forall (m :: Nat) (n :: Nat).
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' :: NatRepr l
-> NatRepr h
-> (forall (n :: Nat).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a)
-> [a]
natForEach' NatRepr l
l NatRepr h
h forall (n :: Nat). LeqProof l n -> LeqProof n h -> NatRepr n -> a
f
  | Just LeqProof l h
LeqProof  <- NatRepr l -> NatRepr h -> Maybe (LeqProof l h)
forall (m :: Nat) (n :: Nat).
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' :: LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a
f' = \LeqProof (l + 1) n
lp LeqProof n h
hp -> LeqProof l n -> LeqProof n h -> NatRepr n -> a
forall (n :: Nat). LeqProof l n -> LeqProof n h -> NatRepr n -> a
f (LeqProof (l + 1) n -> LeqProof l n
forall (n :: Nat) (n' :: Nat) (m :: Nat).
LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 LeqProof (l + 1) n
lp) LeqProof n h
hp
     in LeqProof l l -> LeqProof l h -> NatRepr l -> a
forall (n :: Nat). LeqProof l n -> LeqProof n h -> NatRepr n -> a
f LeqProof l l
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof LeqProof l h
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof NatRepr l
l a -> [a] -> [a]
forall a. a -> [a] -> [a]
: NatRepr (l + 1)
-> NatRepr h
-> (forall (n :: Nat).
    LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a)
-> [a]
forall (l :: Nat) (h :: Nat) a.
NatRepr l
-> NatRepr h
-> (forall (n :: Nat).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a)
-> [a]
natForEach' (NatRepr l -> NatRepr (l + 1)
forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
incNat NatRepr l
l) NatRepr h
h forall (n :: Nat).
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 :: NatRepr l
-> NatRepr h
-> (forall (n :: Nat). (l <= n, n <= h) => NatRepr n -> a)
-> [a]
natForEach NatRepr l
l NatRepr h
h forall (n :: Nat). (l <= n, n <= h) => NatRepr n -> a
f = NatRepr l
-> NatRepr h
-> (forall (n :: Nat).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a)
-> [a]
forall (l :: Nat) (h :: Nat) a.
NatRepr l
-> NatRepr h
-> (forall (n :: Nat).
    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 -> NatRepr n -> a
forall (n :: Nat). (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 :: NatRepr h -> (forall (n :: Nat). (n <= h) => NatRepr n -> a) -> [a]
natFromZero NatRepr h
h forall (n :: Nat). (n <= h) => NatRepr n -> a
f = NatRepr 0
-> NatRepr h
-> (forall (n :: Nat). (0 <= n, n <= h) => NatRepr n -> a)
-> [a]
forall (l :: Nat) (h :: Nat) a.
NatRepr l
-> NatRepr h
-> (forall (n :: Nat). (l <= n, n <= h) => NatRepr n -> a)
-> [a]
natForEach (KnownNat 0 => NatRepr 0
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @0) NatRepr h
h forall (n :: Nat). (n <= h) => NatRepr n -> a
forall (n :: Nat). (0 <= n, 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 :: NatRepr p
-> f 0 -> (forall (n :: Nat). NatRepr n -> f n -> f (n + 1)) -> f p
natRec NatRepr p
n f 0
base forall (n :: Nat). NatRepr n -> f n -> f (n + 1)
ind =
  case NatRepr p -> IsZeroNat p
forall (n :: Nat). NatRepr n -> IsZeroNat n
isZeroNat NatRepr p
n of
    IsZeroNat p
ZeroNat    -> f p
f 0
base
    IsZeroNat p
NonZeroNat -> let n' :: NatRepr n
n' = NatRepr (n + 1) -> NatRepr n
forall (n :: Nat). NatRepr (n + 1) -> NatRepr n
predNat NatRepr p
NatRepr (n + 1)
n
                  in NatRepr n -> f n -> f (n + 1)
forall (n :: Nat). NatRepr n -> f n -> f (n + 1)
ind NatRepr n
n' (NatRepr n
-> f 0 -> (forall (n :: Nat). NatRepr n -> f n -> f (n + 1)) -> f n
forall (p :: Nat) (f :: Nat -> Type).
NatRepr p
-> f 0 -> (forall (n :: Nat). NatRepr n -> f n -> f (n + 1)) -> f p
natRec NatRepr n
n' f 0
base forall (n :: Nat). 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 :: NatRepr p
-> f 0
-> (forall (n :: Nat).
    NatRepr n
    -> (forall (m :: Nat). (m <= n) => NatRepr m -> f m) -> f (n + 1))
-> f p
natRecStrong NatRepr p
p f 0
base forall (n :: Nat).
NatRepr n
-> (forall (m :: Nat). (m <= n) => NatRepr m -> f m) -> f (n + 1)
ind = f 0
-> (forall (n :: Nat).
    NatRepr n
    -> (forall (m :: Nat). (m <= n) => NatRepr m -> f m) -> f (n + 1))
-> NatRepr p
-> f p
forall (p' :: Nat) (f' :: Nat -> Type).
f' 0
-> (forall (n :: Nat).
    NatRepr n
    -> (forall (m :: Nat). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1))
-> NatRepr p'
-> f' p'
natRecStrong' f 0
base forall (n :: Nat).
NatRepr n
-> (forall (m :: Nat). (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' :: f' 0
-> (forall (n :: Nat).
    NatRepr n
    -> (forall (m :: Nat). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1))
-> NatRepr p'
-> f' p'
natRecStrong' f' 0
base' forall (n :: Nat).
NatRepr n
-> (forall (m :: Nat). (m <= n) => NatRepr m -> f' m) -> f' (n + 1)
ind' NatRepr p'
n =
          case NatRepr p' -> IsZeroNat p'
forall (n :: Nat). NatRepr n -> IsZeroNat n
isZeroNat NatRepr p'
n of
            IsZeroNat p'
ZeroNat    -> f' p'
f' 0
base'
            IsZeroNat p'
NonZeroNat -> NatRepr n
-> (forall (m :: Nat). (m <= n) => NatRepr m -> f' m) -> f' (n + 1)
forall (n :: Nat).
NatRepr n
-> (forall (m :: Nat). (m <= n) => NatRepr m -> f' m) -> f' (n + 1)
ind' (NatRepr (n + 1) -> NatRepr n
forall (n :: Nat). NatRepr (n + 1) -> NatRepr n
predNat NatRepr p'
NatRepr (n + 1)
n) (f' 0
-> (forall (n :: Nat).
    NatRepr n
    -> (forall (m :: Nat). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1))
-> NatRepr m
-> f' m
forall (p' :: Nat) (f' :: Nat -> Type).
f' 0
-> (forall (n :: Nat).
    NatRepr n
    -> (forall (m :: Nat). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1))
-> NatRepr p'
-> f' p'
natRecStrong' f' 0
base' forall (n :: Nat).
NatRepr n
-> (forall (m :: Nat). (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 :: NatRepr m
-> NatRepr h
-> f 0
-> (forall (n :: Nat). (n <= h) => NatRepr n -> f n -> f (n + 1))
-> f (m + 1)
natRecBounded NatRepr m
m NatRepr h
h f 0
base forall (n :: Nat). (n <= h) => NatRepr n -> f n -> f (n + 1)
indH =
  case NatRepr m -> Either (m :~: 0) (LeqProof 1 m)
forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr m
m of
    Left m :~: 0
Refl      -> NatRepr 0 -> f 0 -> f (0 + 1)
forall (n :: Nat). (n <= h) => NatRepr n -> f n -> f (n + 1)
indH (KnownNat 0 => NatRepr 0
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @0) f 0
base
    Right LeqProof 1 m
LeqProof ->
      case NatRepr m
-> NatRepr h -> Either (LeqProof m h) (LeqProof m h -> Void)
forall (a :: Nat) (b :: Nat).
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 = LeqProof m h -> LeqProof 1 m -> LeqProof (m - 1) h
forall (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
leqSub (LeqProof m h
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof m h) (LeqProof 1 m
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 m)
          in NatRepr m -> f m -> f (m + 1)
forall (n :: Nat). (n <= h) => NatRepr n -> f n -> f (n + 1)
indH NatRepr m
m (f m -> f (m + 1)) -> f m -> f (m + 1)
forall a b. (a -> b) -> a -> b
$
            case LeqProof (m - 1) h
lemma of { LeqProof (m - 1) h
LeqProof ->
            case NatRepr m -> NatRepr 1 -> ((m - 1) + 1) :~: m
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr m
m (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) of { ((m - 1) + 1) :~: m
Refl ->
              NatRepr (m - 1)
-> NatRepr h
-> f 0
-> (forall (n :: Nat). (n <= h) => NatRepr n -> f n -> f (n + 1))
-> f ((m - 1) + 1)
forall (m :: Nat) (h :: Nat) (f :: Nat -> Type).
(m <= h) =>
NatRepr m
-> NatRepr h
-> f 0
-> (forall (n :: Nat). (n <= h) => NatRepr n -> f n -> f (n + 1))
-> f (m + 1)
natRecBounded @(m - 1) @h @f (NatRepr ((m - 1) + 1) -> NatRepr (m - 1)
forall (n :: Nat). NatRepr (n + 1) -> NatRepr n
predNat NatRepr m
NatRepr ((m - 1) + 1)
m) NatRepr h
h f 0
base forall (n :: Nat). (n <= h) => NatRepr n -> f n -> f (n + 1)
indH
            }}
        Right LeqProof m h -> Void
f {- :: (m <= h) -> Void -} ->
          Void -> f (m + 1)
forall a. Void -> a
absurd (Void -> f (m + 1)) -> Void -> f (m + 1)
forall a b. (a -> b) -> a -> b
$ LeqProof m h -> Void
f (LeqProof m h
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof :: LeqProof m h)

mulCancelR ::
  (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
mulCancelR :: f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2
mulCancelR f1 n1
_ f2 n2
_ f3 c
_ = n1 :~: n2
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 :: p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)
lemmaMul p w
_ q n
_ = (w + ((n - 1) * w)) :~: (n * w)
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom