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

-- |
-- Module      : Data.Tree.AVL.Intern.Balance
-- Description : Balancing algorithm (with proofs) for internalist AVL trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the balancing algorithm over internalist AlmostAVL trees,
-- along with the necessary proofs to ensure (at compile time) that the
-- new tree is AVL (the balance is restored).
module Data.Tree.AVL.Intern.Balance
  ( Balanceable (Balance, balance),
    ProofLtNBalance (proofLtNBalance),
    ProofGtNBalance (proofGtNBalance),
  )
where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Intern.Constructors (AVL (ForkAVL), AlmostAVL (AlmostAVL))
import Data.Tree.AVL.Invariants
  ( BS (Balanced, LeftHeavy, RightHeavy),
    BalancedHeights,
    BalancedState,
    Height,
    US (LeftUnbalanced, NotUnbalanced, RightUnbalanced),
    UnbalancedState,
  )
import Data.Tree.BST.Invariants (GtN, LtN)
import Data.Tree.ITree (Tree (ForkTree))
import Data.Tree.Node (Node)
import Data.Type.Equality (gcastWith, (:~:) (Refl))
import GHC.TypeLits (CmpNat, Nat, type (+), type (<=?))
import Prelude (Bool (True), Ordering (GT, LT))

-- | This type class provides the functionality to balance
-- an `AlmostAVL` @t@ (a tree that came up from an insertion or deletion
-- on an `AVL`).
-- The insertion is defined at the value level and the type level.
class Balanceable (t :: Tree) where
  type Balance (t :: Tree) :: Tree
  balance :: AlmostAVL t -> AVL (Balance t)

instance
  ( us ~ UnbalancedState (Height l) (Height r),
    Balanceable' ('ForkTree l (Node n a) r) us
  ) =>
  Balanceable ('ForkTree l (Node n a) r)
  where
  type Balance ('ForkTree l (Node n a) r) = Balance' ('ForkTree l (Node n a) r) (UnbalancedState (Height l) (Height r))
  balance :: AlmostAVL ('ForkTree l (Node n a) r)
-> AVL (Balance ('ForkTree l (Node n a) r))
balance AlmostAVL ('ForkTree l (Node n a) r)
t = AlmostAVL ('ForkTree l (Node n a) r)
-> Proxy us -> AVL (Balance' ('ForkTree l (Node n a) r) us)
forall (t :: Tree) (us :: US).
Balanceable' t us =>
AlmostAVL t -> Proxy us -> AVL (Balance' t us)
balance' AlmostAVL ('ForkTree l (Node n a) r)
t (Proxy us
forall {k} (t :: k). Proxy t
Proxy :: Proxy us)

-- | This type class provides the functionality to balance
-- an `AlmostAVL` @t@.
-- It's only used by the 'Balanceable' class and it has one extra parameter @us@,
-- which is the `UnbalancedState` of the two sub trees of @t@.
class Balanceable' (t :: Tree) (us :: US) where
  type Balance' (t :: Tree) (us :: US) :: Tree
  balance' :: AlmostAVL t -> Proxy us -> AVL (Balance' t us)

instance
  (BalancedHeights (Height l) (Height r) n ~ 'True) =>
  Balanceable' ('ForkTree l (Node n a) r) 'NotUnbalanced
  where
  type Balance' ('ForkTree l (Node n a) r) 'NotUnbalanced = 'ForkTree l (Node n a) r
  balance' :: AlmostAVL ('ForkTree l (Node n a) r)
-> Proxy 'NotUnbalanced
-> AVL (Balance' ('ForkTree l (Node n a) r) 'NotUnbalanced)
balance' (AlmostAVL AVL l
l Node n a
node AVL r
r) Proxy 'NotUnbalanced
_ = AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL l
l Node n a
node AVL r
r

instance
  ( bs ~ BalancedState (Height ll) (Height lr),
    Rotateable ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced bs
  ) =>
  Balanceable' ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced
  where
  type
    Balance' ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced =
      Rotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced (BalancedState (Height ll) (Height lr))
  balance' :: AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> AVL
     (Balance'
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced)
balance' AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
t Proxy 'LeftUnbalanced
pus = AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy bs
-> AVL
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        bs)
forall (t :: Tree) (us :: US) (bs :: BS).
Rotateable t us bs =>
AlmostAVL t -> Proxy us -> Proxy bs -> AVL (Rotate t us bs)
rotate AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
t Proxy 'LeftUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)

instance
  ( bs ~ BalancedState (Height rl) (Height rr),
    Rotateable ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced bs
  ) =>
  Balanceable' ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced
  where
  type
    Balance' ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced =
      Rotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced (BalancedState (Height rl) (Height rr))
  balance' :: AlmostAVL ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> AVL
     (Balance'
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced)
balance' AlmostAVL ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
t Proxy 'RightUnbalanced
pus = AlmostAVL ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy bs
-> AVL
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        bs)
forall (t :: Tree) (us :: US) (bs :: BS).
Rotateable t us bs =>
AlmostAVL t -> Proxy us -> Proxy bs -> AVL (Rotate t us bs)
rotate AlmostAVL ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
t Proxy 'RightUnbalanced
pus (Proxy bs
forall {k} (t :: k). Proxy t
Proxy :: Proxy bs)

-- | This type class provides the functionality to apply a rotation to
-- an `AlmostAVL` tree @t@.
-- The rotation is defined at the value level and the type level.
class Rotateable (t :: Tree) (us :: US) (bs :: BS) where
  type Rotate (t :: Tree) (us :: US) (bs :: BS) :: Tree
  rotate :: AlmostAVL t -> Proxy us -> Proxy bs -> AVL (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,
    (Height lr <=? Height r) ~ 'True,
    BalancedHeights (Height ll) (1 + Height r) ln ~ 'True,
    BalancedHeights (Height lr) (Height r) n ~ 'True
  ) =>
  Rotateable ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced 'LeftHeavy
  where
  type
    Rotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced 'LeftHeavy =
      'ForkTree ll (Node ln la) ('ForkTree lr (Node n a) r)
  rotate :: AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy 'LeftHeavy
