{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK ignore-exports #-}

-- |
-- Module      : Data.Tree.BST.Intern.Insert
-- Description : Insertion algorithm (with proofs) over internalist BST trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the insertion algorithm over internalist BST trees,
-- along with the necessary proofs to ensure (at compile time) that the
-- key ordering still holds.
module Data.Tree.BST.Intern.Insert
  ( Insertable (Insert, insert),
  )
where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Data.Tree.BST.Intern.Constructors (BST (EmptyBST, ForkBST))
import Data.Tree.BST.Invariants (GtN, LtN)
import Data.Tree.ITree (Tree (EmptyTree, ForkTree))
import Data.Tree.Node (Node, getValue, mkNode)
import Data.Type.Equality (gcastWith, (:~:) (Refl))
import GHC.TypeNats (CmpNat, Nat)
import Prelude
  ( Bool (True),
    Ordering (EQ, GT, LT),
    Show,
    ($),
  )

-- | This type class provides the functionality to insert a node with key @x@ and value type @a@
-- in a `BST` @t@.
-- The insertion is defined at the value level and the type level.
-- The returned tree verifies the `BST` restrictions.
class Insertable (x :: Nat) (a :: Type) (t :: Tree) where
  type Insert (x :: Nat) (a :: Type) (t :: Tree) :: Tree
  insert :: Node x a -> BST t -> BST (Insert x a t)

instance
  (Show a) =>
  Insertable x a 'EmptyTree
  where
  type Insert x a 'EmptyTree = 'ForkTree 'EmptyTree (Node x a) 'EmptyTree
  insert :: Node x a -> BST 'EmptyTree -> BST (Insert x a 'EmptyTree)
insert Node x a
node BST 'EmptyTree
_ = BST 'EmptyTree
-> Node x a
-> BST 'EmptyTree
-> BST ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
ForkBST BST 'EmptyTree
EmptyBST Node x a
node BST 'EmptyTree
EmptyBST

