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

-- |
-- Module      : Data.Tree.AVL.Extern.BalanceProofs
-- Description : Proofs for balance operations for externalist AVL trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the necessary proofs to ensure (at compile time) that the
-- balance algorithm defined in "Data.Tree.AVL.Extern.Balance" respects the key ordering and recovers the height balance.
module Data.Tree.AVL.Extern.BalanceProofs
  ( ProofIsBSTBalance (proofIsBSTBalance),
    ProofLtNBalance (proofLtNBalance),
    ProofGtNBalance (proofGtNBalance),
    ProofIsBalancedBalance (proofIsBalancedBalance),
  )
where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Extern.Balance
  ( Balanceable (Balance),
    Balanceable' (Balance'),
    Rotateable (Rotate),
  )
import Data.Tree.AVL.Extern.Constructors (IsAlmostBalancedT (ForkIsAlmostBalancedT), IsBalancedT (EmptyIsBalancedT, ForkIsBalancedT))
import Data.Tree.AVL.Invariants
  ( BS (Balanced, LeftHeavy, RightHeavy),
    BalancedHeights,
    BalancedState,
    Height,
    US (LeftUnbalanced, NotUnbalanced, RightUnbalanced),
    UnbalancedState,
  )
import Data.Tree.BST.Extern.Constructors (IsBSTT (EmptyIsBSTT, ForkIsBSTT))
import Data.Tree.BST.Invariants (GtN, LtN)
import Data.Tree.ITree (Tree (EmptyTree, ForkTree))
import Data.Tree.Node (Node)
import Data.Type.Equality (gcastWith, (:~:) (Refl))
import GHC.TypeNats (CmpNat, Nat, type (+), type (<=?))
import Prelude (Bool (True), Ordering (GT, LT))

-- | Prove that applying a rebalancing (a composition of rotations)
-- to a `Data.Tree.BST.Extern.Constructors.BST` tree preserves @BST@ condition.
-- The @BST@ invariant was already checked since this proof is called after proofs for `Data.Tree.BST.Extern.Insert.insert` or `Data.Tree.BST.Extern.Delete.delete`.
class ProofIsBSTBalance (t :: Tree) where
  proofIsBSTBalance :: IsBSTT t -> IsBSTT (Balance t)

instance ProofIsBSTBalance 'EmptyTree where
  proofIsBSTBalance :: IsBSTT 'EmptyTree -> IsBSTT (Balance 'EmptyTree)
proofIsBSTBalance IsBSTT 'EmptyTree
_ = IsBSTT 'EmptyTree
IsBSTT (Balance 'EmptyTree)
EmptyIsBSTT

instance
  (us ~ UnbalancedState (Height l) (Height r), ProofIsBSTBalance' ('ForkTree l (Node n a) r) us) =>
  ProofIsBSTBalance ('ForkTree l (Node n a) r)
  where
  proofIsBSTBalance :: IsBSTT ('ForkTree l (Node n a) r)
-> IsBSTT (Balance ('ForkTree l (Node n a) r))
proofIsBSTBalance IsBSTT ('ForkTree l (Node n a) r)
tIsBST = IsBSTT ('ForkTree l (Node n a) r)
-> Proxy us -> IsBSTT (Balance' ('ForkTree l (Node n a) r) us)
forall (t :: Tree) (us :: US).
ProofIsBSTBalance' t us =>
IsBSTT t -> Proxy us -> IsBSTT (Balance' t us)
proofIsBSTBalance' IsBSTT ('ForkTree l (Node n a) r)
tIsBST (Proxy us
forall {k} (t :: k). Proxy t
Proxy :: Proxy us)

-- | Prove that applying a rebalancing (a composition of rotations)
-- to a `Data.Tree.BST.Extern.Constructors.BST` tree preserves @BST@ condition, given the comparison @us@ of the heights of the left and right sub trees.
-- This is called only from `ProofIsBSTBalance`.
-- The @BST@ invariant was already checked since this proof is called after proofs for `Data.Tree.BST.Extern.Insert.insert` or `Data.Tree.BST.Extern.Delete.delete`.
class ProofIsBSTBalance' (t :: Tree) (us :: US) where
  proofIsBSTBalance' :: IsBSTT t -> Proxy us -> IsBSTT (Balance' t us)

instance ProofIsBSTBalance' ('ForkTree l (Node n a) r) 'NotUnbalanced where
  proofIsBSTBalance' :: IsBSTT ('ForkTree l (Node n a) r)
-> Proxy 'NotUnbalanced
-> IsBSTT (Balance' ('ForkTree l (Node n a) r) 'NotUnbalanced)
proofIsBSTBalance' IsBSTT ('ForkTree l (Node n a) r)
tIsBST Proxy 'NotUnbalanced
_ = IsBSTT ('ForkTree l (Node n a) r)
IsBSTT (Balance' ('ForkTree l (Node n a) r) 'NotUnbalanced)
tIsBST

instance
  ( bs ~ BalancedState (Height ll) (Height lr),
    ProofIsBSTRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced bs
  ) =>
  ProofIsBSTBalance' ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced
  where
  proofIsBSTBalance' :: IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> IsBSTT
     (Balance'
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced)
proofIsBSTBalance' IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
tIsBST Proxy 'LeftUnbalanced
pus = IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy bs
-> IsBSTT
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        bs)
forall (t :: Tree) (us :: US) (bs :: BS).
ProofIsBSTRotate t us bs =>
IsBSTT t -> Proxy us -> Proxy bs -> IsBSTT (Rotate t us bs)
proofIsBSTRotate IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
tIsBST Proxy 'LeftUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)

instance
  ( bs ~ BalancedState (Height rl) (Height rr),
    ProofIsBSTRotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced bs
  ) =>
  ProofIsBSTBalance' ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced
  where
  proofIsBSTBalance' :: IsBSTT ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> IsBSTT
     (Balance'
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced)
proofIsBSTBalance' IsBSTT ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
tIsBST Proxy 'RightUnbalanced
pus = IsBSTT ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy bs
-> IsBSTT
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        bs)
forall (t :: Tree) (us :: US) (bs :: BS).
ProofIsBSTRotate t us bs =>
IsBSTT t -> Proxy us -> Proxy bs -> IsBSTT (Rotate t us bs)
proofIsBSTRotate IsBSTT ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
tIsBST Proxy 'RightUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)

