• Home
• About Coq
• Get Coq
• Documentation
• Community

Library Containers.OrderedType

• Ordered Types
  • Strict orders : the StrictOrder class
  • Ordered types : the OrderedType class
  • Specific Ordered types : OrderedType with specific equality
  • Usual Ordered types : OrderedType with Leibniz equality
• Facts about setoid list membership

Library Containers.Tactics

• Tactics for inductives without recursion, nor parameters
  • Equivalence
  • StrictOrder
  • compare_spec
• Tactics for inductives with recursion, but no parameters
  • Equivalence
  • StrictOrder
  • compare_spec
• Tactics for mutual inductives, but no parameters
  • Equivalence
  • StrictOrder
  • compare_spec

Library Containers.OrderedTypeEx

• Useful instances of ordered types
  • Z
  • nat
  • N
  • positive
  • Q
  • bool
  • unit
  • Products
  • Products, revisited
  • Sums
  • Lists of comparable elements
  • Options

Library Containers.Bridge

Library Containers.SetInterface

• Pointwise-equality
• FSet : the interface of sets
• FSetSpecs : finite sets' specification

Library Containers.SetFacts

• Specifications written using equivalences
• Specifications written using boolean predicates
• Equal is a setoid equality
• Subset is a setoid order
• Set operations and morphisms
• Inductive specifications of boolean functions

Library Containers.SetDecide

• Overview
• Facts and Tactics for Propositional Logic
  • Lemmas and Tactics About Decidable Propositions
  • Propositional Equivalences Involving Negation
  • Tactics for Negations
• Auxiliary Tactics
  • Generic Tactics
  • Discarding Irrelevant Hypotheses
  • Turning Set Operators into Propositional Connectives
  • Decidability of FSet Propositions
  • Normalizing Propositions About Equality
  • Considering Decidability of Base Propositions
  • Handling Empty, Subset, and Equal
  • The Core fsetdec Auxiliary Tactics
• The fsetdec Tactic

Library Containers.SetProperties

• Properties of elements
• Conversions between lists and sets
• Fold
  • Induction principles for fold (contributed by S. Lescuyer)
  • Alternative (weaker) specifications for fold
  • Fold is a morphism
  • Fold and other set operators
• Cardinal
  • Characterization of cardinal in terms of fold
  • Old specifications for cardinal.
  • Cardinal and (non-)emptiness
  • Cardinal is a morphism
  • Cardinal and set operators
• Facts about For_all and Exists: since these predicates
• More precise reflexive view of for_all and _exists than the one

Library Containers.SetEqProperties

Library Containers.SetList

Library Containers.SetListInstance

• SetList_FSet : an instance of FSet based on ordered lists
• SetList_FSetSpecs : specifications for SetList_FSet

Library Containers.SetAVL

• Raw
• Trees
• Basic functions on trees: height and cardinal
• Empty Set
• Emptyness test
• Appartness
• Singleton set
• Helper functions
• Insertion
• Join
• Extraction of minimum element
• Merging two trees
• Deletion
• Minimum element
• Maximum element
• Any element
• Concatenation
• Splitting
• Intersection
• Difference
• Union
• Elements
• Filter
• Partition
• for_all and exists
• Map
• Fold
• Subset
• A new comparison algorithm suggested by Xavier Leroy
• Equality test
  • Occurrence in a tree
  • Binary search trees
• Some shortcuts
• Correctness proofs, isolated in a sub-module
• Automation and dedicated tactics
• Basic results about In, lt_tree, gt_tree, height
• Inductions principles
• Empty set
• Emptyness test
• Appartness
• Singleton set
• Helper functions
• Insertion
• Join
• Extraction of minimum element
• Merging two trees
• Deletion
• Minimum element
• Maximum element
• Any element
• Concatenation
• Splitting
• Intersection
• Difference
• Union
• Elements
• Filter
• Partition
• for_all and exists
• Map
• Fold
• Subset
• Comparison
  • Relations eq and lt over trees
• A new comparison algorithm suggested by Xavier Leroy
• Equality test
• Encapsulation

Library Containers.SetAVLInstance

• SetAVL_FSet : an instance of FSet based on AVL trees
• SetAVL_FSetSpecs : specifications for SetAVL_FSet

Library Containers.Sets

• Exporting interface and facts, for direct access
• Loading an implementation

Library Containers.MapInterface

• FMaps : the interface of maps
• FMapSpecs : finite maps' specification

Library Containers.MapNotations

Library Containers.MapFacts

• Facts about weak maps
  • Specifications written using equivalences
  • Specifications written using boolean predicates
• Relations between Equal, Equiv and Equivb.
• Equal is a setoid equality.
• Additional Properties for weak maps
• Elements
• Conversions between maps and association lists.
• Fold
  • Induction principles about fold contributed by S. Lescuyer
  • Additional properties of fold
• Cardinal
• Additional notions over maps
• Emulation of some functions lacking in the interface
• Properties specific to maps with ordered keys
• Inductive specifications of boolean functions

Library Containers.MapList

Library Containers.MapListInstance

• MapList_FMap : an instance of FMap based on List trees
• MapList_FMapSpecs : specifications for MapList_FMap

Library Containers.MapAVL

• The Raw functor
• Trees
• Trees
• Basic functions on trees: height and cardinal
• Empty Map
• Emptyness test
• Appartness
• Helper functions
• Insertion
• Insertion with combining functions : naive and efficient versions
• Adjusting existing mappings
• Extraction of minimum binding
• Merging two trees
• Deletion
• join
• Splitting
• Concatenation
• Elements
• Fold
• Comparison
  • Enumeration of the elements of a tree
• Map
• Map with removal
• Optimized map2
• Map2
• Invariants
  • Occurrence in a tree
  • Binary search trees
• Correctness proofs, isolated in a sub-module
• Automation and dedicated tactics.
• Basic results about MapsTo,
• Empty map
• Emptyness test
• Appartness
• Helper functions
• Insertion
• Insertion with combining function
• Adjusting an existing mapping
• Back to insertion : the efficient version can be
• Extraction of minimum binding
• Merging two trees
• Deletion
• join
• split
• Concatenation
• Elements
• Fold
• Comparison
• Encapsulation

Library Containers.MapAVLInstance

• MapAVL_FMap : an instance of FMap based on AVL trees
• MapAVL_FMapSpecs : specifications for MapAVL_FMap

Library Containers.MapPositive

• An implementation of FMapInterface.S for positive keys.

Library Containers.MapPositiveInstance

• MapPositive_FMap : an instance of FMap for positives
• MapPositive_FMapSpecs : specifications for MapPositive_FMap

Library Containers.CMapPositive

• An implementation of FMapInterface.S for positive keys.

Library Containers.CMapPositiveInstance

• CMapPositive_FMap : an instance of FMap for positives
• CMapPositive_FMapSpecs : specifications for CMapPositive_FMap

Library Containers.Maps

• Exporting interface and facts, for direct access
• Loading an implementation

Library Containers.Generate

Library Containers.SetConstructs

• Mapping a function on a set
• Cartesian product
• Implementation of power sets
• Diagonal product
• Disjoint union

• webmaster
• xhtml valid
• CSS valid