omega for ssrnat

[affeldt-aist]

I am relaying a discussion from gitter. There is the old question of using omega (lia now) with ssrnat. One obvious solution is a bit of Ltac to switch from ssrbool/ssrnat so as to be able to use omega (e.g., https://github.com/affeldt-aist/seplog/blob/master/lib/ssrnat_ext.v#L46-L81, https://sympa.inria.fr/sympa/arc/ssreflect/2008-12/msg00006.html). Should such a tactic make its way into some math-comp repo?

[amahboubi]

Hello, for the record, there is a prototype here. It should work fine with current mathcomp.

[amahboubi]

The archive of the mailing list has another thread about this issue. Here is the relevant message in which I mentioned the previous repository

[thery]

You should contact Frédéric (Besson) he has something based with ppsimpl that makes lia works with ssreflect.

On 12/13/18 3:01 AM, affeldt-aist wrote:

I am relaying a discussion from gitter. There is the old question of using omega (lia now) with ssrnat. One obvious solution is a bit of Ltac to switch from ssrbool/ssrnat so as to be able to use omega (e.g., https://github.com/affeldt-aist/seplog/blob/master/lib/ssrnat_ext.v#L46-L81, https://sympa.inria.fr/sympa/arc/ssreflect/2008-12/msg00006.html). Should such a tactic make its way into some math-comp repo?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/math-comp/math-comp/issues/263, or mute the thread https://github.com/notifications/unsubscribe-auth/AGevtk_ikvcFCxSeqUrTOPLZoQw18Uakks5u4bUUgaJpZM4ZQyUJ.

[thery]

Ok, you can give a try using opam

opam install coq-ppsimpl

Then

Require Import Lia. Require Import PP.Ppsimplmathcomp. From mathcomp Require Import all_ssreflect.

Goal forall m n, n + 2 * n <= 4 * n + 4 * m + 3. move=> m n. ppsimpl. lia.

Laurent

[fajb]

Hello,

ppsimpl has indeed some support for mathcomp. The list of operators that are currently supported can be seen in the source by looking at the file Buildmathcomp.v. From what I see, we have: ssrnat.predn ssrnat.half ssrnat.uphalf plus minus ssrnat.subn mult ssrnat.muln ssrnat.expn ssrnat.maxn ssrnat.minn divn modn gcdn lcmn

If some are missing, contact me. If it is not too much trouble, I would be glad to extend.

Note that I am still not very happy with the implementation:

• I am the only one able to add new operators. (When it fails, the Ltac code does not properly report what when wrong.)
• It is also find it pretty slow (maybe because of Ltac or because this is a relfexive tactic using some depend types....)

Anyhow, I would be glad to get your feedback.

Best,

Frédéric

[CohenCyril]

Hi @fajb, can you point me to the file Buildmathcomp.v.? I cannot find it https://gforge.inria.fr/scm/?group_id=5430...

[fajb]

It should be in the branches 8.7 or 8.8 git clone https://scm.gforge.inria.fr/anonscm/git/ppsimpl/ppsimpl.git ppsimpl cd ppsimpl git checkout -b ppsimpl-8.8 origin/ppsimpl-8.8

[TDiazT]

Just wondering, I've been using this one which is "old" but I am not sure if it's ok or not haha (it works for me at least).

https://github.com/pi8027/formalized-postscript/blob/master/stdlib_ext.v#L43

[affeldt-aist]

@TDiazT This solution is indeed mentioned in the first post of this issue.

[pi8027]

According to coq/coq#9856, we are probably able to use zify directly for ssrnat and ssrint by declaring some class instances (in Coq 8.11 or later).

[fajb]

I really hope so. Though, I considered that it was a bit too soon to advertise the extensibility... If you wish to have a look the relevant files are

• Class declarations https://github.com/coq/coq/blob/master/plugins/micromega/ZifyClasses.v
• Existing instances https://github.com/coq/coq/blob/master/plugins/micromega/ZifyInst.v
• Attempt as encoding boolean operators https://github.com/coq/coq/blob/master/plugins/micromega/ZifyBool.v

[pi8027]

@fajb Thank you for great work. If it does work, we don't need to manipulate the goal twice anymore!

[pi8027]

I have started to implement the class instances to make zify does work for ssrnat and ssrint and see some issues:

• zify doesn't work for overloaded operators, e.g., @eq_op bool_eqType : bool -> bool -> bool and @eq_op nat_eqType : nat -> nat -> bool. (When I tried to define class instances for them forcibly, zify reports an anomaly. So I will report this to the Coq issue tracker later.) We need to replace them with monomorphic ones (e.g., eqb and eqn) before zify. So I would like to have Zify.zify_pre_hook to implement this preprocess.
• I don't see how to define a class instance for is_true : bool -> Prop. ZifyClasses does not seem to support unary predicates.
• I wish to have zify for finite ordinals (ordinal n = {0, ..., n - 1}, defined as follows). But I don't see how to define class instances for dependently-typed objects and functions. Does ppsimpl support this?

  Inductive ordinal (n : nat) : Type :=
    Ordinal : forall m : nat, is_true (m < n) -> ordinal n.
  
  Coercion nat_of_ord (n : nat) (i : ordinal n) : nat :=
    let: @Ordinal _ m _ := i in m.
  

I think I could change zify side to address the first two issues. But I don't see a solution for the last one.

[fajb]

* `zify` doesn't work for overloaded operators, e.g., `@eq_op bool_eqType : bool -> bool -> bool` and `@eq_op nat_eqType : nat -> nat -> bool`. (When I tried to define class instances for them forcibly, `zify` reports an anomaly. So I will report this to the Coq issue tracker later.)

There is already @eq nat, @eq positive... So, maybe this can be fixed. Did you finish the instance definition by Defined? A Qed would trigger an anomaly -- the error message could be improved...

  We need to replace them with monomorphic ones (e.g., `eqb` and `eqn`) before `zify`. So I would like to have `Zify.zify_pre_hook` to implement this preprocess.

This is indeed a workaround.

* I don't see how to define a class instance for `is_true : bool -> Prop`. `ZifyClasses` does not seem to support unary predicates.

Hum, I would propose to unfold is_true. Supporting unary predicates is doable but requires writing some ML code -- this is the hard part.

* I wish to have `zify` for finite ordinals (`ordinal n = {0, ..., n - 1}`, defined as follows). But I don't see how to define class instances for dependently-typed objects and functions. Does `ppsimpl` support this?

Neither zify, nor ppsimpl support dependent types. Sorry...

[fajb]

@pi8027 , ping me when you report the issue for overloading.

[pi8027]

(For the record, I reported the above issue of the anomaly as coq/coq#10779. It will be fixed by coq/coq#10787.)

[pi8027]

I have declared zify class instances for ssrbool, ssrnat, and div. Instances for ssrint and intdiv are not done yet. https://github.com/pi8027/mczify/blob/master/theories/zify.v

[pi8027]

I finished defining instances for most definitions on bool, nat, and int in MathComp, including gcdn, lcmn, coprime, divz, dvdz, gcdz, coprimez, etc. but excluding factorial, modz, and definitions in prime and binomial. Now, zify can handle overloaded operators like @eq_op int_eqType, @GRing.add int_ZmodType, @GRing.mul int_Ring, @GRing.scale _ [lmodType int of int^o], and @Num.le int_numDomainType.

The problem with modz is that it seems to have no corresponding definition in the standard library. Both Z.modulo and Z.rem are slightly different. So this requires some more work.

[pi8027]

I did some improvements on (div|mod|dvd)(n|z). Now micromega tactics can prove the following lemmas:

Lemma dvdz_lcm_6_4 (m : int) : (6 %| m -> 4 %| m -> 12 %| m)%Z.
Proof. lia. Qed.

Lemma divzMA_ge0 (m n p : int) :
  (0 <= n)%R -> (m %/ (n * p))%Z = ((m %/ n) %/ p)%Z.
Proof. nia. Qed.

[pi8027]

I hope the extensible zify tactic will be stable enough in Coq 8.13 thanks to coq/coq#11906 and it will make it easier to support several combinations of versions of Coq and MathComp in mczify. Then it will also be reasonable to migrate mczify to the math-comp organization, make a release, have CI... What about using this roadmap to close this issue?

[affeldt-aist]

What about using this roadmap to close this issue?

I think that you can close the issue with a last conversation item pointing to the wanted "omega tactic for ssreflect" that triggered this thread.

[affeldt-aist]

Use mczify as a replacement for lia.