{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-|
Copyright        : (c) Galois, Inc 2021

@'Fin' n@ is a finite type with exactly @n@ elements. Essentially, they bundle a
'NatRepr' that has an existentially-quantified type parameter with a proof that
its parameter is less than some fixed natural.

They are useful in combination with types of a fixed size. For example 'Fin' is
used as the index in the 'Data.Functor.WithIndex.FunctorWithIndex' instance for
'Data.Parameterized.Vector'. As another example, a @Map ('Fin' n) a@ is a @Map@
that naturally has a fixed size bound of @n@.
-}
module Data.Parameterized.Fin
  ( Fin
  , mkFin
  , mkFinModN
  , buildFin
  , countFin
  , viewFin
  , finFromNatModN
  , finToNat
  , embed
  , tryEmbed
  , minFin
  , incFin
  , fin0Absurd
  , addFinModN
  , subFinModN
  , mulFinModN
  , negFinModN
  , recipFinModN
  ) where

import Data.Hashable (Hashable(..))
import GHC.TypeNats (KnownNat)
import Numeric.Natural (Natural)

import Data.Parameterized.NatRepr
import Data.Parameterized.Some (Some(..))

-- | The type @'Fin' n@ has exactly @n@ inhabitants.
data Fin n =
  -- GHC 8.6 and 8.4 require parentheses around 'i + 1 <= n'
  forall i. (i + 1 <= n) => Fin { ()
_getFin :: NatRepr i }

instance Eq (Fin n) where
  Fin n
i == :: Fin n -> Fin n -> Bool
== Fin n
j = Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
i Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
j

instance Ord (Fin n) where
  compare :: Fin n -> Fin n -> Ordering
compare Fin n
i Fin n
j = Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
i) (Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
j)

instance Hashable (Fin n) where
  hashWithSalt :: Int -> Fin n -> Int
hashWithSalt Int
salt (Fin NatRepr i
i) = Int -> NatRepr i -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt NatRepr i
i

instance (1 <= n, KnownNat n) => Bounded (Fin n) where
  minBound :: Fin n
minBound = NatRepr 0 -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0)
  maxBound :: Fin n
maxBound =
    case NatRepr n -> NatRepr 1 -> ((n - 1) + 1) :~: n
forall (f :: Natural -> *) (m :: Natural) (g :: Natural -> *)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) of
      ((n - 1) + 1) :~: n
Refl -> NatRepr (n - 1) -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin (NatRepr n -> NatRepr (n - 1)
forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n))

-- | Arithmetic is performed modulo @n@.
instance (1 <= n, KnownNat n) => Num (Fin n) where
  + :: Fin n -> Fin n -> Fin n
(+) = NatRepr n -> Fin n -> Fin n -> Fin n
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> Fin n -> Fin n -> Fin n
addFinModN (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n)
  (-) = NatRepr n -> Fin n -> Fin n -> Fin n
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> Fin n -> Fin n -> Fin n
subFinModN (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n)
  * :: Fin n -> Fin n -> Fin n
(*) = NatRepr n -> Fin n -> Fin n -> Fin n
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> Fin n -> Fin n -> Fin n
mulFinModN (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n)
  negate :: Fin n -> Fin n
negate = NatRepr n -> Fin n -> Fin n
forall (n :: Natural). (1 <= n) => NatRepr n -> Fin n -> Fin n
negFinModN (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n)

  -- | We consider all Fin values to be non-negative. Therefore, this always
  -- returns the input unchanged.
  abs :: Fin n -> Fin n
abs = Fin n -> Fin n
forall a. a -> a
id

  -- | We consider all Fin values to be non-negative. Therefore, this always
  -- returns either 'minFin' (i.e., zero) or @'mkFinModN' n (knownNat \@1)@
  -- (i.e., one). Note that in the degenerate case of @'Fin' 1@, these values
  -- will be equal to each other.
  signum :: Fin n -> Fin n
