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
It probably means that Q need to have more structure than a bare Type. I guess at least eqType or even ringType.
Last updated: Feb 08 2023 at 04:04 UTC