Open ecranceMERCE opened 3 years ago
IIRC, the zify
tactic supports only first-order terms and thus does not support polymorphic types (such as products) and parametric instances (such as Op_eqb_pair
). I guess reimplementing zify
in Coq-elpi is a smooth way to get this kind of flexibility.
reimplementing
zify
in Coq-elpi
Learning Coq-elpi and working on this are my main goals in the short term future. I would be glad to talk about this with you when we have a joint meeting!
Hello.
I am planning to use zify / mczify as a source of inspiration for a pre-processing tool whose purpose is to prepare Coq goals before their translation to the SMT-LIB format, a standard input format for automated provers, so that the translation loses the least possible amount of information. The idea is to allow the users to express their goals using various integer types and forms of logic, as well as declare decidable relations or define a precise way to process some of their custom symbols. The pre-processing tool must deal with all these symbols so that the output of the translation has all the integers expressed in the SMT-LIB
Int
type, and the logic in the SMT-LIBBool
type. Therefore, its scope goes beyond arithmetic and the handled symbols are not necessarily contained in the signature of an integer type.I have found a behaviour of zify that could be considered as suboptimal for my needs, although it is perfectly explainable. It is about the handling of pairs.
Running zify on this goal gives the following proof state:
The MathComp
int
type is known, but the constructor used to make values of typeint * int
is unknown (and so is the boolean equality on this type). Thusx
is not in typeZ
in the proof state, and the pair is not made aZ * Z
pair. zify sees an unknown boolean and automatically does a case analysis on it, giving the two weird goals from above, whereas the expected output in my context would be the following:I am not sure whether it is the job of tools like zify or mczify to process that kind of values, as they are not really integers, but the discussion is worth being opened.
I have tried to create kind of generic zify instances that would create the behaviour I am looking for. I did not manage to make them work, I am still struggling with the MathComp
eqType
s. I know this might look less idiomatic for zify but here is my attempt: