{-# 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 = LEProof 'Z m
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 = LEProof n m' -> LEProof ('S n) ('S m')
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc LEProof n m'
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 = r
LE n m => r
k
withLEProof (LESucc LEProof n m
p) LE n m => r
k = LEProof n m -> (LE n m => r) -> r
forall (n :: Nat) (m :: Nat) r. LEProof n m -> (LE n m => r) -> r
withLEProof LEProof n m
p r
LE n m => r
LE n m => r
k
leZero :: LEProof 'Z n
leZero :: forall (m :: Nat). LEProof 'Z m
leZero = LEProof 'Z n
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 = LEProof n m -> LEProof ('S n) ('S m)
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
LEProof n m
p
leRefl :: forall n. SNatI n => LEProof n n
leRefl :: forall (n :: Nat). SNatI n => LEProof n n
leRefl = case SNat n
forall (n :: Nat). SNatI n => SNat n
snat :: SNat n of
SNat n
SZ -> LEProof n n
LEProof 'Z n
forall (m :: Nat). LEProof 'Z m
LEZero
SNat n
SS -> LEProof n1 n1 -> LEProof ('S n1) ('S n1)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc LEProof n1 n1
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 = LEProof n ('S m)
LEProof 'Z ('S m)
forall (m :: Nat). LEProof 'Z m
LEZero
leStep (LESucc LEProof n m
p) = LEProof n m -> LEProof ('S n) ('S m)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc (LEProof n m -> LEProof n ('S m)
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) = LEProof n m -> LEProof n ('S m)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
leStep LEProof n m
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 = (:~:) @Nat n n
(:~:) @Nat n m
forall {k} (a :: k). (:~:) @k a a
Refl
leAsym (LESucc LEProof n m
p) (LESucc LEProof n m
q) = case LEProof n m -> LEProof m n -> (:~:) @Nat n m
forall (n :: Nat) (m :: Nat).
LEProof n m -> LEProof m n -> (:~:) @Nat n m
leAsym LEProof n m
p LEProof m n
LEProof n m
q of (:~:) @Nat n m
Refl -> (:~:) @Nat n n
(:~:) @Nat n m
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
_ = LEProof n p
LEProof 'Z p
forall (m :: Nat). LEProof 'Z m
LEZero
leTrans (LESucc LEProof n m
p) (LESucc LEProof n m
q) = LEProof n m -> LEProof ('S n) ('S m)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc (LEProof n m -> LEProof m m -> LEProof n m
forall (n :: Nat) (m :: Nat) (p :: Nat).
LEProof n m -> LEProof m p -> LEProof n p
leTrans LEProof n m
p LEProof m m
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 (SNat m
forall (n :: Nat). SNatI n => SNat n
snat :: SNat m, SNat n
forall (n :: Nat). SNatI n => SNat n
snat :: SNat n) of
(SNat m
_, SNat n
SZ) -> Void -> LEProof ('S m) n
forall b. Void -> b
forall a b. Absurd a => a -> b
absurd (Neg (LEProof n m)
np LEProof n m
LEProof 'Z m
forall (m :: Nat). LEProof 'Z m
LEZero)
(SNat m
SZ, SNat n
SS) -> LEProof m n1 -> LEProof ('S m) ('S n1)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc LEProof m n1
LEProof 'Z n1
forall (m :: Nat). LEProof 'Z m
LEZero
(SNat m
SS, SNat n
SS) -> LEProof m n1 -> LEProof ('S m) ('S n1)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc (LEProof m n1 -> LEProof ('S m) ('S n1))
-> LEProof m n1 -> LEProof ('S m) ('S n1)
forall a b. (a -> b) -> a -> b
$ Neg (LEProof n1 n1) -> LEProof ('S n1) n1
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Neg (LEProof n m) -> LEProof ('S m) n
leSwap (Neg (LEProof n1 n1) -> LEProof ('S n1) n1)
-> Neg (LEProof n1 n1) -> LEProof ('S n1) n1
forall a b. (a -> b) -> a -> b
$ \LEProof n1 n1
p -> Neg (LEProof n m)
np Neg (LEProof n m) -> Neg (LEProof n m)
forall a b. (a -> b) -> a -> b
$ LEProof n1 n1 -> LEProof ('S n1) ('S n1)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc LEProof n1 n1
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' -> LEProof n m -> LEProof ('S m) n -> void
forall (n :: Nat) (m :: Nat) void.
LEProof n m -> LEProof ('S m) n -> void
leSwap' LEProof n m
p' LEProof n m
LEProof ('S m) n
q
instance LE n m => Boring (LEProof n m) where
boring :: LEProof n m
boring = LEProof n m
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 = LEProof m n -> LEProof ('S n) m -> b
forall (n :: Nat) (m :: Nat) void.
LEProof n m -> LEProof ('S m) n -> void
leSwap' LEProof m n
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 SNat n
forall (n :: Nat). SNatI n => SNat n
snat :: SNat n of
SNat n
SZ -> LEProof n m -> Dec (LEProof n m)
forall a. a -> Dec a
Yes LEProof n m
LEProof 'Z m
forall (m :: Nat). LEProof 'Z m
leZero
SNat n
SS -> Dec (LEProof n m)
Dec (LEProof ('S n1) m)
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 SNat m'
forall (n :: Nat). SNatI n => SNat n
snat :: SNat m' of
SNat m'
SZ -> Neg (LEProof ('S n') m') -> Dec (LEProof ('S n') m')
forall a. Neg a -> Dec a
No (Neg (LEProof ('S n') m') -> Dec (LEProof ('S n') m'))
-> Neg (LEProof ('S n') m') -> Dec (LEProof ('S n') m')
forall a b. (a -> b) -> a -> b
$ \LEProof ('S n') m'
p -> case LEProof ('S n') m'
p of {}
SNat m'
SS -> case Dec (LEProof n' n1)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Dec (LEProof n m)
decideLE of
Yes LEProof n' n1
p -> LEProof ('S n') m' -> Dec (LEProof ('S n') m')
forall a. a -> Dec a
Yes (LEProof n' n1 -> LEProof ('S n') ('S n1)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
leSucc LEProof n' n1
p)
No Neg (LEProof n' n1)
p -> Neg (LEProof ('S n') m') -> Dec (LEProof ('S n') m')
forall a. Neg a -> Dec a
No (Neg (LEProof ('S n') m') -> Dec (LEProof ('S n') m'))
-> Neg (LEProof ('S n') m') -> Dec (LEProof ('S n') m')
forall a b. (a -> b) -> a -> b
$ \LEProof ('S n') m'
p' -> Neg (LEProof n' n1)
p (LEProof ('S n') ('S n1) -> LEProof n' n1
forall (n :: Nat) (m :: Nat). LEProof ('S n) ('S m) -> LEProof n m
lePred LEProof ('S n') m'
LEProof ('S n') ('S n1)
p')
instance (SNatI n, SNatI m) => Decidable (LEProof n m) where
decide :: Dec (LEProof n m)
decide = Dec (LEProof n m)
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 = (:~:) @Nat n n
(:~:) @Nat n 'Z
forall {k} (a :: k). (:~:) @k a a
Refl