as in Z.div_mod_to_equations. It is currently broken and very inefficient.

It seems to me that mczify is helpful to write this kind of glue code. Also, we need zify instances for ringType operators instantiated with Z_ringType. I should probably think about including them in mczify, although the long-term goal is reimplementing the preprocessing/reification procedures such as zify, ring, and field in Coq-Elpi.

The following code is based on one in elliptic-curves-ssr.

From Coq Require Import ZArith ZifyClasses Ring Ring_polynom Field_theory.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
From mathcomp Require Import zify.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory.

Local Open Scope ring_scope.

Definition int_of_Z (n : Z) : int :=
  match n with
  | Z0 => Posz 0
  | Zpos p => Posz (Pos.to_nat p)
  | Zneg p => Negz (Pos.to_nat p).-1
  end.

Definition Z_of_int (n : int) : Z :=
  match n with
  | Posz n => Z.of_nat n
  | Negz n' => Z.opp (Z.of_nat (n' + 1))
  end.

Lemma int_of_ZK : cancel int_of_Z Z_of_int.
Proof. by case=> //= p; lia. Qed.

Instance Op_int_of_Z : UnOp int_of_Z := { TUOp := id; TUOpInj := int_of_ZK }.
Add Zify UnOp Op_int_of_Z.

Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj := fun => erefl }.
Add Zify UnOp Op_Z_of_int.

Lemma Z_of_intK : cancel Z_of_int int_of_Z.
Proof. by move=> ?; lia. Qed.

Lemma Z_eqP : Equality.axiom Z.eqb.
Proof. by move=> x y; apply: (iffP idP); lia. Qed.

Canonical Z_eqType := EqType Z (EqMixin Z_eqP).
Canonical Z_choiceType := ChoiceType Z (CanChoiceMixin int_of_ZK).
Canonical Z_countType := CountType Z (CanCountMixin int_of_ZK).

Definition Z_zmodMixin :=
  ZmodMixin Zplus_assoc Zplus_comm Zplus_0_l Zplus_opp_l.
Canonical Z_zmodType := ZmodType Z Z_zmodMixin.

Definition Z_ringMixin :=
  RingMixin
    Zmult_assoc Zmult_1_l Zmult_1_r Zmult_plus_distr_l Zmult_plus_distr_r isT.
Canonical Z_ringType := RingType Z Z_ringMixin.

Section Ring.

Variable (R : ringType).

Definition R_of_Z (n : Z) : R := (int_of_Z n)%:~R.

Lemma R_of_Z_is_additive : additive R_of_Z.
Proof. by move=> x y; rewrite -mulrzBr /+%R /-%R /=; congr intmul; lia. Qed.

Canonical R_of_Z_additive := Additive R_of_Z_is_additive.

Lemma R_of_Z_is_multiplicative : multiplicative R_of_Z.
Proof. by split=> //= x y; rewrite -intrM /*%R /=; congr intmul; lia. Qed.

Canonical R_of_Z_rmorphism := AddRMorphism R_of_Z_is_multiplicative.

Lemma RE : @ring_eq_ext R +%R *%R -%R eq.
Proof. by split; do! move=> ? _ <-. Qed.

Lemma RZ : ring_morph (R := R) 0 1 +%R *%R (fun x y => x - y) -%R eq
                      0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool R_of_Z.
Proof.
by split=> //=;
  [ exact: rmorphD | exact: rmorphB | exact: rmorphM | exact: raddfN
  | by move=> x y /Zeq_bool_eq -> ].
Qed.

Lemma PN : @power_theory R 1 *%R eq nat nat_of_N (@GRing.exp R).
Proof.
by split=> r [|n] //=; elim: n => //= p <-;
  rewrite (Pos2Nat.inj_xI, Pos2Nat.inj_xO) ?exprS -exprD addnn -mul2n.
Qed.

End Ring.

Lemma RR (R : comRingType) :
  @ring_theory R 0 1 +%R *%R (fun x y => x - y) -%R eq.
Proof.
exact/mk_rt/subrr/(fun _ _ => erefl)/mulrDl/mulrA/mulrC/mul1r/addrA/addrC/add0r.
Qed.

Lemma RF (F : fieldType) :
  @field_theory
    F 0 1 +%R *%R (fun x y => x - y) -%R (fun x y => x / y) (@GRing.inv F) eq.
Proof.
by split => //= [||x /eqP];
  [exact: RR | apply/eqP; rewrite oner_eq0 | exact: mulVf].
Qed.

Definition Rcorrect (R : comRingType) :=
  ring_correct
    (Eqsth R) (RE R) (Rth_ARth (Eqsth R) (RE R) (RR R)) (RZ R) (PN R)
    (triv_div_th (Eqsth R) (RE R) (Rth_ARth (Eqsth R) (RE R) (RR R)) (RZ R)).

Definition Fcorrect (F : fieldType) :=
  Field_correct
    (Eqsth F) (RE F) (congr1 GRing.inv)
    (F2AF (Eqsth F) (RE F) (RF F)) (RZ F) (PN F)
    (triv_div_th (Eqsth F) (RE F) (Rth_ARth (Eqsth F) (RE F) (RR F)) (RZ F)).

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.

With opam install coq-mathcomp-zify on mathcomp/mathcomp:1.17.0-coq-dev, I see

  + (script @ line 9) $ opam install -y -v coq-record-update coq-flocq coq-mathcomp-zify
  The following actions will be performed:
    - install coq-mathcomp-zify dev
    - install coq-record-update 0.3.2
    - install coq-flocq         dev
  ===== 3 to install =====
[...]
   - File "./theories/zify_ssreflect.v", line 136, characters 30-40:
  Error: - Error: The reference Order.diff was not found in the current environment.

The Coq team released Coq 8.19.0 on January 24th, 2024.
The corresponding Coq Platform release 2024.01 should be released before April 30th, 2024.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.19.0.

Coq Platform CI is currently testing opam package coq-mathcomp-zify.1.5.0+2.0+8.16
from official repository https://coq.inria.fr/opam/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.5.0+2.0+8.16/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2024.01, please inform us as soon as possible and before March 31st, 2024!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.19~2024.01+beta1 which already supports Coq version 8.19.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#405

Maybe you are aware of the Coq platform project - if not please have a look at : (https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md)

I and others would appreciate to include mczify into the Coq platform. Are you OK with that? If you say yes you also agree to put reasonable effort into maintaining mczify in the future for new Coq releases. If you would like to see mczify included, please create an issue at the above coq-platform repo. For 8.12 there is nothing else to do - I can take care of e.g. an opam package.

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

Due to this incompleteness, the support for GRing.unit : qualifier 1 int is missing:

Goal forall n : int, n \is a GRing.unit -> (n = 1)%R \/ (n = - 1)%R.
Proof.
move=> n.
Fail lia.
rewrite unfold_in /=.
lia.
Qed.

This is a potential source of incompatibilities such as #2. The right way to get rid of this would be supporting zify_pre_hook on the Coq side. https://github.com/pi8027/mczify/blob/06d29e26dbba204d3259ebca16edfaee23adc3b8/theories/zify.v#L13-L19

I came across a nice example to test mczify. It is to prove that a function is involutive:

Lemma zagierK x y z : 0 < x -> 0 < z -> 
  let zagier t :=
    let: (x, y, z) := t in
    if x < y - z then (x + z.*2, z, y - z - x)
    else if x < y.*2 then (y.*2 - x, y, x + z - y)
    else (x - y.*2, x + z - y, y) in
  zagier (zagier (x, y, z)) = (x, y, z).
Proof.
move=> xP zP /=.
repeat case: leqP => *; congr (_,_,_); lia.
Qed.

