{-# 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.Delete
-- Description : Deletion 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 deletion 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.Delete
  ( Deletable (Delete, delete),
  )
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 delete the node with maximum key value
-- in a `BST` @t@.
-- The deletion is defined at the value level and the type level.
class MaxKeyDeletable (t :: Tree) where
  type MaxKeyDelete (t :: Tree) :: Tree
  maxKeyDelete ::
    (t ~ 'ForkTree l (Node n a1) r) =>
    BST t ->
    BST (MaxKeyDelete t)

instance MaxKeyDeletable ('ForkTree l (Node n a1) 'EmptyTree) where
  type MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree) = l
  maxKeyDelete :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) 'EmptyTree ~ 'ForkTree l (Node n a1) r) =>
BST ('ForkTree l (Node n a1) 'EmptyTree)
-> BST (MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree))
maxKeyDelete (ForkBST BST l
l Node n a
_ BST r
_) = BST l
BST (MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree))
l

instance
  (r ~ 'ForkTree rl (Node rn ra) rr, MaxKeyDeletable r, ProofGtNMaxKeyDelete r n) =>
  MaxKeyDeletable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
  where
  type
    MaxKeyDelete ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) =
      'ForkTree l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
  maxKeyDelete :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a1) r) =>
BST ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> BST
     (MaxKeyDelete
        ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)))
