Stream: Coq users

Topic: Syntax error in nested records?


view this post on Zulip Eric Wieser (Jun 02 2023 at 14:57):

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?

view this post on Zulip Janno (Jun 02 2023 at 14:59):

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.

view this post on Zulip Janno (Jun 02 2023 at 15:00):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:00):

If I use a {| to_add_monoid := _ |} then it tells me that to_add_monoid is not a projection

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:01):

And if I use {| |} by itself I get the error No constructor inference.

view this post on Zulip Janno (Jun 02 2023 at 15:01):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:01):

Aha, I didn't know {| foo.bar := _ |} was legal syntax!

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:03):

  #[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 _

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:04):

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

view this post on Zulip Janno (Jun 02 2023 at 15:06):

I see that your Instances 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.

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:10):

nice, that does the trick!

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:25):

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

view this post on Zulip Gaëtan Gilbert (Jun 02 2023 at 15:41):

https://coq.github.io/doc/master/refman/language/extensions/implicit-arguments.html#coq:flag.Printing-Implicit

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:44):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:44):

Apologies for not making a mwe:

Long code snippet

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:45):

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} _ _

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:45):

But I want it to display @smul and @add_group_neg

view this post on Zulip Janno (Jun 02 2023 at 15:46):

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

view this post on Zulip Janno (Jun 02 2023 at 15:46):

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')

view this post on Zulip Eric Wieser (Jun 02 2023 at 15:48):

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

view this post on Zulip Janno (Jun 02 2023 at 15:49):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 16:00):

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!

view this post on Zulip Janno (Jun 02 2023 at 16:04):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 16:14):

https://arxiv.org/abs/2306.00617

view this post on Zulip Eric Wieser (Jun 02 2023 at 16:14):

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

view this post on Zulip Pierre Roux (Jun 02 2023 at 16:19):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 16:28):

Forgetful inheritance doesn't solve the particular problem above

view this post on Zulip Eric Wieser (Jun 02 2023 at 16:36):

It's hard for me to say whether it's possible for it to affect MathComp; I don't see a typeclass like mathlib'smodule that has both types unbundled; it seems to me that mathcomp has Lmodule, which as far as I can tell bundles the base type.

view this post on Zulip Enrico Tassi (Jun 02 2023 at 19:48):

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.

view this post on Zulip Kazuhiko Sakaguchi (Jun 02 2023 at 20:06):

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.

view this post on Zulip Kazuhiko Sakaguchi (Jun 02 2023 at 20:08):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 20:10):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 20:15):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 20:16):

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

view this post on Zulip Kazuhiko Sakaguchi (Jun 02 2023 at 20:26):

This is my example: incoherent_comring.v

view this post on Zulip Kazuhiko Sakaguchi (Jun 02 2023 at 20:27):

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

view this post on Zulip Paolo Giarrusso (Jun 02 2023 at 20:30):

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

view this post on Zulip Eric Wieser (Jun 02 2023 at 20:34):

Kazuhiko Sakaguchi said:

This is my example: incoherent_comring.v

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

view this post on Zulip Kazuhiko Sakaguchi (Jun 02 2023 at 20:51):

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.

view this post on Zulip Eric Wieser (Jun 02 2023 at 22:02):

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.

view this post on Zulip Kazuhiko Sakaguchi (Jun 03 2023 at 10:42):

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.

view this post on Zulip Eric Wieser (Jun 03 2023 at 11:00):

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

view this post on Zulip Paolo Giarrusso (Jun 03 2023 at 11:04):

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

view this post on Zulip Kazuhiko Sakaguchi (Jun 03 2023 at 11:07):

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

view this post on Zulip Kazuhiko Sakaguchi (Jun 03 2023 at 11:22):

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.

view this post on Zulip Eric Wieser (Jun 03 2023 at 15:06):

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

view this post on Zulip Kazuhiko Sakaguchi (Jun 04 2023 at 13:14):

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