A Constructive Algebraic Hierarchy in Coq

We describe a framework of algebraic structures in the proof assistant Coq. We have developed this framework as part of the FTA project in Nijmegen, in which a constructive proof of the Fundamental Theorem of Algebra has been formalized in Coq. braic hierarchy that is described here is both abstract and ed. Structures like groups and rings are part of it in an abstract way, defining e.g. a ring as a tuple consisting of a group, a binary operation and a constant that together satisfy the properties of a ring. In this way, a ring automatically inherits the group properties of the additive subgroup. The algebraic hierarchy is formalized in Coq by applying a combination of labeled record types and coercions. In the labeled record types of Coq, one can use dependent types: the type of one label may depend on another label. This allows to give a type to a dependent-typed tuple like A, f, a , where A is a set, f an operation on A and a an element of A. Coercions are functions that are used i...

• Type: Journal
• Year: 2002
• Where: JSC
• Authors: Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg
• Keywords: Algebraic Structures, JSC 2002, Proof Assistant Coq, Record Types