I'm trying to translate some contrived Lean code to coq, but am stuck at a syntax error and can't work out how to proceed.

What I have so far is:

```
Module Nested.
Module add_monoid.
Class add_monoid A : Type := { zero : A; add : A → A → A; }.
End add_monoid.
Module add_comm_monoid.
Class add_comm_monoid A : Type := {to_add_monoid : add_monoid.add_monoid A}.
#[export] Existing Instance to_add_monoid.
End add_comm_monoid.
Module semiring.
Class semiring A : Type :=
{ to_add_comm_monoid : add_comm_monoid.add_comm_monoid A; one : A; mul : A → A → A }.
#[export] Existing Instance to_add_comm_monoid.
End semiring.
Module add_group.
Class add_group A : Type := { to_add_monoid : add_monoid.add_monoid A; neg : A → A }.
#[export] Existing Instance to_add_monoid.
End add_group.
Module add_comm_group.
Class add_comm_group A : Type := { to_add_group : add_group.add_group A; neg : A → A }.
#[export] Existing Instance to_add_group.
#[export] Instance to_add_comm_monoid
{A : Type} `{add_comm_group A} : add_comm_monoid.add_comm_monoid A :=
{ to_add_monoid := add_group.to_add_monoid }.
End add_comm_group.
Module ring.
Class ring A : Type := { to_semiring : semiring.semiring A; neg : A → A }.
#[export] Existing Instance ring.to_semiring.
(* @[priority 100] *)
#[export] Instance to_add_comm_group
{A : Type} `{ring A} : add_comm_group.add_comm_group A :=
{ to_add_group := { to_add_monoid := semiring.to_add_monoid; neg := neg } }.
End ring.
end Nested.
```

On the final `to_add_monoid :=`

line I get the error

```
Syntax error: '&' or ':' or '|' or '}' expected after [term level 99] (in [term])
```

Am I missing something obvious? Why can I use `{}`

to construct the outer record but not the inner one?

I think `Instance`

has some special code to allow `{ .. }`

to be used for record values when everywhere else it needs to be `{| .. |}`

. That might be the issue.

And it only works for the outermost record constructor. The whole thing is a quite confusing.

If I use a `{| to_add_monoid := _ |}`

then it tells me that `to_add_monoid`

is not a projection

And if I use `{| |}`

by itself I get the error `No constructor inference.`

You might have to qualify your names since you don't import `add_group`

Aha, I didn't know `{| foo.bar := _ |}`

was legal syntax!

```
#[export] Instance to_add_comm_group
{A : Type} `{ring A} : add_comm_group.add_comm_group A :=
{ to_add_group := {| add_group.to_add_monoid := _; add_group.neg := neg |} }.
```

works, I'm now stuck at the last `_`

My hope was that Coq would solve it for me with `ring.to_semiring`

, `semiring.to_add_comm_monoid`

, and `add_comm_monoid.to_add_monoid`

I see that your `Instance`

s are all `#[export]`

which means they will only be registered when the containing module is imported. (I think.) You can try `#[global]`

as a workaround.

nice, that does the trick!

A related question; how can I look at the full term of `to_add_comm_group`

? If I run

```
Set Printing All.
Print ring.to_add_comm_group.
```

I get

```
ring.to_add_comm_group =
λ (A : Type) (H : ring.ring A),
{|
add_comm_group.to_add_group :=
{|
add_group.to_add_monoid := add_comm_monoid.to_add_monoid;
add_group.neg := ring.neg
|}
|}
: ∀ A : Type, ring.ring A → add_comm_group.add_comm_group A
```

which doesn't tell me what the argument to `add_comm_monoid.to_add_monoid`

is

That doesn't seem to work in my new scenario, though it does solve the example above

Apologies for not making a mwe:

Long code snippet

The very last `Print`

displays

```
another_test =
λ (R : Type) (H : ring.ring R) (r r' : R), neg_smul r r'
: ∀ (R : Type) (H : ring.ring R) (r r' : R),
smul (add_group.neg r) r' = add_group.neg (smul r r')
Arguments another_test _%type_scope {H} _ _
```

But I want it to display `@smul`

and `@add_group_neg`

It works for me. Maybe your editor is silently undoing your `Set Printing ..`

settings?

This is the output of the last print command:

```
another_test =
λ (R : Type) (H : ring.ring R) (r r' : R),
@neg_smul R R H (@ring.to_add_comm_group R H) (@ring.to_semiring R H) (@semiring.to_add_comm_monoid R (@ring.to_semiring R H))
(@semiring_to_module R (@ring.to_semiring R H)) r r'
: ∀ (R : Type) (H : ring.ring R) (r r' : R),
@smul R R (@ring.to_semiring R H) (@semiring.to_add_comm_monoid R (@ring.to_semiring R H))
(@semiring_to_module R (@ring.to_semiring R H))
(@add_group.neg R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R H)) r) r' =
@add_group.neg R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R H))
(@smul R R (@ring.to_semiring R H) (@semiring.to_add_comm_monoid R (@ring.to_semiring R H))
(@semiring_to_module R (@ring.to_semiring R H)) r r')
```