signum Fin n
f
    | Fin n
f Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
== Fin n
forall (n :: Natural). (1 <= n) => Fin n
minFin
    = Fin n
f
    | Bool
otherwise
    = NatRepr n -> NatRepr 1 -> Fin n
forall (n :: Natural) (i :: Natural).
(1 <= n) =>
NatRepr n -> NatRepr i -> Fin n
mkFinModN (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)

  -- | Negative integers are negated, reduced modulo @n@, and then negated
  -- again using 'negFinModN'.
  fromInteger :: Integer -> Fin n
fromInteger Integer
i
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
    = NatRepr n -> Natural -> Fin n
forall (n :: Natural). (1 <= n) => NatRepr n -> Natural -> Fin n
finFromNatModN NatRepr n
n (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i)
    | Bool
otherwise
    = NatRepr n -> Fin n -> Fin n
forall (n :: Natural). (1 <= n) => NatRepr n -> Fin n -> Fin n
negFinModN NatRepr n
n (NatRepr n -> Natural -> Fin n
forall (n :: Natural). (1 <= n) => NatRepr n -> Natural -> Fin n
finFromNatModN NatRepr n
n (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)))
    where
      n :: NatRepr n
n = forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n

-- Equivalent to what a derived Show instance would be, except that we
-- intentionally do not print out the (non-exported) _getFin field name.
instance Show (Fin n) where
  showsPrec :: Int -> Fin n -> ShowS
showsPrec Int
p Fin n
i = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Fin " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> ShowS
forall a. Show a => a -> ShowS
shows (Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
i)

mkFin :: forall i n. (i + 1 <= n) => NatRepr i -> Fin n
mkFin :: forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin = NatRepr i -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin
{-# INLINE mkFin #-}

-- | Construct a @'Fin' n@ value from the number @i@, where @i@ is reduced
-- modulo @n@.
mkFinModN :: (1 <= n) => NatRepr n -> NatRepr i -> Fin n
mkFinModN :: forall (n :: Natural) (i :: Natural).
(1 <= n) =>
NatRepr n -> NatRepr i -> Fin n
mkFinModN NatRepr n
n NatRepr i
i = NatRepr i
-> NatRepr n
-> (((Mod i n + 1) <= n) => NatRepr (Mod i n) -> Fin n)
-> Fin n
forall (m :: Natural) (n :: Natural) a.
(1 <= m) =>
NatRepr n
-> NatRepr m
-> (((Mod n m + 1) <= m) => NatRepr (Mod n m) -> a)
-> a
withModLeq NatRepr i
i NatRepr n
n ((Mod i n + 1) <= n) => NatRepr (Mod i n) -> Fin n
NatRepr (Mod i n) -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin

newtype Fin' n = Fin' { forall (n :: Natural). Fin' n -> Fin (n + 1)
getFin' :: Fin (n + 1) }

buildFin ::
  forall m.
  NatRepr m ->
  (forall n. (n + 1 <= m) => NatRepr n -> Fin (n + 1) -> Fin (n + 1 + 1)) ->
  Fin (m + 1)
buildFin :: forall (m :: Natural).
NatRepr m
-> (forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1)
buildFin NatRepr m
m forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)
f =
  let f' :: forall k. (k + 1 <= m) => NatRepr k -> Fin' k -> Fin' (k + 1)
      f' :: forall (k :: Natural).
((k + 1) <= m) =>
NatRepr k -> Fin' k -> Fin' (k + 1)
f' = (\NatRepr k
n (Fin' Fin (k + 1)
fin) -> Fin ((k + 1) + 1) -> Fin' (k + 1)
forall (n :: Natural). Fin (n + 1) -> Fin' n
Fin' (NatRepr k -> Fin (k + 1) -> Fin ((k + 1) + 1)
forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)
f NatRepr k
n Fin (k + 1)
fin))
  in Fin' m -> Fin (m + 1)