-- | Prove that applying a rotation
-- to a `Data.Tree.BST.Extern.Constructors.BST` tree preserves @BST@ condition.
-- The @BST@ invariant was already checked since this proof is called after proofs for `Data.Tree.BST.Extern.Insert.insert` or `Data.Tree.BST.Extern.Delete.delete`.
class ProofIsBSTRotate (t :: Tree) (us :: US) (bs :: BS) where
  proofIsBSTRotate :: IsBSTT t -> Proxy us -> Proxy bs -> IsBSTT (Rotate t us bs)

-- Left-Left case (Right rotation)
instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    CmpNat n ln ~ 'GT,
    GtN r ln ~ 'True,
    LtN lr n ~ 'True
  ) =>
  ProofIsBSTRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced 'LeftHeavy
  where
  proofIsBSTRotate :: IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy 'LeftHeavy
-> IsBSTT
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        'LeftHeavy)
proofIsBSTRotate (ForkIsBSTT (ForkIsBSTT IsBSTT l
ll Proxy (Node n a)
lnode IsBSTT r
lr) Proxy (Node n a)
node IsBSTT r
r) Proxy 'LeftUnbalanced
_ Proxy 'LeftHeavy
_ =
    IsBSTT l
-> Proxy (Node n a)
-> IsBSTT ('ForkTree r (Node n a) r)
-> IsBSTT ('ForkTree l (Node n a) ('ForkTree r (Node n a) r))
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT l
ll Proxy (Node n a)
lnode (IsBSTT r
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree r (Node n a) r)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT r
lr Proxy (Node n a)
node IsBSTT r
r)

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    CmpNat n ln ~ 'GT,
    GtN r ln ~ 'True,
    LtN lr n ~ 'True
  ) =>
  ProofIsBSTRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced 'Balanced
  where
  proofIsBSTRotate :: IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy 'Balanced
-> IsBSTT
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        'Balanced)
proofIsBSTRotate (ForkIsBSTT (ForkIsBSTT IsBSTT l
ll Proxy (Node n a)
lnode IsBSTT r
lr) Proxy (Node n a)
node IsBSTT r
r) Proxy 'LeftUnbalanced
_ Proxy 'Balanced
_ =
    IsBSTT l
-> Proxy (Node n a)
-> IsBSTT ('ForkTree r (Node n a) r)
-> IsBSTT ('ForkTree l (Node n a) ('ForkTree r (Node n a) r))
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT l
ll Proxy (Node n a)
lnode (IsBSTT r
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree r (Node n a) r)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT r
lr Proxy (Node n a)
node IsBSTT r
r)

-- Right-Right case (Left rotation)
instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    CmpNat n rn ~ 'LT,
    LtN l rn ~ 'True,
    GtN rl n ~ 'True
  ) =>
  ProofIsBSTRotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced 'RightHeavy
  where
  proofIsBSTRotate :: IsBSTT ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'RightHeavy
-> IsBSTT
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'RightHeavy)
proofIsBSTRotate (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node (ForkIsBSTT IsBSTT l
rl Proxy (Node n a)
rnode IsBSTT r
rr)) Proxy 'RightUnbalanced
_ Proxy 'RightHeavy
_ =
    IsBSTT ('ForkTree l (Node n a) l)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree ('ForkTree l (Node n a) l) (Node n a) r)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT l
-> IsBSTT ('ForkTree l (Node n a) l)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node IsBSTT l
rl) Proxy (Node n a)
rnode IsBSTT r
rr

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    CmpNat n rn ~ 'LT,
    LtN l rn ~ 'True,
    GtN rl n ~ 'True
  ) =>
  ProofIsBSTRotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced 'Balanced
  where
  proofIsBSTRotate :: IsBSTT ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'Balanced
-> IsBSTT
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'Balanced)
proofIsBSTRotate (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node (ForkIsBSTT IsBSTT l
rl Proxy (Node n a)
rnode IsBSTT r
rr)) Proxy 'RightUnbalanced
_ Proxy 'Balanced
_ =
    IsBSTT ('ForkTree l (Node n a) l)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree ('ForkTree l (Node n a) l) (Node n a) r)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT l
-> IsBSTT ('ForkTree l (Node n a) l)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node IsBSTT l
rl) Proxy (Node n a)
rnode IsBSTT r
rr

