Pair equality handling

[ecranceMERCE]

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-LIB Bool 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.

Goal forall (x : int), (x, x) == (x, x).

Running zify on this goal gives the following proof state:

x: int
cstr: ((x, x) == (x, x)) = false
-----------------------------------
(1/2)
false = true
(2/2)
false = true

The MathComp int type is known, but the constructor used to make values of type int * int is unknown (and so is the boolean equality on this type). Thus x is not in type Z in the proof state, and the pair is not made a Z * 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:

x: Z
-------------------
(1/1)
(x, x) == (x, x)

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 eqTypes. I know this might look less idiomatic for zify but here is my attempt:

Program Instance Inj_pair
  {T1 U1 T2 U2 : Type} {Inj_T1_U1 : InjTyp T1 U1} {Inj_T2_U2 : InjTyp T2 U2}
  : InjTyp (T1 * T2) (U1 * U2) := {|
  inj := fun p =>
    match p with
    | (x, y) => (inj x, inj y)
    end;
  ZifyClasses.pred := fun p =>
    match p with
    | (x, y) => ZifyClasses.pred x /\ ZifyClasses.pred y
    end
|}.
Next Obligation.
Proof.
  split.
  - apply (cstr t).
  - apply (cstr t0).
Qed.
Add Zify InjTyp Inj_pair.

Program Instance Op_eqb_pair
  {T1 U1 T2 U2 : Type}
  : BinOp (@eq_op (T1 * U1)%type) :=
    {| TBOp := @eq_op (T2 * U2)%type |}.
(* type error: T1 * U1 must be an eqType
   proof of TBOpInj needed *)
Add Zify BinOp Op_eqb_pair.

[pi8027]

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.

[ecranceMERCE]

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!