Data.Tree.BST.Extern.InsertProofs

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.

Documentation

class ProofIsBSTInsert (x :: Nat) (a :: Type) (t :: Tree) where

Prove that inserting a node with key x and element value a in a BST tree preserves the BST condition.

Methods

proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)

Instances

ProofIsBSTInsert x a 'EmptyTree

Defined in Data.Tree.BST.Extern.InsertProofs

Methods

proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT 'EmptyTree -> IsBSTT (Insert x a 'EmptyTree)

(o ~ CmpNat x n, ProofIsBSTInsert' x a ('ForkTree l (Node n a1) r) o) => ProofIsBSTInsert x a ('ForkTree l (Node n a1) r)

Defined in Data.Tree.BST.Extern.InsertProofs

Methods

proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT ('ForkTree l (Node n a1) r) -> IsBSTT (Insert x a ('ForkTree l (Node n a1) r))

class ProofIsBSTInsert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where

Prove that inserting a node with key x and element value a in a 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.

Methods

proofIsBSTInsert' :: Proxy (Node x a) -> IsBSTT t -> Proxy o -> IsBSTT (Insert' x a t o)

class ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where

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.

Methods

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

class ProofGtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where

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.

Methods

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