eq_op operator treated as a binary operator

[ecranceMERCE]

Hello,

I am currently trying to find ways to improve SMTCoq whose purpose is to allow Coq users to use SMT solvers in their proofs. Amongst other considerations, I would like the initial phase of this tool to deal with goals handling several integer types, by injecting these types into Z before translating the goal to the SMT-LIB format. The zify tactic looks interesting to meet this target, because it allows to keep the goals simple while performing the required injections.

As mathcomp users are very likely to handle particular integer types, I found your repository and tried to play with it. However, I am a bit surprised by the way you are handling the == operator:

Indeed, it is defined as a binary operator (BinOp) whereas the binary relation (BinRel) type class exists and would be semantically closer to define an equality operator. I have written a few tests to check this behaviour.

When calling zify with == defined as a binary operator, the tactic generates a lot of hypotheses, probably due to the bool to Z injection caused by BinOp. By contrast, if we define this operator as a binary relation, catching theis_true coercion of mathcomp with it, the obtained goals look much simpler:

https://github.com/ecranceMERCE/zify-tests/blob/e586c9997ec26cee6e1149a419acb3a8d3699500/ring_operations.v#L137-L212

Maybe I am not stepping back enough, and I might run into problems later when defining == as a binary relation. That is why I am opening this issue. Could you tell me more about your decision to treat it as a binary operator?

Note that the smt tactic in SMTCoq can manage the output of the injection made with the BinOp way anyway:

https://github.com/ecranceMERCE/zify-tests/blob/e586c9997ec26cee6e1149a419acb3a8d3699500/smtcoq_after_zify.v#L45-L81

[pi8027]

Hello @ecranceMERCE,

Boolean values are computable but propositions are not. Here is an example where we need to handle == as a binary operator.

Goal forall n m : nat, n < n + nat_of_bool (n <= m + n).

If solvers can handle boolean operators (e.g., coq/coq#11047) and the zify tactic supports to target other types (coq/coq#10982), the obtained goals can be much simpler.

[ecranceMERCE]

Hello,

Thank you very much for the answer. I understand the convenience of a translation going through bool before Z when using booleans in the middle of a computation, which is different from semantically using booleans as relations. Consider this simple goal with ==:

Goal forall x y : int, x == 1 -> y == 0 -> x + y == 1.

It is currently processed by mczify into the following context:

x, y: int
z1: Z
Heqz1: z1 = (Z_of_int x - Z_of_int 1)%Z
z2: Z
H: z2 = 1%Z
z: Z
Heqz: z = (Z_of_int y - Z_of_int 0)%Z
z0: Z
H0: z0 = 1%Z
cstr, cstr0, cstr1, cstr2, cstr3, cstr4: True
H1: (0 <= z0 <= 1)%Z /\ (z = 0%Z <-> z0 = 1%Z)
H2: (0 <= z2 <= 1)%Z /\ (z1 = 0%Z <-> z2 = 1%Z)
z3: Z
Heqz3: z3 = (Z_of_int (x + y) - Z_of_int 1)%Z
z4: Z
H3: (0 <= z4 <= 1)%Z /\ (z3 = 0%Z <-> z4 = 1%Z)
--------------------------------------------------------
1/1
z4 = 1%Z

This is quite massive. Do you think the pull requests you mentioned might improve this result? And how would they? @fajb might be interested in the question.

Thanks again for your interest.

[fajb]

Hi, The current translation is indeed ugly and I suspect it does not scale. (This is not @pi8027 fault, given the current zify, you cannot really do better.) The purpose of PR https://github.com/coq/coq/pull/11047 was to improve lia so that boolean operators (&&, ||,... ) but also comparison operators ( Z.eqb, Z.leb,...) can be treated directly. This would make the work of zify easier without the need to axiomatise boolean operators.

For your example, I think there would be no overhead.

Unfortunately, I got sidetracked...

[fajb]

I have revived PR https://github.com/coq/coq/pull/11047. For the following goal:

Goal forall x y : nat, Nat.eqb x 1 = true ->
                       Nat.eqb y 0 = true ->
                       Nat.eqb (x + y) 1 = true.

After zify, I get:

  x, y : nat
  H0 : (Z.of_nat y =? 0) = true
  H : (Z.of_nat x =? 1) = true
  cstr : 0 <= Z.of_nat y
  cstr0 : 0 <= Z.of_nat x
  ============================
  (Z.of_nat x + Z.of_nat y =? 1) = true

I guess ssreflect would get the same benefit.

[amahboubi]

@fajb Thanks for your answer and for reactivating the PR! Note that declaring == and an instance of BinRel did not wok so bad. The issue in Mathcomp is that == is a generic notation, available for any eqType. So we need to control the cost of testing which occurrences of these instances will be eventually translated to an equality on Z, and which ones should remain "uninterpreted symbols".

[amahboubi]

@pi8027 nice remark, it is indeed cool to be able to handle the coercion bool >-> nat. However, I would say that this should be a secondary goal, compared to a satisfactory translation of boolean equality statements, don't you think?

[fajb]

For zify, there is a convertibility test for declared operators which take the form of an application e.g. @eq_op int_eqType. When zify encounters an @eq_op X, it performs a convertibility test between X and those that are declared. I have no idea how costly it is... Probably arbitrarily. An alternative would be to require to have exactly int_eqType. When we discussed with @pi8027 it did not seem to be a working option for ssreflect...

[fajb]

The up to date PR for boolean operators is https://github.com/coq/coq/pull/11906

[pi8027]

Hi all, I'm sorry for my belated reply. I think now I have time to work on this topic. I will try to reimplement Z-ification for boolean operators in MathComp using coq/coq#11906.

@pi8027 nice remark, it is indeed cool to be able to handle the coercion bool >-> nat. However, I would say that this should be a secondary goal, compared to a satisfactory translation of boolean equality statements, don't you think?

In my opinion, it is better to provide a complete decision procedure for a fragment we want to deal with and then think about efficiency issues. Anyway, I hope this is not a problem anymore with coq/coq#11906.

[pi8027]

@ecranceMERCE @amahboubi I think the current master branches of Coq and mczify solve this issue. If they don't, please let me know by reopening this issue.