I'm using vscoq as an editor. That's rather annoying.

This here seems relevant (but I've never used vscoq): https://github.com/coq-community/vscoq/issues/81

Either way, your print output was all I needed; the translation was a success and Coq has exactly the same gotcha (without `Set Primitive Projections`

) as Lean 3!

Now I am curious: what's the gotcha? Term repetition?

https://arxiv.org/abs/2306.00617

Judgmental equality failures when using certain forms of multiple inheritance. Coq at least doesn't use the dangerous form automatically, whereas Lean does!

Note that in Coq, these things are done a bit differently in the MathComp library which, in its version 2, uses Hierarchy Builder to build the hierarchies. To avoid multiple inheritances issues, we require to satisfy the forgetful inheritance criterion, which is checked by HB while building the hierarchy: https://inria.hal.science/hal-02463336/document

Forgetful inheritance doesn't solve the particular problem above

It's hard for me to say whether it's possible for it to affect MathComp; I don't see a typeclass like mathlib's`module`

that has both types unbundled; it seems to me that mathcomp has `Lmodule`

, which as far as I can tell bundles the base type.

I think @Kazuhiko Sakaguchi and @Cyril Cohen faced something similar, IIRC classes (not structures) in math-comp (1 and 2, if I'm not mistaken) use primitive records/projections to solve eta-related issues.

IIRC, we didn't have any actual eta-related issue in MathComp (except for definitionally involutive duals), but the use of primitive projections visibly shortened the compilation time of MathComp.

Also, I have a small example of incoherence in packed classes caused by nested non-primitive records.

Kazuhiko Sakaguchi said:

Also, I have a small example of incoherence in packed classes caused by nested non-primitive records.

I'd be very interested in seeing that; I was ready to claim that no such incoherence is possible

Though I guess the answer is "use some inductive type which takes a algebraic packed class as a parameter"

And it's just that the type causing the problem can no longer be *another* algebraic structure.

This is my example: incoherent_comring.v

The first four structures are the same as Section 2 of this paper: https://arxiv.org/abs/2002.00620

@Eric Wieser for Set Printing All., see https://github.com/coq-community/vscoq/issues/81#issuecomment-709189814 for the vscoq/coqide version

Kazuhiko Sakaguchi said:

This is my example: incoherent_comring.v

Thanks, I will look once I'm back off mobile!

Eric Wieser said:

Though I guess the answer is "use some inductive type which takes a algebraic packed class as a parameter"

IIUC, this sort of type mismatch can be caused by extending my example with a module-like structure that takes a `semiringType`

instance as a parameter.

I think the key thing that I missed is that even with packed structures you can't pack both R and M into a single structure as then you can't talk about two modules over the same ring.

If you bundle the scalar ring R in the module structure M, there is another issue that you cannot express an abstract module over a concrete ring. So it's natural to have the scalar ring as a parameter of the module structure.

I'd also argue it's natural to put the carrier type as a parameter too, so that you can have modules over two different rings simultaneously! I suppose that you could have `Module2 R S`

as a workaround though

https://arxiv.org/abs/1102.1323 agrees to unbundle everything, but things don't scale too well that way, except maybe in Lean 4

Under the assumption that (1) we use canonical structures or unification hints as the inference mechanism and (2) we want to infer module instances from the carrier type, having the carrier type as a parameter is not an option. Nevertheless, you can define a "tag" for the carrier type and make several instances on the same carrier type coexist. For example, the converse ring is defined this way in MathComp (`^c`

is the tag). https://github.com/math-comp/math-comp/blob/mathcomp-1/mathcomp/algebra/ssralg.v#L1498

I guess the typical example from mathlib is something like "any monoid forms a module over ℕ." In a hierarchy of packed classes, this instance would be expressed as a function:

```
moduleN_of_monoid : monoidType -> moduleType nat.
```

Let's say `moduleN`

is a "tag", which is just an identity function of type `Type -> Type`

. You can trigger its inference through unification problems of the form `moduleN T =? Module.sort ?V`

whose solution is `?V := moduleN_of_monoid ?M`

and `T =? Monoid.sort ?M`

.

The example I have in mind is something more like "pairs of complex numbers are a module both over `C`

and `R`

"

The solution I suggested seems to cover that example. Let's say `C`

is canonically (in other words, by default) a module over `R`

. In MathComp, we call the instances corresponding to the fact that "any ring forms a module/algebra over itself" the "regular" instances, and we have a tag `regular : Type -> Type`

for these. Then, the canonical module instance on `C * C`

(resp. `regular C * regular C`

) is one over `R`

(resp. `C`

).

Last updated: Jun 22 2024 at 15:01 UTC