Stream: Coq users

Topic: Syntax error in nested records?

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?

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.

Janno (Jun 02 2023 at 15:00):

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

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

Eric Wieser (Jun 02 2023 at 15:01):

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

Janno (Jun 02 2023 at 15:01):

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

Eric Wieser (Jun 02 2023 at 15:01):

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

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 _

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

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.

Eric Wieser (Jun 02 2023 at 15:10):

nice, that does the trick!

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

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

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

Eric Wieser (Jun 02 2023 at 15:44):

Apologies for not making a mwe:

Require Import String.
From Coq Require Import Unicode.Utf8.

Module Flat.
  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 :=
  { zero : A; add : A → A → A }.
  #[global] Instance to_add_monoid {A : Type} `{add_comm_monoid A} : add_monoid.add_monoid A :=
  { zero := zero; add := add }.
  End add_comm_monoid.

  Module semiring.
  Class semiring A : Type :=
  { zero : A; add : A → A → A; one : A; mul : A → A → A; }.
  #[global] Instance to_add_monoid {A : Type} `{semiring A} : add_comm_monoid.add_comm_monoid A :=
  { zero := zero; add := add }.
  End semiring.


  Module add_group.
  Class add_group A : Type := { zero : A; add : A → A → A; neg : A → A }.
  #[global] Instance to_add_monoid {A : Type} `{add_group A} : add_monoid.add_monoid A :=
  { zero := zero; add := add }.
  End add_group.

  Module add_comm_group.
  Class add_comm_group A : Type :=
  { zero : A; add : A → A → A; neg : A → A }.
  #[global] Instance to_add_comm_monoid {A : Type} `{add_comm_group A} : add_comm_monoid.add_comm_monoid A :=
  { zero := zero; add := add }.
  #[global] Instance to_add_group {A : Type} `{add_comm_group A} : add_group.add_group A :=
  { zero := zero; add := add; neg := neg }.
  End add_comm_group.

  Module ring.
  Class ring A : Type :=
  { zero : A; add : A → A → A; one : A; mul : A → A → A; neg : A → A }.
  #[global] Instance to_semiring {A : Type} `{ring A} : semiring.semiring A :=
  { zero := zero; add := add; one := one; mul := mul }.
  #[global] Instance to_add_comm_group {A : Type} `{ring A} : add_comm_group.add_comm_group A :=
  { zero := zero; add := add; neg := neg }.
  End ring.

  Class module (A B : Type) `{semiring.semiring A} `{add_comm_monoid.add_comm_monoid B} :=
  { smul : A → B → B }.
  #[global] Instance semiring_to_module (A : Type) `{semiring.semiring A} : module A A := { smul := semiring.mul }.

  Definition a_test (R : Type) `{ring.ring R} : module R R := _.

  Theorem neg_smul {R M : Type} `{ring.ring R} `{add_comm_group.add_comm_group M} `{module R M}
    (r : R) (m : M) :
    smul (add_group.neg r) m = add_group.neg (smul r m).
  Proof.
  Admitted.

  Definition another_test {R : Type} `{ring.ring R} (r : R)
  (r' : R) :
    smul (add_group.neg r) r' = add_group.neg (smul r r') := neg_smul r r'.

End Flat.

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}.
  #[global] Existing Instance to_add_monoid | 1.
  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 }.
  #[global] Existing Instance to_add_comm_monoid | 1.
  End semiring.

  Module add_group.
  Class add_group A : Type := { to_add_monoid : add_monoid.add_monoid A; neg : A → A }.
  #[global] Existing Instance to_add_monoid | 1.
  End add_group.


  Module add_comm_group.
  Class add_comm_group A : Type := { to_add_group : add_group.add_group A }.
  #[global] Existing Instance to_add_group | 1.
  #[global] Instance to_add_comm_monoid
    {A : Type} `{add_comm_group A} : add_comm_monoid.add_comm_monoid A | 10 :=
  { 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 }.
  #[global] Existing Instance ring.to_semiring | 1.
  (* @[priority 100] *)
  #[global] Instance to_add_comm_group
    {A : Type} `{ring A} : add_comm_group.add_comm_group A | 10 :=
  { to_add_group := {| add_group.neg := neg |} }.
  End ring.


  Class module (A B : Type) `{semiring.semiring A} `{add_comm_monoid.add_comm_monoid B} :=
  { smul : A → B → B }.
  #[global] Instance semiring_to_module (A : Type) `{semiring.semiring A} : module A A := { smul := semiring.mul }.

  Definition a_test (R : Type) `{ring.ring R} : module R R := _.

  Theorem neg_smul {R M : Type} `{ring.ring R} `{add_comm_group.add_comm_group M} `{module R M}
    (r : R) (m : M) :
    smul (add_group.neg r) m = add_group.neg (smul r m).
  Proof.
  Admitted.

  Theorem another_test (R : Type) `{ring.ring R} (r : R)
  (r' : R) :
    smul (add_group.neg r) r' = add_group.neg (smul r r').
  Proof.
    apply neg_smul.
  Qed.

  Set Printing Implicit.
  Print another_test.
End Nested.

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

Eric Wieser (Jun 02 2023 at 15:45):

But I want it to display @smul and @add_group_neg

Janno (Jun 02 2023 at 15:46):

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

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

Eric Wieser (Jun 02 2023 at 15:48):

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

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

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!

Janno (Jun 02 2023 at 16:04):

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

Eric Wieser (Jun 02 2023 at 16:14):

https://arxiv.org/abs/2306.00617

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!

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

Eric Wieser (Jun 02 2023 at 16:28):

Forgetful inheritance doesn't solve the particular problem above

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.

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.

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.

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.

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

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"

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.

Kazuhiko Sakaguchi (Jun 02 2023 at 20:26):

This is my example: incoherent_comring.v

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

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

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!

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.

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.

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.

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

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

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

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.

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"

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: Oct 13 2024 at 01:02 UTC