Library HoTT.Tests.Algebra.Groups.Expressions

In this file, we test various aspects of writing group expressions. These kinds of expressions appear throughout the library, but since mathclasses is quite sensitive to subtle changes, we keep this file to document and enforce certain behaviours. We use the Type vernacular command which is like Check but doesn't allow for evars.

We used a fixed universe of groups since the Type command doesn't work with polymorphic universes.

Without opening any scopes, the notation x × y will default to the one in type_scope which is the product type. In this case it will fail since Coq is expecting a type argument rather than x : G.

x^ will be interpreted as path inversion, therefore Coq will complain about its type.

In mc_scope, _ × _ denotes an instance of Mult, which groups do not have. It is useful for rings, see below.

We fail saying that no Mult instance was found for G as expected.

Here ^ is still interpreted as path inversion.

The correct scope for a general group is mc_mult_scope, where x × y is sg_op x y and ^ is inv.

This gets correctly interpreted as the group operation.

So does the group inverse.

Working with abelian groups can be confusing if the correct scopes are not open. We document the correct usage here. Similar to ×, without any scopes open, the following expression fails since Coq interprets it as the sum type.

The - _ notation doesn't have any meaning when the correct scope is not open.

Nor does the subtraction notation.

Opening mc_scope will mean that:

• + becomes the operation of a Plus.
• - x becomes a Negate operation.
• x - y is interpreted as x + (- y) for a Negate and Plus.

Notably, even though these instances exist for Rings, they do not in general for abelian groups as we treat those as groups with a commutative sg_op rather than a plus operation. This allows us to use group lemmas without deforming abelian group expressions. These fail due to a lack of Plus.

This fails due to a lack of Negate.

Opening mc_add_scope will make writing expressions of abelian groups possible.

We can also work with the abelian group with a multiplicative notation, as we would for any group.

This can get confusing if we further allow for additive notations to also be shown, so only one of mc_add_scope and mc_mult_scope should be used.

Sometimes, as when working with rings, we want + to denote plus rather than sg_op. In this case, we include a module with hints which can be imported.

This allows us to write additive notations even though we don't have mc_add_scope or mc_mult_scope open. The disadvantage of working like this however, is that any group lemmas applied to abelian groups will have their plus, zero and negate unfolded to the underlying group operations.