Data.Tree.AVL.Extern.DeleteProofs

Implementation of the necessary proofs to ensure (at compile time) that the deletion algorithm defined in Data.Tree.AVL.Extern.Delete respects the key ordering and height balance restrictions.

Documentation

class ProofIsBSTDelete (x :: Nat) (t :: Tree) where

Prove that deleting a node with key x | in an AVL tree preserves the AVL restrictions.

Methods

proofIsBSTDelete :: Proxy x -> IsBSTT t -> IsBSTT (Delete x t)

Instances

ProofIsBSTDelete x 'EmptyTree

Defined in Data.Tree.AVL.Extern.DeleteProofs

Methods

proofIsBSTDelete :: Proxy x -> IsBSTT 'EmptyTree -> IsBSTT (Delete x 'EmptyTree)

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

Defined in Data.Tree.AVL.Extern.DeleteProofs

Methods

proofIsBSTDelete :: Proxy x -> IsBSTT ('ForkTree l (Node n a1) r) -> IsBSTT (Delete x ('ForkTree l (Node n a1) r))

class ProofIsBSTDelete' (x :: Nat) (t :: Tree) (o :: Ordering) where

Prove that inserting a node with key x and element value a in an AVL tree preserves the AVL restrictions, given that the comparison between x and the root key of the tree equals o. The AVL restrictions were already checked when proofIsBSTInsert was called before. The o parameter guides the proof.

Methods

proofIsBSTDelete' :: Proxy x -> IsBSTT t -> Proxy o -> IsBSTT (Delete' x t o)

class ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where

Prove that deleting a node with key x (lower than n) 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

proofLtNDelete' :: (CmpNat x n ~ 'LT, LtN t n ~ 'True) => Proxy x -> IsBSTT t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True

class ProofGtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where

Prove that deleting a node with key x (greater than n) 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

proofGtNDelete' :: (CmpNat x n ~ 'GT, GtN t n ~ 'True) => Proxy x -> IsBSTT t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True

class ProofMaxKeyDeleteIsBST (t :: Tree) where

Prove that deleting the node with maximum key value in a BST t preserves the BST restrictions. This proof is needed for the delete operation.

Methods

proofMaxKeyDeleteIsBST :: IsBSTT t -> IsBSTT (MaxKeyDelete t)

class ProofGTMaxKey (t :: Tree) (n :: Nat) where

Prove that in a tree t which verifies that GtN t n ~ 'True, the maximum key of t is also greater than n. This proof is needed for the delete operation.

Methods

proofGTMaxKey :: GtN t n ~ 'True => IsBSTT t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT

class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where

Prove that in a tree t which verifies that GtN t n ~ 'True, the tree resulting from the removal of the maximum key of t preserves the GtN invariant. This proof is needed for the delete operation.

Methods

proofGtNMaxKeyDelete :: (MaxKeyDeletable t, GtN t n ~ 'True) => IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True

class ProofLTMaxKey (t :: Tree) (n :: Nat) where

Prove that in a tree t which verifies that LtN t n ~ 'True, the maximum key of t is also less than n. This proof is needed for the delete operation.

Methods

proofLTMaxKey :: LtN t n ~ 'True => IsBSTT t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT

class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where

Prove that in a tree t which verifies that LtN t n ~ 'True, the tree resulting from the removal of the maximum key of t preserves the LtN invariant. This proof is needed for the delete operation.

Methods

proofLtNMaxKeyDelete :: LtN t n ~ 'True => IsBSTT t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True

class ProofMaxKeyDeleteIsBalanced (t :: Tree) where

Prove that deleting the node with maximum key value in an AVL t preserves the AVL restrictions. This proof is needed for the delete operation.

Methods

proofMaxKeyDeleteIsBalanced :: IsBalancedT t -> IsBalancedT (MaxKeyDelete t)

class ProofIsBalancedDelete (x :: Nat) (t :: Tree) where

Prove that deleting a node with key x in an AVL tree preserves the AVL condition.

Methods

proofIsBalancedDelete :: Proxy x -> IsBalancedT t -> IsBalancedT (Delete x t)

Instances

ProofIsBalancedDelete x 'EmptyTree

Defined in Data.Tree.AVL.Extern.DeleteProofs

Methods

proofIsBalancedDelete :: Proxy x -> IsBalancedT 'EmptyTree -> IsBalancedT (Delete x 'EmptyTree)

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

Defined in Data.Tree.AVL.Extern.DeleteProofs

Methods

proofIsBalancedDelete :: Proxy x -> IsBalancedT ('ForkTree l (Node n a1) r) -> IsBalancedT (Delete x ('ForkTree l (Node n a1) r))

class ProofIsBalancedDelete' (x :: Nat) (t :: Tree) (o :: Ordering) where

Prove that deleting a node with key x in an AVL tree preserves the AVL condition, given that the comparison between x and the root key of the tree equals o. The AVL restrictions were already checked when proofIsBSTDelete was called before. The o parameter guides the proof.

Methods

proofIsBalancedDelete' :: Proxy x -> IsBalancedT t -> Proxy o -> IsBalancedT (Delete' x t o)