While writing an example file for Trocq, I got a bug after adding the following lemma to Trocq, relating the length function of lists to itself, so that transfer is possible with goals containing it:
Definition lengthR :
forall (A A' : Type) (AR : A -> A' -> Type)
(l : list A) (l' : list A') (lR : listR A A' AR l l'),
natR (length l) (length l').
As length is not a type former, Trocq will translate it at level $(0,0)$, which does not require more between A and A' than the raw relation, i.e., class $(0,0)$ as well.
However, here is what Trocq prints when accumulating the entry into the Elpi database:
The class $(0,0)$ of AR is not properly detected because it is not formatted as ParamXY.Rel A A'. The required type for this lemma is the following:
Definition lengthR :
forall (A A' : Type) (AR : Param00.Rel A A')
(l : list A) (l' : list A') (lR : listR A A' AR l l'),
natR (length l) (length l').
Note that leaving listR with the following type is fine:
listR : forall (A A' : Type) (AR : A -> A' -> Type), list A -> list A' -> Type
It looks like the tool is strict only on relations between values in Type. For any class different from $(0,0)$, anyway we would write it as ParamXY.Rel A A', but for $(0,0)$ it might be less natural.
I do not really know whether it qualifies as a bug, but it might introduce misunderstandings or silent bugs in the user's development when using Trocq. I think it requires either an exception for $(0,0)$ on occurrences of Type, or a line of documentation to make the expected syntax more explicit.
While writing an example file for Trocq, I got a bug after adding the following lemma to Trocq, relating the
lengthfunction of lists to itself, so that transfer is possible with goals containing it:As
lengthis not a type former, Trocq will translate it at level $(0,0)$, which does not require more betweenAandA'than the raw relation, i.e., class $(0,0)$ as well.However, here is what Trocq prints when accumulating the entry into the Elpi database:
The class $(0,0)$ of
ARis not properly detected because it is not formatted asParamXY.Rel A A'. The required type for this lemma is the following:Note that leaving
listRwith the following type is fine:It looks like the tool is strict only on relations between values in
Type. For any class different from $(0,0)$, anyway we would write it asParamXY.Rel A A', but for $(0,0)$ it might be less natural.I do not really know whether it qualifies as a bug, but it might introduce misunderstandings or silent bugs in the user's development when using Trocq. I think it requires either an exception for $(0,0)$ on occurrences of
Type, or a line of documentation to make the expected syntax more explicit.