-> AVL
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        'LeftHeavy)
rotate (AlmostAVL (ForkAVL AVL l
ll Node n a
lnode AVL r
lr) Node n a
xnode AVL r
r) Proxy 'LeftUnbalanced
_ Proxy 'LeftHeavy
_ =
    AVL l
-> Node n a
-> AVL ('ForkTree r (Node n a) r)
-> AVL ('ForkTree l (Node n a) ('ForkTree r (Node n a) r))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL l
ll Node n a
lnode (AVL r -> Node n a -> AVL r -> AVL ('ForkTree r (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL r
lr Node n a
xnode AVL r
r)

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    CmpNat n ln ~ 'GT,
    GtN r ln ~ 'True,
    LtN lr n ~ 'True,
    (Height lr <=? Height r) ~ 'True,
    BalancedHeights (Height ll) (1 + Height r) ln ~ 'True,
    BalancedHeights (Height lr) (Height r) n ~ 'True
  ) =>
  Rotateable ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced 'Balanced
  where
  type
    Rotate ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r) 'LeftUnbalanced 'Balanced =
      'ForkTree ll (Node ln la) ('ForkTree lr (Node n a) r)
  rotate :: AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
-> Proxy 'LeftUnbalanced
-> Proxy 'Balanced
-> AVL
     (Rotate
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) r)
        'LeftUnbalanced
        'Balanced)
rotate (AlmostAVL (ForkAVL AVL l
ll Node n a
lnode AVL r
lr) Node n a
xnode AVL r
r) Proxy 'LeftUnbalanced
_ Proxy 'Balanced
_ =
    AVL l
