A constructive algebraic hierarchy in Coq
A constructive algebraic hierarchy in Coq
复制标题
DOI：
10.1006/jsco.2002.0552
复制
发表时间：
2002-10-01
影响因子：
0.7
通讯作者：
Zwanenburg, J
中科院分区：
文献类型：
--
作者：
Geuvers, H;Pollack, R;Zwanenburg, J
我们描述了一个框架的代数结构的证明助理Coq。我们开发了这个框架，作为奈梅亨FTA项目的一部分，其中代数基本定理的建设性证明已在Coq中形式化。这里描述的代数层次结构既抽象又结构化。像群和环这样的结构以抽象的方式是它的一部分，例如将环定义为由一个群、一个二元运算和一个常数组成的元组，这些元组一起满足环的性质。通过这种方式，环自动继承加法子群的群属性。代数层次结构在Coq中通过应用标记记录类型和标记子的组合来形式化。在Coq的标记记录类型中，可以使用依赖类型：一个标签的类型可能依赖于另一个标签。这允许我们给一个依赖类型的元组（如[A，f，a]）赋予一个类型，其中A是一个集合，f是对A的操作，a是A的元素。强制是隐式使用的函数（它们由类型检查器推断），并且允许例如使用结构A：= [A，f，a]作为载体集合A的同义词，就像在数学实践中经常做的那样。除了属性的继承和重用之外，代数层次结构已经证明对于重用符号非常有用。(C)2002爱思唯尔科技有限公司。保留所有权利。
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.The algebraic hierarchy that is described here is both abstract and structured. 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 labelled record types and coercions. In the labelled record types of Coq, one can use dependent types: the type of one label may depend on another label. This allows us 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 implicitly (they are inferred by the type checker) and allow, for example, to use the structure A := [A, f, a] as a synonym for the carrier set A, as is often done in mathematical practice. Apart from the inheritance and reuse of properties, the algebraic hierarchy has proven very useful for reusing notations. (C) 2002 Elsevier Science Ltd. All rights reserved.