Library stdpp.options

Library stdpp.base

• Enable implicit generalization.
• Tweak program
• Sealing off definitions
• Non-backtracking type classes
• Typeclass opaque definitions
• Equality
  • Setoid equality
• Type classes
  • Decidable propositions
  • Inhabited types
  • Proof irrelevant types
  • Common properties
  • Generic orders
• Logic
• Common data types
  • Functions
  • Lists
  • Booleans
  • Unit
  • Empty
  • Products
  • Sums
  • Option
  • Sigma types
• Operations on sets
• Monadic operations
• Operations on maps
• Notations for lattices.
• Axiomatization of sets
• Miscellaneous

Library stdpp.tactics

Library stdpp.option

• General definitions and theorems
• Monadic operations
  • Inverses of constructors
• Union, intersection and difference
• Tactics

Library stdpp.fin_map_dom

• Set solver instances

Library stdpp.boolset

Library stdpp.fin_maps

• Axiomatization of finite maps
• Derived operations
• Theorems
  • General properties
  • Properties of the partial_alter operation
  • Properties of the alter operation
  • Properties of the delete operation
  • Properties of the insert operation
  • Properties of the singleton maps
  • Properties of the map operations
  • Properties of conversion to lists
  • Properties of the size operation
  • Properties of conversion from sets
  • Induction principles
  • The fold operation
  • The filter operation
  • Properties of the map_Forall predicate
  • Properties of the merge operation
  • Properties on the map_relation relation
  • Properties on the disjoint maps
  • Properties of the union_with operation
  • Properties of the union operation
  • Properties of the union_list operation
  • Properties of the folding the delete function
  • Properties on conversion to lists that depend on ∪ and ##ₘ
  • Properties of the intersection_with operation
  • Properties of the intersection operation
  • Properties of the difference_with operation
  • Properties of the difference operation
  • Misc properties about the order
  • Setoids
  • The map_seq operation
• Tactics

Library stdpp.fin

• The fin type

Library stdpp.vector

Library stdpp.pmap

• The tree data structure
• Finite sets

Library stdpp.stringmap

• Generating fresh strings

Library stdpp.fin_sets

• The elements operation
• The size operation
• Induction principles
• The set_fold operation
• Minimal elements
• Filter
• Map
• Decision procedures

Library stdpp.mapset

Library stdpp.proof_irrel

Library stdpp.hashset

Library stdpp.pretty

Library stdpp.countable

• Choice principles
• Instances
  • Injection
  • Empty
  • Unit
  • Bool
  • Option
  • Sums
  • Products
  • Lists
  • Numbers
  • Generic trees
  • Sigma

Library stdpp.orders

Library stdpp.natmap

Library stdpp.strings

• Fix scopes
• Decision of equality
• Encoding and decoding

Library stdpp.well_founded

• Theorems on well founded relations

Library stdpp.relations

• Definitions
• General theorems
  • Results about the reflexive-transitive closure rtc
  • Results about nsteps
  • Results about bsteps
  • Results about the transitive closure tc
  • Results about the symmetric closure sc
  • Equivalences between closure operators
  • Results about the reflexive-transitive-symmetric closure rtsc
• Theorems on sub relations

Library stdpp.sets

• Setoids
• Setoids
• Tactics
• Sets with ∪, ∅ and {[_]}
• Sets with ∪, ∩, ∖, ∅ and {[_]}
• Sets with ∪, ∩, ∖, ∅, {[_]}, and ⊤
• Conversion of option and list
• Finite types to sets.
• Guard
• Quantifiers
• Properties of implementations of sets that form a monad

Library stdpp.listset

Library stdpp.streams

Library stdpp.gmap

• The data structure
• Operations on the data structure
• Instantiation of the finite map interface
• Curry and uncurry
• Finite sets

Library stdpp.gmultiset

• A solver for multisets

Library stdpp.prelude

Library stdpp.listset_nodup

Library stdpp.finite

Library stdpp.numbers

• Notations and properties of nat
• Notations and properties of positive
• Notations and properties of N
• Notations and properties of Z
  • bool_to_Z
• Injectivity of casts
• Notations and properties of Qc
• Positive rationals
• Helper for working with accessing lists with wrap-around

Library stdpp.nmap

• Finite sets

Library stdpp.zmap

• Finite sets

Library stdpp.coPset

• The tree data structure
• Packed together + set operations
• Finite sets
• Pick element from infinite sets
• Conversion to psets
• Conversion from psets
• Conversion to and from gsets of positives
• Infinite sets
• Domain of finite maps
• Suffix sets
• Splitting of infinite sets

Library stdpp.coGset

• Pick elements from infinite sets
• Conversion to and from gset
• Conversion to coPset
• Inefficient conversion to arbitrary sets with a top element
• Domain of finite maps

Library stdpp.lexico

Library stdpp.propset

Library stdpp.decidable

• Instances of Decision
• Instances of RelDecision
• Decidable Sigma types

Library stdpp.list

• Definitions
• Basic tactics on lists
• General theorems
  • Properties of the reverse function
  • Properties of the elem_of predicate
  • Properties of the NoDup predicate
  • Set operations on lists
  • Properties of the last function
  • Properties of the head function
  • Properties of the take function
  • Properties of the drop function
  • Properties of the replicate function
  • Properties of the resize function
  • Properties of the rotate function
  • Properties of the rotate_take function
  • Properties of the reshape function
  • Properties of sublist_lookup and sublist_alter
  • Properties of the mask function
  • Properties of the Permutation predicate
  • Properties of the filter function
  • Properties of the prefix and suffix predicates
  • Properties of the sublist predicate
  • Properties of included
  • Properties of the Forall and Exists predicate
  • Properties of the Forall2 predicate
• Properties of the find function
• Properties of the monadic operations
  • Properties of the permutations function
  • Properties of the folding functions
  • Properties of the zip_with and zip functions
• Relection over lists
• Tactics

Library stdpp.list_numbers

• Definitions
  • Conversion of integers to and from little endian
• Properties
  • Properties of the seq function
  • Properties of the seqZ function
  • Properties of the sum_list function
  • Properties of the mjoin function that rely on sum_list
  • Properties of the max_list function
  • Properties of the Z_to_little_endian and little_endian_to_Z functions

Library stdpp.functions

Library stdpp.hlist

Library stdpp.sorting

• • Properties of the Sorted and StronglySorted predicate
  • Correctness of merge sort

Library stdpp.infinite

• Generic constructions

Library stdpp.nat_cancel

Library stdpp.namespaces

Library stdpp.telescopes

Library stdpp.binders