-> Node n a
-> AVL ('ForkTree r (Node n a) r)
-> AVL ('ForkTree l (Node n a) ('ForkTree r (Node n a) r))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL l
ll Node n a
lnode (AVL r -> Node n a -> AVL r -> AVL ('ForkTree r (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL r
lr Node n a
xnode AVL r
r)

-- Right-Right case (Left rotation)
instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    (Height l <=? Height rl) ~ 'True,
    CmpNat n rn ~ 'LT,
    LtN l rn ~ 'True,
    GtN rl n ~ 'True,
    BalancedHeights (1 + Height rl) (Height rr) rn ~ 'True,
    BalancedHeights (Height l) (Height rl) n ~ 'True
  ) =>
  Rotateable ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced 'RightHeavy
  where
  type
    Rotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced 'RightHeavy =
      'ForkTree ('ForkTree l (Node n a) rl) (Node rn ra) rr
  rotate :: AlmostAVL ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'RightHeavy
-> AVL
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'RightHeavy)
rotate (AlmostAVL AVL l
l Node n a
xnode (ForkAVL AVL l
rl Node n a
rnode AVL r
rr)) Proxy 'RightUnbalanced
_ Proxy 'RightHeavy
_ =
    AVL ('ForkTree l (Node n a) l)
-> Node n a
-> AVL r
-> AVL ('ForkTree ('ForkTree l (Node n a) l) (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL (AVL l -> Node n a -> AVL l -> AVL ('ForkTree l (Node n a) l)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL l
l Node n a
xnode AVL l
rl) Node n a
rnode AVL r
rr

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    (Height l <=? Height rl) ~ 'True,
    CmpNat n rn ~ 'LT,
    LtN l rn ~ 'True,
    GtN rl n ~ 'True,
    BalancedHeights (1 + Height rl) (Height rr) rn ~ 'True,
    BalancedHeights (Height l) (Height rl) n ~ 'True
  ) =>
  Rotateable ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced 'Balanced
  where
  type
    Rotate ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr)) 'RightUnbalanced 'Balanced =
      'ForkTree ('ForkTree l (Node n a) rl) (Node rn ra) rr
  rotate :: AlmostAVL ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'Balanced
-> AVL
     (Rotate
        ('ForkTree l (Node n a) ('ForkTree rl (Node rn ra) rr))
        'RightUnbalanced
        'Balanced)
