在 Coq 表示法中使用隐式类型类参数答案

【问题标题】：Using Implicit Type Class Parameters in Coq Notation在 Coq 表示法中使用隐式类型类参数
【发布时间】：2018-01-23 04:06:30
【问题描述】：

我正试图围绕 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 的隐式参数，它实际上并不存在于全局范围内的任何地方（所以我不能通过@ 引用它987654332@)。这个问题向我表明我要么使用错误的类型类，要么不了解如何将符号与隐式变量集成。有人能指出我正确的方向吗？

回答（2018 年 1 月 25 日）

基于Anton Trunov's response，我能够编写以下内容，它有效：

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;

}.

【问题讨论】：

标签： syntax typeclass coq notation

【解决方案1】：

以下是 Pierre Castéran 和 Matthieu Sozeau 在A Gentle Introduction to Type Classes and Relations in Coq (§3.9.2) 中解决此问题的方法：

同上的一个解决方案是声明一个单例类型类来表示二元运算符：
Class monoid_binop (A:Type) := monoid_op : A -> A -> A.
注意：与多字段类类型不同，monoid_op 不是构造函数，而是透明常量，因此 monoid_op f 可以 δβ-reduced 为 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
}.

【讨论】：

太好了，谢谢！我会试一试，如果我遇到任何问题，请告诉您。

【解决方案2】：

Pierre Castéran 和 Matthiu Sozeau 以这种方式处理它可能是有充分理由的。

但不会

Definition group_op {S op} {G : @Group S op} := op.
Infix "*" := group_op.

也在这里工作？（我只尝试了两个非常基本的测试用例。）

这样可以避免您更改 Group 的定义。

【讨论】：