The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Armaël,

There is a way to instrument type class resolution in "forward mode" :

Hint Extern 100 (0 <= _) => shelve : 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.
  unshelve rewrite a_le_b.
(*
______________________________________(1/2)
c * b <= c * d
______________________________________(2/2)
0 <= c
*)
  all:assumption.
Qed.

The external hint shelves the sub-goal instead of solving it. Then the unshelve tactical set it back for the user to solve.

I tested the modified code with both 8.5 and the current 8.6 branch.

I wonder how well this trick is known by heavy users of type classes.

Théo

Le mar. 6 déc. 2016 à 18:03, Armaël Guéneau <armael.gueneau AT ens-lyon.fr> a écrit :

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