rotate (AlmostAVL AVL l
l Node n a
xnode (ForkAVL AVL l
rl Node n a
rnode AVL r
rr)) Proxy 'RightUnbalanced
_ Proxy 'Balanced
_ =
    AVL ('ForkTree l (Node n a) l)
-> Node n a
-> AVL r
-> AVL ('ForkTree ('ForkTree l (Node n a) l) (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL (AVL l -> Node n a -> AVL l -> AVL ('ForkTree l (Node n a) l)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL l
l Node n a
xnode AVL l
rl) Node n a
rnode AVL r
rr

-- Left-Right case (First left rotation, then right rotation)
instance
  ( l ~ 'ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr),
    (Height ll <=? Height lrl) ~ 'True,
    GtN r lrn ~ 'True,
    LtN ll lrn ~ 'True,
    LtN lrr n ~ 'True,
    (Height lrr <=? Height r) ~ 'True,
    CmpNat n lrn ~ 'GT,
    CmpNat ln lrn ~ 'LT,
    GtN lrl ln ~ 'True,
    BalancedHeights (1 + Height lrl) (1 + Height r) lrn ~ 'True,
    BalancedHeights (Height ll) (Height lrl) ln ~ 'True,
    BalancedHeights (Height lrr) (Height r) n ~ 'True
  ) =>
  Rotateable ('ForkTree ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr)) (Node n a) r) 'LeftUnbalanced 'RightHeavy
  where
  type
    Rotate ('ForkTree ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr)) (Node n a) r) 'LeftUnbalanced 'RightHeavy =
      'ForkTree ('ForkTree ll (Node ln la) lrl) (Node lrn lra) ('ForkTree lrr (Node n a) r)
  rotate :: AlmostAVL
  ('ForkTree
     ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
     (Node n a)
     r)
-> Proxy 'LeftUnbalanced
-> Proxy 'RightHeavy
-> AVL
     (Rotate
        ('ForkTree
           ('ForkTree ll (Node ln la) ('ForkTree lrl (Node lrn lra) lrr))
           (Node n a)
           r)
        'LeftUnbalanced
        'RightHeavy)
rotate (AlmostAVL (ForkAVL AVL l
ll Node n a
lnode (ForkAVL AVL l
lrl Node n a
lrnode AVL r
lrr)) Node n a
xnode AVL r
r) Proxy 'LeftUnbalanced
_ Proxy 'RightHeavy
_ =
    AVL ('ForkTree l (Node n a) l)
-> Node n a
-> AVL ('ForkTree r (Node n a) r)
-> AVL
     ('ForkTree
        ('ForkTree l (Node n a) l) (Node n a) ('ForkTree r (Node n a) r))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL (AVL l -> Node n a -> AVL l -> AVL ('ForkTree l (Node n a) l)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL l
ll Node n a
lnode AVL l
lrl) Node n a
lrnode (AVL r -> Node n a -> AVL r -> AVL ('ForkTree r (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL r
lrr Node n a
xnode AVL r
r)

-- Right-Left case (First right rotation, then left rotation)
instance
  ( r ~ 'ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr,
    (Height l <=? Height rll) ~ 'True,
    CmpNat rn rln ~ 'GT,
    CmpNat n rln ~ 'LT,
    LtN l rln ~ 'True,
    (Height rlr <=? Height rr) ~ 'True,
    GtN rr rln ~ 'True,
    GtN rll n ~ 'True,
    LtN rlr rn ~ 'True,
    BalancedHeights (1 + Height rll) (1 + Height rr) rln ~ 'True,
    BalancedHeights (Height l) (Height rll) n ~ 'True,
    BalancedHeights (Height rlr) (Height rr) rn ~ 'True
  ) =>
  Rotateable ('ForkTree l (Node n a) ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr)) 'RightUnbalanced 'LeftHeavy
  where
  type
    Rotate ('ForkTree l (Node n a) ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr)) 'RightUnbalanced 'LeftHeavy =
      'ForkTree ('ForkTree l (Node n a) rll) (Node rln rla) ('ForkTree rlr (Node rn ra) rr)
  rotate :: AlmostAVL
  ('ForkTree
     l
     (Node n a)
     ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
-> Proxy 'RightUnbalanced
-> Proxy 'LeftHeavy
-> AVL
     (Rotate
        ('ForkTree
           l
           (Node n a)
           ('ForkTree ('ForkTree rll (Node rln rla) rlr) (Node rn ra) rr))
        'RightUnbalanced
        'LeftHeavy)
rotate (AlmostAVL AVL l
l Node n a
xnode (ForkAVL (ForkAVL AVL l
rll Node n a
rlnode AVL r
rlr) Node n a
rnode AVL r
rr)) Proxy 'RightUnbalanced
_ Proxy 'LeftHeavy
_ =
    AVL ('ForkTree l (Node n a) l)
-> Node n a
-> AVL ('ForkTree r (Node n a) r)
-> AVL
     ('ForkTree
        ('ForkTree l (Node n a) l) (Node n a) ('ForkTree r (Node n a) r))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL (AVL l -> Node n a -> AVL l -> AVL ('ForkTree l (Node n a) l)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL l
l Node n a
xnode AVL l
rll) Node n a
rlnode (AVL r -> Node n a -> AVL r -> AVL ('ForkTree r (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL r
rlr Node n a
rnode AVL 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) =>
    AlmostAVL t ->
    Proxy n ->
    LtN (Balance t) n :~: 'True

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) =>
AlmostAVL ('ForkTree l (Node n1 a) r)
-> Proxy n -> LtN (Balance ('ForkTree l (Node n1 a) r)) n :~: 'True
proofLtNBalance AlmostAVL ('ForkTree l (Node n1 a) r)
pt 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 (AlmostAVL ('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) =>
AlmostAVL t
-> Proxy n -> Proxy us -> LtN (Balance' t us) n :~: 'True
proofLtNBalance' AlmostAVL ('ForkTree l (Node n1 a) r)
pt 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 `UnbalancedState` @us@ of the tree.
-- The @us@ parameter guides the proof.
class ProofLtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
  proofLtNBalance' ::
    (LtN t n ~ 'True) =>
    AlmostAVL 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) =>
AlmostAVL ('ForkTree l (Node n1 a) r)
-> Proxy n
-> Proxy 'NotUnbalanced
-> LtN (Balance' ('ForkTree l (Node n1 a) r) 'NotUnbalanced) n
   :~: 'True
proofLtNBalance' AlmostAVL ('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) =>
AlmostAVL ('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' AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
pt 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 (AlmostAVL ('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) =>
AlmostAVL t
-> Proxy n
-> Proxy us
-> Proxy bs
-> LtN (Rotate t us bs) n :~: 'True
proofLtNRotate AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
pt 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) =>
AlmostAVL ('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' AlmostAVL ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
pt 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 (AlmostAVL ('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) =>
AlmostAVL t
-> Proxy n
-> Proxy us
-> Proxy bs
-> LtN (Rotate t us bs) n :~: 'True
proofLtNRotate AlmostAVL ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
pt 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) =>
    AlmostAVL 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) =>
AlmostAVL ('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 AlmostAVL ('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) =>
AlmostAVL ('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 AlmostAVL ('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) =>
AlmostAVL ('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 AlmostAVL ('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) =>
AlmostAVL ('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 AlmostAVL ('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) =>
AlmostAVL
  ('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 AlmostAVL
  ('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) =>
AlmostAVL
  ('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 AlmostAVL
  ('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) =>
    AlmostAVL t ->
    Proxy n ->
    GtN (Balance t) n :~: 'True

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) =>
AlmostAVL ('ForkTree l (Node n1 a) r)
-> Proxy n -> GtN (Balance ('ForkTree l (Node n1 a) r)) n :~: 'True
proofGtNBalance AlmostAVL ('ForkTree l (Node n1 a) r)
t 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 (AlmostAVL ('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) =>
AlmostAVL t
-> Proxy n -> Proxy us -> GtN (Balance' t us) n :~: 'True
proofGtNBalance' AlmostAVL ('ForkTree l (Node n1 a) r)
t 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 `UnbalancedState` @us@ of the tree.
-- The @us@ parameter guides the proof.
class ProofGtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
  proofGtNBalance' ::
    (GtN t n ~ 'True) =>
    AlmostAVL 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) =>
AlmostAVL ('ForkTree l (Node n1 a) r)
-> Proxy n
-> Proxy 'NotUnbalanced
-> GtN (Balance' ('ForkTree l (Node n1 a) r) 'NotUnbalanced) n
   :~: 'True
proofGtNBalance' AlmostAVL ('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) =>
AlmostAVL ('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' AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
t 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 (AlmostAVL ('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) =>
AlmostAVL t
-> Proxy n
-> Proxy us
-> Proxy bs
-> GtN (Rotate t us bs) n :~: 'True
proofGtNRotate AlmostAVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a) r)
t 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) =>
AlmostAVL ('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' AlmostAVL ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
t 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 (AlmostAVL ('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) =>
AlmostAVL t
-> Proxy n
-> Proxy us
-> Proxy bs
-> GtN (Rotate t us bs) n :~: 'True
proofGtNRotate AlmostAVL ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
t 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) =>
    AlmostAVL 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) =>
AlmostAVL ('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 AlmostAVL ('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) =>
AlmostAVL ('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 AlmostAVL ('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) =>
AlmostAVL ('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 AlmostAVL ('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) =>
AlmostAVL ('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 AlmostAVL ('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) =>
AlmostAVL
  ('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 AlmostAVL
  ('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) =>
AlmostAVL
  ('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 AlmostAVL
  ('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