Library stdpp.options

Library stdpp.base

• Enable implicit generalization.
• Tweak program
• Sealing off definitions
• Solving type class instances
• 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

• The "o" family of tactics equips pose proof, destruct, inversion,

Library stdpp.option

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

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
  • Induction principles
  • Properties of conversion from sets
  • The fold operation
  • Properties of the map_Forall predicate
  • Properties of the map_Exists predicate
  • The filter operation
  • Properties of the merge operation
  • Properties on the map_relation relation
  • Properties of the map_agree operation
  • 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
  • The map_seqZ operation
  • The map_img (image/codomain) operation
  • The map_compose operation
• Tactics

Library stdpp.fin

• The fin type

Library stdpp.vector

Library stdpp.pmap

• The trie 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
• Bind
• OMap
• 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 tree data structure
• 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
• 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

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
  • Interaction between the take/drop/reverse functions
  • Other lemmas that use take/drop in their proof.
  • 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 the Forall and Exists predicate
  • Properties of the Forall2 predicate
  • Properties of subseteq
• 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
• Reflection 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

Library stdpp.ssreflect

Library stdpp.bitvector.definitions

• bitvector library
• Settings
• Preliminary definitions
• BvWf
• Definition of bv n
• Typeclass instances for bv n
• bv_saturate: Add range facts about bit vectors to the context
• Operations on bv n
• Operations on bv n and Z
• Operations on bv n and bool
• Notation for bv operations
• bv_wrap_simplify: typeclass-based automation for simplifying bv_wrap
• Lemmas about bv n operations
  • Unfolding lemmas for the operations.
  • Properties of bv operations
  • Lemmas about bv_to_little and bv_of_little
  • Lemmas about bv_seq
  • Lemmas about bv and bool
• bvn
• Opaqueness

Library stdpp.bitvector.tactics

• bitvector tactics
• Settings
• General tactics
• General lemmas
• bv_simplify rewrite database
• bv_unfold
• bv_unfolded_simplify rewrite database
• bv_unfolded_to_arith rewrite database
• Reduction of closed terms
• bv_simplify tactic
• bv_solve tactic

Library stdpp.bitvector.bitvector

Library stdpp.unstable.bitblast

• bitblast tactic: Solve integer goals by bitwise reasoning
• Settings
• Helper lemmas to upstream
  • bitranges
• simpl_bool
• simplify_bitblast_index
• Main typeclasses for bitblast
  • IsPowerOfTwo
  • BitblastBounded
  • Bitblast
• Tactics
  • Helper definitions and lemmas for the tactics
  • Core tactics
  • Tactic notations