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

Question

我正在努力研究 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) 的 shorthand。在处理部分时，这很简单：

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) 来引用它）。这个问题向我表明我使用的类型类是错误的，或者不明白如何将符号与隐式变量集成。有人能给我指出正确的方向吗？

回答（2018 年 1 月 25 日）

基于，我能够写出以下有效的代码：

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;

}.

Answer 1

以下是 Pierre Casté运行和 Matthieu Sozeau 在 A Gentle Introduction to Type Classes and Relations in Coq (§3.9.2) 中如何解决这个问题：

A solution from ibid. consists in declaring a singleton type class for representing binary operators:
Class monoid_binop (A:Type) := monoid_op : A -> A -> A.
Nota: Unlike multi-field class types, monoid_op is not a constructor, but a transparent constant such that monoid_op f can be δβ-reduced into f.

It is now possible to declare an infix notation:
Delimit Scope M_scope with M.
Infix "*" := monoid_op: M_scope.
Open Scope M_scope.
We can now give a new definition of Monoid, using the type monoid_binop A instead of A → A → A, and the infix notation x * y instead of 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
}.

Answer 2

Pierre Casté运行和 Matthiu Sozeau 以这种方式处理问题可能是有充分理由的。

但不会

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

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

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

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

Using Implicit Type Class Parameters in Coq Notation

syntax

typeclass

coq

notation

回答（2018 年 1 月 25 日）