-
Math-Components
- Mathematical Components library
- The Mathematical Components library is a set of Coq libraries that cover the prerequisites for the mechanization of the proof of the Odd Order Theorem.
- https://math-comp.github.io/
-
Math-comp-analysis
- This is an extension of the Math-components library (a library for Coq) to cover real analysis.
- This library adds definitions and theorems to the Math-components library for real numbers and their mathematical structures.
- https://github.com/math-comp/analysis
-
Hierarchy Builder
- High level commands to declare and evolve a hierarchy based on packed classes.
- Hierarchy Builder is a high level language for Coq to build hierarchies of algebraic structures and to make these hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder and abbreviation that let the hierarchy developer describe an actual interface for their library. Behind that interface the developer can provide appropriate code to ensure retro compatibility.
- https://github.com/math-comp/hierarchy-builder
-
Trocq
- Proof transfer across morphism, mono, epi or iso in Coq.
- Trocq is a prototype of a modular parametricity plugin for Coq, aiming to perform proof transfer by translating the goal into an associated goal featuring the target data structures as well as a rich parametricity witness from which a function justifying the goal substitution can be extracted. The plugin features a hierarchy of parametricity witness types, ranging from structure-less relations to a new formulation of type equivalence, gathering several pre-existing parametricity translations, including univalent parametricity and CoqEAL, in the same framework. This modular translation performs a fine-grained analysis and generates witnesses that are rich enough to preprocess the goal yet are not always a full-blown type equivalence, allowing to perform proof transfer with the power of univalent parametricity, but trying not to pull in the univalence axiom in cases where it is not required. The translation is implemented in Coq-Elpi and features transparent and readable code with respect to a sequent-style theoretical presentation.
- https://github.com/coq-community/trocq
