Pragmatic Quotient Types in Coq

Cyril Cohen 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In intensional type theory, it is not always possible to form the quotient of a type by an equivalence relation. However, quotients are extremely useful when formalizing mathematics, especially in algebra. We provide a Coq library with a pragmatic approach in two complementary components. First, we provide a framework to work with quotient types in an axiomatic manner. Second, we program construction mechanisms for some specific cases where it is possible to build a quotient type. This library was helpful in implementing the types of rational fractions, multivariate polynomials, field extensions and real algebraic numbers.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01966714
Contributor : Cyril Cohen <>
Submitted on : Saturday, December 29, 2018 - 2:55:57 PM
Last modification on : Thursday, February 7, 2019 - 3:37:33 PM
Long-term archiving on : Saturday, March 30, 2019 - 1:18:18 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01966714, version 1

Collections

Citation

Cyril Cohen. Pragmatic Quotient Types in Coq. International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.16. ⟨hal-01966714⟩

Share

Metrics

Record views

31

Files downloads

58