forall (n :: Natural). Fin' n -> Fin (n + 1)
getFin' (NatRepr m
-> Fin' 0
-> (forall (k :: Natural).
    ((k + 1) <= m) =>
    NatRepr k -> Fin' k -> Fin' (k + 1))
-> Fin' m
forall (m :: Natural) (f :: Natural -> *).
NatRepr m
-> f 0
-> (forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> f n -> f (n + 1))
-> f m
natRecStrictlyBounded NatRepr m
m (Fin (0 + 1) -> Fin' 0
forall (n :: Natural). Fin (n + 1) -> Fin' n
Fin' Fin 1
Fin (0 + 1)
forall (n :: Natural). (1 <= n) => Fin n
minFin) NatRepr n -> Fin' n -> Fin' (n + 1)
forall (k :: Natural).
((k + 1) <= m) =>
NatRepr k -> Fin' k -> Fin' (k + 1)
f')

-- | Count all of the numbers up to @m@ that meet some condition.
countFin ::
  NatRepr m ->
  (forall n. (n + 1 <= m) => NatRepr n -> Fin (n + 1) -> Bool) ->
  Fin (m + 1)
countFin :: forall (m :: Natural).
NatRepr m
-> (forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> Fin (n + 1) -> Bool)
-> Fin (m + 1)
countFin NatRepr m
m forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Bool
f =
  NatRepr m
-> (forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1)
forall (m :: Natural).
NatRepr m
-> (forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1)
buildFin NatRepr m
m ((forall (n :: Natural).
  ((n + 1) <= m) =>
  NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
 -> Fin (m + 1))
-> (forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1)
forall a b. (a -> b) -> a -> b
$
    \NatRepr n
n Fin (n + 1)
count ->
      if NatRepr n -> Fin (n + 1) -> Bool
forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Bool
f NatRepr n
n Fin (n + 1)
count
      then Fin (n + 1) -> Fin ((n + 1) + 1)
forall (n :: Natural). Fin n -> Fin (n + 1)
incFin Fin (n + 1)
count
      else case Fin (n + 1) -> LeqProof (n + 1) ((n + 1) + 1)
forall (f :: Natural -> *) (z :: Natural).
f z -> LeqProof z (z + 1)
leqSucc Fin (n + 1)
count of
              LeqProof (n + 1) ((n + 1) + 1)
LeqProof -> Fin (n + 1) -> Fin ((n + 1) + 1)
forall (n :: Natural) (m :: Natural). (n <= m) => Fin n -> Fin m
embed Fin (n + 1)
count

viewFin ::  (forall i. (i + 1 <= n) => NatRepr i -> r) -> Fin n -> r
viewFin :: forall (n :: Natural) r.
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r)
-> Fin n -> r
viewFin forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r
f (Fin NatRepr i
i) = NatRepr i -> r
forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r
f NatRepr i
i

-- | Construct a @'Fin' n@ value from a 'Natural' input, where the input is
-- reduced modulo @n@.
finFromNatModN :: forall n. (1 <= n) => NatRepr n -> Natural -> Fin n
finFromNatModN :: forall (n :: Natural). (1 <= n) => NatRepr n -> Natural -> Fin n
finFromNatModN NatRepr n
n Natural
i
  | Some NatRepr x
i' <- Natural -> Some NatRepr
mkNatRepr Natural
i
  = NatRepr n -> NatRepr x -> Fin n
forall (n :: Natural) (i :: Natural).
(1 <= n) =>
NatRepr n -> NatRepr i -> Fin n
mkFinModN NatRepr n
n NatRepr x
i'

