Stream: math-comp users

Topic: Ring Quotient Error

view this post on Zulip Daniel Kirk (Jun 25 2021 at 14:58):

I'm trying to make the ZmodQuotType notation found in "ring_quotient.v" work, however I keep getting the same errors.
To demonstrate, consider the following lemma:

Lemma MyError o mul Q mix : forall (a : (RingQuotType o mul Q mix)), a == a.

This statement does not typecheck and gives the error:

In environment
o : ?T
mul : ?T1 -> ?T1 -> ?T1
Q : Type
mix : ?T0
x : phantom (quot_class_of ?T1 ?qT) (quot_class ?qT)
The term "x" has type "phantom (quot_class_of ?T1 ?qT) (quot_class ?qT)"
while it is expected to have type "phantom (quot_class_of ?T1 Q) ?qc".

Taking a deeper look at the definition in "ring_quotient.v" we find:

Notation RingQuotType o mul Q mix :=
  (@RingQuotType_pack _ _ _ _ _ o mul Q _ _ _ _ id id mix).

The error seems to come from the two id symbols. I'm not too familiar with phantom types but I guess these are to ensure the quot and ring types are compatible. Replacing them with underscores allows the lemma to typecheck but I'm not sure that is the right thing to do.
Can anyone shed any light on this error? (Also the same thing happens with the ZmodQuotType notation).

view this post on Zulip Florent Hivert (Jul 06 2021 at 17:00):

It probably means that Q need to have more structure than a bare Type. I guess at least eqType or even ringType.

view this post on Zulip Cyril Cohen (Aug 14 2021 at 13:36):

(deleted)

Last updated: Dec 07 2023 at 14:02 UTC