How to represent mathematical structures in Coq?

For the sake of example, let’s say I want to represent semigroups in Coq. There are quite a few different ways to go about this.

A semigroup is a set plus a binary operation, which is associative.

Record Sg := {
  C : Type;
  app : C -> C -> C;
  assoc : forall a b c, app (app a b) c = app a (app b c);

1: Should Sg have its carrier as a field (as above), or as an index?

Record Sg (C : Type) := {
  app : C -> C -> C;
  assoc : ...;

This makes it easier to represent types which are carriers of multiple structures.

(* A function for C that is both a Sg and a Foo *)
Definition f (C : Type) (Sg_C : Sg C) (Foo_C : Foo C) := ...

But you could also say the same of the app operation in the Sg record, it could be associated with different algebraic structures, so should it be an index too?

2: Should the laws be in a separate record?

Record Sg (C : Type) := {
  app : C -> C -> C;

Record LawfulSg (C : Type) (sg : Sg C) : Prop := {
  assoc : ...

There are various advantages of keeping proof terms separate from “computational” terms. One is performance (you don’t need to worry about choosing an evaluation order which avoids reducing expensive proof terms if they don’t occur in the first place). Another is that if you have proof terms lying around sooner or later you’ll run into issues of proof relevance, as you try to relate functions which consume or produce proof terms.

3: Here again we have the choice of representing the subject of the laws as an index (above) or as a field:

Record LawfulSg (C : Type) := {
  sg :> Sg C;
  assoc : ...;

What other alternatives are there? Is there a recommended approach? Can you point me to literature discussing the trade-offs?

1 Like

“Bundling is bad” is what Spitters and van der Weegen say:

It might not be completely up-to-date, but it should be a good starting point.

1 Like

Section 2.14
in Homotopy Type Theory: Univalent Foundations of Mathematics
discusses this issue and even uses the same example for it.
The discussion does not address the question of bundling,
but it does show how the typical univalence axiom relates
to the separation of members from laws (or computations from proofs).
In particular, the axiom makes it unnecessary to perform the separation,
because the equality of laws, at least for set-like types,
follows directly from the transport lemma and the equivalence of types.

1 Like

in, the algebraic structures are encapsulated in two layers. take semigroup as an example. there is an IsSemigroup record and Semigroup record.

record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
    isMagma : IsMagma ∙
    assoc   : Associative ∙

  open IsMagma isMagma public

record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
    Carrier     : Set c
    _≈_         : Rel Carrier ℓ
    _∙_         : Op₂ Carrier
    isSemigroup : IsSemigroup _≈_ _∙_

  open IsSemigroup isSemigroup public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public using (rawMagma)

in general, IsBlah is a predicate over both carrier and operations. in some sense, though, it doesn’t represent the mathematical structure itself but just states that there is a mathematical structure with the carrier and operations. Blah, in turn, represents the structure. I think it makes a lot of sense, because in text book math, a structure is often stated as a tuple of carrier and operations, together with the laws.

The most relevant paper given the maturity of their development is

This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular allows multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to support a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the handiness of a classical setting, without requiring any axiom. Finally, we show how externally extensible some of these instances are by discussing a lemma seminal in defining the discrete logarithm, and a matrix decomposition problem.

1 Like

Arguably the fundamental choice in formalizing structures in proof assistants is whether to use:

  • Type classes
  • Records and unification hints (canonical structures)
  • Modules (functors)

I don’t think anybody is using modules for this in a large scale these days. Both MathClasses/CoRN and Lean’s Mathlib uses typeclasses, while Mathematical Components (linked by @ejgallego) uses canonical structures.


This is very much a F.A.Q. , and there are many resources and discussions around yet we never seem to converge to a canonical Coq F.A.Q :frowning:

I’d even say that this is a very hairy topic as a few papers on the subject do actually make wrong claims :slight_smile: :slight_smile:

I’ll shut up for now, a few more related links:


Some more discussion here I like the theory combinators mentioned at the bottom of that page. (Sorry, I’m only allowed one link.)
The coq developers are working on improving the treatment of algebraic structures.

Meanwhile, both the math-components and the math-classes approaches work reasonable well.