The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

Hi list,

I'm trying to setup definitions to be able to rewrite wrt Z.le in 
arithmetic expressions (which live in Z).
For example, I can define the following instance to be able to rewrite 
under Z.add:

    Program Instance proper_Zplus: Proper (Z.le ++> Z.le ++> Z.le) Z.add.
    Next Obligation. do 6 intro. omega. Qed.

This one works well, as illustrated in the following example:

    Goal (forall a b c d, a <= b -> c + b <= c + d -> c + a <= c + d).
      intros ? ? ? ? a_le_b cb_le_cd.
      rewrite a_le_b.
      assumption.
    Qed.


However, I have issues trying to do the same with multiplication. 
"Proper (Z.le ++> Z.le ++> Z.le) Z.mul" is
not true in general, so I'd like to add a side condition asserting that 
the constant under which I rewrite
is non-negative.

This gives me this first instance, which allows to rewrite on the right 
of Z.mul:

    Program Instance proper_Zmult_right:
      forall x, 0 <= x ->
      Proper (Z.le ++> Z.le) (Z.mul x).
    Next Obligation. do 3 intro. nia. Qed.

This instance doesn't work as is; a previous thread 
(https://sympa.inria.fr/sympa/arc/coq-club/2013-03/msg00101.html)
seems to suggest that a way to make it work is by adding a hint

Hint Extern 100 (0 <= _) => assumption : typeclass_instances.

and then asserting the side-condition before rewriting with this instance.
Inserting this hint feels a bit hackish, and having to assert the side 
condition beforehand is not super convenient.

Moreover, I can't manage to define an similar instance to rewrite on the 
left of Z.mul. The following doesn't work:

    Program Instance proper_Zmult_left:
      forall y, 0 <= y ->
      Proper (Z.le ++> Z.le) (fun x => Z.mul x y).
    Next Obligation. do 3 intro. nia. Qed.

(attached is a minimal Coq script with the definitions & test cases)

Is there a better way of doing this setup so that rewriting under Z.mul 
works?
More generally, how do people prove and handle inequalities between 
arithmetic expressions?

— Armaël
Require Import ZArith.
Require Import Psatz.
Local Open Scope Z_scope.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Program Instance proper_Zplus: Proper (Z.le ++> Z.le ++> Z.le) Z.add.
Next Obligation. do 6 intro. omega. Qed.

Goal (forall a b c d, a <= b -> c + b <= c + d -> c + a <= c + d).
  intros ? ? ? ? a_le_b cb_le_cd.
  rewrite a_le_b.
  assumption.
Qed.

Program Instance proper_Zmult_left:
  forall x, 0 <= x ->
  Proper (Z.le ++> Z.le) (Z.mul x).
Next Obligation. do 3 intro. nia. Qed.

Hint Extern 100 (0 <= _) => assumption : typeclass_instances.

Goal forall a b c d, a <= b -> 0 <= c -> c * b <= c * d -> c * a <= c * d.
  intros ? ? ? ? a_le_b O_le_c cb_le_cd.
  rewrite a_le_b.
  assumption.
Qed.

Program Instance proper_Zmult_right:
  forall y, 0 <= y ->
  Proper (Z.le ++> Z.le) (fun x => Z.mul x y).
Next Obligation. do 3 intro. nia. Qed.

Goal forall a b c d, a <= b -> 0 <= c -> b * c <= d * c -> a * c <= d * c.
  intros ? ? ? ? a_le_b O_le_c bc_le_dc.
  (* rewrite a_le_b. *)
Abort.