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?
This topic was moved here from #Coq users > How to define a lmod_porder Type with my_display by Karl Palmskog.
this looks like the most relevant stream, but there is also #Hierarchy Builder devs & users
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
.
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?
The order display is however meant to be fixed to ring_display
as soon as the order is compatible with the ring operations.
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