Enzo Crance (Jan 25 2021 at 16:53): Enzo Crance (Jan 25 2021 at 16:53):Good evening. I am slowly learning Coq-Elpi and experimenting with it. Somehow it looks like the Coq typechecker does not behave the same way in Coq-Elpi and in Coq.
Let me show an example with the MathComp int type and ring notations.
Variable x : int.
Check (2%:Z + x * 3)%R.
This gives int_Zmodtype in Coq whereas coq.typecheck under an Elpi Query gives a type error because it thinks 3 is of type nat.
Elpi Query lp:{{ T = {{ (2%:Z + x * 3)%R }}, coq.typecheck T Ty Diag. }}.
Illegal application:
The term "GRing.mul" of type "forall R : ringType, R -> R -> R"
cannot be applied to the terms
"int_Ring" : "ringType"
"x" : "int"
"3" : "nat"
The 3rd term has type "nat" which should be coercible to
"GRing.Ring.sort int_Ring".
Is there an external reason for that, like Elpi not having access to some notations / coercions / structure instances? As I am far from being an expert on these topics, I cannot manage to find the origin of the error. Do you have an idea? Thanks in advance!
Enrico Tassi (Jan 25 2021 at 16:59):Long story short: Coq has many typecheckers ;-)
The one behind Check is available via the elaborate-skeleton API https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L878 .
The one you are calling is used internally in Coq in many places, but I don't think there is a command like Check for it. It cannot insert coercions (compare the the types of the two APIs, one cannot return an update term, but only assign its metavariables).
Enrico Tassi (Jan 25 2021 at 17:00):If you look for skeleton around in the file, you may find a few more APIs and comments on this "data".
Enrico Tassi (Jan 25 2021 at 17:03):The idea of "skeletons" is that the API does not modify that term, but rather use it as a skeleton to produce a new term which is somewhat related, but may contain more nodes (eg coercions).
Last updated: Oct 13 2024 at 01:02 UTC