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

Question

I am having a hard time understanding the mechanism of structures with inheritance (18.9) in an example (and coercion in Coq in general).

From a paper about MathClasses, there is an example of structure with inheritance (:>) between SemiRing and 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 
}.

I understand that mathematically, the multiplication and addition operations (semiring_{mult,plus}_m) in a SemiRing is each a CommutativeMonoid. Also, the the classes SemiRing and CommutativeMonoid are predicate functions similar to conjunction /\.

From the manual linked above,

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

But I don't see how this works computationally in the example above. In terms of order, do we prove that something A is a SemiRing first, or do we prove CommutativeMonoid A first?

After we prove one of these two properties of A, do we also need to prove the other? If not, how can Coq automatically deduce that using the declaration above?

Answer 1

You can do it, so to say, either way. Let's build an instance of the SemiRing typeclass for the natural numbers. The first variant can be found in the MathClasses library (here). Note: I've installed a recent MathClasses version via OPAM, so some names are a bit different.

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.

We can see here, that we've proved all the properties we need for SemiRings. And we've done it without building intermediate instances for CommutativeMonoid, Monoid, etc. -- all the way up to Setoid. Because of the coercion mechanism we can use our SemiRing nat as an instance of any of the "predecessor" typeclasses:

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.

But if we ask Coq to print instances of the Monoid typeclass (Print Instances Monoid.), then we won't find those two instances we've implicitly built.

The above could be called a top-down approach: we build an instance of the most expressive typeclass and then we get the ability to use it as a more abstract entity.

---

The other way is to use the bottom-up approach: we start with the least expressive typeclass and gradually build our instances up to the most expressive typeclass.

(* ... 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.

If we now

Print Instances Monoid.

we get

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

since we've built (and named) the instances explicitly. A quick example:

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