{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Nat.LE (
LE (..),
LEProof (..),
withLEProof,
decideLE,
leZero,
leSucc,
leRefl,
leStep,
leAsym,
leTrans,
leSwap,
leSwap',
leStepL,
lePred,
proofZeroLEZero,
) where
import Data.Boring (Boring (..), Absurd (..))
import Data.Type.Dec (Dec (..), Decidable (..), Neg)
import Data.Typeable (Typeable)
import Data.Type.Nat
import TrustworthyCompat
data LEProof n m where
LEZero :: LEProof 'Z m
LESucc :: LEProof n m -> LEProof ('S n) ('S m)
deriving (Typeable)
deriving instance Show (LEProof n m)
instance Eq (LEProof n m) where
LEProof n m
_ == :: LEProof n m -> LEProof n m -> Bool
== LEProof n m
_ = Bool
True
instance Ord (LEProof n m) where
compare :: LEProof n m -> LEProof n m -> Ordering
compare LEProof n m
_ LEProof n m
_ = Ordering
EQ
class LE n m where
leProof :: LEProof n m
instance LE 'Z m where
leProof :: LEProof 'Z m
leProof = forall (m :: Nat). LEProof 'Z m
LEZero
instance (m ~ 'S m', LE n m') => LE ('S n) m where
leProof :: LEProof ('S n) m
leProof = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
leProof
withLEProof :: LEProof n m -> (LE n m => r) -> r
withLEProof :: forall (n :: Nat) (m :: Nat) r. LEProof n m -> (LE n m => r) -> r
withLEProof LEProof n m
LEZero LE n m => r
k = LE n m => r
k
withLEProof (LESucc LEProof n m
p) LE n m => r
k = forall (n :: Nat) (m :: Nat) r. LEProof n m -> (LE n m => r) -> r
withLEProof LEProof n m
p LE n m => r
k
leZero :: LEProof 'Z n
leZero :: forall (m :: Nat). LEProof 'Z m
leZero = forall (m :: Nat). LEProof 'Z m
LEZero
leSucc :: LEProof n m -> LEProof ('S n) ('S m)
leSucc :: forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
leSucc = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc
lePred :: LEProof ('S n) ('S m) -> LEProof n m
lePred :: forall (n :: Nat) (m :: Nat). LEProof ('S n) ('S m) -> LEProof n m
lePred (LESucc LEProof n m
p) = LEProof n m
p
leRefl :: forall n. SNatI n => LEProof n n
leRefl :: forall (n :: Nat). SNatI n => LEProof n n
leRefl = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat n of
SNat n
SZ -> forall (m :: Nat). LEProof 'Z m
LEZero
SNat n
SS -> forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc forall (n :: Nat). SNatI n => LEProof n n
leRefl
leStep :: LEProof n m -> LEProof n ('S m)
leStep :: forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
leStep LEProof n m
LEZero = forall (m :: Nat). LEProof 'Z m
LEZero
leStep (LESucc LEProof n m
p) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc (forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
leStep LEProof n m
p)
leStepL :: LEProof ('S n) m -> LEProof n m
leStepL :: forall (n :: Nat) (m :: Nat). LEProof ('S n) m -> LEProof n m
leStepL (LESucc LEProof n m
p) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
leStep LEProof n m
p
leAsym :: LEProof n m -> LEProof m n -> n :~: m
leAsym :: forall (n :: Nat) (m :: Nat).
LEProof n m -> LEProof m n -> (:~:) @Nat n m
leAsym LEProof n m
LEZero LEProof m n
LEZero = forall {k} (a :: k). (:~:) @k a a
Refl
leAsym (LESucc LEProof n m
p) (LESucc LEProof n m
q) = case forall (n :: Nat) (m :: Nat).
LEProof n m -> LEProof m n -> (:~:) @Nat n m
leAsym LEProof n m
p LEProof n m
q of (:~:) @Nat n m
Refl -> forall {k} (a :: k). (:~:) @k a a
Refl
leTrans :: LEProof n m -> LEProof m p -> LEProof n p
leTrans :: forall (n :: Nat) (m :: Nat) (p :: Nat).
LEProof n m -> LEProof m p -> LEProof n p
leTrans LEProof n m
LEZero LEProof m p
_ = forall (m :: Nat). LEProof 'Z m
LEZero
leTrans (LESucc LEProof n m
p) (LESucc LEProof n m
q) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc (forall (n :: Nat) (m :: Nat) (p :: Nat).
LEProof n m -> LEProof m p -> LEProof n p
leTrans LEProof n m
p LEProof n m
q)
leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n
leSwap :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Neg (LEProof n m) -> LEProof ('S m) n
leSwap Neg (LEProof n m)
np = case (forall (n :: Nat). SNatI n => SNat n
snat :: SNat m, forall (n :: Nat). SNatI n => SNat n
snat :: SNat n) of
(SNat m
_, SNat n
SZ) -> forall a b. Absurd a => a -> b
absurd (Neg (LEProof n m)
np forall (m :: Nat). LEProof 'Z m
LEZero)
(SNat m
SZ, SNat n
SS) -> forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc forall (m :: Nat). LEProof 'Z m
LEZero
(SNat m
SS, SNat n
SS) -> forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Neg (LEProof n m) -> LEProof ('S m) n
leSwap forall a b. (a -> b) -> a -> b
$ \LEProof n n
p -> Neg (LEProof n m)
np forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc LEProof n n
p
leSwap' :: LEProof n m -> LEProof ('S m) n -> void
leSwap' :: forall (n :: Nat) (m :: Nat) void.
LEProof n m -> LEProof ('S m) n -> void
leSwap' LEProof n m
p (LESucc LEProof n m
q) = case LEProof n m
p of LESucc LEProof n m
p' -> forall (n :: Nat) (m :: Nat) void.
LEProof n m -> LEProof ('S m) n -> void
leSwap' LEProof n m
p' LEProof n m
q
instance LE n m => Boring (LEProof n m) where
boring :: LEProof n m
boring = forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
leProof
instance (LE m n, n' ~ 'S n) => Absurd (LEProof n' m) where
absurd :: forall b. LEProof n' m -> b
absurd = forall (n :: Nat) (m :: Nat) void.
LEProof n m -> LEProof ('S m) n -> void
leSwap' forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
leProof
decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)
decideLE :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Dec (LEProof n m)
decideLE = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat n of
SNat n
SZ -> forall a. a -> Dec a
Yes forall (m :: Nat). LEProof 'Z m
leZero
SNat n
SS -> forall (n' :: Nat) (m' :: Nat).
(SNatI n', SNatI m') =>
Dec (LEProof ('S n') m')
caseSnm
where
caseSnm :: forall n' m'. (SNatI n', SNatI m') => Dec (LEProof ('S n') m')
caseSnm :: forall (n' :: Nat) (m' :: Nat).
(SNatI n', SNatI m') =>
Dec (LEProof ('S n') m')
caseSnm = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat m' of
SNat m'
SZ -> forall a. Neg a -> Dec a
No forall a b. (a -> b) -> a -> b
$ \LEProof ('S n') m'
p -> case LEProof ('S n') m'
p of {}
SNat m'
SS -> case forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Dec (LEProof n m)
decideLE of
Yes LEProof n' n
p -> forall a. a -> Dec a
Yes (forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
leSucc LEProof n' n
p)
No Neg (LEProof n' n)
p -> forall a. Neg a -> Dec a
No forall a b. (a -> b) -> a -> b
$ \LEProof ('S n') m'
p' -> Neg (LEProof n' n)
p (forall (n :: Nat) (m :: Nat). LEProof ('S n) ('S m) -> LEProof n m
lePred LEProof ('S n') m'
p')
instance (SNatI n, SNatI m) => Decidable (LEProof n m) where
decide :: Dec (LEProof n m)
decide = forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Dec (LEProof n m)
decideLE
proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z
proofZeroLEZero :: forall (n :: Nat). LEProof n 'Z -> (:~:) @Nat n 'Z
proofZeroLEZero LEProof n 'Z
LEZero = forall {k} (a :: k). (:~:) @k a a
Refl