maxKeyDelete (ForkBST BST l
l Node n a
node BST r
r) =
    (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    BST
      ('ForkTree
         l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
-> BST
     ('ForkTree
        l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST r -> Proxy n -> GtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
BST t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete BST r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) (((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
  BST
    ('ForkTree
       l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
 -> BST
      ('ForkTree
         l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    BST
      ('ForkTree
         l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
-> BST
     ('ForkTree
        l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall a b. (a -> b) -> a -> b
$
      BST l
-> Node n a
-> BST (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
-> BST
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
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 -> BST (MaxKeyDelete r)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
BST t -> BST (MaxKeyDelete t)
maxKeyDelete BST r
r)

-- | This type class provides the functionality to get the key, type and value of the node
-- with maximum key value in a `BST` @t@.
-- The lookup is defined at the value level and the type level.
-- Since the keys are only kept at the type level,
-- there's no value level getter of the maximum key.
class Maxable (t :: Tree) where
  type MaxKey (t :: Tree) :: Nat
  type MaxValue (t :: Tree) :: Type
  maxValue ::
    (t ~ 'ForkTree l (Node n a1) r) =>
    BST t ->
    MaxValue t

instance Maxable ('ForkTree l (Node n a1) 'EmptyTree) where
  type MaxKey ('ForkTree l (Node n a1) 'EmptyTree) = n
  type MaxValue ('ForkTree l (Node n a1) 'EmptyTree) = a1
  maxValue :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) 'EmptyTree ~ 'ForkTree l (Node n a1) r) =>
BST ('ForkTree l (Node n a1) 'EmptyTree)
-> MaxValue ('ForkTree l (Node n a1) 'EmptyTree)
maxValue (ForkBST BST l
_ Node n a
node BST r
_) = Node n a -> a
forall (k :: Nat) a. Node k a -> a
getValue Node n a
node

instance
  (Maxable ('ForkTree rl (Node rn ra) rr)) =>
  Maxable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
  where
  type
    MaxKey ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) =
      MaxKey ('ForkTree rl (Node rn ra) rr)
  type
    MaxValue ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) =
      MaxValue ('ForkTree rl (Node rn ra) rr)
  maxValue :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a1) r) =>
BST ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> MaxValue
     ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
maxValue (ForkBST BST l
_ Node n a
_ BST r
r) = BST r -> MaxValue r
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(Maxable t, t ~ 'ForkTree l (Node n a1) r) =>
BST t -> MaxValue t
maxValue BST r
r

-- | This type class provides the functionality to delete a node with key @x@
-- in a `BST` @t@.
-- The deletion is defined at the value level and the type level.
-- The returned tree verifies the BST invariant.
class Deletable (x :: Nat) (t :: Tree) where
  type Delete (x :: Nat) (t :: Tree) :: Tree
  delete :: Proxy x -> BST t -> BST (Delete x t)

instance Deletable x 'EmptyTree where
  type Delete x 'EmptyTree = 'EmptyTree
  delete :: Proxy x -> BST 'EmptyTree -> BST (Delete x 'EmptyTree)
delete Proxy x
_ BST 'EmptyTree
_ = BST 'EmptyTree
BST (Delete x 'EmptyTree)
EmptyBST

instance
  ( o ~ CmpNat x n,
    Deletable' x ('ForkTree l (Node n a1) r) o
  ) =>
  Deletable x ('ForkTree l (Node n a1) r)
  where
  type Delete x ('ForkTree l (Node n a1) r) = Delete' x ('ForkTree l (Node n a1) r) (CmpNat x n)
  delete :: Proxy x
-> BST ('ForkTree l (Node n a1) r)
-> BST (Delete x ('ForkTree l (Node n a1) r))
delete Proxy x
px BST ('ForkTree l (Node n a1) r)
t = Proxy x
-> BST ('ForkTree l (Node n a1) r)
-> Proxy o
-> BST (Delete' x ('ForkTree l (Node n a1) r) o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
Deletable' x t o =>
Proxy x -> BST t -> Proxy o -> BST (Delete' x t o)
delete' Proxy x
px 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 delete a node with key @x@
-- in a non empty `BST` @t@.
-- It's only used by the 'Deletable' 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 Deletable' (x :: Nat) (t :: Tree) (o :: Ordering) where
  type Delete' (x :: Nat) (t :: Tree) (o :: Ordering) :: Tree
  delete' :: Proxy x -> BST t -> Proxy o -> BST (Delete' x t o)

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ where
  type Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ = 'EmptyTree
  delete' :: Proxy x
-> BST ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> BST
     (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
delete' Proxy x
_ BST ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
_ Proxy 'EQ
_ = BST 'EmptyTree
BST (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
EmptyBST

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ where
  type
    Delete' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ =
      'ForkTree rl (Node rn ra) rr
  delete' :: Proxy x
-> BST
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> BST
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
delete' Proxy x
_ (ForkBST BST l
_ Node n a
_ BST r
r) Proxy 'EQ
_ = BST r
BST
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
r

instance Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ where
  type
    Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ =
      'ForkTree ll (Node ln la) lr
  delete' :: Proxy x
-> BST
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> BST
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
        'EQ)
delete' Proxy x
_ (ForkBST BST l
l Node n a
_ BST r
_) Proxy 'EQ
_ = BST l
BST
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
     'EQ)
l

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    LtN (MaxKeyDelete l) (MaxKey l) ~ 'True,
    GtN r (MaxKey l) ~ 'True,
    Show (MaxValue l),
    MaxKeyDeletable l,
    Maxable l,
    ProofLtNMaxKeyDelete l n,
    ProofLTMaxKey l n
  ) =>
  Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ
  where
  type
    Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ =
      'ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node (MaxKey ('ForkTree ll (Node ln la) lr)) (MaxValue ('ForkTree ll (Node ln la) lr)))
        ('ForkTree rl (Node rn ra) rr)
  delete' :: Proxy x
-> BST
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n a1)
        ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> BST
     (Delete'
        x
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a1)
           ('ForkTree rl (Node rn ra) rr))
        'EQ)
delete' Proxy x
_ (ForkBST BST l
l Node n a
_ BST r
r) Proxy 'EQ
_ =
    (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    BST
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> BST
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        ('ForkTree rl (Node rn ra) rr))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST l -> Proxy n -> LtN (MaxKeyDelete l) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNMaxKeyDelete t n, LtN t n ~ 'True) =>
BST t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
proofLtNMaxKeyDelete BST l
l Proxy n
pn) (((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n ~ 'True) =>
  BST
    ('ForkTree
       (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
       (Node
          (MaxKey ('ForkTree ll (Node ln la) lr))
          (MaxValue ('ForkTree ll (Node ln la) lr)))
       ('ForkTree rl (Node rn ra) rr)))
 -> BST
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    BST
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> BST
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        ('ForkTree rl (Node rn ra) rr))
forall a b. (a -> b) -> a -> b
$
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n :~: 'LT)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
    BST
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> BST
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        ('ForkTree rl (Node rn ra) rr))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST l -> Proxy n -> CmpNat (MaxKey l) n :~: 'LT
forall (t :: Tree) (n :: Nat).
(ProofLTMaxKey t n, LtN t n ~ 'True) =>
BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
proofLTMaxKey BST l
l Proxy n
pn) (((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
  BST
    ('ForkTree
       (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
       (Node
          (MaxKey ('ForkTree ll (Node ln la) lr))
          (MaxValue ('ForkTree ll (Node ln la) lr)))
       ('ForkTree rl (Node rn ra) rr)))
 -> BST
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
    BST
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> BST
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        ('ForkTree rl (Node rn ra) rr))
forall a b. (a -> b) -> a -> b
$
        BST (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
-> BST r
-> BST
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        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 (MaxKeyDelete l)
BST (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
l' Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node' BST r
r
    where
      pn :: Proxy n
pn = Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n
      l' :: BST (MaxKeyDelete l)
l' = BST l -> BST (MaxKeyDelete l)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
BST t -> BST (MaxKeyDelete t)
maxKeyDelete BST l
l
      node' :: Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node' = Proxy (MaxKey ('ForkTree ll (Node ln la) lr))
-> MaxValue ('ForkTree ll (Node ln la) lr)
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy (MaxKey l)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (MaxKey l)) (BST l -> MaxValue l
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(Maxable t, t ~ 'ForkTree l (Node n a1) r) =>
BST t -> MaxValue t
maxValue BST l
l)

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT where
  type
    Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT =
      'ForkTree 'EmptyTree (Node n a1) r
  delete' :: Proxy x
-> BST ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> BST (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
delete' Proxy x
_ BST ('ForkTree 'EmptyTree (Node n a1) r)
t Proxy 'LT
_ = BST ('ForkTree 'EmptyTree (Node n a1) r)
BST (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
t

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    o ~ CmpNat x ln,
    Deletable' x l o,
    ProofLtNDelete' x l n o
  ) =>
  Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT
  where
  type
    Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT =
      'ForkTree (Delete' x ('ForkTree ll (Node ln la) lr) (CmpNat x ln)) (Node n a1) r
  delete' :: Proxy x
-> BST ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r)
-> Proxy 'LT
-> BST
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT)
delete' Proxy x
px (ForkBST BST l
l Node n a
node BST r
r) Proxy 'LT
_ =
    (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    BST
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r))
-> BST
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> BST l -> Proxy n -> Proxy o -> LtN (Delete' x l o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNDelete' x t n o, LtN t n ~ 'True) =>
Proxy x
-> BST t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px BST l
l (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
  BST
    ('ForkTree
       (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r))
 -> BST
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r))
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    BST
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r))
-> BST
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
forall a b. (a -> b) -> a -> b
$
      BST (Delete' x ('ForkTree ll (Node ln la) lr) o)
-> Node n a
-> BST r
-> BST
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) 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 BST (Delete' x l o)
BST (Delete' x ('ForkTree ll (Node ln la) lr) o)
l' Node n a
node BST r
r
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o
      l' :: BST (Delete' x l o)
l' = Proxy x -> BST l -> Proxy o -> BST (Delete' x l o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
Deletable' x t o =>
Proxy x -> BST t -> Proxy o -> BST (Delete' x t o)
delete' Proxy x
px BST l
l Proxy o
po

instance Deletable' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT where
  type Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT = 'ForkTree l (Node n a1) 'EmptyTree
  delete' :: Proxy x
-> BST ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> BST (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
delete' Proxy x
_ BST ('ForkTree l (Node n a1) 'EmptyTree)
t Proxy 'GT
_ = BST ('ForkTree l (Node n a1) 'EmptyTree)
BST (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
t

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    o ~ CmpNat x rn,
    Deletable' x r o,
    ProofGtNDelete' x r n o
  ) =>
  Deletable' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT
  where
  type
    Delete' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT =
      'ForkTree l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) (CmpNat x rn))
  delete' :: Proxy x
-> BST ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'GT
-> BST
     (Delete'
        x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT)
delete' Proxy x
px (ForkBST BST l
l Node n a
node BST r
r) Proxy 'GT
_ =
    (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    BST
      ('ForkTree
         l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
-> BST
     ('ForkTree
        l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> BST r -> Proxy n -> Proxy o -> GtN (Delete' x r o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNDelete' x t n o, GtN t n ~ 'True) =>
Proxy x
-> BST t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px BST r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
  BST
    ('ForkTree
       l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
 -> BST
      ('ForkTree
         l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    BST
      ('ForkTree
         l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
-> BST
     ('ForkTree
        l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall a b. (a -> b) -> a -> b
$
      BST l
-> Node n a
-> BST (Delete' x ('ForkTree rl (Node rn ra) rr) o)
-> BST
     ('ForkTree
        l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) 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 BST (Delete' x r o)
BST (Delete' x ('ForkTree rl (Node rn ra) rr) o)
r'
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o
      r' :: BST (Delete' x r o)
r' = Proxy x -> BST r -> Proxy o -> BST (Delete' x r o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
Deletable' x t o =>
Proxy x -> BST t -> Proxy o -> BST (Delete' x t o)
delete' Proxy x
px BST r
r Proxy o
po

-- | Prove that deleting a node with key @x@ (lower than @n@)
-- 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 ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofLtNDelete' ::
    (LtN t n ~ 'True) =>
    Proxy x ->
    BST t ->
    Proxy n ->
    Proxy o ->
    LtN (Delete' x t o) n :~: 'True

instance ProofLtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) n 'EQ where
  proofLtNDelete' :: (LtN ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Proxy x
-> BST ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'EQ
-> LtN
     (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) 'EQ) n
   :~: 'True
proofLtNDelete' Proxy x
_ BST ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = LtN
  (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) 'EQ) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (LtN ('ForkTree rl (Node rn ra) rr) n ~ 'True) =>
  ProofLtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'EQ
  where
  proofLtNDelete' :: (LtN
   ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
   n
 ~ 'True) =>
Proxy x
-> BST
     ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'EQ
-> LtN
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
     n
   :~: 'True
proofLtNDelete' Proxy x
_ BST
  ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
_ Proxy n
_ Proxy 'EQ
_ = LtN
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (LtN ('ForkTree ll (Node ln la) lr) n ~ 'True) =>
  ProofLtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree) n 'EQ
  where
  proofLtNDelete' :: (LtN
   ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
   n
 ~ 'True) =>
Proxy x
-> BST
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'EQ
-> LtN
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
        'EQ)
     n
   :~: 'True
proofLtNDelete' Proxy x
_ BST
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = LtN
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    LtN l n ~ 'True,
    LtN r n ~ 'True,
    ProofLTMaxKey l n,
    ProofLtNMaxKeyDelete l n
  ) =>
  ProofLtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'EQ
  where
  proofLtNDelete' :: (LtN
   ('ForkTree
      ('ForkTree ll (Node ln la) lr)
      (Node n1 a1)
      ('ForkTree rl (Node rn ra) rr))
   n
 ~ 'True) =>
Proxy x
-> BST
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n1 a1)
        ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'EQ
-> LtN
     (Delete'
        x
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n1 a1)
           ('ForkTree rl (Node rn ra) rr))
        'EQ)
     n
   :~: 'True
proofLtNDelete' Proxy x
_ (ForkBST BST l
l Node n a
_ BST r
_) Proxy n
pn Proxy 'EQ
_ =
    (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
      (If
         (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
     (If
        (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST l -> Proxy n -> LtN (MaxKeyDelete l) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNMaxKeyDelete t n, LtN t n ~ 'True) =>
BST t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
proofLtNMaxKeyDelete BST l
l Proxy n
pn) (((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n ~ 'True) =>
  If
    (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
    (If
       (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
       'True
       (TypeError ...))
    (TypeError ...)
  :~: 'True)
 -> If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
      (If
         (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
      (If
         (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
     (If
        (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n :~: 'LT)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
      (If
         (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
     (If
        (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST l -> Proxy n -> CmpNat (MaxKey l) n :~: 'LT
forall (t :: Tree) (n :: Nat).
(ProofLTMaxKey t n, LtN t n ~ 'True) =>
BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
proofLTMaxKey BST l
l Proxy n
pn) (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
If
  (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
  (If
     (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
     'True
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance ProofLtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT where
  proofLtNDelete' :: (LtN ('ForkTree 'EmptyTree (Node n1 a1) r) n ~ 'True) =>
Proxy x
-> BST ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
   :~: 'True
proofLtNDelete' Proxy x
_ BST ('ForkTree 'EmptyTree (Node n1 a1) r)
_ Proxy n
_ Proxy 'LT
_ = LtN (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    o ~ CmpNat x ln,
    LtN l n ~ 'True,
    ProofLtNDelete' x l n o
  ) =>
  ProofLtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n 'LT
  where
  proofLtNDelete' :: (LtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n
 ~ 'True) =>
Proxy x
-> BST ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) 'LT)
     n
   :~: 'True
proofLtNDelete' Proxy x
px (ForkBST BST l
l Node n a
_ BST r
_) Proxy n
pn Proxy 'LT
_ =
    (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    If
      (CmpNat n1 n == 'LT)
      (If
         (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
         (If (LtN r n) 'True (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'LT)
     (If
        (LtN (Delete' x ('ForkTree ll (Node ln la) 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 (Proxy x
-> BST l -> Proxy n -> Proxy o -> LtN (Delete' x l o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNDelete' x t n o, LtN t n ~ 'True) =>
Proxy x
-> BST t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px BST l
l Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'LT)
  (If
     (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
     (If (LtN r n) 'True (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance ProofLtNDelete' x ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT where
  proofLtNDelete' :: (LtN ('ForkTree l (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Proxy x
-> BST ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> LtN (Delete' x ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
   :~: 'True
proofLtNDelete' Proxy x
_ BST ('ForkTree l (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'GT
_ = LtN (Delete' x ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

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

-- | Prove that deleting a node with key @x@ (greater than @n@)
-- 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 ProofGtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofGtNDelete' ::
    (GtN t n ~ 'True) =>
    Proxy x ->
    BST t ->
    Proxy n ->
    Proxy o ->
    GtN (Delete' x t o) n :~: 'True

instance ProofGtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) n 'EQ where
  proofGtNDelete' :: (GtN ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Proxy x
-> BST ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'EQ
-> GtN
     (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) 'EQ) n
   :~: 'True
proofGtNDelete' Proxy x
_ BST ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = GtN
  (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) 'EQ) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (GtN ('ForkTree rl (Node rn ra) rr) n ~ 'True) =>
  ProofGtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'EQ
  where
  proofGtNDelete' :: (GtN
   ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
   n
 ~ 'True) =>
Proxy x
-> BST
     ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'EQ
-> GtN
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
     n
   :~: 'True
proofGtNDelete' Proxy x
_ BST
  ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
_ Proxy n
_ Proxy 'EQ
_ = GtN
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (GtN ('ForkTree ll (Node ln la) lr) n ~ 'True) =>
  ProofGtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree) n 'EQ
  where
  proofGtNDelete' :: (GtN
   ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
   n
 ~ 'True) =>
Proxy x
-> BST
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'EQ
-> GtN
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
        'EQ)
     n
   :~: 'True
proofGtNDelete' Proxy x
_ BST
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = GtN
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    GtN l n ~ 'True,
    GtN r n ~ 'True,
    ProofGTMaxKey l n,
    ProofGtNMaxKeyDelete l n
  ) =>
  ProofGtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n 'EQ
  where
  proofGtNDelete' :: (GtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n
 ~ 'True) =>
Proxy x
-> BST ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'EQ
-> GtN
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) 'EQ)
     n
   :~: 'True
proofGtNDelete' Proxy x
_ (ForkBST BST l
l Node n a
_ BST r
_) Proxy n
pn Proxy 'EQ
_ =
    (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
      (If
         (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
     (If
        (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST l -> Proxy n -> GtN (MaxKeyDelete l) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
BST t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete BST l
l Proxy n
pn) (((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n ~ 'True) =>
  If
    (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
    (If
       (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
       'True
       (TypeError ...))
    (TypeError ...)
  :~: 'True)
 -> If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
      (If
         (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
      (If
         (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
     (If
        (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n :~: 'GT)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'GT) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
      (If
         (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
     (If
        (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST l -> Proxy n -> CmpNat (MaxKey l) n :~: 'GT
forall (t :: Tree) (n :: Nat).
(ProofGTMaxKey t n, GtN t n ~ 'True) =>
BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT
proofGTMaxKey BST l
l Proxy n
pn) (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'GT) =>
If
  (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
  (If
     (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
     'True
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance ProofGtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT where
  proofGtNDelete' :: (GtN ('ForkTree 'EmptyTree (Node n1 a1) r) n ~ 'True) =>
Proxy x
-> BST ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
   :~: 'True
proofGtNDelete' Proxy x
_ BST ('ForkTree 'EmptyTree (Node n1 a1) r)
_ Proxy n
_ Proxy 'LT
_ = GtN (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    o ~ CmpNat x ln,
    GtN l n ~ 'True,
    ProofGtNDelete' x l n o
  ) =>
  ProofGtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n 'LT
  where
  proofGtNDelete' :: (GtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n
 ~ 'True) =>
Proxy x
-> BST ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) 'LT)
     n
   :~: 'True
proofGtNDelete' Proxy x
px (ForkBST BST l
l Node n a
_ BST r
_) Proxy n
pn Proxy 'LT
_ =
    (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    If
      (CmpNat n1 n == 'GT)
      (If
         (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
         (If (GtN r n) 'True (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'GT)
     (If
        (GtN (Delete' x ('ForkTree ll (Node ln la) 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 (Proxy x
-> BST l -> Proxy n -> Proxy o -> GtN (Delete' x l o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNDelete' x t n o, GtN t n ~ 'True) =>
Proxy x
-> BST t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px BST l
l Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'GT)
  (If
     (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
     (If (GtN r n) 'True (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance ProofGtNDelete' x ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT where
  proofGtNDelete' :: (GtN ('ForkTree l (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Proxy x
-> BST ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> GtN (Delete' x ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
   :~: 'True
proofGtNDelete' Proxy x
_ BST ('ForkTree l (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'GT
_ = GtN (Delete' x ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

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

-- | Prove that in a `BST` @t@ which verifies that @GtN t n ~ 'True@,
-- the maximum key of @t@ is also greater than @n@.
-- This proof is needed for the `delete` operation.
class ProofGTMaxKey (t :: Tree) (n :: Nat) where
  proofGTMaxKey ::
    (GtN t n ~ 'True) =>
    BST t ->
    Proxy n ->
    CmpNat (MaxKey t) n :~: 'GT

instance
  (CmpNat n1 n ~ 'GT) =>
  ProofGTMaxKey ('ForkTree l (Node n1 a) 'EmptyTree) n
  where
  proofGTMaxKey :: (GtN ('ForkTree l (Node n1 a) 'EmptyTree) n ~ 'True) =>
BST ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'GT
proofGTMaxKey BST ('ForkTree l (Node n1 a) 'EmptyTree)
_ Proxy n
_ = CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'GT
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    GtN r n ~ 'True,
    ProofGTMaxKey r n
  ) =>
  ProofGTMaxKey ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofGTMaxKey :: (GtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
BST ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> CmpNat
     (MaxKey ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))) n
   :~: 'GT
proofGTMaxKey (ForkBST BST l
_ Node n a
_ BST r
r) Proxy n
pn =
    (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT)
-> ((CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'GT) =>
    CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT)
-> CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST r -> Proxy n -> CmpNat (MaxKey r) n :~: 'GT
forall (t :: Tree) (n :: Nat).
(ProofGTMaxKey t n, GtN t n ~ 'True) =>
BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT
proofGTMaxKey BST r
r Proxy n
pn) (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'GT) =>
CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT
forall {k} (a :: k). a :~: a
Refl

-- | Prove that in a `BST` @t@ which verifies that @GtN t n ~ 'True@,
-- the tree resulting from the removal of the maximum key of @t@ preserves the `GtN` invariant.
-- This proof is needed for the `delete` operation.
class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where
  proofGtNMaxKeyDelete ::
    (GtN t n ~ 'True) =>
    BST t ->
    Proxy n ->
    GtN (MaxKeyDelete t) n :~: 'True

instance
  (GtN l n ~ 'True) =>
  ProofGtNMaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree) n
  where
  proofGtNMaxKeyDelete :: (GtN ('ForkTree l (Node n1 a) 'EmptyTree) n ~ 'True) =>
BST ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> GtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n
   :~: 'True
proofGtNMaxKeyDelete BST ('ForkTree l (Node n1 a) 'EmptyTree)
_ Proxy n
_ = GtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    GtN r n ~ 'True,
    ProofGtNMaxKeyDelete r n
  ) =>
  ProofGtNMaxKeyDelete ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofGtNMaxKeyDelete :: (GtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
BST ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> GtN
     (MaxKeyDelete
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)))
     n
   :~: 'True
proofGtNMaxKeyDelete (ForkBST BST l
_ Node n a
_ BST r
r) Proxy n
pn =
    (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    If
      (CmpNat n1 n == 'GT)
      (If
         (GtN l n)
         (If
            (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
            'True
            (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'GT)
     (If
        (GtN l n)
        (If
           (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
           'True
           (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST r -> Proxy n -> GtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
BST t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete BST r
r Proxy n
pn) (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
If
  (CmpNat n1 n == 'GT)
  (If
     (GtN l n)
     (If
        (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
        'True
        (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that in a `BST` @t@ which verifies that @LtN t n ~ 'True@,
-- the maximum key of @t@ is also less than @n@.
-- This proof is needed for the delete operation.
class ProofLTMaxKey (t :: Tree) (n :: Nat) where
  proofLTMaxKey ::
    (LtN t n ~ 'True) =>
    BST t ->
    Proxy n ->
    CmpNat (MaxKey t) n :~: 'LT

instance (CmpNat n1 n ~ 'LT) => ProofLTMaxKey ('ForkTree l (Node n1 a) 'EmptyTree) n where
  proofLTMaxKey :: (LtN ('ForkTree l (Node n1 a) 'EmptyTree) n ~ 'True) =>
BST ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'LT
proofLTMaxKey BST ('ForkTree l (Node n1 a) 'EmptyTree)
_ Proxy n
_ = CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'LT
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    LtN r n ~ 'True,
    ProofLTMaxKey r n
  ) =>
  ProofLTMaxKey ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofLTMaxKey :: (LtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
BST ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> CmpNat
     (MaxKey ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))) n
   :~: 'LT
proofLTMaxKey (ForkBST BST l
_ Node n a
_ BST r
r) Proxy n
pn =
    (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT)
-> ((CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'LT) =>
    CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT)
-> CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST r -> Proxy n -> CmpNat (MaxKey r) n :~: 'LT
forall (t :: Tree) (n :: Nat).
(ProofLTMaxKey t n, LtN t n ~ 'True) =>
BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
proofLTMaxKey BST r
r Proxy n
pn) (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'LT) =>
CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT
forall {k} (a :: k). a :~: a
Refl

-- | Prove that in a `BST` @t@ which verifies that @LtN t n ~ 'True@,
-- the tree resulting from the removal of the maximum key of @t@ preserves the `LtN` invariant.
-- This proof is needed for the delete operation.
class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where
  proofLtNMaxKeyDelete ::
    (LtN t n ~ 'True) =>
    BST t ->
    Proxy n ->
    LtN (MaxKeyDelete t) n :~: 'True

instance
  (LtN l n ~ 'True) =>
  ProofLtNMaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree) n
  where
  proofLtNMaxKeyDelete :: (LtN ('ForkTree l (Node n1 a) 'EmptyTree) n ~ 'True) =>
BST ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> LtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n
   :~: 'True
proofLtNMaxKeyDelete BST ('ForkTree l (Node n1 a) 'EmptyTree)
_ Proxy n
_ = LtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    LtN r n ~ 'True,
    ProofLtNMaxKeyDelete r n
  ) =>
  ProofLtNMaxKeyDelete ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofLtNMaxKeyDelete :: (LtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
BST ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> LtN
     (MaxKeyDelete
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)))
     n
   :~: 'True
proofLtNMaxKeyDelete (ForkBST BST l
_ Node n a
_ BST r
r) Proxy n
pn =
    (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    If
      (CmpNat n1 n == 'LT)
      (If
         (LtN l n)
         (If
            (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
            'True
            (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'LT)
     (If
        (LtN l n)
        (If
           (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
           'True
           (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (BST r -> Proxy n -> LtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNMaxKeyDelete t n, LtN t n ~ 'True) =>
BST t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
proofLtNMaxKeyDelete BST r
r Proxy n
pn) (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
If
  (CmpNat n1 n == 'LT)
  (If
     (LtN l n)
     (If
        (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
        'True
        (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl