具有继承 (:>) 的结构如何在 Coq 中工作？

Question

我很难理解示例中 structures with inheritance (18.9) 的机制（以及 Coq 中的强制转换）。

从一篇关于 MathClasses 的论文中，有一个在 SemiRing 和 CommutativeMonoid 之间具有继承 (:>) 的结构示例：

Class SemiRing A {e: Equiv} {plus: RingPlus A} {mult: RingMult A}
  {zero: RingZero A} {one: RingOne A}: Prop :=
{
   semiring_mult_monoid:> CommutativeMonoid A (op:=mult)(unit:=one)
 ; semiring_plus_monoid:> CommutativeMonoid A (op:=plus)(unit:=zero)
 ; semiring_distr:> Distribute mult plus
 ; semiring_left_absorb:> LeftAbsorb mult zero 
}.

我理解在数学上，SemiRing 中的乘法和加法运算 (semiring_{mult,plus}_m) 各是一个 CommutativeMonoid。此外，类 SemiRing 和 CommutativeMonoid 是类似于连词 /\.

的谓词函数

根据上面链接的手册，

If ident_i:>term_i, then ident_i is automatically declared as coercion from ident to the class of term_i.

但在上面的示例中，我看不到这是如何计算的。在顺序上，我们是先证明A是SemiRing，还是先证明CommutativeMonoid A？

我们证明了A的这两个性质中的一个之后，还需要证明另一个吗？如果不是，Coq 如何使用上面的声明自动推断出它？

Answer 1

你可以做到，可以这么说，无论哪种方式。让我们为自然数构建一个 SemiRing 类型类的实例。第一个变体可以在 MathClasses 库中找到（here). Note: I've installed a recent MathClasses version via OPAM，所以有些名字有点不同。

Require Import Coq.Arith.Arith.
Require Import MathClasses.interfaces.abstract_algebra.

Instance nat_equiv: Equiv nat := eq.
Instance nat_plus: Plus nat := Peano.plus.
Instance nat_0: Zero nat := 0%nat.
Instance nat_1: One nat := 1%nat.
Instance nat_mult: Mult nat := Peano.mult.

Instance: SemiRing nat.
Proof.
  repeat (split; try apply _); repeat intro.
         now apply plus_assoc.
        now apply plus_0_r.
       now apply plus_comm.
      now apply mult_assoc.
     now apply mult_1_l.
    now apply mult_1_r.
   now apply mult_comm.
  now apply mult_plus_distr_l.
Qed.

我们可以在这里看到，我们已经证明了 SemiRing 所需的所有属性。我们在没有为 CommutativeMonoid、Monoid 等构建中间实例的情况下完成了这项工作——一直到 Setoid。由于强制机制，我们可以使用 SemiRing nat 作为 "predecessor" 类型类的 any 的实例：

Goal @CommutativeMonoid nat _ plus 0. Proof. apply nat_semiring. Qed.
Goal @Monoid nat _ mult 1. Proof. apply nat_semiring. Qed.
Goal Setoid nat. Proof. apply nat_semiring. Qed.

但是如果我们要求 Coq 打印 Monoid 类型类 (Print Instances Monoid.) 的实例，那么我们将找不到我们已经 隐式 [=44] 的那两个实例=] 建成。

以上可以称为自上而下的方法：我们构建最具表现力的类型类的实例，然后我们能够将其用作更抽象的实体。

另一种方法是使用自下而上的方法：我们从表现力最低的类型类开始，逐渐构建我们的实例，直到表现力最强的类型类。

(* ... boilerplate skipped ... *) Ltac deduce_fields := split; try exact _; try easy. Instance: Equivalence nat_equiv. deduce_fields. Qed. Instance nat_setoid: Setoid nat. unfold Setoid. deduce_fields. Qed. Instance nat_semigroup_plus: @SemiGroup nat _ plus. deduce_fields. exact plus_assoc. Qed. Instance nat_semigroup_mult: @SemiGroup nat _ mult. deduce_fields. exact mult_assoc. Qed. Instance nat_monoid_plus: @Monoid nat _ plus 0. deduce_fields. exact plus_0_r. Qed. Instance nat_monoid_mult: @Monoid nat _ mult 1. deduce_fields. exact mult_1_l. exact mult_1_r. Qed. Instance nat_comm_monoid_plus: @CommutativeMonoid nat _ plus 0. deduce_fields. exact plus_comm. Qed. Instance nat_comm_monoid_mult: @CommutativeMonoid nat _ mult 1. deduce_fields. exact mult_comm. Qed. Instance nat_semiring: SemiRing nat. deduce_fields. exact mult_plus_distr_l. Qed.

如果我们现在

Print Instances Monoid.

我们得到

(* ... *) nat_monoid_plus : Monoid nat nat_monoid_mult : Monoid nat (* ... *)

因为我们明确地构建（并命名）了实例。一个简单的例子：

Goal @Monoid nat _ plus 0. exact nat_monoid_plus. (* apply nat_semiring works too *) Qed.

Answer 2

阅读此声明的另一种方法是：

Class SemiRing A {e: Equiv} {plus: RingPlus A} {mult: RingMult A}
  {zero: RingZero A} {one: RingOne A}: Prop :=
{
   semiring_mult_monoid : CommutativeMonoid A (op:=mult)(unit:=one)
 ; semiring_plus_monoid : CommutativeMonoid A (op:=plus)(unit:=zero)
 ; semiring_distr       : Distribute mult plus
 ; semiring_left_absorb : LeftAbsorb mult zero 
}.

加上相应的强制：

Coercion SemiRing A ...   >-> CommutativeMonoid A ...
Coercion SemiRing A _ m p >-> Distribute m p

等...

具有继承 (:>) 的结构如何在 Coq 中工作？

How do Structures with Inheritance (:>) work in Coq?

coq

coercion