finToNat :: Fin n -> Natural
finToNat :: forall (n :: Natural). Fin n -> Natural
finToNat (Fin NatRepr i
i) = NatRepr i -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr i
i
{-# INLINABLE finToNat #-}

embed :: forall n m. (n <= m) => Fin n -> Fin m
embed :: forall (n :: Natural) (m :: Natural). (n <= m) => Fin n -> Fin m
embed =
  (forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> Fin m)
-> Fin n -> Fin m
forall (n :: Natural) r.
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r)
-> Fin n -> r
viewFin
    (\(NatRepr i
x :: NatRepr o) ->
      case LeqProof (i + 1) n -> LeqProof n m -> LeqProof (i + 1) m
forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (LeqProof (i + 1) n
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof (o + 1) n) (LeqProof n m
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof n m) of
        LeqProof (i + 1) m
LeqProof -> NatRepr i -> Fin m
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin NatRepr i
x
    )

tryEmbed :: NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)
tryEmbed :: forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)
tryEmbed NatRepr n
n NatRepr m
m Fin n
i =
  case NatRepr n -> NatRepr m -> Maybe (LeqProof n m)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq NatRepr n
n NatRepr m
m of
    Just LeqProof n m
LeqProof -> Fin m -> Maybe (Fin m)
forall a. a -> Maybe a
Just (Fin n -> Fin m
forall (n :: Natural) (m :: Natural). (n <= m) => Fin n -> Fin m
embed Fin n
i)
    Maybe (LeqProof n m)
Nothing -> Maybe (Fin m)
forall a. Maybe a
Nothing

-- | The smallest element of @'Fin' n@
minFin :: (1 <= n) => Fin n
minFin :: forall (n :: Natural). (1 <= n) => Fin n
minFin = NatRepr 0 -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0)
{-# INLINABLE minFin #-}

incFin :: forall n. Fin n -> Fin (n + 1)
incFin :: forall (n :: Natural). Fin n -> Fin (n + 1)
incFin (Fin (NatRepr i
i :: NatRepr i)) =
  case LeqProof (i + 1) n
-> LeqProof 1 1 -> LeqProof ((i + 1) + 1) (n + 1)
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 (i + 1) n
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof (i + 1) n) (LeqProof 1 1
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 1) of
    LeqProof ((i + 1) + 1) (n + 1)
LeqProof -> NatRepr (i + 1) -> Fin (n + 1)
forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin (NatRepr i -> NatRepr (i + 1)
forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr i
i)

-- | It is not possible to construct an element of @'Fin' 0@.
fin0Absurd :: Fin 0 -> a
fin0Absurd :: forall a. Fin 0 -> a
fin0Absurd =
  (forall (i :: Natural). ((i + 1) <= 0) => NatRepr i -> a)