instance
  ( o ~ CmpNat x n,
    Insertable' x a ('ForkTree l (Node n a1) r) o
  ) =>
  Insertable x a ('ForkTree l (Node n a1) r)
  where
  type Insert x a ('ForkTree l (Node n a1) r) = Insert' x a ('ForkTree l (Node n a1) r) (CmpNat x n)
  insert :: Node x a
-> BST ('ForkTree l (Node n a1) r)
-> BST (Insert x a ('ForkTree l (Node n a1) r))
insert Node x a
n BST ('ForkTree l (Node n a1) r)
t = Node x a
-> BST ('ForkTree l (Node n a1) r)
-> Proxy o
-> BST (Insert' x a ('ForkTree l (Node n a1) r) o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> BST t -> Proxy o -> BST (Insert' x a t o)
insert' Node x a
n BST ('ForkTree l (Node n a1) r)
t (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)

-- | This type class provides the functionality to insert a node with key @x@ and value type @a@
-- in a non empty `BST` @t@.
-- It's only used by the 'Insertable' class and it has one extra parameter @o@,
-- which is the type level comparison of @x@ with the key value of the root node.
-- The @o@ parameter guides the insertion.
class Insertable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
  type Insert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) :: Tree
  insert' :: Node x a -> BST t -> Proxy o -> BST (Insert' x a t o)

instance
  (Show a) =>
  Insertable' x a ('ForkTree l (Node n a1) r) 'EQ
  where
  type Insert' x a ('ForkTree l (Node n a1) r) 'EQ = 'ForkTree l (Node n a) r
  insert' :: Node x a
-> BST ('ForkTree l (Node n a1) r)
-> Proxy 'EQ
-> BST (Insert' x a ('ForkTree l (Node n a1) r) 'EQ)
insert' Node x a
node (ForkBST BST l
l Node n a
_ BST r
r) Proxy 'EQ
_ = BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
ForkBST BST l
l Node n a
node' BST r
r
    where
      node' :: Node n a
node' = Proxy n -> a -> Node n a
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Node x a -> a
forall (k :: Nat) a. Node k a -> a
getValue Node x a
node)

instance
  ( CmpNat x n ~ 'LT,
    Show a
  ) =>
  Insertable' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT
  where
  type
    Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT =
      'ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a1) r
  insert' :: Node x a
-> BST ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> BST (Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
insert' Node x a
node (ForkBST BST l
_ Node n a
node' BST r
r) Proxy 'LT
_ =
    BST ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Node n a
-> BST r
-> BST
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
ForkBST (BST 'EmptyTree
-> Node x a
-> BST 'EmptyTree
-> BST ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
ForkBST BST 'EmptyTree
EmptyBST Node x a
node BST 'EmptyTree
EmptyBST) Node n a
node' BST r
r

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    CmpNat x n ~ 'LT,
    Insertable' x a l o,
    ProofLtNInsert' x a ('ForkTree ll (Node ln lna) lr) n o
  ) =>
  Insertable' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT
  where
  type
    Insert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT =
      'ForkTree (Insert' x a ('ForkTree ll (Node ln lna) lr) (CmpNat x ln)) (Node n a1) r
  insert' :: Node x a
-> BST ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r)
-> Proxy 'LT
-> BST
     (Insert'
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT)
insert' Node x a
node (ForkBST BST l
l Node n a
node' BST r
r) Proxy 'LT
_ =
    (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    BST
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r))
-> BST
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> BST l -> Proxy n -> Proxy o -> LtN (Insert x a l) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Node x a
-> BST t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True
proofLtNInsert' Node x a
node BST l
l (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
Proxy (CmpNat x ln)
po) (((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
   ~ 'True) =>
  BST
    ('ForkTree
       (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r))
 -> BST
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r))
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    BST
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r))
-> BST
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
forall a b. (a -> b) -> a -> b
$
      BST (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Node n a
-> BST r
-> BST
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
ForkBST (Node x a -> BST l -> Proxy o -> BST (Insert' x a l o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> BST t -> Proxy o -> BST (Insert' x a t o)
insert' Node x a
node BST l
l Proxy o
Proxy (CmpNat x ln)
po) Node n a
node' BST r
r
    where
      po :: Proxy (CmpNat x ln)
po = Proxy (CmpNat x ln)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (CmpNat x ln)

instance
  ( CmpNat x n ~ 'GT,
    Show a
  ) =>
  Insertable' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT
  where
  type
    Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT =
      'ForkTree l (Node n a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
  insert' :: Node x a
-> BST ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> BST (Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
insert' Node x a
node (ForkBST BST l
l Node n a
node' BST r
_) Proxy 'GT
_ = BST l
-> Node n a
-> BST ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> BST
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
ForkBST BST l
l Node n a
node' (BST 'EmptyTree
-> Node x a
-> BST 'EmptyTree
-> BST ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
ForkBST BST 'EmptyTree
EmptyBST Node x a
node BST 'EmptyTree
EmptyBST)

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    CmpNat x n ~ 'GT,
    Insertable' x a r o,
    ProofGtNInsert' x a ('ForkTree rl (Node rn rna) rr) n o
  ) =>
  Insertable' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT
  where
  type
    Insert' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT =
      'ForkTree l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) (CmpNat x rn))
  insert' :: Node x a
-> BST ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy 'GT
-> BST
     (Insert'
        x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT)
insert' Node x a
node (ForkBST BST l
l Node n a
node' BST r
r) Proxy 'GT
_ =
    (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    BST
      ('ForkTree
         l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
-> BST
     ('ForkTree
        l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> BST r -> Proxy n -> Proxy o -> GtN (Insert x a r) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Node x a
-> BST t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True
proofGtNInsert' Node x a
node BST r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
   ~ 'True) =>
  BST
    ('ForkTree
       l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
 -> BST
      ('ForkTree
         l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    BST
      ('ForkTree
         l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
-> BST
     ('ForkTree
        l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall a b. (a -> b) -> a -> b
$
      BST l
-> Node n a
-> BST (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> BST
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)
ForkBST BST l
l Node n a
node' (Node x a -> BST r -> Proxy o -> BST (Insert' x a r o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> BST t -> Proxy o -> BST (Insert' x a t o)
insert' Node x a
node BST r
r Proxy o
po)
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o

-- | Prove that inserting a node with key @x@ (lower than @n@) and element value @a@
-- in a `BST` @t@ which verifies @LtN t n ~ 'True@ preserves the `LtN` invariant,
-- given that the comparison between @x@ and the root key of the tree equals @o@.
-- The @o@ parameter guides the proof.
class ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofLtNInsert' ::
    (CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
    Node x a ->
    BST t ->
    Proxy n ->
    Proxy o ->
    LtN (Insert x a t) n :~: 'True

instance
  (CmpNat x n1 ~ 'EQ) =>
  ProofLtNInsert' x a ('ForkTree l (Node n1 a1) r) n 'EQ
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT, LtN ('ForkTree l (Node n1 a1) r) n ~ 'True) =>
Node x a
-> BST ('ForkTree l (Node n1 a1) r)
-> Proxy n
-> Proxy 'EQ
-> LtN (Insert x a ('ForkTree l (Node n1 a1) r)) n :~: 'True
proofLtNInsert' Node x a
_ BST ('ForkTree l (Node n1 a1) r)
_ Proxy n
_ Proxy 'EQ
_ = LtN (Insert x a ('ForkTree l (Node n1 a1) r)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (CmpNat x n1 ~ 'LT) =>
  ProofLtNInsert' x a ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT,
 LtN ('ForkTree 'EmptyTree (Node n1 a1) r) n ~ 'True) =>
Node x a
-> BST ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN (Insert x a ('ForkTree 'EmptyTree (Node n1 a1) r)) n
   :~: 'True
proofLtNInsert' Node x a
_ BST ('ForkTree 'EmptyTree (Node n1 a1) r)
_ Proxy n
_ Proxy 'LT
_ = LtN (Insert x a ('ForkTree 'EmptyTree (Node n1 a1) r)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    CmpNat x n1 ~ 'LT,
    LtN l n ~ 'True,
    ProofLtNInsert' x a l n o
  ) =>
  ProofLtNInsert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r) n 'LT
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT,
 LtN ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r) n
 ~ 'True) =>
Node x a
-> BST ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN
     (Insert
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r))
     n
   :~: 'True
proofLtNInsert' Node x a
node (ForkBST BST l
l Node n a
_ BST r
_) Proxy n
pn Proxy 'LT
_ =
    (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    If
      (CmpNat n1 n == 'LT)
      (If
         (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n)
         (If (LtN r n) 'True (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'LT)
     (If
        (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n)
        (If (LtN r n) 'True (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> BST l -> Proxy n -> Proxy o -> LtN (Insert x a l) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Node x a
-> BST t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True
proofLtNInsert' Node x a
node BST l
l Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'LT)
  (If
     (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n)
     (If (LtN r n) 'True (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (CmpNat x n1 ~ 'GT) =>
  ProofLtNInsert' x a ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT,
 LtN ('ForkTree l (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Node x a
-> BST ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> LtN (Insert x a ('ForkTree l (Node n1 a1) 'EmptyTree)) n
   :~: 'True
proofLtNInsert' Node x a
_ BST ('ForkTree l (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'GT
_ = LtN (Insert x a ('ForkTree l (Node n1 a1) 'EmptyTree)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    CmpNat x n1 ~ 'GT,
    LtN r n ~ 'True,
    ProofLtNInsert' x a r n o
  ) =>
  ProofLtNInsert' x a ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)) n 'GT
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT,
 LtN ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)) n
 ~ 'True) =>
Node x a
-> BST ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy n
-> Proxy 'GT
-> LtN
     (Insert
        x a ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)))
     n
   :~: 'True
proofLtNInsert' Node x a
node (ForkBST BST l
_ Node n a
_ BST r
r) Proxy n
pn Proxy 'GT
_ =
    (LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n :~: 'True)
-> ((LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    If
      (CmpNat n1 n == 'LT)
      (If
         (LtN l n)
         (If
            (LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n)
            'True
            (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'LT)
     (If
        (LtN l n)
        (If
           (LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n)
           'True
           (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> BST r -> Proxy n -> Proxy o -> LtN (Insert x a r) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Node x a
-> BST t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True
proofLtNInsert' Node x a
node BST r
r Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'LT)
  (If
     (LtN l n)
     (If
        (LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n)
        'True
        (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that inserting a node with key @x@ (greater than @n@) and element value @a@
-- in a `BST` @t@ which verifies @GtN t n ~ 'True@ preserves the `GtN` invariant,
-- given that the comparison between @x@ and the root key of the tree equals @o@.
-- The @o@ parameter guides the proof.
class ProofGtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofGtNInsert' ::
    (CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
    Node x a ->
    BST t ->
    Proxy n ->
    Proxy o ->
    GtN (Insert x a t) n :~: 'True

instance
  (CmpNat x n1 ~ 'EQ) =>
  ProofGtNInsert' x a ('ForkTree l (Node n1 a1) r) n 'EQ
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT, GtN ('ForkTree l (Node n1 a1) r) n ~ 'True) =>
Node x a
-> BST ('ForkTree l (Node n1 a1) r)
-> Proxy n
-> Proxy 'EQ
-> GtN (Insert x a ('ForkTree l (Node n1 a1) r)) n :~: 'True
proofGtNInsert' Node x a
_ BST ('ForkTree l (Node n1 a1) r)
_ Proxy n
_ Proxy 'EQ
_ = GtN (Insert x a ('ForkTree l (Node n1 a1) r)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (CmpNat x n1 ~ 'LT) =>
  ProofGtNInsert' x a ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT,
 GtN ('ForkTree 'EmptyTree (Node n1 a1) r) n ~ 'True) =>
Node x a
-> BST ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN (Insert x a ('ForkTree 'EmptyTree (Node n1 a1) r)) n
   :~: 'True
proofGtNInsert' Node x a
_ BST ('ForkTree 'EmptyTree (Node n1 a1) r)
_ Proxy n
_ Proxy 'LT
_ = GtN (Insert x a ('ForkTree 'EmptyTree (Node n1 a1) r)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    CmpNat x n1 ~ 'LT,
    GtN l n ~ 'True,
    ProofGtNInsert' x a l n o
  ) =>
  ProofGtNInsert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r) n 'LT
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT,
 GtN ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r) n
 ~ 'True) =>
Node x a
-> BST ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN
     (Insert
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r))
     n
   :~: 'True
proofGtNInsert' Node x a
node (ForkBST BST l
l Node n a
_ BST r
_) Proxy n
pn Proxy 'LT
_ =
    (GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n :~: 'True)
-> ((GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    If
      (CmpNat n1 n == 'GT)
      (If
         (GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n)
         (If (GtN r n) 'True (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'GT)
     (If
        (GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n)
        (If (GtN r n) 'True (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> BST l -> Proxy n -> Proxy o -> GtN (Insert x a l) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Node x a
-> BST t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True
proofGtNInsert' Node x a
node BST l
l Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'GT)
  (If
     (GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n)
     (If (GtN r n) 'True (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (CmpNat x n1 ~ 'GT) =>
  ProofGtNInsert' x a ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT,
 GtN ('ForkTree l (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Node x a
-> BST ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> GtN (Insert x a ('ForkTree l (Node n1 a1) 'EmptyTree)) n
   :~: 'True
proofGtNInsert' Node x a
_ BST ('ForkTree l (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'GT
_ = GtN (Insert x a ('ForkTree l (Node n1 a1) 'EmptyTree)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    CmpNat x n1 ~ 'GT,
    GtN r n ~ 'True,
    ProofGtNInsert' x a r n o
  ) =>
  ProofGtNInsert' x a ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)) n 'GT
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT,
 GtN ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)) n
 ~ 'True) =>
Node x a
-> BST ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy n
-> Proxy 'GT
-> GtN
     (Insert
        x a ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)))
     n
   :~: 'True
proofGtNInsert' Node x a
node (ForkBST BST l
_ Node n a
_ BST r
r) Proxy n
pn Proxy 'GT
_ =
    (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    If
      (CmpNat n1 n == 'GT)
      (If
         (GtN l n)
         (If
            (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n)
            'True
            (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'GT)
     (If
        (GtN l n)
        (If
           (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n)
           'True
           (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> BST r -> Proxy n -> Proxy o -> GtN (Insert x a r) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Node x a
-> BST t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True
proofGtNInsert' Node x a
node BST r
r Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'GT)
  (If
     (GtN l n)
     (If
        (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n)
        'True
        (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl