Data.Tree.AVL.Extern.InsertProofs

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

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 BST condition.

Methods

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

Instances

ProofIsBSTInsert x a 'EmptyTree

Defined in Data.Tree.AVL.Extern.InsertProofs

Methods

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

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

Defined in Data.Tree.AVL.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 BST condition, given that the comparison between x and the root key of the tree equals o. The BST restrictions were 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

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

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

Methods

proofIsBalancedInsert :: Proxy (Node x a) -> IsBalancedT t -> IsBalancedT (Insert x a t)

Instances

ProofIsBalancedInsert x a 'EmptyTree

Defined in Data.Tree.AVL.Extern.InsertProofs

Methods

proofIsBalancedInsert :: Proxy (Node x a) -> IsBalancedT 'EmptyTree -> IsBalancedT (Insert x a 'EmptyTree)

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

Defined in Data.Tree.AVL.Extern.InsertProofs

Methods

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

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

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

Methods

proofIsBalancedInsert' :: Proxy (Node x a) -> IsBalancedT t -> Proxy o -> IsBalancedT (Insert' x a t o)