{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
module Data.Type.Nat.LT (
    LT (..),
    LTProof,
    withLTProof,
    -- * Lemmas
    ltReflAbsurd,
    ltSymAbsurd,
    ltTrans,
    ) where

import Data.Type.Nat
import Data.Type.Nat.LE

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

-- | An evidence \(n < m\) which is the same as (\1 + n \le m\).
type LTProof n m = LEProof ('S n) m

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

-- | Less-Than-or. \(<\). Well-founded relation on 'Nat'.
--
-- GHC can solve this for us!
--
-- >>> ltProof :: LTProof Nat0 Nat4
-- LESucc LEZero
--
-- >>> ltProof :: LTProof Nat2 Nat4
-- LESucc (LESucc (LESucc LEZero))
--
-- >>> ltProof :: LTProof Nat3 Nat3
-- ...
-- ...error...
-- ...
--
class LT (n :: Nat) (m :: Nat) where
    ltProof :: LTProof n m

instance LE ('S n) m => LT n m where
    ltProof :: LTProof n m
ltProof = LTProof n m
forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
leProof

withLTProof :: LTProof n m -> (LT n m => r) -> r
withLTProof :: forall (n :: Nat) (m :: Nat) r. LTProof n m -> (LT n m => r) -> r
withLTProof LTProof n m
p LT n m => r
f = LTProof n m -> (LE ('S n) m => r) -> r
forall (n :: Nat) (m :: Nat) r. LEProof n m -> (LE n m => r) -> r
withLEProof LTProof n m
p r
LE ('S n) m => r
LT n m => r
f -- eta expansion needed for old GHC

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

-- | \(\forall n : \mathbb{N}, n < n \to \bot \)
ltReflAbsurd :: LTProof n n -> a
ltReflAbsurd :: forall (n :: Nat) a. LTProof n n -> a
ltReflAbsurd (LESucc LEProof n1 m1
p) = LTProof m1 m1 -> a
forall (n :: Nat) a. LTProof n n -> a
ltReflAbsurd LEProof n1 m1
LTProof m1 m1
p

-- | \(\forall n\, m : \mathbb{N}, n < m \to m < n \to \bot \)
ltSymAbsurd :: LTProof n m -> LTProof m n -> a
ltSymAbsurd :: forall (n :: Nat) (m :: Nat) a. LTProof n m -> LTProof m n -> a
ltSymAbsurd (LESucc LEProof n1 m1
p) (LESucc LEProof n1 m1
q) = LTProof m1 m1 -> LTProof m1 m1 -> a
forall (n :: Nat) (m :: Nat) a. LTProof n m -> LTProof m n -> a
ltSymAbsurd LEProof n1 m1
LTProof m1 m1
p LEProof n1 m1
LTProof m1 m1
q

-- | \(\forall n\, m\, p : \mathbb{N}, n < m \to m < p \to n < p \)
ltTrans :: LTProof n m -> LTProof m p -> LTProof n p
ltTrans :: forall (n :: Nat) (m :: Nat) (p :: Nat).
LTProof n m -> LTProof m p -> LTProof n p
ltTrans LTProof n m
p (LESucc LEProof n1 m1
q) = LEProof ('S n) m1 -> LEProof ('S n) ('S m1)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
leStep (LEProof ('S n) m1 -> LEProof ('S n) ('S m1))
-> LEProof ('S n) m1 -> LEProof ('S n) ('S m1)
forall a b. (a -> b) -> a -> b
$ LTProof n m -> LEProof m m1 -> LEProof ('S n) m1
forall (n :: Nat) (m :: Nat) (p :: Nat).
LEProof n m -> LEProof m p -> LEProof n p
leTrans LTProof n m
p LEProof m m1
LEProof n1 m1
q