Library FSetInterface

• Ordered types
• Non-dependent signature
• Dependent signature
• Ordered types properties

Library FSetBridge

• From non-dependent signature S to dependent signature Sdep.
• From dependent signature Sdep to non-dependent signature S.

Library FSetProperties

• Alternative (weaker) specification for fold,
• Induction principle over sets

Library FSetList

• Functions over lists
  • The set operations.
  • Proofs of set operation specifications.
• Encapsulation

Library FSetRBT

• Red-black trees
• Occurrence in a tree
• Binary search trees
• Balanced red-black trees
• Sets as red-black trees
• Logical appartness
• Empty set
• Emptyness test
• Appartness
• Singleton set
• Insertion
• Deletion
• From lists to red-black trees
• Elements
• Isomorphism with FSetList
• Union
• Intersection
• Difference
• Equality test
• Inclusion test
• Fold
• Cardinal
• Filter
• Minimum element
• Maximum element
• Any element
• Comparison

Library FSetAVL

• Trees
• Occurrence in a tree
• Binary search trees
• AVL trees
• Sets as AVL trees
• Logical appartness
• Empty set
• Emptyness test
• Appartness
• Singleton set
• Helper functions
• Insertion
• Join
• Extraction of minimum and maximum element
• Merging two trees
• Deletion
• Minimum element
• Maximum element
• Any element
• Concatenation
• Splitting
• Intersection
• Difference
• Elements
• Cardinal
• Union
• Filter
• Partition
• Subset
• Fold
• Comparison
  • Relations eq and lt over trees
  • Comparison algorithm
  • Lists of trees
  • Termination of compare_aux
  • Lemmas for the correctness of compare
  • compare_aux and compare
• Equality test

Library FSet

Index

---

This page has been generated by coqdoc