我试图把头放在Coq中的类型类上（我过去曾涉猎它，但与经验丰富的用户相去甚远）。作为练习，我试图编写一个小组理论库。这是我想出的：
Class Group {S : Type} {op : S → S → S} := {
id : S;
inverse : S → S;
id_left {x} : (op id x) = x;
id_right {x} : (op x id) = x;
assoc {x y z} : (op (op x y) z) = (op x (op y z));
right_inv {x} : (op x (inverse x)) = id;
}.
我特别喜欢隐式S和op参数（假设我正确理解了它们）。
对逆进行一些表示很容易：
Notation "- x" := (@inverse _ _ _ x)
(at level 35, right associativity) : group_scope.
现在，我想作x * y一个简写(op x y)。使用节时，这很简单：
Section Group.
Context {S} {op} { G : @Group S op }.
(* Reserved at top of file *)
Notation "x * y" := (op x y) : group_scope.
(* ... *)
End Group.
但是，由于这是在节中声明的，因此该符号在其他位置不可访问。如果可能的话，我想在全球范围内声明该符号。我遇到的问题（与相对inverse）是，由于op是的隐式参数Group，因此它在全局范围中实际上不存在（因此我无法通过引用它(@op _ _ _ x y)）。这个问题向我表明我要么使用了错误的类型类，要么不理解如何将符号与隐式变量集成在一起。有人能指出我正确的方向吗？
根据安东·特鲁诺夫（Anton Trunov）的回应，我能够编写出如下的作品：
Reserved Notation "x * y" (at level 40, left associativity).
Class alg_group_binop (S : Type) := alg_group_op : S → S → S.
Delimit Scope group_scope with group.
Infix "*" := alg_group_op: group_scope.
Open Scope group_scope.
Class Group {S : Type} {op : alg_group_binop S} : Type := {
id : S;
inverse : S → S;
id_left {x} : id * x = x;
id_right {x} : x * id = x;
assoc {x y z} : (x * y) * z = x * (y * z);
right_inv {x} : x * (inverse x) = id;
}.
皮埃尔·卡斯特兰（PierreCastéran）和马修·索索（Matthieu Sozeau）在《对Coq中的类型类和关系的温和介绍》（第3.9.2节）中解决了此问题：
同上的解决方案。在于声明一个用于表示二进制运算符的单例类型类：
Class monoid_binop (A:Type) := monoid_op : A -> A -> A.注意：与多字段类类型不同，
monoid_op它不是构造函数，而是一个透明常数，monoid_op f可以将δβ简化为f。现在可以声明一个中缀符号：
Delimit Scope M_scope with M. Infix "*" := monoid_op: M_scope. Open Scope M_scope.现在，我们可以
Monoid使用类型monoid_binop A代替A → A → A，并使用中缀表示法x * y代替来给出的新定义monoid_op x y：Class Monoid (A:Type) (dot : monoid_binop A) (one : A) : Type := { dot_assoc : forall x y z:A, x*(y*z) = x*y*z; one_left : forall x, one * x = x; one_right : forall x, x * one = x }.
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句