Stream: math-comp users

Topic: How to define a lmod_porder Type with my_display


view this post on Zulip Xiaoquan Xu (Feb 11 2024 at 08:01):

I want to define a lmod_porder Type with a new display like this:

Fact test_display : unit. Proof. by []. Qed.

HB.structure Definition TestN (R: numFieldType) :=
  { T of GRing.Lmodule R T & Order.POrder test_display T}.

But Coq told that:

Error: The structures display_problem_TestN and Num_POrderedZmodule are incompatible: the coercion between them cannot be synthesized: In environment
R : numFieldType
T : Type
c : axioms_ R T
The term "Order_isPOrder_mixin _ _ c" has type
"Order.isPOrder.axioms_ test_display T (eqtype_hasDecEq_mixin _ _ c)"
while it is expected to have type
"Order.isPOrder.axioms_ ring_display T (eqtype_hasDecEq_mixin _ _ c)".

It seems that the compiler is trying to convert my new type to Num.POrderedZmodule(constructed by ring_display), which is not in my expectation. What should I do?

view this post on Zulip Notification Bot (Feb 11 2024 at 08:29):

This topic was moved here from #Coq users > How to define a lmod_porder Type with my_display by Karl Palmskog.

view this post on Zulip Karl Palmskog (Feb 11 2024 at 08:29):

this looks like the most relevant stream, but there is also #Hierarchy Builder devs & users

view this post on Zulip Quentin VERMANDE (Feb 11 2024 at 10:34):

HB is trying to define a coercion from TestN.type to porderZmodType, which is normal since any lmodule is a zmodule. However, porderZmodType forces the display to be ring_display for some reason, which defeats the point of displays as I understand it. You can open an issue on mathcomp's github and for now, unless someone finds a hack, you have to use ring_display.

view this post on Zulip Cyril Cohen (Feb 13 2024 at 10:37):

The analysis of @Quentin VERMANDE . The specialization to ring_display is probably done too early (i.e. porderZmodType). I'm not sure though whether we can fix this... Could you submit an issue or a PR trying to fix this?

view this post on Zulip Cyril Cohen (Feb 13 2024 at 10:38):

The order display is however meant to be fixed to ring_display as soon as the order is compatible with the ring operations.

view this post on Zulip Quentin VERMANDE (Feb 13 2024 at 18:42):

I thought displays were meant to be decided at the instance level. So a simple fix would be to generalize the definitions of the structures over the display, am I wrong?


Last updated: Oct 13 2024 at 01:02 UTC