{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE EmptyCase             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeOperators         #-}

{-# LANGUAGE UndecidableInstances  #-}
module Data.Type.Nat.LE.ReflStep (
    -- * Relation
    LEProof (..),
    fromZeroSucc,
    toZeroSucc,
    -- * Decidability
    decideLE,
    -- * Lemmas
    -- ** Constructor like
    leZero,
    leSucc,
    leRefl,
    leStep,
    -- ** Partial order
    leAsym,
    leTrans,
    -- ** Total order
    leSwap,
    leSwap',
    -- ** More
    leStepL,
    lePred,
    proofZeroLEZero,
    ) where

import Data.Boring   (Absurd (..), Boring (..))
import Data.Type.Dec (Dec (..), Decidable (..), Neg)
import Data.Typeable (Typeable)

import qualified Control.Category as C

import           Data.Type.Nat
import qualified Data.Type.Nat.LE  as ZeroSucc
import           TrustworthyCompat

-------------------------------------------------------------------------------
-- Proof
-------------------------------------------------------------------------------

-- | An evidence of \(n \le m\). /refl+step/ definition.
data LEProof n m where
    LERefl :: LEProof n n
    LEStep :: LEProof n m -> LEProof n ('S m)
  deriving (Typeable)

deriving instance Show (LEProof n m)

-- | 'LEProof' values are unique (not @'Boring'@ though!).
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

-- | The other variant ('Data.Type.Nat.LE.LEPRoof') isn't 'C.Category',
-- because 'Data.Type.Nat.LE.leRefl` requires 'SNat' evidence.
instance C.Category LEProof where
    id :: forall (a :: Nat). LEProof a a
id  = forall (a :: Nat). LEProof a a
leRefl
    . :: forall (b :: Nat) (c :: Nat) (a :: Nat).
LEProof b c -> LEProof a b -> LEProof a c
(.) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (n :: Nat) (m :: Nat) (p :: Nat).
LEProof n m -> LEProof m p -> LEProof n p
leTrans

-------------------------------------------------------------------------------
-- Conversion
-------------------------------------------------------------------------------

-- | Convert from /zero+succ/ to /refl+step/ definition.
--
-- Inverse of 'toZeroSucc'.
--
fromZeroSucc :: forall n m. SNatI m => ZeroSucc.LEProof n m -> LEProof n m
fromZeroSucc :: forall (n :: Nat) (m :: Nat). SNatI m => LEProof n m -> LEProof n m
fromZeroSucc LEProof n m
ZeroSucc.LEZero     = forall (n :: Nat). SNatI n => LEProof 'Z n
leZero
fromZeroSucc (ZeroSucc.LESucc LEProof n m
p) = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat m of
    SNat m
SS -> forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
leSucc (forall (n :: Nat) (m :: Nat). SNatI m => LEProof n m -> LEProof n m
fromZeroSucc LEProof n m
p)
    -- q  -> case q of {} -- for older GHC

-- | Convert /refl+step/ to /zero+succ/ definition.
--
-- Inverse of 'fromZeroSucc'.
--
toZeroSucc :: SNatI n => LEProof n m -> ZeroSucc.LEProof n m
toZeroSucc :: forall (n :: Nat) (m :: Nat). SNatI n => LEProof n m -> LEProof n m
toZeroSucc LEProof n m
LERefl     = forall (n :: Nat). SNatI n => LEProof n n
ZeroSucc.leRefl
toZeroSucc (LEStep LEProof n m
p) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
ZeroSucc.leStep (forall (n :: Nat) (m :: Nat). SNatI n => LEProof n m -> LEProof n m
toZeroSucc LEProof n m
p)

-------------------------------------------------------------------------------
-- Lemmas
-------------------------------------------------------------------------------

-- | \(\forall n : \mathbb{N}, 0 \le n \)
leZero :: forall n. SNatI n => LEProof 'Z n
leZero :: forall (n :: Nat). SNatI n => LEProof 'Z n
leZero = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat n of
    SNat n
SZ -> forall (a :: Nat). LEProof a a
LERefl
    SNat n
SS -> forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
LEStep forall (n :: Nat). SNatI n => LEProof 'Z n
leZero

-- | \(\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m \)
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
LERefl     = forall (a :: Nat). LEProof a a
LERefl
leSucc (LEStep LEProof n m
p) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
LEStep (forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
leSucc LEProof n m
p)

-- | \(\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m \)
lePred :: LEProof ('S n) ('S m) -> LEProof n m
lePred :: forall (n :: Nat) (m :: Nat). LEProof ('S n) ('S m) -> LEProof n m
lePred LEProof ('S n) ('S m)
LERefl              = forall (a :: Nat). LEProof a a
LERefl
lePred (LEStep LEProof ('S n) m
LERefl)     = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
LEStep forall (a :: Nat). LEProof a a
LERefl
lePred (LEStep (LEStep LEProof ('S n) m
q)) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
LEStep (forall (n :: Nat) (m :: Nat). LEProof ('S n) m -> LEProof n m
leStepL LEProof ('S n) m
q)

-- | \(\forall n : \mathbb{N}, n \le n \)
leRefl :: LEProof n n
leRefl :: forall (a :: Nat). LEProof a a
leRefl = forall (a :: Nat). LEProof a a
LERefl

-- | \(\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m \)
leStep :: LEProof n m -> LEProof n ('S m)
leStep :: forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
leStep = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
LEStep

-- | \(\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m \)
leStepL :: LEProof ('S n) m -> LEProof n m
leStepL :: forall (n :: Nat) (m :: Nat). LEProof ('S n) m -> LEProof n m
leStepL LEProof ('S n) m
LERefl     = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
LEStep forall (a :: Nat). LEProof a a
LERefl
leStepL (LEStep LEProof ('S n) m
p) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
LEStep (forall (n :: Nat) (m :: Nat). LEProof ('S n) m -> LEProof n m
leStepL LEProof ('S n) m
p)

-- | \(\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m \)
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
LERefl LEProof m n
_ = forall {k} (a :: k). (:~:) @k a a
Refl
leAsym LEProof n m
_ LEProof m n
LERefl = forall {k} (a :: k). (:~:) @k a a
Refl
leAsym (LEStep LEProof n m
p) (LEStep LEProof m m
q) = case forall (n :: Nat) (m :: Nat).
LEProof n m -> LEProof m n -> (:~:) @Nat n m
leAsym (forall (n :: Nat) (m :: Nat). LEProof ('S n) m -> LEProof n m
leStepL LEProof n m
p) (forall (n :: Nat) (m :: Nat). LEProof ('S n) m -> LEProof n m
leStepL LEProof m m
q) of
    (:~:) @Nat m m
Refl -> forall {k} (a :: k). (:~:) @k a a
Refl

-- | \(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \)
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
p LEProof m p
LERefl     = LEProof n m
p
leTrans LEProof n m
p (LEStep LEProof m m
q) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
LEStep forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) (p :: Nat).
LEProof n m -> LEProof m p -> LEProof n p
leTrans LEProof n m
p LEProof m m
q

-- | \(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \)
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 (n :: Nat). SNatI n => LEProof 'Z n
leZero)
    (SNat m
SZ, SNat n
SS) -> forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
leSucc forall (n :: Nat). SNatI n => LEProof 'Z n
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

-- | \(\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) \)
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 LEProof ('S m) n
LERefl     = case LEProof n m
p of LEStep LEProof n m
p' -> forall (n :: Nat) (m :: Nat) void.
LEProof n m -> LEProof ('S m) n -> void
leSwap' (forall (n :: Nat) (m :: Nat). LEProof ('S n) m -> LEProof n m
leStepL LEProof n m
p') forall (a :: Nat). LEProof a a
LERefl
leSwap' LEProof n m
p (LEStep LEProof ('S m) m
q) = forall (n :: Nat) (m :: Nat) void.
LEProof n m -> LEProof ('S m) n -> void
leSwap' (forall (n :: Nat) (m :: Nat). LEProof ('S n) m -> LEProof n m
leStepL LEProof n m
p) LEProof ('S m) m
q

-------------------------------------------------------------------------------
-- Boring
-------------------------------------------------------------------------------

-- | @since 0.2.1
instance (ZeroSucc.LE n m, SNatI m) => Boring (LEProof n m) where
    boring :: LEProof n m
boring = forall (n :: Nat) (m :: Nat). SNatI m => LEProof n m -> LEProof n m
fromZeroSucc forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
ZeroSucc.leProof

-- | @since 0.2.1
instance (ZeroSucc.LE m n, n' ~ 'S n, SNatI 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
ZeroSucc.leSwap' forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
ZeroSucc.leProof forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (m :: Nat). SNatI n => LEProof n m -> LEProof n m
toZeroSucc

-------------------------------------------------------------------------------
-- Decidability
-------------------------------------------------------------------------------

-- | Find the @'LEProof' n m@, i.e. compare numbers.
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 (n :: Nat). SNatI n => LEProof 'Z n
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 {} -- ooh, GHC is smart!
        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

-------------------------------------------------------------------------------
-- More lemmas
---------------------------------------------------------------------------------

-- | \(\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0 \)
proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z
proofZeroLEZero :: forall (n :: Nat). LEProof n 'Z -> (:~:) @Nat n 'Z
proofZeroLEZero LEProof n 'Z
LERefl = forall {k} (a :: k). (:~:) @k a a
Refl