-> Fin 0 -> a
forall (n :: Natural) r.
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r)
-> Fin n -> r
viewFin
    (\(NatRepr i
x :: NatRepr o) ->
      case NatRepr i -> NatRepr 1 -> (i + 1) :~: (1 + i)
forall (f :: Natural -> *) (m :: Natural) (g :: Natural -> *)
       (n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm NatRepr i
x (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) of
        (i + 1) :~: (1 + i)
Refl ->
          case forall (n :: Natural) (n' :: Natural) (m :: Natural).
LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 @1 @o @0 LeqProof (i + 1) 0
LeqProof (1 + i) 0
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof of {})

-- | Add two @'Fin' n@ values and reduce the result modulo @n@.
addFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n
addFinModN :: forall (n :: Natural).
(1 <= n) =>
NatRepr n -> Fin n -> Fin n -> Fin n
addFinModN NatRepr n
n (Fin NatRepr i
x) (Fin NatRepr i
y) = NatRepr n -> NatRepr (i + i) -> Fin n
forall (n :: Natural) (i :: Natural).
(1 <= n) =>
NatRepr n -> NatRepr i -> Fin n
mkFinModN NatRepr n
n (NatRepr i -> NatRepr i -> NatRepr (i + i)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr i
x NatRepr i
y)

-- | Subtract two @'Fin' n@ values and reduce the result modulo @n@.
subFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n
subFinModN :: forall (n :: Natural).
(1 <= n) =>
NatRepr n -> Fin n -> Fin n -> Fin n
subFinModN NatRepr n
n Fin n
x Fin n
y = NatRepr n -> Fin n -> Fin n -> Fin n
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> Fin n -> Fin n -> Fin n
addFinModN NatRepr n
n Fin n
x (NatRepr n -> Fin n -> Fin n
forall (n :: Natural). (1 <= n) => NatRepr n -> Fin n -> Fin n
negFinModN NatRepr n
n Fin n
y)

-- | Multiply two @'Fin' n@ values and reduce the result modulo @n@.
mulFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n
mulFinModN :: forall (n :: Natural).
(1 <= n) =>
NatRepr n -> Fin n -> Fin n -> Fin n
mulFinModN NatRepr n
n (Fin NatRepr i
x) (Fin NatRepr i
y) = NatRepr n -> NatRepr (i * i) -> Fin n
forall (n :: Natural) (i :: Natural).
(1 <= n) =>
NatRepr n -> NatRepr i -> Fin n
mkFinModN NatRepr n
n (NatRepr i -> NatRepr i -> NatRepr (i * i)
forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply NatRepr i
x NatRepr i
y)

-- | Given a value @i :: 'Fin' n@ value, negate it. That is, if @i@ is zero,
-- then return @i@ unchanged, and if @i@ is non-zero, then compute @n - i@.
-- This is a negation in the sense that it is an additive inverse: adding @i@
-- to its negation will yield 'minFin'.
negFinModN :: forall n. (1 <= n) => NatRepr n -> Fin n -> Fin n
negFinModN :: forall (n :: Natural). (1 <= n) => NatRepr n -> Fin n -> Fin n
negFinModN NatRepr n
n (Fin (NatRepr i
i :: NatRepr i))
  | LeqProof i n
LeqProof <- forall (n :: Natural) (n' :: Natural) (m :: Natural).
LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 @i @1 @n LeqProof (i + 1) n
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof
  = NatRepr n -> NatRepr (n - i) -> Fin n
forall (n :: Natural) (i :: Natural).
(1 <= n) =>
NatRepr n -> NatRepr i -> Fin n
mkFinModN NatRepr n
n (NatRepr n -> NatRepr i -> NatRepr (n - i)
forall (n :: Natural) (m :: Natural).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
subNat NatRepr n
n NatRepr i
i)

-- | Given a value @i :: 'Fin' n@, compute the reciprocal (i.e., the modular
-- inverse) if one exists. That is, attempt to compute @i^-1@ such that
-- @i * i^-1@ equals @1@ modulo @n@. Note that a reciprocal will only exist if
-- @i@ and @n@ are relatively prime, i.e., if @gcd i n == 1@. If they are not
-- relatively prime, then this function will return 'Nothing'.
--
-- Note that in the degenerate case where @n == 1@, this function will always
-- return @Just 0@. The value @0@ is the only element of @'Fin' 1@, and @0@ is
-- its own reciprocal.
recipFinModN :: forall n. (1 <= n) => NatRepr n -> Fin n -> Maybe (Fin n)
recipFinModN :: forall (n :: Natural).
(1 <= n) =>
NatRepr n -> Fin n -> Maybe (Fin n)
recipFinModN NatRepr n
n (Fin NatRepr i
i) = NatRepr i
-> NatRepr n
-> (forall (r :: Natural).
    ((r + 1) <= n, Mod (i * r) n ~ 1) =>
    NatRepr r -> Fin n)
-> Maybe (Fin n)
forall (n :: Natural) (m :: Natural) a.
(1 <= m) =>
NatRepr n
-> NatRepr m
-> (forall (r :: Natural).
    ((r + 1) <= m, Mod (n * r) m ~ 1) =>
    NatRepr r -> a)
-> Maybe a
withRecipModNat NatRepr i
i NatRepr n
n NatRepr r -> Fin n
forall (r :: Natural).
((r + 1) <= n, Mod (i * r) n ~ 1) =>
NatRepr r -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin