{-# 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  #-}
-- | Less-than-or-equal relation for (unary) natural numbers 'Nat'.
--
-- There are at least three ways to encode this relation.
--
-- * \(zero : 0 \le m\) and \(succ : n \le m \to 1 + n \le 1 + m\) (this module),
--
-- * \(refl : n \le n \) and \(step : n \le m \to n \le 1 + m\) ("Data.Type.Nat.LE.ReflStep"),
--
-- * \(ex : \exists p. n + p \equiv m \) (tricky in Haskell).
--
-- Depending on a situation, usage ergonomics are different.
--
module Data.Type.Nat.LE (
    -- * Relation
    LE (..),
    LEProof (..),
    withLEProof,
    -- * Decidability
    decideLE,
    -- * Lemmas
    -- ** Constructor like
    leZero,
    leSucc,
    leRefl,
    leStep,
    -- ** Partial order
    leAsym,
    leTrans,
    -- ** Total order
    leSwap,
    leSwap',
    -- ** More
    leStepL,
    lePred,
    proofZeroLEZero,
    ) where

import Data.Type.Dec      (Dec (..), Decidable (..), Neg)
import Data.Typeable      (Typeable)
import Data.Void          (absurd)

import Data.Type.Nat
import TrustworthyCompat

-- $setup
-- >>> import Data.Type.Nat

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

-- | An evidence of \(n \le m\). /zero+succ/ definition.
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)

-- | '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

-------------------------------------------------------------------------------
-- Class
-------------------------------------------------------------------------------

-- | Total order of 'Nat', less-than-or-Equal-to, \( \le \).
--
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

-- | Constructor 'LE' dictionary from 'LEProof'.
withLEProof :: LEProof n m -> (LE n m => r) -> r
withLEProof :: 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 LE n m => r
LE n m => r
k

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

-- | \(\forall n : \mathbb{N}, 0 \le n \)
leZero :: LEProof 'Z n
leZero :: LEProof 'Z n
leZero = LEProof 'Z n
forall (m :: Nat). LEProof 'Z m
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 :: 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

-- | \(\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m \)
lePred :: LEProof ('S n) ('S m) -> LEProof n m
lePred :: LEProof ('S n) ('S m) -> LEProof n m
lePred (LESucc LEProof n m
p) = LEProof n m
LEProof n m
p

-- | \(\forall n : \mathbb{N}, n \le n \)
leRefl :: forall n. SNatI n => LEProof n n
leRefl :: LEProof n n
leRefl = case SNat n
forall (n :: Nat). SNatI n => SNat n
snat :: SNat n of
    SNat n
SZ -> LEProof n n
forall (m :: Nat). LEProof 'Z m
LEZero
    SNat n
SS -> LEProof n n -> LEProof ('S n) ('S n)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc LEProof n n
forall (n :: Nat). SNatI n => LEProof n n
leRefl

-- | \(\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m \)
leStep :: LEProof n m -> LEProof n ('S m)
leStep :: LEProof n m -> LEProof n ('S m)
leStep LEProof n m
LEZero     = LEProof n ('S m)
forall (m :: Nat). LEProof 'Z m
LEZero
leStep (LESucc LEProof n m
p) = LEProof n ('S m) -> LEProof ('S n) ('S ('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)

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

-- | \(\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 :: LEProof n m -> LEProof m p -> LEProof n p
leTrans LEProof n m
LEZero     LEProof m p
_          = LEProof n 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)
-- leTrans (LESucc _) q = case q of {}

-- | \(\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 :: 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 a. Void -> a
absurd (Neg (LEProof n m)
np LEProof n m
forall (m :: Nat). LEProof 'Z m
LEZero)
    (SNat m
SZ, SNat n
SS) -> LEProof 'Z n -> LEProof ('S 'Z) ('S n)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc LEProof 'Z n
forall (m :: Nat). LEProof 'Z m
LEZero
    (SNat m
SS, SNat n
SS) -> LEProof ('S n) n -> LEProof ('S ('S n)) ('S n)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
LESucc (LEProof ('S n) n -> LEProof ('S ('S n)) ('S n))
-> LEProof ('S n) n -> LEProof ('S ('S n)) ('S n)
forall a b. (a -> b) -> a -> b
$ Neg (LEProof n n) -> LEProof ('S n) n
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Neg (LEProof n m) -> LEProof ('S m) n
leSwap (Neg (LEProof n n) -> LEProof ('S n) n)
-> Neg (LEProof n n) -> LEProof ('S n) n
forall a b. (a -> b) -> a -> b
$ \LEProof n n
p -> Neg (LEProof n m)
np Neg (LEProof n m) -> Neg (LEProof n m)
forall a b. (a -> b) -> a -> b
$ LEProof n n -> LEProof ('S n) ('S n)
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) \)
--
-- >>> leProof :: LEProof Nat2 Nat3
-- LESucc (LESucc LEZero)
--
-- >>> leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))
-- LESucc (LESucc (LESucc LEZero))
--
-- >>> lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))
-- LESucc (LESucc LEZero)
--
leSwap' :: LEProof n m -> LEProof ('S m) n -> void
leSwap' :: 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

-------------------------------------------------------------------------------
-- Dedidablity
-------------------------------------------------------------------------------

-- | Find the @'LEProof' n m@, i.e. compare numbers.
decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)
decideLE :: Dec (LEProof n m)
decideLE = case SNat n
forall (n :: Nat). SNatI n => SNat n
snat :: SNat n of
    SNat n
SZ -> LEProof 'Z m -> Dec (LEProof 'Z m)
forall a. a -> Dec a
Yes LEProof 'Z m
forall (m :: Nat). LEProof 'Z m
leZero
    SNat n
SS -> Dec (LEProof n 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 :: 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 {} -- ooh, GHC is smart!
        SNat m'
SS -> case Dec (LEProof n' n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Dec (LEProof n m)
decideLE of
            Yes LEProof n' n
p -> LEProof ('S n') ('S n) -> Dec (LEProof ('S n') ('S n))
forall a. a -> Dec a
Yes (LEProof n' n -> LEProof ('S n') ('S n)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof ('S n) ('S m)
leSucc LEProof n' n
p)
            No  Neg (LEProof n' n)
p -> Neg (LEProof ('S n') ('S n)) -> Dec (LEProof ('S n') ('S n))
forall a. Neg a -> Dec a
No (Neg (LEProof ('S n') ('S n)) -> Dec (LEProof ('S n') ('S n)))
-> Neg (LEProof ('S n') ('S n)) -> Dec (LEProof ('S n') ('S n))
forall a b. (a -> b) -> a -> b
$ \LEProof ('S n') ('S n)
p' -> Neg (LEProof n' n)
p (LEProof ('S n') ('S n) -> LEProof n' n
forall (n :: Nat) (m :: Nat). LEProof ('S n) ('S m) -> LEProof n m
lePred LEProof ('S n') ('S n)
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

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

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