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

-- |
-- Module      : Data.Tree.BST.Extern.InsertProofs
-- Description : Proofs for insertion over externalist BST 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
-- insertion algorithm defined in "Data.Tree.BST.Extern.Insert" respects the key ordering.
module Data.Tree.BST.Extern.InsertProofs
  ( ProofIsBSTInsert (proofIsBSTInsert),
  )
where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Data.Tree.BST.Extern.Constructors (IsBSTT (EmptyIsBSTT, ForkIsBSTT))
import Data.Tree.BST.Extern.Insert
  ( Insertable (Insert),
    Insertable' (Insert'),
  )
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)
import Prelude (Bool (True), Ordering (EQ, GT, LT), ($))

-- | Prove that inserting a node with key @x@ and element value @a@
-- in a `Data.Tree.BST.Extern.Constructors.BST` tree preserves the @BST@ condition.
class ProofIsBSTInsert (x :: Nat) (a :: Type) (t :: Tree) where
  proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)

instance ProofIsBSTInsert x a 'EmptyTree where
  proofIsBSTInsert :: Proxy (Node x a)
-> IsBSTT 'EmptyTree -> IsBSTT (Insert x a 'EmptyTree)
proofIsBSTInsert Proxy (Node x a)
node IsBSTT 'EmptyTree
_ = IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
node IsBSTT 'EmptyTree
EmptyIsBSTT

instance
  ( o ~ CmpNat x n,
    ProofIsBSTInsert' x a ('ForkTree l (Node n a1) r) o
  ) =>
  ProofIsBSTInsert x a ('ForkTree l (Node n a1) r)
  where
  proofIsBSTInsert :: Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) r)
-> IsBSTT (Insert x a ('ForkTree l (Node n a1) r))
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT ('ForkTree l (Node n a1) r)
tIsBST = Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) r)
-> Proxy o
-> IsBSTT (Insert' x a ('ForkTree l (Node n a1) r) o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
ProofIsBSTInsert' x a t o =>
Proxy (Node x a) -> IsBSTT t -> Proxy o -> IsBSTT (Insert' x a t o)
proofIsBSTInsert' Proxy (Node x a)
pNode IsBSTT ('ForkTree l (Node n a1) r)
tIsBST (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)

-- | Prove that inserting a node with key @x@ and element value @a@
-- in a `Data.Tree.BST.Extern.Constructors.BST` tree preserves the BST condition, given that the comparison between
-- @x@ and the root key of the tree equals @o@.
-- The @BST@ condition was already checked when `proofIsBSTInsert` was called before.
-- The @o@ parameter guides the proof.
class ProofIsBSTInsert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
  proofIsBSTInsert' :: Proxy (Node x a) -> IsBSTT t -> Proxy o -> IsBSTT (Insert' x a t o)

instance ProofIsBSTInsert' x a ('ForkTree l (Node n a1) r) 'EQ where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) r)
-> Proxy 'EQ
-> IsBSTT (Insert' x a ('ForkTree l (Node n a1) r) 'EQ)
proofIsBSTInsert' Proxy (Node x a)
_ (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
_ IsBSTT r
r) Proxy 'EQ
_ = IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT IsBSTT l
l Proxy (Node n a)
pNode IsBSTT r
r
    where
      pNode :: Proxy (Node n a)
pNode = Proxy (Node n a)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node n a)

instance
  (CmpNat x n ~ 'LT) =>
  ProofIsBSTInsert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT
  where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> IsBSTT (Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
proofIsBSTInsert' Proxy (Node x a)
_ (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
pNode' IsBSTT r
r) Proxy 'LT
_ =
    IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT (IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT) Proxy (Node n a)
pNode' IsBSTT r
r
    where
      pNode :: Proxy (Node x a)
pNode = Proxy (Node x a)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node x a)

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    CmpNat x n ~ 'LT,
    ProofIsBSTInsert' x a l o,
    ProofLtNInsert' x a l n o
  ) =>
  ProofIsBSTInsert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT
  where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r)
-> Proxy 'LT
-> IsBSTT
     (Insert'
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT)
proofIsBSTInsert' Proxy (Node x a)
_ (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
pNode' IsBSTT r
r) Proxy 'LT
_ =
    (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    IsBSTT
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r))
-> IsBSTT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy (Node x a)
-> IsBSTT l
-> Proxy n
-> Proxy o
-> LtN (Insert' x a l o) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Insert' x a t o) n :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode IsBSTT l
l (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
   ~ 'True) =>
  IsBSTT
    ('ForkTree
       (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r))
 -> IsBSTT
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r))
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    IsBSTT
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r))
-> IsBSTT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
forall a b. (a -> b) -> a -> b
$
      IsBSTT (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT (Proxy (Node x a) -> IsBSTT l -> Proxy o -> IsBSTT (Insert' x a l o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
ProofIsBSTInsert' x a t o =>
Proxy (Node x a) -> IsBSTT t -> Proxy o -> IsBSTT (Insert' x a t o)
proofIsBSTInsert' Proxy (Node x a)
pNode IsBSTT l
l Proxy o
po) Proxy (Node n a)
pNode' IsBSTT r
r
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o
      pNode :: Proxy (Node x a)
pNode = Proxy (Node x a)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node x a)

instance
  (CmpNat x n ~ 'GT) =>
  ProofIsBSTInsert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT
  where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> IsBSTT (Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
proofIsBSTInsert' Proxy (Node x a)
_ (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
pNode' IsBSTT r
_) Proxy 'GT
_ =
    IsBSTT l
-> Proxy (Node n a)
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> IsBSTT
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT IsBSTT l
l Proxy (Node n a)
pNode' (IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT)
    where
      pNode :: Proxy (Node x a)
pNode = Proxy (Node x a)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node x a)

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    CmpNat x n ~ 'GT,
    ProofIsBSTInsert' x a r o,
    ProofGtNInsert' x a r n o
  ) =>
  ProofIsBSTInsert' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT
  where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy 'GT
-> IsBSTT
     (Insert'
        x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT)
proofIsBSTInsert' Proxy (Node x a)
_ (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
pNode' IsBSTT r
r) Proxy 'GT
_ =
    (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    IsBSTT
      ('ForkTree
         l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
-> IsBSTT
     ('ForkTree
        l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy (Node x a)
-> IsBSTT r
-> Proxy n
-> Proxy o
-> GtN (Insert' x a r o) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Insert' x a t o) n :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode IsBSTT r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
   ~ 'True) =>
  IsBSTT
    ('ForkTree
       l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
 -> IsBSTT
      ('ForkTree
         l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    IsBSTT
      ('ForkTree
         l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
-> IsBSTT
     ('ForkTree
        l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall a b. (a -> b) -> a -> b
$
      IsBSTT l
-> Proxy (Node n a)
-> IsBSTT (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> IsBSTT
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT IsBSTT l
l Proxy (Node n a)
pNode' (Proxy (Node x a) -> IsBSTT r -> Proxy o -> IsBSTT (Insert' x a r o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
ProofIsBSTInsert' x a t o =>
Proxy (Node x a) -> IsBSTT t -> Proxy o -> IsBSTT (Insert' x a t o)
proofIsBSTInsert' Proxy (Node x a)
pNode IsBSTT r
r Proxy o
po)
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o
      pNode :: Proxy (Node x a)
pNode = Proxy (Node x a)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node x a)

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

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

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

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

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

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

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

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

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

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

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

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