-- Left-Right case (First left rotation, then right rotation)
instance
  ( lr ~ 'ForkTree lrl (Node lrn lra) lrr,
    l ~ 'ForkTree ll (Node ln la) lr,
    CmpNat n lrn ~ 'GT,
    GtN r lrn ~ 'True,
    CmpNat ln lrn ~ 'LT,
    LtN ll lrn ~ 'True,
    GtN lrl ln ~ 'True,
    LtN lrr n ~ 'True
  ) =>
  ProofIsBSTRotate ('ForkTree ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr)) (Node n a) r) 'LeftUnbalanced 'RightHeavy
  where
  proofIsBSTRotate :: IsBSTT
  ('ForkTree
     ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
     (Node n a)
     r)
-> Proxy 'LeftUnbalanced
-> Proxy 'RightHeavy
-> IsBSTT
     (Rotate
        ('ForkTree
           ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
           (Node n a)
           r)
        'LeftUnbalanced
        'RightHeavy)
proofIsBSTRotate (ForkIsBSTT (ForkIsBSTT IsBSTT l
ll Proxy (Node n a)
lnode (ForkIsBSTT IsBSTT l
lrl Proxy (Node n a)
lrnode IsBSTT r
lrr)) Proxy (Node n a)
node IsBSTT r
r) Proxy 'LeftUnbalanced
_ Proxy 'RightHeavy
_ =
    IsBSTT ('ForkTree l (Node n a) l)
-> Proxy (Node n a)
-> IsBSTT ('ForkTree r (Node n a) r)
-> IsBSTT
     ('ForkTree
        ('ForkTree l (Node n a) l) (Node n a) ('ForkTree r (Node n a) r))
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT l
-> IsBSTT ('ForkTree l (Node n a) l)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT l
ll Proxy (Node n a)
lnode IsBSTT l
lrl) Proxy (Node n a)
lrnode (IsBSTT r
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree r (Node n a) r)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT r
lrr Proxy (Node n a)
node IsBSTT r
r)

-- Right-Left case (First right rotation, then left rotation)
instance
  ( rl ~ 'ForkTree rll (Node rln rla) rlr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    CmpNat rn rln ~ 'GT,
    GtN rr rln ~ 'True,
    CmpNat n rln ~ 'LT,
    LtN l rln ~ 'True,
    GtN rll n ~ 'True,
    LtN rlr rn ~ 'True
  ) =>
  ProofIsBSTRotate ('ForkTree l (Node n a) ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr)) 'RightUnbalanced 'LeftHeavy
  where
  proofIsBSTRotate :: IsBSTT
  ('ForkTree
     l
     (Node n a)
     ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'LeftHeavy
-> IsBSTT
     (Rotate
        ('ForkTree
           l
           (Node n a)
           ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
        'RightUnbalanced
        'LeftHeavy)
proofIsBSTRotate (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node (ForkIsBSTT (ForkIsBSTT IsBSTT l
rll Proxy (Node n a)
rlnode IsBSTT r
rlr) Proxy (Node n a)
rnode IsBSTT r
rr)) Proxy 'RightUnbalanced
_ Proxy 'LeftHeavy
_ =
    IsBSTT ('ForkTree l (Node n a) l)
-> Proxy (Node n a)
-> IsBSTT ('ForkTree r (Node n a) r)
-> IsBSTT
     ('ForkTree
        ('ForkTree l (Node n a) l) (Node n a) ('ForkTree r (Node n a) r))
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT l
-> IsBSTT ('ForkTree l (Node n a) l)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node IsBSTT l
rll) Proxy (Node n a)
rlnode (IsBSTT r
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree r (Node n a) r)
forall (l :: Tree) (r :: Nat) (n :: Tree) a.
(LtN l r ~ 'True, GtN n r ~ 'True) =>
IsBSTT l
-> Proxy (Node r a)
-> IsBSTT n
-> IsBSTT ('ForkTree l (Node r a) n)
ForkIsBSTT IsBSTT r
rlr Proxy (Node n a)
rnode IsBSTT r
rr)

-- | Prove that rebalancing a tree @t@ which verifies @LtN t n ~ 'True@ preserves the `LtN` invariant.
class ProofLtNBalance (t :: Tree) (n :: Nat) where
  proofLtNBalance ::
    (LtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    LtN (Balance t) n :~: 'True

instance ProofLtNBalance 'EmptyTree n where
  proofLtNBalance :: (LtN 'EmptyTree n ~ 'True) =>
IsBSTT 'EmptyTree
-> Proxy n -> LtN (Balance 'EmptyTree) n :~: 'True
proofLtNBalance IsBSTT 'EmptyTree
_ Proxy n
_ = LtN (Balance 'EmptyTree) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( us ~ UnbalancedState (Height l) (Height r),
    ProofLtNBalance' ('ForkTree l (Node n1 a) r) n us
  ) =>
  ProofLtNBalance ('ForkTree l (Node n1 a) r) n
  where
  proofLtNBalance :: (LtN ('ForkTree l (Node n1 a) r) n ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) r)
-> Proxy n -> LtN (Balance ('ForkTree l (Node n1 a) r)) n :~: 'True
proofLtNBalance IsBSTT ('ForkTree l (Node n1 a) r)
tIsBST Proxy n
pn = (LtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True)
-> ((LtN (Balance' ('ForkTree l (Node n1 a) r) us) n ~ 'True) =>
    LtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True)
-> LtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT ('ForkTree l (Node n1 a) r)
-> Proxy n
-> Proxy us
-> LtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True
forall (t :: Tree) (n :: Nat) (us :: US).
(ProofLtNBalance' t n us, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> Proxy us -> LtN (Balance' t us) n :~: 'True
proofLtNBalance' IsBSTT ('ForkTree l (Node n1 a) r)
tIsBST Proxy n
pn (Proxy us
forall {k} (t :: k). Proxy t
Proxy :: Proxy us)) (LtN (Balance' ('ForkTree l (Node n1 a) r) us) n ~ 'True) =>
LtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that rebalancing a tree @t@ which verifies @LtN t n ~ 'True@ preserves the `LtN` invariant,
-- given the unbalanced state @us@ of the tree.
class ProofLtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
  proofLtNBalance' ::
    (LtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    Proxy us ->
    LtN (Balance' t us) n :~: 'True

instance ProofLtNBalance' ('ForkTree l (Node n1 a) r) n 'NotUnbalanced where
  proofLtNBalance' :: (LtN ('ForkTree l (Node n1 a) r) n ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) r)
-> Proxy n
-> Proxy 'NotUnbalanced
-> LtN (Balance' ('ForkTree l (Node n1 a) r) 'NotUnbalanced) n
   :~: 'True
proofLtNBalance' IsBSTT ('ForkTree l (Node n1 a) r)
_ Proxy n
_ Proxy 'NotUnbalanced
_ = LtN (Balance' ('ForkTree l (Node n1 a) r) 'NotUnbalanced) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( bs ~ BalancedState (Height ll) (Height lr),
    ProofLtNRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n 'LeftUnbalanced bs
  ) =>
  ProofLtNBalance' ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n 'LeftUnbalanced
  where
  proofLtNBalance' :: (LtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n
 ~ 'True) =>
IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> LtN
     (Balance'
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced)
     n
   :~: 'True
proofLtNBalance' IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
tIsBST Proxy n
pn Proxy 'LeftUnbalanced
pus = (LtN
   (Rotate
      ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
      'LeftUnbalanced
      bs)
   n
 :~: 'True)
-> ((LtN
       (Rotate
          ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
          'LeftUnbalanced
          bs)
       n
     ~ 'True) =>
    LtN
      (Rotate
         ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
         'LeftUnbalanced
         bs)
      n
    :~: 'True)
-> LtN
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced
        bs)
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> Proxy bs
-> LtN
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced
        bs)
     n
   :~: 'True
forall (t :: Tree) (n :: Nat) (us :: US) (bs :: BS).
(ProofLtNRotate t n us bs, LtN t n ~ 'True) =>
IsBSTT t
-> Proxy n
-> Proxy us
-> Proxy bs
-> LtN (Rotate t us bs) n :~: 'True
proofLtNRotate IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
tIsBST Proxy n
pn Proxy 'LeftUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)) (LtN
   (Rotate
      ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
      'LeftUnbalanced
      bs)
   n
 ~ 'True) =>
LtN
  (Rotate
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
     'LeftUnbalanced
     bs)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( bs ~ BalancedState (Height rl) (Height rr),
    ProofLtNRotate ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n 'RightUnbalanced bs
  ) =>
  ProofLtNBalance' ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n 'RightUnbalanced
  where
  proofLtNBalance' :: (LtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> LtN
     (Balance'
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced)
     n
   :~: 'True
proofLtNBalance' IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
tIsBST Proxy n
pn Proxy 'RightUnbalanced
pus = (LtN
   (Rotate
      ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
      'RightUnbalanced
      bs)
   n
 :~: 'True)
-> ((LtN
       (Rotate
          ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
          'RightUnbalanced
          bs)
       n
     ~ 'True) =>
    LtN
      (Rotate
         ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
         'RightUnbalanced
         bs)
      n
    :~: 'True)
-> LtN
     (Rotate
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        bs)
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> Proxy bs
-> LtN
     (Rotate
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        bs)
     n
   :~: 'True
forall (t :: Tree) (n :: Nat) (us :: US) (bs :: BS).
(ProofLtNRotate t n us bs, LtN t n ~ 'True) =>
IsBSTT t
-> Proxy n
-> Proxy us
-> Proxy bs
-> LtN (Rotate t us bs) n :~: 'True
proofLtNRotate IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
tIsBST Proxy n
pn Proxy 'RightUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)) (LtN
   (Rotate
      ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
      'RightUnbalanced
      bs)
   n
 ~ 'True) =>
LtN
  (Rotate
     ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
     'RightUnbalanced
     bs)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that applying a rotation to a tree @t@ which verifies @LtN t n ~ 'True@ preserves the `LtN` invariant.
class ProofLtNRotate (t :: Tree) (n :: Nat) (us :: US) (bs :: BS) where
  proofLtNRotate ::
    (LtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    Proxy us ->
    Proxy bs ->
    LtN (Rotate t us bs) n :~: 'True

-- Left-Left case (Right rotation)
instance
  (LtN ll n ~ 'True, CmpNat ln n ~ 'LT, LtN lr n ~ 'True, LtN r n ~ 'True) =>
  ProofLtNRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n 'LeftUnbalanced 'LeftHeavy
  where
  proofLtNRotate :: (LtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n
 ~ 'True) =>
IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> Proxy 'LeftHeavy
-> LtN
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced
        'LeftHeavy)
     n
   :~: 'True
proofLtNRotate IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
_ Proxy n
_ Proxy 'LeftUnbalanced
_ Proxy 'LeftHeavy
_ = LtN
  (Rotate
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
     'LeftUnbalanced
     'LeftHeavy)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (LtN ll n ~ 'True, CmpNat ln n ~ 'LT, LtN lr n ~ 'True, LtN r n ~ 'True) =>
  ProofLtNRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n 'LeftUnbalanced 'Balanced
  where
  proofLtNRotate :: (LtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n
 ~ 'True) =>
IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> Proxy 'Balanced
-> LtN
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced
        'Balanced)
     n
   :~: 'True
proofLtNRotate IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
_ Proxy n
_ Proxy 'LeftUnbalanced
_ Proxy 'Balanced
_ = LtN
  (Rotate
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
     'LeftUnbalanced
     'Balanced)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- Right-Right case (Left rotation)
instance
  (LtN l n ~ 'True, LtN rl n ~ 'True, CmpNat rn n ~ 'LT, LtN rr n ~ 'True) =>
  ProofLtNRotate ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n 'RightUnbalanced 'RightHeavy
  where
  proofLtNRotate :: (LtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> Proxy 'RightHeavy
-> LtN
     (Rotate
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'RightHeavy)
     n
   :~: 'True
proofLtNRotate IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
_ Proxy n
_ Proxy 'RightUnbalanced
_ Proxy 'RightHeavy
_ = LtN
  (Rotate
     ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
     'RightUnbalanced
     'RightHeavy)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (LtN l n ~ 'True, LtN rl n ~ 'True, CmpNat rn n ~ 'LT, LtN rr n ~ 'True) =>
  ProofLtNRotate ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n 'RightUnbalanced 'Balanced
  where
  proofLtNRotate :: (LtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> Proxy 'Balanced
-> LtN
     (Rotate
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'Balanced)
     n
   :~: 'True
proofLtNRotate IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
_ Proxy n
_ Proxy 'RightUnbalanced
_ Proxy 'Balanced
_ = LtN
  (Rotate
     ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
     'RightUnbalanced
     'Balanced)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- Left-Right case (First left rotation, then right rotation)
instance
  (LtN ll n ~ 'True, CmpNat ln n ~ 'LT, LtN lrl n ~ 'True, CmpNat lrn n ~ 'LT, LtN lrr n ~ 'True, LtN r n ~ 'True) =>
  ProofLtNRotate ('ForkTree ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr)) (Node n1 a) r) n 'LeftUnbalanced 'RightHeavy
  where
  proofLtNRotate :: (LtN
   ('ForkTree
      ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
      (Node n1 a)
      r)
   n
 ~ 'True) =>
IsBSTT
  ('ForkTree
     ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
     (Node n1 a)
     r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> Proxy 'RightHeavy
-> LtN
     (Rotate
        ('ForkTree
           ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
           (Node n1 a)
           r)
        'LeftUnbalanced
        'RightHeavy)
     n
   :~: 'True
proofLtNRotate IsBSTT
  ('ForkTree
     ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
     (Node n1 a)
     r)
_ Proxy n
_ Proxy 'LeftUnbalanced
_ Proxy 'RightHeavy
_ = LtN
  (Rotate
     ('ForkTree
        ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
        (Node n1 a)
        r)
     'LeftUnbalanced
     'RightHeavy)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- Right-Left case (First right rotation, then left rotation)
instance
  (LtN l n ~ 'True, LtN rll n ~ 'True, CmpNat rln n ~ 'LT, LtN rlr n ~ 'True, CmpNat rn n ~ 'LT, LtN rr n ~ 'True) =>
  ProofLtNRotate ('ForkTree l (Node n1 a) ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr)) n 'RightUnbalanced 'LeftHeavy
  where
  proofLtNRotate :: (LtN
   ('ForkTree
      l
      (Node n1 a)
      ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
   n
 ~ 'True) =>
IsBSTT
  ('ForkTree
     l
     (Node n1 a)
     ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> Proxy 'LeftHeavy
-> LtN
     (Rotate
        ('ForkTree
           l
           (Node n1 a)
           ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
        'RightUnbalanced
        'LeftHeavy)
     n
   :~: 'True
proofLtNRotate IsBSTT
  ('ForkTree
     l
     (Node n1 a)
     ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
_ Proxy n
_ Proxy 'RightUnbalanced
_ Proxy 'LeftHeavy
_ = LtN
  (Rotate
     ('ForkTree
        l
        (Node n1 a)
        ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
     'RightUnbalanced
     'LeftHeavy)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that rebalancing a tree @t@ which verifies @GtN t n ~ 'True@ preserves the `GtN` invariant.
class ProofGtNBalance (t :: Tree) (n :: Nat) where
  proofGtNBalance ::
    (GtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    GtN (Balance t) n :~: 'True

instance ProofGtNBalance 'EmptyTree n where
  proofGtNBalance :: (GtN 'EmptyTree n ~ 'True) =>
IsBSTT 'EmptyTree
-> Proxy n -> GtN (Balance 'EmptyTree) n :~: 'True
proofGtNBalance IsBSTT 'EmptyTree
_ Proxy n
_ = GtN (Balance 'EmptyTree) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( us ~ UnbalancedState (Height l) (Height r),
    ProofGtNBalance' ('ForkTree l (Node n1 a) r) n us
  ) =>
  ProofGtNBalance ('ForkTree l (Node n1 a) r) n
  where
  proofGtNBalance :: (GtN ('ForkTree l (Node n1 a) r) n ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) r)
-> Proxy n -> GtN (Balance ('ForkTree l (Node n1 a) r)) n :~: 'True
proofGtNBalance IsBSTT ('ForkTree l (Node n1 a) r)
tIsBST Proxy n
pn = (GtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True)
-> ((GtN (Balance' ('ForkTree l (Node n1 a) r) us) n ~ 'True) =>
    GtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True)
-> GtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT ('ForkTree l (Node n1 a) r)
-> Proxy n
-> Proxy us
-> GtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True
forall (t :: Tree) (n :: Nat) (us :: US).
(ProofGtNBalance' t n us, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> Proxy us -> GtN (Balance' t us) n :~: 'True
proofGtNBalance' IsBSTT ('ForkTree l (Node n1 a) r)
tIsBST Proxy n
pn (Proxy us
forall {k} (t :: k). Proxy t
Proxy :: Proxy us)) (GtN (Balance' ('ForkTree l (Node n1 a) r) us) n ~ 'True) =>
GtN (Balance' ('ForkTree l (Node n1 a) r) us) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that rebalancing a tree @t@ which verifies @GtN t n ~ 'True@ preserves the `GtN` invariant,
-- given the unbalanced state @us@ of the tree.
class ProofGtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
  proofGtNBalance' ::
    (GtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    Proxy us ->
    GtN (Balance' t us) n :~: 'True

instance ProofGtNBalance' ('ForkTree l (Node n1 a) r) n 'NotUnbalanced where
  proofGtNBalance' :: (GtN ('ForkTree l (Node n1 a) r) n ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) r)
-> Proxy n
-> Proxy 'NotUnbalanced
-> GtN (Balance' ('ForkTree l (Node n1 a) r) 'NotUnbalanced) n
   :~: 'True
proofGtNBalance' IsBSTT ('ForkTree l (Node n1 a) r)
_ Proxy n
_ Proxy 'NotUnbalanced
_ = GtN (Balance' ('ForkTree l (Node n1 a) r) 'NotUnbalanced) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( bs ~ BalancedState (Height ll) (Height lr),
    ProofGtNRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n 'LeftUnbalanced bs
  ) =>
  ProofGtNBalance' ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n 'LeftUnbalanced
  where
  proofGtNBalance' :: (GtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n
 ~ 'True) =>
IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> GtN
     (Balance'
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced)
     n
   :~: 'True
proofGtNBalance' IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
tIsBST Proxy n
pn Proxy 'LeftUnbalanced
pus = (GtN
   (Rotate
      ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
      'LeftUnbalanced
      bs)
   n
 :~: 'True)
-> ((GtN
       (Rotate
          ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
          'LeftUnbalanced
          bs)
       n
     ~ 'True) =>
    GtN
      (Rotate
         ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
         'LeftUnbalanced
         bs)
      n
    :~: 'True)
-> GtN
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced
        bs)
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> Proxy bs
-> GtN
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced
        bs)
     n
   :~: 'True
forall (t :: Tree) (n :: Nat) (us :: US) (bs :: BS).
(ProofGtNRotate t n us bs, GtN t n ~ 'True) =>
IsBSTT t
-> Proxy n
-> Proxy us
-> Proxy bs
-> GtN (Rotate t us bs) n :~: 'True
proofGtNRotate IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
tIsBST Proxy n
pn Proxy 'LeftUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)) (GtN
   (Rotate
      ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
      'LeftUnbalanced
      bs)
   n
 ~ 'True) =>
GtN
  (Rotate
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
     'LeftUnbalanced
     bs)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( bs ~ BalancedState (Height rl) (Height rr),
    ProofGtNRotate ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n 'RightUnbalanced bs
  ) =>
  ProofGtNBalance' ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n 'RightUnbalanced
  where
  proofGtNBalance' :: (GtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> GtN
     (Balance'
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced)
     n
   :~: 'True
proofGtNBalance' IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
tIsBST Proxy n
pn Proxy 'RightUnbalanced
pus = (GtN
   (Rotate
      ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
      'RightUnbalanced
      bs)
   n
 :~: 'True)
-> ((GtN
       (Rotate
          ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
          'RightUnbalanced
          bs)
       n
     ~ 'True) =>
    GtN
      (Rotate
         ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
         'RightUnbalanced
         bs)
      n
    :~: 'True)
-> GtN
     (Rotate
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        bs)
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> Proxy bs
-> GtN
     (Rotate
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        bs)
     n
   :~: 'True
forall (t :: Tree) (n :: Nat) (us :: US) (bs :: BS).
(ProofGtNRotate t n us bs, GtN t n ~ 'True) =>
IsBSTT t
-> Proxy n
-> Proxy us
-> Proxy bs
-> GtN (Rotate t us bs) n :~: 'True
proofGtNRotate IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
tIsBST Proxy n
pn Proxy 'RightUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)) (GtN
   (Rotate
      ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
      'RightUnbalanced
      bs)
   n
 ~ 'True) =>
GtN
  (Rotate
     ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
     'RightUnbalanced
     bs)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that applying a rotation to a tree @t@ which verifies @GtN t n ~ 'True@ preserves the `GtN` invariant.
class ProofGtNRotate (t :: Tree) (n :: Nat) (us :: US) (bs :: BS) where
  proofGtNRotate ::
    (GtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    Proxy us ->
    Proxy bs ->
    GtN (Rotate t us bs) n :~: 'True

-- Left-Left case (Right rotation)
instance
  (GtN ll n ~ 'True, CmpNat ln n ~ 'GT, GtN lr n ~ 'True, GtN r n ~ 'True) =>
  ProofGtNRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n 'LeftUnbalanced 'LeftHeavy
  where
  proofGtNRotate :: (GtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n
 ~ 'True) =>
IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> Proxy 'LeftHeavy
-> GtN
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced
        'LeftHeavy)
     n
   :~: 'True
proofGtNRotate IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
_ Proxy n
_ Proxy 'LeftUnbalanced
_ Proxy 'LeftHeavy
_ = GtN
  (Rotate
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
     'LeftUnbalanced
     'LeftHeavy)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (GtN ll n ~ 'True, CmpNat ln n ~ 'GT, GtN lr n ~ 'True, GtN r n ~ 'True) =>
  ProofGtNRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n 'LeftUnbalanced 'Balanced
  where
  proofGtNRotate :: (GtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r) n
 ~ 'True) =>
IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> Proxy 'Balanced
-> GtN
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
        'LeftUnbalanced
        'Balanced)
     n
   :~: 'True
proofGtNRotate IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
_ Proxy n
_ Proxy 'LeftUnbalanced
_ Proxy 'Balanced
_ = GtN
  (Rotate
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
     'LeftUnbalanced
     'Balanced)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- Right-Right case (Left rotation)
instance
  (GtN l n ~ 'True, GtN rl n ~ 'True, CmpNat rn n ~ 'GT, GtN rr n ~ 'True) =>
  ProofGtNRotate ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n 'RightUnbalanced 'RightHeavy
  where
  proofGtNRotate :: (GtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> Proxy 'RightHeavy
-> GtN
     (Rotate
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'RightHeavy)
     n
   :~: 'True
proofGtNRotate IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
_ Proxy n
_ Proxy 'RightUnbalanced
_ Proxy 'RightHeavy
_ = GtN
  (Rotate
     ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
     'RightUnbalanced
     'RightHeavy)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (GtN l n ~ 'True, GtN rl n ~ 'True, CmpNat rn n ~ 'GT, GtN rr n ~ 'True) =>
  ProofGtNRotate ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n 'RightUnbalanced 'Balanced
  where
  proofGtNRotate :: (GtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> Proxy 'Balanced
-> GtN
     (Rotate
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'Balanced)
     n
   :~: 'True
proofGtNRotate IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
_ Proxy n
_ Proxy 'RightUnbalanced
_ Proxy 'Balanced
_ = GtN
  (Rotate
     ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
     'RightUnbalanced
     'Balanced)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- Left-Right case (First left rotation, then right rotation)
instance
  (GtN ll n ~ 'True, CmpNat ln n ~ 'GT, GtN lrl n ~ 'True, CmpNat lrn n ~ 'GT, GtN lrr n ~ 'True, GtN r n ~ 'True) =>
  ProofGtNRotate ('ForkTree ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr)) (Node n1 a) r) n 'LeftUnbalanced 'RightHeavy
  where
  proofGtNRotate :: (GtN
   ('ForkTree
      ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
      (Node n1 a)
      r)
   n
 ~ 'True) =>
IsBSTT
  ('ForkTree
     ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
     (Node n1 a)
     r)
-> Proxy n
-> Proxy 'LeftUnbalanced
-> Proxy 'RightHeavy
-> GtN
     (Rotate
        ('ForkTree
           ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
           (Node n1 a)
           r)
        'LeftUnbalanced
        'RightHeavy)
     n
   :~: 'True
proofGtNRotate IsBSTT
  ('ForkTree
     ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
     (Node n1 a)
     r)
_ Proxy n
_ Proxy 'LeftUnbalanced
_ Proxy 'RightHeavy
_ = GtN
  (Rotate
     ('ForkTree
        ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
        (Node n1 a)
        r)
     'LeftUnbalanced
     'RightHeavy)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- Right-Left case (First right rotation, then left rotation)
instance
  (GtN l n ~ 'True, GtN rll n ~ 'True, CmpNat rln n ~ 'GT, GtN rlr n ~ 'True, CmpNat rn n ~ 'GT, GtN rr n ~ 'True) =>
  ProofGtNRotate ('ForkTree l (Node n1 a) ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr)) n 'RightUnbalanced 'LeftHeavy
  where
  proofGtNRotate :: (GtN
   ('ForkTree
      l
      (Node n1 a)
      ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
   n
 ~ 'True) =>
IsBSTT
  ('ForkTree
     l
     (Node n1 a)
     ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
-> Proxy n
-> Proxy 'RightUnbalanced
-> Proxy 'LeftHeavy
-> GtN
     (Rotate
        ('ForkTree
           l
           (Node n1 a)
           ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
        'RightUnbalanced
        'LeftHeavy)
     n
   :~: 'True
proofGtNRotate IsBSTT
  ('ForkTree
     l
     (Node n1 a)
     ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
_ Proxy n
_ Proxy 'RightUnbalanced
_ Proxy 'LeftHeavy
_ = GtN
  (Rotate
     ('ForkTree
        l
        (Node n1 a)
        ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
     'RightUnbalanced
     'LeftHeavy)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that applying a rebalancing (composition of rotations)
-- to an `Almost Balanced` tree returns a `Balanced Tree`.
--
-- An `Almost Balanced` tree is a tree @t ~ 'ForkTree l (Node n a) r@ which verifies all the following conditions:
--
--  * @IsBalanced l ~ 'True@
--
--  * @IsBalanced r ~ 'True@
--
-- In other words, it's a tree with left and right `Data.Tree.AVL.Extern.Constructors.AVL` sub trees that may not be balanced at the root.
class ProofIsBalancedBalance (t :: Tree) where
  proofIsBalancedBalance :: IsAlmostBalancedT t -> IsBalancedT (Balance t)

instance ProofIsBalancedBalance 'EmptyTree where
  proofIsBalancedBalance :: IsAlmostBalancedT 'EmptyTree -> IsBalancedT (Balance 'EmptyTree)
proofIsBalancedBalance IsAlmostBalancedT 'EmptyTree
_ = IsBalancedT 'EmptyTree
IsBalancedT (Balance 'EmptyTree)
EmptyIsBalancedT

instance
  ( us ~ UnbalancedState (Height l) (Height r),
    LtN l n ~ 'True,
    GtN r n ~ 'True,
    ProofIsBalancedBalance' ('ForkTree l (Node n a) r) us
  ) =>
  ProofIsBalancedBalance ('ForkTree l (Node n a) r)
  where
  proofIsBalancedBalance :: IsAlmostBalancedT ('ForkTree l (Node n a) r)
-> IsBalancedT (Balance ('ForkTree l (Node n a) r))
proofIsBalancedBalance IsAlmostBalancedT ('ForkTree l (Node n a) r)
tIsAlmostBalanced = IsAlmostBalancedT ('ForkTree l (Node n a) r)
-> Proxy us -> IsBalancedT (Balance' ('ForkTree l (Node n a) r) us)
forall (t :: Tree) (us :: US) (l :: Tree) (n :: Nat) a (r :: Tree).
(ProofIsBalancedBalance' t us, t ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT t -> Proxy us -> IsBalancedT (Balance' t us)
proofIsBalancedBalance' IsAlmostBalancedT ('ForkTree l (Node n a) r)
tIsAlmostBalanced (Proxy us
forall {k} (t :: k). Proxy t
Proxy :: Proxy us)

-- | Prove that applying a rebalancing (a composition of rotations)
-- to an `Almost AVL` tree returns an `Data.Tree.AVL.Extern.Constructors.AVL`, given the comparison @us@ of the heights of the left and right sub trees.
-- This is called only from `ProofIsBalancedBalance`.
class ProofIsBalancedBalance' (t :: Tree) (us :: US) where
  proofIsBalancedBalance' ::
    (t ~ 'ForkTree l (Node n a) r, LtN l n ~ 'True, GtN r n ~ 'True) =>
    IsAlmostBalancedT t ->
    Proxy us ->
    IsBalancedT (Balance' t us)

-- | `NotUnbalanced` implies @BalancedHeights (Height l) (Height r) n ~ 'True@
instance (BalancedHeights (Height l) (Height r) n ~ 'True) => ProofIsBalancedBalance' ('ForkTree l (Node n a) r) 'NotUnbalanced where
  proofIsBalancedBalance' :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree l (Node n a) r ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT ('ForkTree l (Node n a) r)
-> Proxy 'NotUnbalanced
-> IsBalancedT (Balance' ('ForkTree l (Node n a) r) 'NotUnbalanced)
proofIsBalancedBalance' (ForkIsAlmostBalancedT IsBalancedT l
l Proxy (Node n a)
node IsBalancedT r
r) Proxy 'NotUnbalanced
_ = IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT l
l Proxy (Node n a)
node IsBalancedT r
r

instance
  ( bs ~ BalancedState (Height ll) (Height lr),
    ProofIsBalancedRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced bs
  ) =>
  ProofIsBalancedBalance' ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced
  where
  proofIsBalancedBalance' :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r
 ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> IsBalancedT
     (Balance'
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced)
proofIsBalancedBalance' IsAlmostBalancedT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
tIsAlmostBalanced Proxy 'LeftUnbalanced
pus = IsAlmostBalancedT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy bs
-> IsBalancedT
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        bs)
forall (t :: Tree) (us :: US) (bs :: BS) (l :: Tree) (n :: Nat) a
       (r :: Tree).
(ProofIsBalancedRotate t us bs, t ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT t
-> Proxy us -> Proxy bs -> IsBalancedT (Rotate t us bs)
proofIsBalancedRotate IsAlmostBalancedT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
tIsAlmostBalanced Proxy 'LeftUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)

instance
  ( bs ~ BalancedState (Height rl) (Height rr),
    ProofIsBalancedRotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced bs
  ) =>
  ProofIsBalancedBalance' ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced
  where
  proofIsBalancedBalance' :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT
  ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> IsBalancedT
     (Balance'
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced)
proofIsBalancedBalance' IsAlmostBalancedT
  ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
tIsAlmostBalanced Proxy 'RightUnbalanced
pus = IsAlmostBalancedT
  ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy bs
-> IsBalancedT
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        bs)
forall (t :: Tree) (us :: US) (bs :: BS) (l :: Tree) (n :: Nat) a
       (r :: Tree).
(ProofIsBalancedRotate t us bs, t ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT t
-> Proxy us -> Proxy bs -> IsBalancedT (Rotate t us bs)
proofIsBalancedRotate IsAlmostBalancedT
  ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
tIsAlmostBalanced Proxy 'RightUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)

-- | Prove that applying a rotation
-- to an `Almost AVL` tree returns an `Data.Tree.AVL.Extern.Constructors.AVL` tree.
class ProofIsBalancedRotate (t :: Tree) (us :: US) (bs :: BS) where
  proofIsBalancedRotate ::
    (t ~ 'ForkTree l (Node n a) r, LtN l n ~ 'True, GtN r n ~ 'True) =>
    IsAlmostBalancedT t ->
    Proxy us ->
    Proxy bs ->
    IsBalancedT (Rotate t us bs)

-- Left-Left case (Right rotation)
instance
  ( (Height lr <=? Height r) ~ 'True,
    BalancedHeights (Height ll) (1 + Height r) ln ~ 'True,
    BalancedHeights (Height lr) (Height r) n ~ 'True
  ) =>
  ProofIsBalancedRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced 'LeftHeavy
  where
  proofIsBalancedRotate :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r
 ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy 'LeftHeavy
-> IsBalancedT
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        'LeftHeavy)
proofIsBalancedRotate (ForkIsAlmostBalancedT (ForkIsBalancedT IsBalancedT l
ll Proxy (Node n a)
lnode IsBalancedT r
lr) Proxy (Node n a)
node IsBalancedT r
r) Proxy 'LeftUnbalanced
_ Proxy 'LeftHeavy
_ =
    IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT ('ForkTree r (Node n a) r)
-> IsBalancedT ('ForkTree l (Node n a) ('ForkTree r (Node n a) r))
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT l
ll Proxy (Node n a)
lnode (IsBalancedT r
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree r (Node n a) r)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT r
lr Proxy (Node n a)
node IsBalancedT r
r)

instance
  ( (Height lr <=? Height r) ~ 'True,
    BalancedHeights (Height ll) (1 + Height r) ln ~ 'True,
    BalancedHeights (Height lr) (Height r) n ~ 'True
  ) =>
  ProofIsBalancedRotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced 'Balanced
  where
  proofIsBalancedRotate :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r
 ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy 'Balanced
-> IsBalancedT
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        'Balanced)
proofIsBalancedRotate (ForkIsAlmostBalancedT (ForkIsBalancedT IsBalancedT l
ll Proxy (Node n a)
lnode IsBalancedT r
lr) Proxy (Node n a)
node IsBalancedT r
r) Proxy 'LeftUnbalanced
_ Proxy 'Balanced
_ =
    IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT ('ForkTree r (Node n a) r)
-> IsBalancedT ('ForkTree l (Node n a) ('ForkTree r (Node n a) r))
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT l
ll Proxy (Node n a)
lnode (IsBalancedT r
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree r (Node n a) r)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT r
lr Proxy (Node n a)
node IsBalancedT r
r)

-- Right-Right case (Left rotation)
instance
  ( (Height l <=? Height rl) ~ 'True,
    BalancedHeights (1 + Height rl) (Height rr) rn ~ 'True,
    BalancedHeights (Height l) (Height rl) n ~ 'True
  ) =>
  ProofIsBalancedRotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced 'RightHeavy
  where
  proofIsBalancedRotate :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT
  ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'RightHeavy
-> IsBalancedT
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'RightHeavy)
proofIsBalancedRotate (ForkIsAlmostBalancedT IsBalancedT l
l Proxy (Node n a)
node (ForkIsBalancedT IsBalancedT l
rl Proxy (Node n a)
rnode IsBalancedT r
rr)) Proxy 'RightUnbalanced
_ Proxy 'RightHeavy
_ =
    IsBalancedT ('ForkTree l (Node n a) l)
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree ('ForkTree l (Node n a) l) (Node n a) r)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT (IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT l
-> IsBalancedT ('ForkTree l (Node n a) l)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT l
l Proxy (Node n a)
node IsBalancedT l
rl) Proxy (Node n a)
rnode IsBalancedT r
rr

instance
  ( (Height l <=? Height rl) ~ 'True,
    BalancedHeights (1 + Height rl) (Height rr) rn ~ 'True,
    BalancedHeights (Height l) (Height rl) n ~ 'True
  ) =>
  ProofIsBalancedRotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced 'Balanced
  where
  proofIsBalancedRotate :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT
  ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'Balanced
-> IsBalancedT
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'Balanced)
proofIsBalancedRotate (ForkIsAlmostBalancedT IsBalancedT l
l Proxy (Node n a)
node (ForkIsBalancedT IsBalancedT l
rl Proxy (Node n a)
rnode IsBalancedT r
rr)) Proxy 'RightUnbalanced
_ Proxy 'Balanced
_ =
    IsBalancedT ('ForkTree l (Node n a) l)
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree ('ForkTree l (Node n a) l) (Node n a) r)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT (IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT l
-> IsBalancedT ('ForkTree l (Node n a) l)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT l
l Proxy (Node n a)
node IsBalancedT l
rl) Proxy (Node n a)
rnode IsBalancedT r
rr

-- Left-Right case (First left rotation, then right rotation)
instance
  ( (Height ll <=? Height lrl) ~ 'True,
    BalancedHeights (1 + Height lrl) (1 + Height r) lrn ~ 'True,
    (Height lrr <=? Height r) ~ 'True,
    BalancedHeights (Height lrr) (Height r) n ~ 'True,
    BalancedHeights (Height ll) (Height lrl) ln ~ 'True
  ) =>
  ProofIsBalancedRotate ('ForkTree ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr)) (Node n a) r) 'LeftUnbalanced 'RightHeavy
  where
  proofIsBalancedRotate :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree
   ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
   (Node n a)
   r
 ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT
  ('ForkTree
     ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
     (Node n a)
     r)
-> Proxy 'LeftUnbalanced
-> Proxy 'RightHeavy
-> IsBalancedT
     (Rotate
        ('ForkTree
           ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
           (Node n a)
           r)
        'LeftUnbalanced
        'RightHeavy)
proofIsBalancedRotate (ForkIsAlmostBalancedT (ForkIsBalancedT IsBalancedT l
ll Proxy (Node n a)
lnode (ForkIsBalancedT IsBalancedT l
lrl Proxy (Node n a)
lrnode IsBalancedT r
lrr)) Proxy (Node n a)
node IsBalancedT r
r) Proxy 'LeftUnbalanced
_ Proxy 'RightHeavy
_ =
    IsBalancedT ('ForkTree l (Node n a) l)
-> Proxy (Node n a)
-> IsBalancedT ('ForkTree r (Node n a) r)
-> IsBalancedT
     ('ForkTree
        ('ForkTree l (Node n a) l) (Node n a) ('ForkTree r (Node n a) r))
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT (IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT l
-> IsBalancedT ('ForkTree l (Node n a) l)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT l
ll Proxy (Node n a)
lnode IsBalancedT l
lrl) Proxy (Node n a)
lrnode (IsBalancedT r
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree r (Node n a) r)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT r
lrr Proxy (Node n a)
node IsBalancedT r
r)

-- Right-Left case (First right rotation, then left rotation)
instance
  ( (Height l <=? Height rll) ~ 'True,
    BalancedHeights (1 + Height rll) (1 + Height rr) rln ~ 'True,
    (Height rlr <=? Height rr) ~ 'True,
    BalancedHeights (Height rlr) (Height rr) rn ~ 'True,
    BalancedHeights (Height l) (Height rll) n ~ 'True
  ) =>
  ProofIsBalancedRotate ('ForkTree l (Node n a) ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr)) 'RightUnbalanced 'LeftHeavy
  where
  proofIsBalancedRotate :: forall (l :: Tree) (n :: Nat) a (r :: Tree).
('ForkTree
   l
   (Node n a)
   ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr)
 ~ 'ForkTree l (Node n a) r,
 LtN l n ~ 'True, GtN r n ~ 'True) =>
IsAlmostBalancedT
  ('ForkTree
     l
     (Node n a)
     ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'LeftHeavy
-> IsBalancedT
     (Rotate
        ('ForkTree
           l
           (Node n a)
           ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
        'RightUnbalanced
        'LeftHeavy)
proofIsBalancedRotate (ForkIsAlmostBalancedT IsBalancedT l
l Proxy (Node n a)
node (ForkIsBalancedT (ForkIsBalancedT IsBalancedT l
rll Proxy (Node n a)
rlnode IsBalancedT r
rlr) Proxy (Node n a)
rnode IsBalancedT r
rr)) Proxy 'RightUnbalanced
_ Proxy 'LeftHeavy
_ =
    IsBalancedT ('ForkTree l (Node n a) l)
-> Proxy (Node n a)
-> IsBalancedT ('ForkTree r (Node n a) r)
-> IsBalancedT
     ('ForkTree
        ('ForkTree l (Node n a) l) (Node n a) ('ForkTree r (Node n a) r))
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT (IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT l
-> IsBalancedT ('ForkTree l (Node n a) l)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT l
l Proxy (Node n a)
node IsBalancedT l
rll) Proxy (Node n a)
rlnode (IsBalancedT r
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree r (Node n a) r)
forall (l :: Tree) (r :: Tree) (n :: Nat) a.
(BalancedHeights (Height l) (Height r) n ~ 'True) =>
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
ForkIsBalancedT IsBalancedT r
rlr Proxy (Node n a)
rnode IsBalancedT r
rr)