I updated to mathcomp 1.11.0 which unfortunately had the effect that your zify adoption (thanks for it!) does not compile any more.

The lemmas:

Lemma Op_int_min_subproof 
Lemma Op_int_max_subproof

fail. The lemma minrP used to prove the first seems to have been deprecated and moved to mathcomp.algebra.ssrnum.mc_1_10.Num.Theory. But even after importing this, case minrP fails and I couldn't figure out why (mathcomp newbie).

@pi8027 could you please do a release (I can do the OPAM package if you want) so that we have a release compatible with Coq 8.17? (since 8.17 is in the CI, this should mostly be a matter of hitting the release button on github)

The Coq team released Coq 8.16+rc1 on June 01, 2022.
The corresponding Coq Platform release 2022.09 should be released before September 15, 2022.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.16+rc1.

Coq Platform CI is currently testing opam package coq-mathcomp-zify.1.2.0+1.12+8.13
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.2.0+1.12+8.13/opam. This means we had to weaken some version restrictions in the opam package, but no other changes were required.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.09, please inform us as soon as possible and before August 31, 2022!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#274

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.17+rc1.

Coq Platform CI is currently testing opam package coq-mathcomp-zify.1.3.0+1.12+8.13
from official repository https://coq.inria.fr/opam/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.3.0+1.12+8.13/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.03, please inform us as soon as possible and before March 21st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#335

The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.15.0.

Coq Platform CI is currently testing opam package coq-mathcomp-zify.1.2.0+1.12+8.13
from official repository https://coq.inria.fr/opam/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.2.0+1.12+8.13/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.02, please inform us as soon as possible and before February 14, 2022!

The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#193

I have some performance issue with goals with large context.
The following file takes 25s (only the last two assumptions are needed
to solve it) (My real example takes more than 4m)

ex.txt

When I compile the project I get the following error:

$ make
...
File "./theories/zify.v", line 14, characters 28-37:
Error: The reference applySpec was not found in the current environment.

(I updated to Coq to revision d03529ab8fec0cad5705b5f775e43ef26c0dedcb)

We need a test suite automatically run by CI, and also extensive test cases to detect regressions. I think it makes sense to include example.v in it.

• nat_of_pos, nat_of_bin, pos_of_nat, and bin_of_nat (in ssrnat.v).
• fact_rec and factorial (in ssrnat.v).
• operators for finite ordinals (in fintype.v).
• prime, logn, pdiv, max_pdiv, and totient (in prime.v).
• up_log (in prime.v, available only from MathComp 1.14.0, see math-comp/math-comp#823).
• binomial_rec, binomial, ffact_rec, and falling_factorial (in binomial.v).
• Order.min and Order.max for natdvd (in order.v).
• Order.lteif and Order.leif for bool, nat, natdvd, and int (in order.v and ssrint.v).
• exprz for int (in ssrint.v).
• operators for rational numbers (in rat.v).

The interfaces for ordered types (such as porderType, latticeType, and orderType) and their overloaded operators (le, lt, min, max, meet, join, bottom, top, ...) are new in MathComp 1.11.0.

I see. Did you think about structuring your work differently, say having a separate file for the operators new in mathcomp 1.11 and then having collection files for mathcomp 1.10 and 1.11 which require those component files which are applicable? This might make it easier to maintain your work.

Do you think it would be possible to factor the differences between Coq versions into one file, so that the majority of the content in different Coq version branches would be identical?

Originally posted by @MSoegtropIMC in #9 (comment)

The Coq team released Coq 8.18.0 on September 7th, 2023.
The corresponding Coq Platform release 2023.10 should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.18.0.

Coq Platform CI is currently testing opam package coq-mathcomp-zify.1.5.0+2.0+8.16
from official repository https://coq.inria.fr/opam/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.5.0+2.0+8.16/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.10, please inform us as soon as possible and before October 31st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1 which already supports Coq version 8.18.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#372